for X being set
for D being a_partition of X
for S being Subset of (partition_topology D) holds
( S is open iff S is closed ) by Th18, Th19;