let seq1, seq2 be Real_Sequence; ( 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
; ( 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; verum