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