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 )

( 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

hence
( A \/ B is connected & A \/ C is connected )
by A1, A2, A3, A4; :: thesis: verumA \/ 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

end;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

hence
A \/ B is connected
by Th15; :: thesis: verumQ = {} 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 A7, XBOOLE_1:45

.= (P \/ Q) \/ C by A9, XBOOLE_1:4 ;

end;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 :: 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 A10, Th1, Th7;

then P c= B by A9, XBOOLE_1:7, XBOOLE_1:73;

then P,C are_separated by A8, Th7;

then A13: P,Q \/ C are_separated by A10, Th8;

[#] GX = P \/ (Q \/ C) by A11, XBOOLE_1:4;

hence ( P = {} GX or Q = {} GX ) by A5, A13; :: thesis: verum

end;then P misses A by A10, Th1, Th7;

then P c= B by A9, XBOOLE_1:7, XBOOLE_1:73;

then P,C are_separated by A8, Th7;

then A13: P,Q \/ C are_separated by A10, Th8;

[#] GX = P \/ (Q \/ C) by A11, XBOOLE_1:4;

hence ( P = {} GX or Q = {} GX ) by A5, A13; :: thesis: verum

now :: thesis: ( not A c= P or P = {} GX or Q = {} GX )

hence
( P = {} GX or Q = {} GX )
by A6, A9, A10, A12, Th16, XBOOLE_1:7; :: thesis: verumassume
A c= P
; :: thesis: ( P = {} GX or Q = {} GX )

then Q misses A by A10, Th1, Th7;

then Q c= B by A9, XBOOLE_1:7, XBOOLE_1:73;

then Q,C are_separated by A8, Th7;

then A14: Q,P \/ C are_separated by A10, Th8;

[#] GX = Q \/ (P \/ C) by A11, XBOOLE_1:4;

hence ( P = {} GX or Q = {} GX ) by A5, A14; :: thesis: verum

end;then Q misses A by A10, Th1, Th7;

then Q c= B by A9, XBOOLE_1:7, XBOOLE_1:73;

then Q,C are_separated by A8, Th7;

then A14: Q,P \/ C are_separated by A10, Th8;

[#] GX = Q \/ (P \/ C) by A11, XBOOLE_1:4;

hence ( P = {} GX or Q = {} GX ) by A5, A14; :: thesis: verum