for FT being non empty filled RelStr
for A, B being Subset of FT st FT is symmetric holds
( A,B are_separated iff A misses B ^b ) by Th8;