let seq1, seq2 be ExtREAL_sequence; :: thesis: ( ( for n being Nat holds seq1 . n <= seq2 . n ) implies ( lim_inf seq1 <= lim_inf seq2 & lim_sup seq1 <= lim_sup seq2 ) )
assume for n being Nat holds seq1 . n <= seq2 . n ; :: thesis: ( lim_inf seq1 <= lim_inf seq2 & lim_sup seq1 <= lim_sup seq2 )
then for n being Nat holds
( (inferior_realsequence seq1) . n <= (inferior_realsequence seq2) . n & (superior_realsequence seq1) . n <= (superior_realsequence seq2) . n ) by Th2;
hence ( lim_inf seq1 <= lim_inf seq2 & lim_sup seq1 <= lim_sup seq2 ) by Th1, MESFUNC5:55; :: thesis: verum