let seq1, seq2 be ExtREAL_sequence; :: thesis: ( ( for n being Nat holds seq1 . n <= seq2 . n ) implies inf (rng seq1) <= inf (rng seq2) )
assume A1: for n being Nat holds seq1 . n <= seq2 . n ; :: thesis: inf (rng seq1) <= inf (rng seq2)

now

let x be ext-real number ; :: thesis: ( x in rng seq2 implies inf (rng seq1) <= x )

A2: now

let n be Element of NAT ; :: thesis: inf (rng seq1) <= seq2 . n
dom seq1 = NAT by FUNCT_2:def 1;
then A3: seq1 . n in rng seq1 by FUNCT_1:def 5;
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: verum

end;

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

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: verum