:: deftheorem defines with_1st_class_subsets ISOMICHI:def 9 :
for T being TopSpace holds
( T is with_1st_class_subsets iff ex A being Subset of T st A is 1st_class );