theorem :: UNIFORM3:41

for X being non empty set
for D being a_partition of X holds OpenClosedSet (partition_topology D) = the topology of (partition_topology D)