let seq be ExtREAL_sequence; :: thesis: for rseq being Real_Sequence st seq = rseq holds

( seq is bounded_below iff rseq is V71() )

let rseq be Real_Sequence; :: thesis: ( seq = rseq implies ( seq is bounded_below iff rseq is V71() ) )

assume A1: seq = rseq ; :: thesis: ( seq is bounded_below iff rseq is V71() )

then consider q being Real such that

A4: for n being Nat holds q < rseq . n by SEQ_2:def 4;

hence rng seq is bounded_below by XXREAL_2:def 9; :: according to RINFSUP2:def 3 :: thesis: verum

( seq is bounded_below iff rseq is V71() )

let rseq be Real_Sequence; :: thesis: ( seq = rseq implies ( seq is bounded_below iff rseq is V71() ) )

assume A1: seq = rseq ; :: thesis: ( seq is bounded_below iff rseq is V71() )

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

assume
rseq is V71()
; :: thesis: seq is bounded_below assume
seq is bounded_below
; :: thesis: rseq is V71()

then rng rseq is bounded_below by A1;

then consider p being Real such that

A2: p is LowerBound of rng rseq by XXREAL_2:def 9;

A3: for y being Real st y in rng rseq holds

p <= y by A2, XXREAL_2:def 2;

end;then rng rseq is bounded_below by A1;

then consider p being Real such that

A2: p is LowerBound of rng rseq by XXREAL_2:def 9;

A3: for y being Real st y in rng rseq holds

p <= y by A2, XXREAL_2:def 2;

now :: thesis: for n being Nat holds p - 1 < rseq . n

hence
rseq is V71()
by SEQ_2:def 4; :: thesis: verumlet n be Nat; :: thesis: p - 1 < rseq . n

n in NAT by ORDINAL1:def 12;

then rseq . n in rng rseq by FUNCT_2:4;

then p - 1 < (rseq . n) - 0 by A3, XREAL_1:15;

hence p - 1 < rseq . n ; :: thesis: verum

end;n in NAT by ORDINAL1:def 12;

then rseq . n in rng rseq by FUNCT_2:4;

then p - 1 < (rseq . n) - 0 by A3, XREAL_1:15;

hence p - 1 < rseq . n ; :: thesis: verum

then consider q being Real such that

A4: for n being Nat holds q < rseq . n by SEQ_2:def 4;

now :: thesis: for r being ExtReal st r in rng seq holds

q <= r

then
q is LowerBound of rng seq
by XXREAL_2:def 2;q <= r

let r be ExtReal; :: thesis: ( r in rng seq implies q <= r )

assume r in rng seq ; :: thesis: q <= r

then ex x being object st

( x in dom rseq & r = rseq . x ) by A1, FUNCT_1:def 3;

hence q <= r by A4; :: thesis: verum

end;assume r in rng seq ; :: thesis: q <= r

then ex x being object st

( x in dom rseq & r = rseq . x ) by A1, FUNCT_1:def 3;

hence q <= r by A4; :: thesis: verum

hence rng seq is bounded_below by XXREAL_2:def 9; :: according to RINFSUP2:def 3 :: thesis: verum