let seq be ExtREAL_sequence; :: thesis: ( lim_sup seq = lim_inf seq & lim_inf seq in REAL implies ex k being Element of NAT st seq ^\ k is bounded )
assume that
A1: lim_sup seq = lim_inf seq and
A2: lim_inf seq in REAL ; :: thesis: ex k being Element of NAT st seq ^\ k is bounded
reconsider a = lim_inf seq as Real by A2;
set K1 = a + 1;
ex k1 being Element of NAT st (superior_realsequence seq) . k1 <= a + 1

proof

assume A3: for k1 being Element of NAT holds not (superior_realsequence seq) . k1 <= a + 1 ; :: thesis: contradiction

now

let x be ext-real number ; :: thesis: ( x in rng (superior_realsequence seq) implies a + 1 <= x )
assume x in rng (superior_realsequence seq) ; :: thesis: a + 1 <= x
then ex n being set st
( n in dom (superior_realsequence seq) & x = (superior_realsequence seq) . n ) by FUNCT_1:def 5;
hence a + 1 <= x by A3; :: thesis: verum

end;

then a + 1 is LowerBound of rng (superior_realsequence seq) by XXREAL_2:def 2;
then a + 1 <= a by A1, XXREAL_2:def 4;
hence contradiction by XREAL_1:31; :: thesis: verum

end;

then consider k1 being Element of NAT such that
A4: (superior_realsequence seq) . k1 <= a + 1 ;
set K2 = a - 1;
ex k2 being Element of NAT st a - 1 <= (inferior_realsequence seq) . k2

proof

assume A5: for k2 being Element of NAT holds not a - 1 <= (inferior_realsequence seq) . k2 ; :: thesis: contradiction

now

let x be ext-real number ; :: thesis: ( x in rng (inferior_realsequence seq) implies x <= a - 1 )
assume x in rng (inferior_realsequence seq) ; :: thesis: x <= a - 1
then ex n being set st
( n in dom (inferior_realsequence seq) & x = (inferior_realsequence seq) . n ) by FUNCT_1:def 5;
hence x <= a - 1 by A5; :: thesis: verum

end;

then a - 1 is UpperBound of rng (inferior_realsequence seq) by XXREAL_2:def 1;
then a <= a - 1 by XXREAL_2:def 3;
then a + 0 < (a - 1) + 1 by XREAL_1:10;
hence contradiction ; :: thesis: verum

end;

then consider k2 being Element of NAT such that
A6: a - 1 <= (inferior_realsequence seq) . k2 ;
take k = max k1,k2; :: thesis: seq ^\ k is bounded
k2 <= k by XXREAL_0:25;
then (inferior_realsequence seq) . k2 <= (inferior_realsequence seq) . k by Th7;
then A7: a - 1 <= (inferior_realsequence seq) . k by A6, XXREAL_0:2;
k1 <= k by XXREAL_0:25;
then (superior_realsequence seq) . k <= (superior_realsequence seq) . k1 by Th7;
then A8: (superior_realsequence seq) . k <= a + 1 by A4, XXREAL_0:2;
A9: for n being Element of NAT st k <= n holds
( seq . n <= a + 1 & a - 1 <= seq . n )

proof

let n be Element of NAT ; :: thesis: ( k <= n implies ( seq . n <= a + 1 & a - 1 <= seq . n ) )
A10: (inferior_realsequence seq) . n <= seq . n by Th8;
assume A11: k <= n ; :: thesis: ( seq . n <= a + 1 & a - 1 <= seq . n )
then (superior_realsequence seq) . n <= (superior_realsequence seq) . k by Th7;
then A12: (superior_realsequence seq) . n <= a + 1 by A8, XXREAL_0:2;
(inferior_realsequence seq) . k <= (inferior_realsequence seq) . n by A11, Th7;
then A13: a - 1 <= (inferior_realsequence seq) . n by A7, XXREAL_0:2;
seq . n <= (superior_realsequence seq) . n by Th8;
hence ( seq . n <= a + 1 & a - 1 <= seq . n ) by A12, A13, A10, XXREAL_0:2; :: thesis: verum

end;

now

let x be ext-real number ; :: thesis: ( x in rng (seq ^\ k) implies x <= a + 1 )
assume x in rng (seq ^\ k) ; :: thesis: x <= a + 1
then consider n being set such that
A14: n in dom (seq ^\ k) and
A15: x = (seq ^\ k) . n by FUNCT_1:def 5;
reconsider n = n as Element of NAT by A14;
A16: k <= n + k by NAT_1:11;
x = seq . (n + k) by A15, NAT_1:def 3;
hence x <= a + 1 by A9, A16; :: thesis: verum

end;

then a + 1 is UpperBound of rng (seq ^\ k) by XXREAL_2:def 1;
hence rng (seq ^\ k) is bounded_above by XXREAL_2:def 10; :: according to RINFSUP2:def 4,RINFSUP2:def 5 :: thesis: seq ^\ k is bounded_below

now

let x be ext-real number ; :: thesis: ( x in rng (seq ^\ k) implies a - 1 <= x )
assume x in rng (seq ^\ k) ; :: thesis: a - 1 <= x
then consider n being set such that
A17: n in dom (seq ^\ k) and
A18: x = (seq ^\ k) . n by FUNCT_1:def 5;
reconsider n = n as Element of NAT by A17;
A19: k <= n + k by NAT_1:11;
x = seq . (n + k) by A18, NAT_1:def 3;
hence a - 1 <= x by A9, A19; :: thesis: verum

end;

then a - 1 is LowerBound of rng (seq ^\ k) by XXREAL_2:def 2;
hence rng (seq ^\ k) is bounded_below by XXREAL_2:def 9; :: according to RINFSUP2:def 3 :: thesis: verum