let GX be TopSpace; :: thesis: for A, B, C being Subset of GX st A is connected & A c= B \/ C & B,C are_separated & not A c= B holds

A c= C

let A, B, C be Subset of GX; :: thesis: ( A is connected & A c= B \/ C & B,C are_separated & not A c= B implies A c= C )

assume that

A1: A is connected and

A2: A c= B \/ C and

A3: B,C are_separated ; :: thesis: ( A c= B or A c= C )

A4: A /\ C c= C by XBOOLE_1:17;

A /\ B c= B by XBOOLE_1:17;

then A5: A /\ B,A /\ C are_separated by A3, A4, Th7;

A6: (A /\ B) \/ (A /\ C) = A /\ (B \/ C) by XBOOLE_1:23

.= A by A2, XBOOLE_1:28 ;

assume that

A7: not A c= B and

A8: not A c= C ; :: thesis: contradiction

A meets C by A2, A7, XBOOLE_1:73;

then A9: A /\ C <> {} ;

A meets B by A2, A8, XBOOLE_1:73;

then A10: A /\ B <> {} ;

then A <> {} GX ;

hence contradiction by A1, A10, A9, A5, A6, Th15; :: thesis: verum

A c= C

let A, B, C be Subset of GX; :: thesis: ( A is connected & A c= B \/ C & B,C are_separated & not A c= B implies A c= C )

assume that

A1: A is connected and

A2: A c= B \/ C and

A3: B,C are_separated ; :: thesis: ( A c= B or A c= C )

A4: A /\ C c= C by XBOOLE_1:17;

A /\ B c= B by XBOOLE_1:17;

then A5: A /\ B,A /\ C are_separated by A3, A4, Th7;

A6: (A /\ B) \/ (A /\ C) = A /\ (B \/ C) by XBOOLE_1:23

.= A by A2, XBOOLE_1:28 ;

assume that

A7: not A c= B and

A8: not A c= C ; :: thesis: contradiction

A meets C by A2, A7, XBOOLE_1:73;

then A9: A /\ C <> {} ;

A meets B by A2, A8, XBOOLE_1:73;

then A10: A /\ B <> {} ;

then A <> {} GX ;

hence contradiction by A1, A10, A9, A5, A6, Th15; :: thesis: verum