for X being set
for D being a_partition of X
for O being closed Subset of (partition_topology D) holds O is open