:: deftheorem defines are_separated CONNSP_1:def 1 :
for GX being TopStruct
for A, B being Subset of GX holds
( A,B are_separated iff ( Cl A misses B & A misses Cl B ) );