let r be real number ; :: thesis: for seq being Real_Sequence st seq is bounded_below holds
( r = inf seq iff ( ( for n being Element of NAT holds r <= seq . n ) & ( for s being real number st 0 < s holds
ex k being Element of NAT st seq . k < r + s ) ) )
let seq be Real_Sequence; :: thesis: ( seq is bounded_below implies ( r = inf seq iff ( ( for n being Element of NAT holds r <= seq . n ) & ( for s being real number st 0 < s holds
ex k being Element of NAT st seq . k < r + s ) ) ) )
set R = rng seq;
assume seq is bounded_below ; :: thesis: ( r = inf seq iff ( ( for n being Element of NAT holds r <= seq . n ) & ( for s being real number st 0 < s holds
ex k being Element of NAT st seq . k < r + s ) ) )
then A1: rng seq is bounded_below by Th6;
A2: rng seq <> {} by RELAT_1:64;
A3: ( ( for n being Element of NAT holds r <= seq . n ) & ( for s being real number st 0 < s holds
ex k being Element of NAT st seq . k < r + s ) implies r = inf seq )

proof

assume that
A4: for n being Element of NAT holds r <= seq . n and
A5: for s being real number st 0 < s holds
ex k being Element of NAT st seq . k < r + s ; :: thesis: r = inf seq

A6: now

let s be real number ; :: thesis: ( 0 < s implies ex r2 being real number st
( r2 in rng seq & r2 < r + s ) )
assume 0 < s ; :: thesis: ex r2 being real number st
( r2 in rng seq & r2 < r + s )
then consider k being Element of NAT such that
A7: seq . k < r + s by A5;
consider r2 being real number such that
A8: ( r2 in rng seq & r2 = seq . k ) by FUNCT_2:6;
take r2 = r2; :: thesis: ( r2 in rng seq & r2 < r + s )
thus ( r2 in rng seq & r2 < r + s ) by A7, A8; :: thesis: verum

end;

now

let r1 be real number ; :: thesis: ( r1 in rng seq implies r <= r1 )
assume r1 in rng seq ; :: thesis: r <= r1
then ex n being set st
( n in dom seq & seq . n = r1 ) by FUNCT_1:def 5;
hence r <= r1 by A4; :: thesis: verum

end;

hence r = inf seq by A1, A2, A6, SEQ_4:def 5; :: thesis: verum

end;

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

proof

assume A9: r = inf seq ; :: thesis: ( ( for n being Element of NAT holds r <= seq . n ) & ( for s being real number st 0 < s holds
ex k being Element of NAT st seq . k < r + s ) )

A10: now

let s be real number ; :: thesis: ( 0 < s implies ex k being Element of NAT st seq . k < r + s )
assume 0 < s ; :: thesis: ex k being Element of NAT st seq . k < r + s
then consider r2 being real number such that
A11: r2 in rng seq and
A12: r2 < r + s by A1, A2, A9, SEQ_4:def 5;
consider k being Element of NAT such that
A13: r2 = seq . k by A11, SETLIM_1:4;
take k = k; :: thesis: seq . k < r + s
thus seq . k < r + s by A12, A13; :: thesis: verum

end;

now

let n be Element of NAT ; :: thesis: r <= seq . n
seq . n in rng seq by FUNCT_2:6;
hence r <= seq . n by A1, A9, SEQ_4:def 5; :: thesis: verum

end;

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

end;

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