let c, a, b be ext-real number ; :: thesis: ( c <= a & c <= b & ( for d being ext-real number 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 ext-real number 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, Def9;
hence c = min (a,b) by A3, Th1; :: thesis: verum