for FT being non empty RelStr
for A, B being Subset of FT st FT is symmetric holds
( A,B are_separated iff ( A ^f misses B & A misses B ^f ) ) by FIN_TOPO:12;