let seq be Real_Sequence; :: thesis: ( seq is V89() implies inferior_realsequence seq is V48() )
assume seq is V89() ; :: thesis: inferior_realsequence seq is V48()
then for n being Element of NAT holds (inferior_realsequence seq) . n <= (inferior_realsequence seq) . (n + 1) by Th48;
hence inferior_realsequence seq is V48() by SEQM_3:def 8; :: thesis: verum