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

A2: now :: thesis: for m being Nat holds upper_bound Y2 >= (inferior_realsequence seq) . m

let m be Nat; :: thesis: upper_bound Y2 >= (inferior_realsequence seq) . m
reconsider Y1 = { (seq . k1) where k1 is 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 real-bounded by A1, Th33;
then Y2 is bounded_above ;
then A4: upper_bound Y2 >= seq . (n + m) by A3, SEQ_4:def 1;
m <= n + m by NAT_1:11;
then A5: seq . (n + m) in Y1 ;
Y1 is real-bounded by A1, Th33;
then Y1 is bounded_below ;
then A6: seq . (n + m) >= lower_bound Y1 by A5, SEQ_4:def 2;
(inferior_realsequence seq) . m = lower_bound Y1 by Def4;
hence upper_bound Y2 >= (inferior_realsequence seq) . m by A6, A4, XXREAL_0:2; :: thesis: verum

end;

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