let seq be Real_Sequence; :: thesis: ( seq is bounded_below iff rng seq is bounded_below )
A1: ( seq is bounded_below implies rng seq is bounded_below )

proof

assume seq is bounded_below ; :: thesis: rng seq is bounded_below
then consider t being real number such that
A2: for n being Element of NAT holds t < seq . n by SEQ_2:def 4;

now

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

end;

hence rng seq is bounded_below by SEQ_4:def 2; :: thesis: verum

end;

( rng seq is bounded_below implies seq is bounded_below )

proof

assume rng seq is bounded_below ; :: thesis: seq is bounded_below
then consider t being real number such that
A3: for r being real number st r in rng seq holds
t <= r by SEQ_4:def 2;

now

let n be Element of NAT ; :: thesis: t - 1 < seq . n
t <= seq . n by A3, FUNCT_2:6;
hence t - 1 < seq . n by Lm1; :: thesis: verum

end;

hence seq is bounded_below by SEQ_2:def 4; :: thesis: verum

end;

hence ( seq is bounded_below iff rng seq is bounded_below ) by A1; :: thesis: verum