let FT be non empty RelStr ; :: thesis: for A, B being Subset of FT st FT is symmetric & A is_a_component_of FT & B is_a_component_of FT & not A = B holds
A,B are_separated
let A, B be Subset of FT; :: thesis: ( FT is symmetric & A is_a_component_of FT & B is_a_component_of FT & not A = B implies A,B are_separated )
assume A1: ( FT is symmetric & A is_a_component_of FT & B is_a_component_of FT ) ; :: thesis: ( A = B or A,B are_separated )
assume that
A2: A <> B and
A3: not A,B are_separated ; :: thesis: contradiction
( A is connected & B is connected ) by A1, Def4;
then A4: A \/ B is connected by A1, A3, Th34;
( A c= A \/ B & B c= A \/ B ) by XBOOLE_1:7;
then ( A = A \/ B & B = A \/ B ) by A1, A4, Def4;
hence contradiction by A2; :: thesis: verum