let x, y be ext-real number ; :: thesis: max x,y = max {x,y}

now

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

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

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

end;

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

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

end;

end;

end;

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