let S be Subset of T; :: thesis: ( S is empty implies S is closed )
assume S is empty ; :: thesis: S is closed
then X: S = {} T ;
the carrier of T in the topology of T by Def1;
hence ([#] T) \ S is open by Def5, X; :: according to PRE_TOPC:def 6 :: thesis: verum