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

( 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