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;