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 A1: FT is symmetric ; :: thesis: ( A,B are_separated iff ( A ^f misses B & A misses B ^f ) )
then A2: A ^b = A ^f by FIN_TOPO:17;
B ^b = B ^f by A1, FIN_TOPO:17;
hence ( A,B are_separated iff ( A ^f misses B & A misses B ^f ) ) by A2, Def1; :: thesis: verum