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