let A, B be non empty bounded_above Subset of REAL; :: thesis: upper_bound (A \/ B) = max ((upper_bound A),(upper_bound B))
set r = max ((upper_bound A),(upper_bound B));
A1: max ((upper_bound A),(upper_bound B)) >= upper_bound B by XXREAL_0:25;
A2: for r1 being Real st ( for t being Real st t in A \/ B holds
t <= r1 ) holds
max ((upper_bound A),(upper_bound B)) <= r1

proof

let r1 be Real; :: thesis: ( ( for t being Real st t in A \/ B holds
t <= r1 ) implies max ((upper_bound A),(upper_bound B)) <= r1 )
assume A3: for t being Real st t in A \/ B holds
t <= r1 ; :: thesis: max ((upper_bound A),(upper_bound B)) <= r1

now :: thesis: for t being Real st t in B holds
t <= r1

let t be Real; :: thesis: ( t in B implies t <= r1 )
assume t in B ; :: thesis: t <= r1
then t in A \/ B by XBOOLE_0:def 3;
hence t <= r1 by A3; :: thesis: verum

end;

then A4: upper_bound B <= r1 by Th45;

now :: thesis: for t being Real st t in A holds
t <= r1

let t be Real; :: thesis: ( t in A implies t <= r1 )
assume t in A ; :: thesis: t <= r1
then t in A \/ B by XBOOLE_0:def 3;
hence t <= r1 by A3; :: thesis: verum

end;

then upper_bound A <= r1 by Th45;
hence max ((upper_bound A),(upper_bound B)) <= r1 by A4, XXREAL_0:28; :: thesis: verum

end;

A5: max ((upper_bound A),(upper_bound B)) >= upper_bound A by XXREAL_0:25;
for t being Real st t in A \/ B holds
t <= max ((upper_bound A),(upper_bound B))

proof

let t be Real; :: thesis: ( t in A \/ B implies t <= max ((upper_bound A),(upper_bound B)) )
assume t in A \/ B ; :: thesis: t <= max ((upper_bound A),(upper_bound B))
then ( t in A or t in B ) by XBOOLE_0:def 3;
then ( upper_bound A >= t or upper_bound B >= t ) by Def1;
hence t <= max ((upper_bound A),(upper_bound B)) by A5, A1, XXREAL_0:2; :: thesis: verum

end;

hence upper_bound (A \/ B) = max ((upper_bound A),(upper_bound B)) by A2, Th46; :: thesis: verum