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

A2: now :: thesis: for t being Real st ( for s being Real st s in q3 ++ X holds
s <= t ) holds
q3 + (upper_bound X) <= t

let t be Real; :: thesis: ( ( for s being Real st s in q3 ++ X holds
s <= t ) implies q3 + (upper_bound X) <= t )
assume A3: for s being Real st s in q3 ++ X holds
s <= t ; :: thesis: q3 + (upper_bound X) <= t

now :: thesis: for s being Real st s in X holds
s <= t - q3

let s be Real; :: thesis: ( s in X implies s <= t - q3 )
assume s in X ; :: thesis: s <= t - q3
then q3 + s <= t by A3, MEMBER_1:141;
hence s <= t - q3 by XREAL_1:19; :: thesis: verum

end;

then upper_bound X <= t - q3 by SEQ_4:45;
hence q3 + (upper_bound X) <= t by XREAL_1:19; :: thesis: verum

end;

now :: thesis: for s being Real st s in q3 ++ X holds
s <= q3 + (upper_bound X)

let s be Real; :: thesis: ( s in q3 ++ X implies s <= q3 + (upper_bound X) )
assume s in q3 ++ X ; :: thesis: s <= q3 + (upper_bound X)
then s in { (q3 + r3) where r3 is Real : r3 in X } by Lm5;
then consider r3 being Real such that
A4: q3 + r3 = s and
A5: r3 in X ;
r3 <= upper_bound X by A1, A5, SEQ_4:def 1;
hence s <= q3 + (upper_bound X) by A4, XREAL_1:6; :: thesis: verum

end;

hence upper_bound (q3 ++ X) = q3 + (upper_bound X) by A2, SEQ_4:46; :: thesis: verum