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 ( ( 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 ) ) )
assume that
A1: ( seq1 is bounded & seq2 is bounded ) and
A2: for n being Element of NAT holds seq1 . n <= seq2 . n ; :: thesis: ( ( 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 ) )

now

let n be Element of NAT ; :: thesis: ( (superior_realsequence seq1) . n <= (superior_realsequence seq2) . n & (inferior_realsequence seq1) . n <= (inferior_realsequence seq2) . n )
reconsider Y1 = { (seq1 . k1) where k1 is Element of NAT : n <= k1 } as Subset of REAL by Th29;
reconsider Y2 = { (seq2 . k2) where k2 is Element of NAT : n <= k2 } as Subset of REAL by Th29;
A3: ( (superior_realsequence seq1) . n = sup Y1 & (superior_realsequence seq2) . n = sup Y2 ) by Def5;
A4: ( (inferior_realsequence seq1) . n = inf Y1 & (inferior_realsequence seq2) . n = inf Y2 ) by Def4;
A5: ( Y1 <> {} & Y2 <> {} ) by SETLIM_1:1;
A6: ( Y1 is bounded & Y2 is bounded ) by A1, Th33;
then A7: ( Y1 is bounded_above & Y1 is bounded_below ) by XXREAL_2:def 11;
A8: ( Y2 is bounded_above & Y2 is bounded_below ) by A6, XXREAL_2:def 11;

A9: now

let r be real number ; :: thesis: ( r in Y1 implies r <= sup Y2 )
assume r in Y1 ; :: thesis: r <= sup Y2
then consider k being Element of NAT such that
A10: ( r = seq1 . k & n <= k ) ;
A11: r <= seq2 . k by A2, A10;
seq2 . k in Y2 by A10;
then seq2 . k <= sup Y2 by A8, SEQ_4:def 4;
hence r <= sup Y2 by A11, XXREAL_0:2; :: thesis: verum

end;

now

let r be real number ; :: thesis: ( r in Y2 implies inf Y1 <= r )
assume r in Y2 ; :: thesis: inf Y1 <= r
then consider k being Element of NAT such that
A12: ( r = seq2 . k & n <= k ) ;
A13: seq1 . k <= r by A2, A12;
seq1 . k in Y1 by A12;
then inf Y1 <= seq1 . k by A7, SEQ_4:def 5;
hence inf Y1 <= r by A13, XXREAL_0:2; :: thesis: verum

end;

then for r being Real st r in Y2 holds
inf Y1 <= r ;
hence ( (superior_realsequence seq1) . n <= (superior_realsequence seq2) . n & (inferior_realsequence seq1) . n <= (inferior_realsequence seq2) . n ) by A3, A4, A5, A9, COMPLSP1:84, TOPMETR3:1; :: thesis: verum

end;

hence ( ( 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 ) ) ; :: thesis: verum