let n be Nat; :: thesis:
let r be Real; :: thesis:
let seq be Real_Sequence; :: thesis:
reconsider Y1 = { (seq . k) where k is Nat : n <= k } as Subset of REAL by Th29;
assume seq is bounded_below ; :: thesis:
then A1: ( not Y1 is empty & Y1 is bounded_below ) by Th32, SETLIM_1:1;
thus ( r = (inferior_realsequence seq) . n implies ( ( for k being Nat holds r <= seq . (n + k) ) & ( for s being Real st 0 < s holds
ex k being Nat st seq . (n + k) < r + s ) ) ) :: thesis:

let s be Real; :: thesis:
assume 0 < s ; :: thesis:
then consider r1 being Real such that
A4: r1 in Y1 and
A5: r1 < r + s by A1, A2, SEQ_4:def 2;
consider k1 being Nat such that
A6: r1 = seq . k1 and
A7: n <= k1 by A4;
consider k2 being Nat such that
A8: k1 = n + k2 by A7, NAT_1:10;
thus ex k being Nat st seq . (n + k) < r + s by A5, A6, A8; :: thesis:

end;

for k being Nat holds r <= seq . (n + k)

let k be Nat; :: thesis:
seq . (n + k) in Y1 by SETLIM_1:1;
hence r <= seq . (n + k) by A1, A2, SEQ_4:def 2; :: thesis:

end;

hence ( ( for k being Nat holds r <= seq . (n + k) ) & ( for s being Real st 0 < s holds
ex k being Nat st seq . (n + k) < r + s ) ) by A3; :: thesis:

end;

assume that
A9: for k being Nat holds r <= seq . (n + k) and
A10: for s being Real st 0 < s holds
ex k being Nat st seq . (n + k) < r + s ; :: thesis:
A11: for s being Real st 0 < s holds
ex r1 being Real st
( r1 in Y1 & r1 < r + s )

let s be Real; :: thesis:
assume 0 < s ; :: thesis:
then consider k being Nat such that
A12: seq . (n + k) < r + s by A10;
n + k >= n by NAT_1:11;
then seq . (n + k) in Y1 ;
hence ex r1 being Real st
( r1 in Y1 & r1 < r + s ) by A12; :: thesis:

end;

for r1 being Real st r1 in Y1 holds
r <= r1

let r1 be Real; :: thesis:
assume r1 in Y1 ; :: thesis:
then consider k1 being Nat such that
A13: r1 = seq . k1 and
A14: n <= k1 ;
consider k2 being Nat such that
A15: k1 = n + k2 by A14, NAT_1:10;
thus r <= r1 by A9, A13, A15; :: thesis:

end;