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