for X being TopSpace
for A1, A2 being Subset of X st A1 is open & A2 is open holds
A1,A2 are_weakly_separated