let seq1, seq2 be ExtREAL_sequence; :: thesis:
assume A1: for n being Nat holds seq1 . n <= seq2 . n ; :: thesis:

let x be ExtReal; :: thesis:

A2: now :: thesis:

let n be Element of NAT ; :: thesis:
dom seq1 = NAT by FUNCT_2:def 1;
then A3: seq1 . n in rng seq1 by FUNCT_1:def 3;
A4: seq1 . n <= seq2 . n by A1;
inf (rng seq1) is LowerBound of rng seq1 by XXREAL_2:def 4;
then inf (rng seq1) <= seq1 . n by A3, XXREAL_2:def 2;
hence inf (rng seq1) <= seq2 . n by A4, XXREAL_0:2; :: thesis:

end;

assume x in rng seq2 ; :: thesis:
then ex z being object st
( z in dom seq2 & x = seq2 . z ) by FUNCT_1:def 3;
hence inf (rng seq1) <= x by A2; :: thesis:

end;

then inf (rng seq1) is LowerBound of rng seq2 by XXREAL_2:def 2;
hence inf (rng seq1) <= inf (rng seq2) by XXREAL_2:def 4; :: thesis: