let GX be TopSpace; :: thesis: for A, B being Subset of GX st A is connected & B is connected & not A,B are_separated holds

A \/ B is connected

let A, B be Subset of GX; :: thesis: ( A is connected & B is connected & not A,B are_separated implies A \/ B is connected )

assume that

A1: A is connected and

A2: B is connected and

A3: not A,B are_separated ; :: thesis: A \/ B is connected

assume not A \/ B is connected ; :: thesis: contradiction

then consider P, Q being Subset of GX such that

A4: A \/ B = P \/ Q and

A5: P,Q are_separated and

A6: P <> {} GX and

A7: Q <> {} GX by Th15;

A8: ( not A c= Q or not B c= P ) by A3, A5, Th7;

P misses Q by A5, Th1;

then A9: P /\ Q = {} ;

hence contradiction by A1, A2, A4, A5, A10, A8, A14, Th16, XBOOLE_1:7; :: thesis: verum

A \/ B is connected

let A, B be Subset of GX; :: thesis: ( A is connected & B is connected & not A,B are_separated implies A \/ B is connected )

assume that

A1: A is connected and

A2: B is connected and

A3: not A,B are_separated ; :: thesis: A \/ B is connected

assume not A \/ B is connected ; :: thesis: contradiction

then consider P, Q being Subset of GX such that

A4: A \/ B = P \/ Q and

A5: P,Q are_separated and

A6: P <> {} GX and

A7: Q <> {} GX by Th15;

A8: ( not A c= Q or not B c= P ) by A3, A5, Th7;

P misses Q by A5, Th1;

then A9: P /\ Q = {} ;

A10: now :: thesis: ( A c= P implies not B c= P )

A11:
P c= P \/ Q
by XBOOLE_1:7;

assume that

A12: A c= P and

A13: B c= P ; :: thesis: contradiction

A \/ B c= P by A12, A13, XBOOLE_1:8;

then P \/ Q = P by A4, A11;

hence contradiction by A7, A9, XBOOLE_1:7, XBOOLE_1:28; :: thesis: verum

end;assume that

A12: A c= P and

A13: B c= P ; :: thesis: contradiction

A \/ B c= P by A12, A13, XBOOLE_1:8;

then P \/ Q = P by A4, A11;

hence contradiction by A7, A9, XBOOLE_1:7, XBOOLE_1:28; :: thesis: verum

A14: now :: thesis: ( A c= Q implies not B c= Q )

( not A c= P or not B c= Q )
by A3, A5, Th7;A15:
Q c= Q \/ P
by XBOOLE_1:7;

assume that

A16: A c= Q and

A17: B c= Q ; :: thesis: contradiction

A \/ B c= Q by A16, A17, XBOOLE_1:8;

then Q \/ P = Q by A4, A15;

hence contradiction by A6, A9, XBOOLE_1:7, XBOOLE_1:28; :: thesis: verum

end;assume that

A16: A c= Q and

A17: B c= Q ; :: thesis: contradiction

A \/ B c= Q by A16, A17, XBOOLE_1:8;

then Q \/ P = Q by A4, A15;

hence contradiction by A6, A9, XBOOLE_1:7, XBOOLE_1:28; :: thesis: verum

hence contradiction by A1, A2, A4, A5, A10, A8, A14, Th16, XBOOLE_1:7; :: thesis: verum