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