let X, Y be ext-real-membered set ; :: thesis: for x being UpperBound of X
for y being UpperBound of Y holds max x,y is UpperBound of X \/ Y
let x be UpperBound of X; :: thesis: for y being UpperBound of Y holds max x,y is UpperBound of X \/ Y
let y be UpperBound of Y; :: thesis: max x,y is UpperBound of X \/ Y
let a be ext-real number ; :: according to XXREAL_2:def 1 :: thesis: ( a in X \/ Y implies a <= max x,y )
assume A1: a in X \/ Y ; :: thesis: a <= max x,y

per cases ( a in X or a in Y ) by A1, XBOOLE_0:def 3;

suppose A2: a in X ; :: thesis: a <= max x,y

A3: x <= max x,y by XXREAL_0:25;
a <= x by A2, Def1;
hence a <= max x,y by A3, XXREAL_0:2; :: thesis: verum

end;

suppose A4: a in Y ; :: thesis: a <= max x,y

A5: y <= max x,y by XXREAL_0:25;
a <= y by A4, Def1;
hence a <= max x,y by A5, XXREAL_0:2; :: thesis: verum

end;

end;