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