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 ExtReal; :: 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;