let x, y be ExtReal; :: thesis: max (x,y) = max {x,y}

now :: thesis: ( ( x <= y & max {x,y} = y ) or ( y < x & max {x,y} = x ) )

per cases ( x <= y or y < x ) ;

case A1: x <= y ; :: thesis: max {x,y} = y

A2: for z being UpperBound of {x,y} holds y <= z by Lm4;
y is UpperBound of {x,y} by A1, Lm3;
hence max {x,y} = y by A2, Def3; :: thesis: verum

end;

case A3: y < x ; :: thesis: max {x,y} = x

A4: for z being UpperBound of {x,y} holds x <= z by Lm4;
x is UpperBound of {x,y} by A3, Lm3;
hence max {x,y} = x by A4, Def3; :: thesis: verum

end;

end;

end;

hence max (x,y) = max {x,y} by XXREAL_0:def 10; :: thesis: verum