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

proof

let t be real number ; :: thesis: ( t in A \/ B implies t <= max (sup A),(sup B) )
assume t in A \/ B ; :: thesis: t <= max (sup A),(sup B)
then ( t in A or t in B ) by XBOOLE_0:def 3;
then ( sup A >= t or sup B >= t ) by SEQ_4:def 4;
hence t <= max (sup A),(sup B) by A1, XXREAL_0:2; :: thesis: verum

end;

for r1 being real number st ( for t being real number st t in A \/ B holds
t <= r1 ) holds
max (sup A),(sup B) <= r1

proof

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

now

let t be real number ; :: 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 A4: sup A <= r1 by SEQ_4:62;

now

let t be real number ; :: 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 sup B <= r1 by SEQ_4:62;
hence max (sup A),(sup B) <= r1 by A4, XXREAL_0:28; :: thesis: verum

end;

hence sup (A \/ B) = max (sup A),(sup B) by A2, SEQ_4:63; :: thesis: verum