let n be Element of NAT ; :: thesis: for seq being Real_Sequence st seq is bounded holds
sup (inferior_realsequence seq) <= (superior_realsequence seq) . n
let seq be Real_Sequence; :: thesis: ( seq is bounded implies sup (inferior_realsequence seq) <= (superior_realsequence seq) . n )
reconsider Y2 = { (seq . k2) where k2 is Element of NAT : n <= k2 } as Subset of REAL by Th29;
assume A1: seq is bounded ; :: thesis: sup (inferior_realsequence seq) <= (superior_realsequence seq) . n

A2: now

let m be Element of NAT ; :: thesis: sup Y2 >= (inferior_realsequence seq) . m
reconsider Y1 = { (seq . k1) where k1 is Element of NAT : m <= k1 } as Subset of REAL by Th29;
n <= n + m by NAT_1:11;
then A3: seq . (n + m) in Y2 ;
Y2 is bounded by A1, Th33;
then Y2 is bounded_above by XXREAL_2:def 11;
then A4: sup Y2 >= seq . (n + m) by A3, SEQ_4:def 4;
m <= n + m by NAT_1:11;
then A5: seq . (n + m) in Y1 ;
Y1 is bounded by A1, Th33;
then Y1 is bounded_below by XXREAL_2:def 11;
then A6: seq . (n + m) >= inf Y1 by A5, SEQ_4:def 5;
(inferior_realsequence seq) . m = inf Y1 by Def4;
hence sup Y2 >= (inferior_realsequence seq) . m by A6, A4, XXREAL_0:2; :: thesis: verum

end;

(superior_realsequence seq) . n = sup Y2 by Def5;
hence sup (inferior_realsequence seq) <= (superior_realsequence seq) . n by A2, Th9; :: thesis: verum