let X be non empty TopSpace; :: thesis: for Y being non trivial monotone-convergence T_0-TopSpace st oContMaps X,Y is complete & oContMaps X,Y is continuous holds
InclPoset the topology of X is continuous
let Y be non trivial monotone-convergence T_0-TopSpace; :: thesis: ( oContMaps X,Y is complete & oContMaps X,Y is continuous implies InclPoset the topology of X is continuous )
assume A1: ( oContMaps X,Y is complete & oContMaps X,Y is continuous ) ; :: thesis: InclPoset the topology of X is continuous
then Sierpinski_Space is_Retract_of Y by Th25, Th26;
then A2: ( oContMaps X,Sierpinski_Space is complete & oContMaps X,Sierpinski_Space is continuous ) by A1, Th24;
InclPoset the topology of X, oContMaps X,Sierpinski_Space are_isomorphic by Th6;
hence InclPoset the topology of X is continuous by A2, WAYBEL15:11, WAYBEL_1:7; :: thesis: verum