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 Th24, Th25;
then A2: ( oContMaps (X,Sierpinski_Space) is complete & oContMaps (X,Sierpinski_Space) is continuous ) by A1, Th23;
InclPoset the topology of X, oContMaps (X,Sierpinski_Space) are_isomorphic by Th6;
hence InclPoset the topology of X is continuous by A2, WAYBEL15:9, WAYBEL_1:6; :: thesis: verum