let seq be Real_Sequence; :: thesis: ( seq is V88() implies superior_realsequence seq is V49() )
assume seq is V88() ; :: thesis: superior_realsequence seq is V49()
then for n being Element of NAT holds (superior_realsequence seq) . (n + 1) <= (superior_realsequence seq) . n by Th49;
hence superior_realsequence seq is V49() by SEQM_3:def 9; :: thesis: verum