let seq1, seq2 be Real_Sequence; :: thesis: ( seq1 is bounded & seq2 is bounded & ( for n being Element of NAT holds seq1 . n <= seq2 . n ) implies ( lim_sup seq1 <= lim_sup seq2 & lim_inf seq1 <= lim_inf seq2 ) )
assume A1: ( seq1 is bounded & seq2 is bounded & ( for n being Element of NAT holds seq1 . n <= seq2 . n ) ) ; :: thesis: ( lim_sup seq1 <= lim_sup seq2 & lim_inf seq1 <= lim_inf seq2 )
then A2: ( superior_realsequence seq1 is convergent & inferior_realsequence seq1 is convergent & superior_realsequence seq2 is convergent & inferior_realsequence seq2 is convergent ) by Th59, Th60;
A3: ( ( for n being Element of NAT holds (superior_realsequence seq1) . n <= (superior_realsequence seq2) . n ) & ( for n being Element of NAT holds (inferior_realsequence seq1) . n <= (inferior_realsequence seq2) . n ) ) by A1, Th77;
( seq1 is bounded_above & seq1 is bounded_below & seq2 is bounded_above & seq2 is bounded_below ) by A1;
then A4: ( superior_realsequence seq1 is non-increasing & inferior_realsequence seq1 is non-decreasing & superior_realsequence seq2 is non-increasing & inferior_realsequence seq2 is non-decreasing ) by Th52, Th53;
( superior_realsequence seq1 is bounded & inferior_realsequence seq1 is bounded & superior_realsequence seq2 is bounded & inferior_realsequence seq2 is bounded ) by A1, Th58;
then ( superior_realsequence seq1 is bounded_below & inferior_realsequence seq1 is bounded_above & superior_realsequence seq2 is bounded_below & inferior_realsequence seq2 is bounded_above ) ;
then ( lim (superior_realsequence seq1) = inf (superior_realsequence seq1) & lim (inferior_realsequence seq1) = sup (inferior_realsequence seq1) & lim (superior_realsequence seq2) = inf (superior_realsequence seq2) & lim (inferior_realsequence seq2) = sup (inferior_realsequence seq2) ) by A4, Th24, Th25;
hence ( lim_sup seq1 <= lim_sup seq2 & lim_inf seq1 <= lim_inf seq2 ) by A2, A3, SEQ_2:32; :: thesis: verum