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

A2: now

let s be real number ; :: thesis: ( s in q3 ++ X implies s >= q3 + (inf X) )
assume s in q3 ++ X ; :: thesis: s >= q3 + (inf X)
then consider r3 being Real such that
A3: ( q3 + r3 = s & r3 in X ) ;
r3 >= inf X by A1, A3, SEQ_4:def 5;
hence s >= q3 + (inf 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 t <= q3 + (inf X) )
assume A4: for s being real number st s in q3 ++ X holds
s >= t ; :: thesis: t <= q3 + (inf X)

now

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

end;

then inf X >= t - q3 by SEQ_4:60;
hence t <= q3 + (inf X) by XREAL_1:22; :: thesis: verum

end;

hence inf (q3 ++ X) = q3 + (inf X) by A2, SEQ_4:61; :: thesis: verum