let X be non empty TopSpace; :: thesis: for Y being monotone-convergence T_0-TopSpace holds oContMaps X,Y is up-complete
let Y be monotone-convergence T_0-TopSpace; :: thesis: oContMaps X,Y is up-complete
ContMaps X,(Omega Y) is full directed-sups-inheriting SubRelStr of (Omega Y) |^ the carrier of X by WAYBEL24:def 3, WAYBEL25:43;
hence oContMaps X,Y is up-complete by YELLOW16:5; :: thesis: verum