:: deftheorem defines are_weakly_separated TSEP_1:def 5 :
for X being TopStruct
for A1, A2 being Subset of X holds
( A1,A2 are_weakly_separated iff A1 \ A2,A2 \ A1 are_separated );