let n be Element of 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 Element of 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

let m be Element of NAT ; :: thesis: lower_bound Y2 <= (superior_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_below by XXREAL_2:def 11;
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 bounded by A1, Th33;
then Y1 is bounded_above by XXREAL_2:def 11;
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