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 )

_{3}[Y]
; :: thesis: InclPoset the topology of Y is continuous

then S_{4}[Y]
by Lm2;

then S_{5}[Y]
by Lm4;

then S_{6}[Y]
by Lm5;

hence InclPoset the topology of Y is continuous by Lm7; :: thesis: verum

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

assume
Sassume
InclPoset the topology of Y is continuous
; :: thesis: S_{3}[Y]

then S_{6}[Y]
by Lm8;

then S_{4}[Y]
by Lm6;

hence S_{3}[Y]
by Lm3; :: thesis: verum

end;then S

then S

hence S

then S

then S

then S

hence InclPoset the topology of Y is continuous by Lm7; :: thesis: verum