for seq1, seq2 being Real_Sequence st seq1 is bounded & seq2 is bounded & ( for n being Nat holds seq1 . n <= seq2 . n ) holds
( lim_sup seq1 <= lim_sup seq2 & lim_inf seq1 <= lim_inf seq2 )