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

per cases ( z in A or z in B ) by A1, XBOOLE_0:def 3;

suppose A2: z in A ; :: thesis: z <= max x,y

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

end;

suppose A4: z in B ; :: thesis: z <= max x,y

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

end;

end;