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
A3: max a,b <= c by A1, Def9;
( a <= max a,b & b <= max a,b ) by Th25;
then c <= max a,b by A2;
hence c = max a,b by A3, Th1; :: thesis: verum