theorem Th75: :: RINFSUP1:75

for seq1, seq2 being Real_Sequence st seq1 is bounded & seq2 is bounded & ( for n being Nat holds seq1 . n <= seq2 . n ) holds
( ( 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 ) )