let seq be ExtREAL_sequence; :: thesis:
assume that
A1: lim_sup seq = lim_inf seq and
A2: lim_inf seq in REAL ; :: thesis:
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

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

let x be ExtReal; :: thesis:
assume x in rng (superior_realsequence seq) ; :: thesis:
then ex n being object st
( n in dom (superior_realsequence seq) & x = (superior_realsequence seq) . n ) by FUNCT_1:def 3;
hence a + 1 <= x by A3; :: thesis:

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:29; :: thesis:

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

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

let x be ExtReal; :: thesis:
assume x in rng (inferior_realsequence seq) ; :: thesis:
then ex n being object st
( n in dom (inferior_realsequence seq) & x = (inferior_realsequence seq) . n ) by FUNCT_1:def 3;
hence x <= a - 1 by A5; :: thesis:

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:8;
hence contradiction ; :: thesis:

end;

then consider k2 being Element of NAT such that
A6: a - 1 <= (inferior_realsequence seq) . k2 ;
take k = max (k1,k2); :: thesis:
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 )

let n be Element of NAT ; :: thesis:
A10: (inferior_realsequence seq) . n <= seq . n by Th8;
assume A11: k <= n ; :: thesis:
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:

end;

let x be ExtReal; :: thesis:
assume x in rng (seq ^\ k) ; :: thesis:
then consider n being object such that
A14: n in dom (seq ^\ k) and
A15: x = (seq ^\ k) . n by FUNCT_1:def 3;
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:

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:

let x be ExtReal; :: thesis:
assume x in rng (seq ^\ k) ; :: thesis:
then consider n being object such that
A17: n in dom (seq ^\ k) and
A18: x = (seq ^\ k) . n by FUNCT_1:def 3;
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:

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: