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 Th16;
A8: ( not A c= Q or not B c= P ) by A3, A5, Th8;
P misses Q by A5, Th2;
then A9: P /\ Q = {} by XBOOLE_0:def 7;

A10: now

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, XBOOLE_0:def 10;
hence contradiction by A7, A9, XBOOLE_1:7, XBOOLE_1:28; :: thesis: verum

end;

A14: now

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, XBOOLE_0:def 10;
hence contradiction by A6, A9, XBOOLE_1:7, XBOOLE_1:28; :: thesis: verum

end;

( not A c= P or not B c= Q ) by A3, A5, Th8;
hence contradiction by A1, A2, A4, A5, A10, A8, A14, Th17, XBOOLE_1:7; :: thesis: verum