for X being non empty TopSpace
for A1, A2 being Subset of X st A1,A2 constitute_a_decomposition holds
( A1 is closed iff A2 is open ) by Th11;