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: S3[Y]
then S6[Y] by Lm8;
then S4[Y] by Lm6;
hence S3[Y] by Lm3; :: thesis: verum
end;
assume S3[Y] ; :: thesis: InclPoset the topology of Y is continuous
then S4[Y] by Lm2;
then S5[Y] by Lm4;
then S6[Y] by Lm5;
hence InclPoset the topology of Y is continuous by Lm7; :: thesis: verum