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