let n be Element of NAT ; :: thesis: for seq being Real_Sequence st seq is non-decreasing & seq is bounded_above holds
(superior_realsequence seq) . n = (superior_realsequence seq) . (n + 1)
let seq be Real_Sequence; :: thesis: ( seq is non-decreasing & seq is bounded_above implies (superior_realsequence seq) . n = (superior_realsequence seq) . (n + 1) )
assume A1: ( seq is non-decreasing & seq is bounded_above ) ; :: thesis: (superior_realsequence seq) . n = (superior_realsequence seq) . (n + 1)
then seq . n <= (superior_realsequence seq) . (n + 1) by Th67;
then max (((superior_realsequence seq) . (n + 1)),(seq . n)) = (superior_realsequence seq) . (n + 1) by XXREAL_0:def 10;
hence (superior_realsequence seq) . n = (superior_realsequence seq) . (n + 1) by A1, Th49; :: thesis: verum