let n be Nat; :: thesis: for seq being Real_Sequence st seq is bounded holds
(inferior_realsequence seq) . n <= (superior_realsequence seq) . n
let seq be Real_Sequence; :: thesis: ( seq is bounded implies (inferior_realsequence seq) . n <= (superior_realsequence seq) . n )
reconsider Y1 = { (seq . k) where k is Nat : n <= k } as Subset of REAL by Th29;
assume A1: seq is bounded ; :: thesis: (inferior_realsequence seq) . n <= (superior_realsequence seq) . n
A2: Y1 <> {} by SETLIM_1:1;
( (superior_realsequence seq) . n = upper_bound Y1 & (inferior_realsequence seq) . n = lower_bound Y1 ) by Def4, Def5;
hence (inferior_realsequence seq) . n <= (superior_realsequence seq) . n by A1, A2, Th33, SEQ_4:11; :: thesis: verum