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)

hence sup (rng L) <= sup (rng G) by XXREAL_2:def 3; :: thesis: verum

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;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

now :: thesis: for x being ExtReal st x in rng L holds

x <= sup (rng G)

then
sup (rng G) is UpperBound of rng L
by XXREAL_2:def 1;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;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

hence sup (rng L) <= sup (rng G) by XXREAL_2:def 3; :: thesis: verum