:: 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 } ;