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

A2: now :: thesis: for m being Nat holds lower_bound Y2 <= (superior_realsequence seq) . m

let m be Nat; :: thesis: lower_bound Y2 <= (superior_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_below ;
then A4: lower_bound Y2 <= seq . (n + m) by A3, SEQ_4:def 2;
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_above ;
then A6: seq . (n + m) <= upper_bound Y1 by A5, SEQ_4:def 1;
(superior_realsequence seq) . m = upper_bound Y1 by Def5;
hence lower_bound Y2 <= (superior_realsequence seq) . m by A6, A4, XXREAL_0:2; :: thesis: verum

end;

(inferior_realsequence seq) . n = lower_bound Y2 by Def4;
hence (inferior_realsequence seq) . n <= lower_bound (superior_realsequence seq) by A2, Th10; :: thesis: verum