let GX be TopSpace; :: thesis: for A, B being Subset of GX st A is_a_component_of GX & B is_a_component_of GX & not A = B holds
A,B are_separated
let A, B be Subset of GX; :: thesis: ( A is_a_component_of GX & B is_a_component_of GX & not A = B implies A,B are_separated )
assume that
A1: A is_a_component_of GX and
A2: B is_a_component_of GX ; :: thesis: ( A = B or A,B are_separated )
( A <> B implies A,B are_separated )

proof

A3: B c= A \/ B by XBOOLE_1:7;
A4: A c= A \/ B by XBOOLE_1:7;
assume that
A5: A <> B and
A6: not A,B are_separated ; :: thesis: contradiction
A7: A is connected by A1, Def5;
B is connected by A2, Def5;
then A \/ B is connected by A6, A7, Th18;
then A = A \/ B by A1, A4, Def5;
hence contradiction by A2, A5, A7, A3, Def5; :: thesis: verum

end;

hence ( A = B or A,B are_separated ) ; :: thesis: verum