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 that
A1: FT is symmetric and
A2: A is_a_component_of FT and
A3: B is_a_component_of FT ; :: thesis: ( A = B or A,B are_separated )
A4: A is connected by A2, Def4;
A5: A c= A \/ B by XBOOLE_1:7;
assume that
A6: A <> B and
A7: not A,B are_separated ; :: thesis: contradiction
B is connected by A3, Def4;
then A \/ B is connected by A1, A7, A4, Th34;
then ( B c= A \/ B & A = A \/ B ) by A2, A5, Def4, XBOOLE_1:7;
hence contradiction by A3, A6, A4, Def4; :: thesis: verum