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

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

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

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

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

end;

then lower_bound X >= t - q3 by SEQ_4:43;
hence t <= q3 + (lower_bound X) by XREAL_1:20; :: thesis: verum

end;

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

let s be Real; :: thesis: ( s in q3 ++ X implies s >= q3 + (lower_bound X) )
assume s in q3 ++ X ; :: thesis: s >= q3 + (lower_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 >= lower_bound X by A1, A5, SEQ_4:def 2;
hence s >= q3 + (lower_bound X) by A4, XREAL_1:6; :: thesis: verum

end;

hence lower_bound (q3 ++ X) = q3 + (lower_bound X) by A2, SEQ_4:44; :: thesis: verum