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