:: deftheorem defines T_1/2 TOPGEN_4:def 8 :
for T being TopSpace holds
( T is T_1/2 iff for A being Subset of T holds Der A is closed );