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;

assume that

A5: A <> B and

A6: not A,B are_separated ; :: thesis: contradiction

B is connected by A3;

then A \/ B is connected by A1, A6, A4, Th33;

then ( B c= A \/ B & A = A \/ B ) by A2, XBOOLE_1:7;

hence contradiction by A3, A5, A4; :: thesis: verum

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;

assume that

A5: A <> B and

A6: not A,B are_separated ; :: thesis: contradiction

B is connected by A3;

then A \/ B is connected by A1, A6, A4, Th33;

then ( B c= A \/ B & A = A \/ B ) by A2, XBOOLE_1:7;

hence contradiction by A3, A5, A4; :: thesis: verum