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

proof

given s being real number 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 number 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 Element of NAT holds not t + 1 <= seq . b₁
let n be Element of NAT ; :: thesis: not t + 1 <= seq . n
( seq . n <= t & t < t + 1 ) by A2, FUNCT_2:4, XREAL_1:29, XXREAL_2:def 1;
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 Element of NAT holds not seq . b₁ <= s - 1
let n be Element of NAT ; :: thesis: not seq . n <= s - 1
s < s + 1 by XREAL_1:29;
then A3: s - 1 < s by XREAL_1:19;
seq . n >= s by A1, FUNCT_2:4, XXREAL_2:def 2;
hence not seq . n <= s - 1 by A3, XXREAL_0:2; :: thesis: verum

end;

given t being real number such that A4: for n being Element of 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 bounded )
given s being real number such that A5: for n being Element of NAT holds seq . n > s ; :: according to SEQ_2:def 4 :: thesis: rng seq is 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 ext-real number ; :: 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 set st
( n in dom seq & seq . n = r ) by FUNCT_1:def 3;
hence s <= r by A5; :: thesis: verum

end;

take t ; :: according to XXREAL_2:def 10 :: thesis: t is UpperBound of rng seq
let r be ext-real number ; :: 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 set st
( n in dom seq & seq . n = r ) by FUNCT_1:def 3;
hence r <= t by A4; :: thesis: verum