let seq be ExtREAL_sequence; :: thesis: for rseq being Real_Sequence st seq = rseq holds
( seq is bounded_below iff rseq is bounded_below )
let rseq be Real_Sequence; :: thesis: ( seq = rseq implies ( seq is bounded_below iff rseq is bounded_below ) )
assume A1: seq = rseq ; :: thesis: ( seq is bounded_below iff rseq is bounded_below )

hereby :: thesis: ( rseq is bounded_below implies seq is bounded_below )

assume seq is bounded_below ; :: thesis: rseq is bounded_below
then rng rseq is bounded_below by A1, Def3;
then consider p being real number such that
A2: for y being real number st y in rng rseq holds
p <= y by SEQ_4:def 2;

now

let n be Element of NAT ; :: thesis: p - 1 < rseq . n
rseq . n in rng rseq by FUNCT_2:6;
then p - 1 < (rseq . n) - 0 by A2, XREAL_1:17;
hence p - 1 < rseq . n ; :: thesis: verum

end;

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

end;

assume rseq is bounded_below ; :: thesis: seq is bounded_below
then consider q being real number such that
A3: for n being Element of NAT holds q < rseq . n by SEQ_2:def 4;
A4: q in REAL by XREAL_0:def 1;

now

let r be ext-real number ; :: thesis: ( r in rng seq implies q <= r )
assume r in rng seq ; :: thesis: q <= r
then ex x being set st
( x in dom rseq & r = rseq . x ) by A1, FUNCT_1:def 5;
hence q <= r by A3; :: thesis: verum

end;

then q is LowerBound of rng seq by XXREAL_2:def 2;
hence rng seq is bounded_below by A4, SUPINF_1:def 12; :: according to RINFSUP2:def 3 :: thesis: verum