:: deftheorem defines T_1-reflex T_1TOPSP:def 2 :
for T being non empty TopSpace holds T_1-reflex T = space (Intersection (Closed_Partitions T));