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 that
A1: seq1 is bounded and
A2: seq2 is bounded and
A3: for n being Element of NAT holds seq1 . n <= seq2 . n ; :: thesis: ( lim_sup seq1 <= lim_sup seq2 & lim_inf seq1 <= lim_inf seq2 )
A4: ( superior_realsequence seq1 is convergent & inferior_realsequence seq1 is convergent ) by A1, Th59, Th60;
superior_realsequence seq2 is bounded by A2, Th58;
then A5: lim (superior_realsequence seq2) = inf (superior_realsequence seq2) by A2, Th25, Th53;
inferior_realsequence seq1 is bounded by A1, Th58;
then A6: lim (inferior_realsequence seq1) = sup (inferior_realsequence seq1) by A1, Th24, Th52;
superior_realsequence seq1 is bounded by A1, Th58;
then A7: lim (superior_realsequence seq1) = inf (superior_realsequence seq1) by A1, Th25, Th53;
A8: ( superior_realsequence seq2 is convergent & inferior_realsequence seq2 is convergent ) by A2, Th59, Th60;
inferior_realsequence seq2 is bounded by A2, Th58;
then A9: lim (inferior_realsequence seq2) = sup (inferior_realsequence seq2) by A2, Th24, Th52;
( ( 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, A2, A3, Th77;
hence ( lim_sup seq1 <= lim_sup seq2 & lim_inf seq1 <= lim_inf seq2 ) by A4, A8, A7, A6, A5, A9, SEQ_2:32; :: thesis: verum