theorem Th40: :: WAYBEL25:40

for X being non empty TopSpace
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