let FT be non empty filled RelStr ; :: thesis: for A, B being Subset of FT st FT is symmetric holds
( A,B are_separated iff A misses B ^b )
let A, B be Subset of FT; :: thesis: ( FT is symmetric implies ( A,B are_separated iff A misses B ^b ) )
assume A1: FT is symmetric ; :: thesis: ( A,B are_separated iff A misses B ^b )
thus ( A,B are_separated implies A misses B ^b ) by Def1; :: thesis: ( A misses B ^b implies A,B are_separated )
thus ( A misses B ^b implies A,B are_separated ) :: thesis: verum

proof

assume A2: A misses B ^b ; :: thesis: A,B are_separated
then A ^b misses B by A1, Th8;
hence A,B are_separated by A2, Def1; :: thesis: verum

end;