let a, c, b be ext-real number ; :: thesis: ( a <= c & b <= c & ( for d being ext-real number st a <= d & b <= d holds
c <= d ) implies c = max (a,b) )
assume that
A1: ( a <= c & b <= c ) and
A2: for d being ext-real number st a <= d & b <= d holds
c <= d ; :: thesis: c = max (a,b)
( a <= max (a,b) & b <= max (a,b) ) by Th25;
then A3: c <= max (a,b) by A2;
max (a,b) <= c by A1, Def10;
hence c = max (a,b) by A3, Th1; :: thesis: verum