let FT be non empty RelStr ; :: thesis: 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 ) )
let A, B be Subset of FT; :: thesis: ( FT is symmetric implies ( A,B are_separated iff ( A ^f misses B & A misses B ^f ) ) )
assume FT is symmetric ; :: thesis: ( A,B are_separated iff ( A ^f misses B & A misses B ^f ) )
then ( A ^b = A ^f & B ^b = B ^f ) by FIN_TOPO:17;
hence ( A,B are_separated iff ( A ^f misses B & A misses B ^f ) ) by Def1; :: thesis: verum