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 :: thesis: for x being ExtReal st x in rng seq2 holds
inf (rng seq1) <= x

let x be ExtReal; :: thesis: ( x in rng seq2 implies inf (rng seq1) <= x )

A2: now :: thesis: for n being Element of NAT holds inf (rng seq1) <= seq2 . n

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

end;

assume x in rng seq2 ; :: thesis: inf (rng seq1) <= x
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: 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