let X be non empty TopSpace; :: thesis: for Y being monotone-convergence T_0-TopSpace
for N being net of ContMaps X,(Omega Y)
for f, g being Function of X,(Omega Y) st f = "\/" (rng the mapping of N),((Omega Y) |^ the carrier of X) & ex_sup_of rng the mapping of N,(Omega Y) |^ the carrier of X & g in rng the mapping of N holds
g <= f
let Y be monotone-convergence T_0-TopSpace; :: thesis: for N being net of ContMaps X,(Omega Y)
for f, g being Function of X,(Omega Y) st f = "\/" (rng the mapping of N),((Omega Y) |^ the carrier of X) & ex_sup_of rng the mapping of N,(Omega Y) |^ the carrier of X & g in rng the mapping of N holds
g <= f
let N be net of ContMaps X,(Omega Y); :: thesis: for f, g being Function of X,(Omega Y) st f = "\/" (rng the mapping of N),((Omega Y) |^ the carrier of X) & ex_sup_of rng the mapping of N,(Omega Y) |^ the carrier of X & g in rng the mapping of N holds
g <= f
let f, g be Function of X,(Omega Y); :: thesis: ( f = "\/" (rng the mapping of N),((Omega Y) |^ the carrier of X) & ex_sup_of rng the mapping of N,(Omega Y) |^ the carrier of X & g in rng the mapping of N implies g <= f )
set m = the mapping of N;
set L = (Omega Y) |^ the carrier of X;
set s = "\/" (rng the mapping of N),((Omega Y) |^ the carrier of X);
assume that
A1: f = "\/" (rng the mapping of N),((Omega Y) |^ the carrier of X) and
A2: ex_sup_of rng the mapping of N,(Omega Y) |^ the carrier of X and
A3: g in rng the mapping of N ; :: thesis: g <= f
reconsider g1 = g as Element of ((Omega Y) |^ the carrier of X) by WAYBEL24:19;
rng the mapping of N is_<=_than "\/" (rng the mapping of N),((Omega Y) |^ the carrier of X) by A2, YELLOW_0:def 9;
then g1 <= "\/" (rng the mapping of N),((Omega Y) |^ the carrier of X) by A3, LATTICE3:def 9;
hence g <= f by A1, WAYBEL10:12; :: thesis: verum