let seq1, seq2 be Real_Sequence; :: thesis: ( seq1 is bounded & seq2 is bounded & ( for n being 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 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, Th57, Th58;
superior_realsequence seq2 is bounded by A2, Th56;
then A5: lim (superior_realsequence seq2) = lower_bound (superior_realsequence seq2) by A2, Th25, Th51;
inferior_realsequence seq1 is bounded by A1, Th56;
then A6: lim (inferior_realsequence seq1) = upper_bound (inferior_realsequence seq1) by A1, Th24, Th50;
superior_realsequence seq1 is bounded by A1, Th56;
then A7: lim (superior_realsequence seq1) = lower_bound (superior_realsequence seq1) by A1, Th25, Th51;
A8: ( superior_realsequence seq2 is convergent & inferior_realsequence seq2 is convergent ) by A2, Th57, Th58;
inferior_realsequence seq2 is bounded by A2, Th56;
then A9: lim (inferior_realsequence seq2) = upper_bound (inferior_realsequence seq2) by A2, Th24, Th50;
( ( for n being Nat holds (superior_realsequence seq1) . n <= (superior_realsequence seq2) . n ) & ( for n being Nat holds (inferior_realsequence seq1) . n <= (inferior_realsequence seq2) . n ) ) by A1, A2, A3, Th75;
hence ( lim_sup seq1 <= lim_sup seq2 & lim_inf seq1 <= lim_inf seq2 ) by A4, A8, A7, A6, A5, A9, SEQ_2:18; :: thesis: verum