let q3 be Real; :: thesis: for X being non empty Subset of REAL st X is bounded_above holds
sup (q3 ++ X) = q3 + (sup X)
let X be non empty Subset of REAL ; :: thesis: ( X is bounded_above implies sup (q3 ++ X) = q3 + (sup X) )
assume A1: X is bounded_above ; :: thesis: sup (q3 ++ X) = q3 + (sup X)
set i = q3 + (sup X);

A2: now

let s be real number ; :: thesis: ( s in q3 ++ X implies s <= q3 + (sup X) )
assume s in q3 ++ X ; :: thesis: s <= q3 + (sup X)
then consider r3 being Real such that
A3: ( q3 + r3 = s & r3 in X ) ;
r3 <= sup X by A1, A3, SEQ_4:def 4;
hence s <= q3 + (sup X) by A3, XREAL_1:8; :: thesis: verum

end;

now

let t be real number ; :: thesis: ( ( for s being real number st s in q3 ++ X holds
s <= t ) implies q3 + (sup X) <= t )
assume A4: for s being real number st s in q3 ++ X holds
s <= t ; :: thesis: q3 + (sup X) <= t

now

let s be real number ; :: thesis: ( s in X implies s <= t - q3 )
assume s in X ; :: thesis: s <= t - q3
then q3 + s in q3 ++ X ;
then q3 + s <= t by A4;
hence s <= t - q3 by XREAL_1:21; :: thesis: verum

end;

then sup X <= t - q3 by SEQ_4:62;
hence q3 + (sup X) <= t by XREAL_1:21; :: thesis: verum

end;

hence sup (q3 ++ X) = q3 + (sup X) by A2, SEQ_4:63; :: thesis: verum