let n be Nat; :: thesis: for seq being Real_Sequence st seq is non-increasing holds
(superior_realsequence seq) . (n + 1) <= seq . n
let seq be Real_Sequence; :: thesis: ( seq is non-increasing implies (superior_realsequence seq) . (n + 1) <= seq . n )
reconsider Y1 = { (seq . k) where k is Nat : n + 1 <= k } as Subset of REAL by Th29;
A1: (superior_realsequence seq) . (n + 1) = upper_bound Y1 by Def5;
assume A2: seq is non-increasing ; :: thesis: (superior_realsequence seq) . (n + 1) <= seq . n
then upper_bound Y1 = seq . (n + 1) by Th35;
hence (superior_realsequence seq) . (n + 1) <= seq . n by A2, A1; :: thesis: verum