:: deftheorem defines are_separated FINTOPO4:def 1 :
for FT being non empty RelStr
for A, B being Subset of FT holds
( A,B are_separated iff ( A ^b misses B & A misses B ^b ) );