begin
theorem Th2:
theorem Th5:
theorem Th11:
:: deftheorem defines Closed_Partitions T_1TOPSP:def 1 :
for T being non empty TopSpace holds Closed_Partitions T = { A where A is a_partition of the carrier of T : A is closed } ;
:: 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));
theorem Th12:
:: 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));
theorem Th13:
theorem Th14:
theorem Th15:
theorem Th16:
:: deftheorem defines T_1-reflex T_1TOPSP:def 4 :
for T, S being non empty TopSpace
for f being continuous Function of T,S
for b4 being continuous Function of (T_1-reflex T),(T_1-reflex S) holds
( b4 = T_1-reflex f iff (T_1-reflect S) * f = b4 * (T_1-reflect T) );