let GX be TopSpace; :: thesis: for A, B being Subset of GX st A is a_component & B is a_component & not A = B holds

A,B are_separated

let A, B be Subset of GX; :: thesis: ( A is a_component & B is a_component & not A = B implies A,B are_separated )

assume that

A1: A is a_component and

A2: B is a_component ; :: thesis: ( A = B or A,B are_separated )

( A <> B implies A,B are_separated )

A,B are_separated

let A, B be Subset of GX; :: thesis: ( A is a_component & B is a_component & not A = B implies A,B are_separated )

assume that

A1: A is a_component and

A2: B is a_component ; :: thesis: ( A = B or A,B are_separated )

( A <> B implies A,B are_separated )

proof

hence
( A = B or A,B are_separated )
; :: thesis: verum
A3:
B c= A \/ B
by XBOOLE_1:7;

A4: A c= A \/ B by XBOOLE_1:7;

assume A5: A <> B ; :: thesis: A,B are_separated

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

then A \/ B is connected by A1, A2, Th17;

then A = A \/ B by A1, A4;

hence contradiction by A1, A2, A5, A3; :: thesis: verum

end;A4: A c= A \/ B by XBOOLE_1:7;

assume A5: A <> B ; :: thesis: A,B are_separated

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

then A \/ B is connected by A1, A2, Th17;

then A = A \/ B by A1, A4;

hence contradiction by A1, A2, A5, A3; :: thesis: verum