let L, G be ExtREAL_sequence; :: thesis: ( ( for n being Nat holds L . n <= G . n ) implies sup (rng L) <= sup (rng G) )
assume A1: for n being Nat holds L . n <= G . n ; :: thesis: sup (rng L) <= sup (rng G)

A2: now :: thesis: for n being Element of NAT holds L . n <= sup (rng G)

let n be Element of NAT ; :: thesis: L . n <= sup (rng G)
dom G = NAT by FUNCT_2:def 1;
then A3: G . n in rng G by FUNCT_1:def 3;
A4: L . n <= G . n by A1;
sup (rng G) is UpperBound of rng G by XXREAL_2:def 3;
then G . n <= sup (rng G) by A3, XXREAL_2:def 1;
hence L . n <= sup (rng G) by A4, XXREAL_0:2; :: thesis: verum

end;

now :: thesis: for x being ExtReal st x in rng L holds
x <= sup (rng G)

let x be ExtReal; :: thesis: ( x in rng L implies x <= sup (rng G) )
assume x in rng L ; :: thesis: x <= sup (rng G)
then ex z being object st
( z in dom L & x = L . z ) by FUNCT_1:def 3;
hence x <= sup (rng G) by A2; :: thesis: verum

end;

then sup (rng G) is UpperBound of rng L by XXREAL_2:def 1;
hence sup (rng L) <= sup (rng G) by XXREAL_2:def 3; :: thesis: verum