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;
t is LowerBound of rng seq

proof

let r be ext-real number ; :: according to XXREAL_2:def 2 :: thesis: ( not r in rng seq or 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 XXREAL_2:def 9; :: 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
B3: t is LowerBound of rng seq by XXREAL_2:def 9;
A3: for r being real number st r in rng seq holds
t <= r by B3, XXREAL_2: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