for X being TopSpace
for A1, A2 being Subset of X st A1 \/ A2 is open & A1,A2 are_separated holds
( A1 is open & A2 is open )