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

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