let seq1, seq2 be Real_Sequence; :: thesis: ( seq1 is bounded & seq2 is bounded & ( for n being Nat holds seq1 . n <= seq2 . n ) implies ( ( 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 ) ) )
assume that
A1: seq1 is bounded and
A2: seq2 is bounded and
A3: for n being Nat holds seq1 . n <= seq2 . n ; :: thesis: ( ( 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 ) )

now :: thesis: for n being Nat holds
( (superior_realsequence seq1) . n <= (superior_realsequence seq2) . n & (inferior_realsequence seq1) . n <= (inferior_realsequence seq2) . n )

let n be Nat; :: thesis: ( (superior_realsequence seq1) . n <= (superior_realsequence seq2) . n & (inferior_realsequence seq1) . n <= (inferior_realsequence seq2) . n )
reconsider Y2 = { (seq2 . k2) where k2 is Nat : n <= k2 } as Subset of REAL by Th29;
reconsider Y1 = { (seq1 . k1) where k1 is Nat : n <= k1 } as Subset of REAL by Th29;
A4: ( Y1 <> {} & Y2 <> {} ) by SETLIM_1:1;
A5: ( (inferior_realsequence seq1) . n = lower_bound Y1 & (inferior_realsequence seq2) . n = lower_bound Y2 ) by Def4;
Y1 is real-bounded by A1, Th33;
then A6: Y1 is bounded_below ;

now :: thesis: for r being Real st r in Y2 holds
lower_bound Y1 <= r

let r be Real; :: thesis: ( r in Y2 implies lower_bound Y1 <= r )
assume r in Y2 ; :: thesis: lower_bound Y1 <= r
then consider k being Nat such that
A7: r = seq2 . k and
A8: n <= k ;
seq1 . k in Y1 by A8;
then A9: lower_bound Y1 <= seq1 . k by A6, SEQ_4:def 2;
seq1 . k <= r by A3, A7;
hence lower_bound Y1 <= r by A9, XXREAL_0:2; :: thesis: verum

end;

then A10: for r being Real st r in Y2 holds
lower_bound Y1 <= r ;
Y2 is real-bounded by A2, Th33;
then A11: Y2 is bounded_above ;

A12: now :: thesis: for r being Real st r in Y1 holds
r <= upper_bound Y2

let r be Real; :: thesis: ( r in Y1 implies r <= upper_bound Y2 )
assume r in Y1 ; :: thesis: r <= upper_bound Y2
then consider k being Nat such that
A13: r = seq1 . k and
A14: n <= k ;
seq2 . k in Y2 by A14;
then A15: seq2 . k <= upper_bound Y2 by A11, SEQ_4:def 1;
r <= seq2 . k by A3, A13;
hence r <= upper_bound Y2 by A15, XXREAL_0:2; :: thesis: verum

end;

( (superior_realsequence seq1) . n = upper_bound Y1 & (superior_realsequence seq2) . n = upper_bound Y2 ) by Def5;
hence ( (superior_realsequence seq1) . n <= (superior_realsequence seq2) . n & (inferior_realsequence seq1) . n <= (inferior_realsequence seq2) . n ) by A5, A4, A12, A10, SEQ_4:113, SEQ_4:144; :: thesis: verum

end;

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