:: deftheorem defines partition_topology UNIFORM3:def 19 :
for X being set
for D being a_partition of X holds partition_topology D = TopStruct(# X,(UniCl D) #);