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 ^b misses B )
let A, B be Subset of FT; :: thesis: ( FT is symmetric implies ( A,B are_separated iff A ^b misses B ) )
assume A1: FT is symmetric ; :: thesis: ( A,B are_separated iff A ^b misses B )
thus ( A,B are_separated implies A ^b misses B ) by Def1; :: thesis: ( A ^b misses B implies A,B are_separated )
thus ( A ^b misses B implies A,B are_separated ) :: thesis: verum

proof

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

end;