let GX be TopSpace; :: thesis: for A, B, C being Subset of GX st GX is connected & A is connected & ([#] GX) \ A = B \/ C & B,C are_separated holds
( A \/ B is connected & A \/ C is connected )
let A, B, C be Subset of GX; :: thesis: ( GX is connected & A is connected & ([#] GX) \ A = B \/ C & B,C are_separated implies ( A \/ B is connected & A \/ C is connected ) )
assume that
A1: GX is connected and
A2: A is connected and
A3: ([#] GX) \ A = B \/ C and
A4: B,C are_separated ; :: thesis: ( A \/ B is connected & A \/ C is connected )

now

let A, B, C be Subset of GX; :: thesis: ( GX is connected & A is connected & ([#] GX) \ A = B \/ C & B,C are_separated implies A \/ B is connected )
assume that
A5: GX is connected and
A6: A is connected and
A7: ([#] GX) \ A = B \/ C and
A8: B,C are_separated ; :: thesis: A \/ B is connected

now

let P, Q be Subset of GX; :: thesis: ( A \/ B = P \/ Q & P,Q are_separated & not P = {} GX implies Q = {} GX )
assume that
A9: A \/ B = P \/ Q and
A10: P,Q are_separated ; :: thesis: ( P = {} GX or Q = {} GX )
A11: [#] GX = A \/ (B \/ C) by A7, XBOOLE_1:45
.= (P \/ Q) \/ C by A9, XBOOLE_1:4 ;

A12: now

assume A c= Q ; :: thesis: ( P = {} GX or Q = {} GX )
then P misses A by A10, Th2, Th8;
then P c= B by A9, XBOOLE_1:7, XBOOLE_1:73;
then P,C are_separated by A8, Th8;
then A13: P,Q \/ C are_separated by A10, Th9;
[#] GX = P \/ (Q \/ C) by A11, XBOOLE_1:4;
hence ( P = {} GX or Q = {} GX ) by A5, A13, Def2; :: thesis: verum

end;

now

assume A c= P ; :: thesis: ( P = {} GX or Q = {} GX )
then Q misses A by A10, Th2, Th8;
then Q c= B by A9, XBOOLE_1:7, XBOOLE_1:73;
then Q,C are_separated by A8, Th8;
then A14: Q,P \/ C are_separated by A10, Th9;
[#] GX = Q \/ (P \/ C) by A11, XBOOLE_1:4;
hence ( P = {} GX or Q = {} GX ) by A5, A14, Def2; :: thesis: verum

end;

hence ( P = {} GX or Q = {} GX ) by A6, A9, A10, A12, Th17, XBOOLE_1:7; :: thesis: verum

end;

hence A \/ B is connected by Th16; :: thesis: verum

end;

hence ( A \/ B is connected & A \/ C is connected ) by A1, A2, A3, A4; :: thesis: verum