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

now

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

end;

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