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

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