let seq be Real_Sequence; :: thesis: ( rng seq is real-bounded iff seq is bounded )
thus ( rng seq is real-bounded implies seq is bounded ) :: thesis: ( seq is bounded implies rng seq is real-bounded )

proof

given s being Real such that A1: s is LowerBound of rng seq ; :: according to XXREAL_2:def 9,XXREAL_2:def 11 :: thesis: ( not rng seq is bounded_above or seq is bounded )
given t being Real such that A2: t is UpperBound of rng seq ; :: according to XXREAL_2:def 10 :: thesis: seq is bounded
thus seq is bounded_above :: according to SEQ_2:def 8 :: thesis: seq is bounded_below

proof

take t + 1 ; :: according to SEQ_2:def 3 :: thesis: for b₁ being set holds not t + 1 <= seq . b₁
let n be Nat; :: thesis: not t + 1 <= seq . n
A3: n in NAT by ORDINAL1:def 12;
( seq . n <= t & t < t + 1 ) by A2, FUNCT_2:4, XREAL_1:29, XXREAL_2:def 1, A3;
hence not t + 1 <= seq . n by XXREAL_0:2; :: thesis: verum

end;

take s - 1 ; :: according to SEQ_2:def 4 :: thesis: for b₁ being set holds not seq . b₁ <= s - 1
let n be Nat; :: thesis: not seq . n <= s - 1
s < s + 1 by XREAL_1:29;
then A4: s - 1 < s by XREAL_1:19;
A5: n in NAT by ORDINAL1:def 12;
seq . n >= s by A1, FUNCT_2:4, XXREAL_2:def 2, A5;
hence not seq . n <= s - 1 by A4, XXREAL_0:2; :: thesis: verum

end;

given t being Real such that A6: for n being Nat holds seq . n < t ; :: according to SEQ_2:def 3,SEQ_2:def 8 :: thesis: ( not seq is bounded_below or rng seq is real-bounded )
given s being Real such that A7: for n being Nat holds seq . n > s ; :: according to SEQ_2:def 4 :: thesis: rng seq is real-bounded
thus rng seq is bounded_below :: according to XXREAL_2:def 11 :: thesis: rng seq is bounded_above

proof

take s ; :: according to XXREAL_2:def 9 :: thesis: s is LowerBound of rng seq
let r be ExtReal; :: according to XXREAL_2:def 2 :: thesis: ( not r in rng seq or s <= r )
assume r in rng seq ; :: thesis: s <= r
then ex n being object st
( n in dom seq & seq . n = r ) by FUNCT_1:def 3;
hence s <= r by A7; :: thesis: verum

end;

take t ; :: according to XXREAL_2:def 10 :: thesis: t is UpperBound of rng seq
let r be ExtReal; :: according to XXREAL_2:def 1 :: thesis: ( not r in rng seq or r <= t )
assume r in rng seq ; :: thesis: r <= t
then ex n being object st
( n in dom seq & seq . n = r ) by FUNCT_1:def 3;
hence r <= t by A6; :: thesis: verum