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 such that
A2: for n being Nat holds t < seq . n by SEQ_2:def 4;
t is LowerBound of rng seq

proof

let r be ExtReal; :: 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 object st
( n in dom seq & seq . n = r ) by FUNCT_1:def 3;
hence t <= r by A2; :: thesis: verum

end;

hence rng seq is bounded_below ; :: 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 such that
A3: t is LowerBound of rng seq ;
A4: for r being Real st r in rng seq holds
t <= r by A3, XXREAL_2:def 2;

now :: thesis: for n being Nat holds t - 1 < seq . n

let n be Nat; :: thesis: t - 1 < seq . n
A5: n in NAT by ORDINAL1:def 12;
t <= seq . n by A4, FUNCT_2:4, A5;
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