let Y be T_0-TopSpace; :: thesis: ( InclPoset the topology of Y is continuous iff for X being non empty TopSpace holds Theta (X,Y) is isomorphic )

hereby :: thesis: ( ( for X being non empty TopSpace holds Theta (X,Y) is isomorphic ) implies InclPoset the topology of Y is continuous )

assume InclPoset the topology of Y is continuous ; :: thesis: S₃[Y]
then S₆[Y] by Lm8;
then S₄[Y] by Lm6;
hence S₃[Y] by Lm3; :: thesis: verum

end;

assume S₃[Y] ; :: thesis: InclPoset the topology of Y is continuous
then S₄[Y] by Lm2;
then S₅[Y] by Lm4;
then S₆[Y] by Lm5;
hence InclPoset the topology of Y is continuous by Lm7; :: thesis: verum