let GX be TopSpace; :: thesis: for A, B being Subset of GX st A is closed & B is closed & A \/ B is connected & A /\ B is connected holds
( A is connected & B is connected )
let A, B be Subset of GX; :: thesis: ( A is closed & B is closed & A \/ B is connected & A /\ B is connected implies ( A is connected & B is connected ) )
assume that
A1: A is closed and
A2: B is closed ; :: thesis: ( not A \/ B is connected or not A /\ B is connected or ( A is connected & B is connected ) )
assume that
A3: A \/ B is connected and
A4: A /\ B is connected ; :: thesis: ( A is connected & B is connected )
A5: GX | (A \/ B) is connected by A3, Def3;
A6: A \/ B = [#] (GX | (A \/ B)) by PRE_TOPC:def 10;
set AB = A \/ B;
reconsider A1 = A as Subset of (GX | (A \/ B)) by A6, XBOOLE_1:7;
reconsider B1 = B as Subset of (GX | (A \/ B)) by A6, XBOOLE_1:7;
A7: ([#] (GX | (A \/ B))) \ (A1 /\ B1) = (A1 \ B1) \/ (B1 \ A1) by A6, XBOOLE_1:55;
A8: (A1 /\ B1) \/ (A1 \ B1) = A1 by XBOOLE_1:51;
A9: (A1 /\ B1) \/ (B1 \ A1) = B1 by XBOOLE_1:51;
A10: A /\ ([#] (GX | (A \/ B))) = A by A6, XBOOLE_1:7, XBOOLE_1:28;
B /\ ([#] (GX | (A \/ B))) = B by A6, XBOOLE_1:7, XBOOLE_1:28;
then ( A1 is closed & B1 is closed ) by A1, A2, A10, PRE_TOPC:43;
then A11: A1 \ B1,B1 \ A1 are_separated by Th10;
A1 /\ B1 is connected by A4, Th24;
then ( A1 is connected & B1 is connected ) by A5, A7, A8, A9, A11, Th21;
hence ( A is connected & B is connected ) by Th24; :: thesis: verum