let n be Nat; :: thesis: for seq being Real_Sequence st seq is bounded_above holds
(superior_realsequence seq) . (n + 1) <= (superior_realsequence seq) . n
let seq be Real_Sequence; :: thesis: ( seq is bounded_above implies (superior_realsequence seq) . (n + 1) <= (superior_realsequence seq) . n )
A1: (superior_realsequence seq) . (n + 1) <= max (((superior_realsequence seq) . (n + 1)),(seq . n)) by XXREAL_0:25;
assume seq is bounded_above ; :: thesis: (superior_realsequence seq) . (n + 1) <= (superior_realsequence seq) . n
hence (superior_realsequence seq) . (n + 1) <= (superior_realsequence seq) . n by A1, Th47; :: thesis: verum