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 :: 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
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 :: thesis: for P, Q being Subset of GX st A \/ B = P \/ Q & P,Q are_separated & not P = {} GX holds
Q = {} GX
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
.= (P \/ Q) \/ C by ;
A12: now :: thesis: ( not A c= Q or P = {} GX or Q = {} GX )
assume A c= Q ; :: thesis: ( P = {} GX or Q = {} GX )
then P misses A by ;
then P c= B by ;
then P,C are_separated by ;
then A13: P,Q \/ C are_separated by ;
[#] GX = P \/ (Q \/ C) by ;
hence ( P = {} GX or Q = {} GX ) by ; :: thesis: verum
end;
now :: thesis: ( not A c= P or P = {} GX or Q = {} GX )
assume A c= P ; :: thesis: ( P = {} GX or Q = {} GX )
then Q misses A by ;
then Q c= B by ;
then Q,C are_separated by ;
then A14: Q,P \/ C are_separated by ;
[#] GX = Q \/ (P \/ C) by ;
hence ( P = {} GX or Q = {} GX ) by ; :: thesis: verum
end;
hence ( P = {} GX or Q = {} GX ) by ; :: thesis: verum
end;
hence A \/ B is connected by Th15; :: thesis: verum
end;
hence ( A \/ B is connected & A \/ C is connected ) by A1, A2, A3, A4; :: thesis: verum