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;
hence g <= f by A1, WAYBEL10:11; :: thesis: verum