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 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;
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 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;
hence ( P = {} GX or Q = {} GX ) by A6, A9, A10, A12, Th16, XBOOLE_1:7; :: 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