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)

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;

end;

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;z <= x by A2, Def1;

hence z <= max (x,y) by A3, XXREAL_0:2; :: thesis: verum

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;z <= y by A4, Def1;

hence z <= max (x,y) by A5, XXREAL_0:2; :: thesis: verum