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 ) )
set AB = A \/ B;
A3: A \/ B = [#] (GX | (A \/ B)) by PRE_TOPC:def 5;
then reconsider B1 = B as Subset of (GX | (A \/ B)) by XBOOLE_1:7;
reconsider A1 = A as Subset of (GX | (A \/ B)) by A3, XBOOLE_1:7;
A4: ([#] (GX | (A \/ B))) \ (A1 /\ B1) = (A1 \ B1) \/ (B1 \ A1) by A3, XBOOLE_1:55;
B /\ ([#] (GX | (A \/ B))) = B by A3, XBOOLE_1:7, XBOOLE_1:28;
then A5: B1 is closed by A2, PRE_TOPC:13;
A /\ ([#] (GX | (A \/ B))) = A by A3, XBOOLE_1:7, XBOOLE_1:28;
then A1 is closed by A1, PRE_TOPC:13;
then A6: A1 \ B1,B1 \ A1 are_separated by A5, Th9;
assume that
A7: A \/ B is connected and
A8: A /\ B is connected ; :: thesis: ( A is connected & B is connected )
A9: GX | (A \/ B) is connected by A7;
A10: A1 /\ B1 is connected by A8, Th23;
(A1 /\ B1) \/ (B1 \ A1) = B1 by XBOOLE_1:51;
then A11: B1 is connected by A9, A4, A6, A10, Th20;
(A1 /\ B1) \/ (A1 \ B1) = A1 by XBOOLE_1:51;
then A1 is connected by A9, A4, A6, A10, Th20;
hence ( A is connected & B is connected ) by A11, Th23; :: thesis: verum