theorem Th55: :: MESFUNC5:55

for L, G being ExtREAL_sequence st ( for n being Nat holds L . n <= G . n ) holds
sup (rng L) <= sup (rng G)