let a, b, c be ExtReal; :: thesis: ( c <= a & c <= b & ( for d being ExtReal st d <= a & d <= b holds

d <= c ) implies c = min (a,b) )

assume that

A1: ( c <= a & c <= b ) and

A2: for d being ExtReal st d <= a & d <= b holds

d <= c ; :: thesis: c = min (a,b)

( min (a,b) <= a & min (a,b) <= b ) by Th17;

then A3: min (a,b) <= c by A2;

c <= min (a,b) by A1, Def8;

hence c = min (a,b) by A3, Th1; :: thesis: verum

d <= c ) implies c = min (a,b) )

assume that

A1: ( c <= a & c <= b ) and

A2: for d being ExtReal st d <= a & d <= b holds

d <= c ; :: thesis: c = min (a,b)

( min (a,b) <= a & min (a,b) <= b ) by Th17;

then A3: min (a,b) <= c by A2;

c <= min (a,b) by A1, Def8;

hence c = min (a,b) by A3, Th1; :: thesis: verum