:: deftheorem Def11 defines with_3rd_class_subsets ISOMICHI:def 11 :
for T being TopSpace holds
( T is with_3rd_class_subsets iff ex A being Subset of T st A is 3rd_class );