let n be Element of 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 )
assume A1: seq is bounded ; :: thesis: (inferior_realsequence seq) . n <= (superior_realsequence seq) . n
reconsider Y1 = { (seq . k) where k is Element of NAT : n <= k } as Subset of REAL by Th29;
A2: (superior_realsequence seq) . n = sup Y1 by Def5;
A3: (inferior_realsequence seq) . n = inf Y1 by Def4;
( Y1 <> {} & Y1 is bounded ) by A1, Th33, SETLIM_1:1;
hence (inferior_realsequence seq) . n <= (superior_realsequence seq) . n by A2, A3, SEQ_4:24; :: thesis: verum