:: deftheorem Def10 defines with_2nd_class_subsets ISOMICHI:def 10 :
for T being TopSpace holds
( T is with_2nd_class_subsets iff ex A being Subset of T st A is 2nd_class );