let GX be TopSpace; 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; ( 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
; ( 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
; 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; verum