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

proof

assume r = (inferior_realsequence seq) . n ; :: thesis: ( ( for k being Element of NAT holds r <= seq . (n + k) ) & ( for s being real number st 0 < s holds
ex k being Element of NAT st seq . (n + k) < r + s ) )
then A3: r = inf Y1 by Def4;
A4: for k being Element of NAT holds r <= seq . (n + k)

proof

let k be Element of NAT ; :: thesis: r <= seq . (n + k)
seq . (n + k) in Y1 by SETLIM_1:1;
hence r <= seq . (n + k) by A2, A3, SEQ_4:def 5; :: thesis: verum

end;

for s being real number st 0 < s holds
ex k being Element of NAT st seq . (n + k) < r + s

proof

let s be real number ; :: thesis: ( 0 < s implies ex k being Element of NAT st seq . (n + k) < r + s )
assume A5: 0 < s ; :: thesis: ex k being Element of NAT st seq . (n + k) < r + s
consider r1 being real number such that
A6: ( r1 in Y1 & r1 < r + s ) by A2, A3, A5, SEQ_4:def 5;
consider k1 being Element of NAT such that
A7: ( r1 = seq . k1 & n <= k1 ) by A6;
consider k2 being Nat such that
A8: k1 = n + k2 by A7, NAT_1:10;
k2 in NAT by ORDINAL1:def 13;
hence ex k being Element of NAT st seq . (n + k) < r + s by A6, A7, A8; :: thesis: verum

end;

hence ( ( for k being Element of NAT holds r <= seq . (n + k) ) & ( for s being real number st 0 < s holds
ex k being Element of NAT st seq . (n + k) < r + s ) ) by A4; :: thesis: verum

end;

assume that
A9: for k being Element of NAT holds r <= seq . (n + k) and
A10: for s being real number st 0 < s holds
ex k being Element of NAT st seq . (n + k) < r + s ; :: thesis: r = (inferior_realsequence seq) . n
A11: for r1 being real number st r1 in Y1 holds
r <= r1

proof

let r1 be real number ; :: thesis: ( r1 in Y1 implies r <= r1 )
assume A12: r1 in Y1 ; :: thesis: r <= r1
consider k1 being Element of NAT such that
A13: ( r1 = seq . k1 & n <= k1 ) by A12;
consider k2 being Nat such that
A14: k1 = n + k2 by A13, NAT_1:10;
k2 in NAT by ORDINAL1:def 13;
hence r <= r1 by A9, A13, A14; :: thesis: verum

end;

for s being real number st 0 < s holds
ex r1 being real number st
( r1 in Y1 & r1 < r + s )

proof

let s be real number ; :: thesis: ( 0 < s implies ex r1 being real number st
( r1 in Y1 & r1 < r + s ) )
assume A15: 0 < s ; :: thesis: ex r1 being real number st
( r1 in Y1 & r1 < r + s )
consider k being Element of NAT such that
A16: seq . (n + k) < r + s by A10, A15;
n + k >= n by NAT_1:11;
then seq . (n + k) in Y1 ;
then consider r1 being real number such that
A17: ( r1 in Y1 & r1 = seq . (n + k) ) ;
thus ex r1 being real number st
( r1 in Y1 & r1 < r + s ) by A16, A17; :: thesis: verum

end;

then r = inf Y1 by A2, A11, SEQ_4:def 5;
hence r = (inferior_realsequence seq) . n by Def4; :: thesis: verum