:: deftheorem defines T_1-reflect T_1TOPSP:def 3 :
for T being non empty TopSpace holds T_1-reflect T = Proj (Intersection (Closed_Partitions T));