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;
P misses Q by A5, Th2;
then A8: P /\ Q = {} by XBOOLE_0:def 7;

A9: now

assume ( A c= P & B c= P ) ; :: thesis: contradiction
then ( A \/ B c= P & P c= P \/ Q ) by XBOOLE_1:7, XBOOLE_1:8;
then P \/ Q = P by A4, XBOOLE_0:def 10;
hence contradiction by A7, A8, XBOOLE_1:7, XBOOLE_1:28; :: thesis: verum

end;

A10: ( not A c= P or not B c= Q ) by A3, A5, Th8;
A11: ( not A c= Q or not B c= P ) by A3, A5, Th8;

now

assume ( A c= Q & B c= Q ) ; :: thesis: contradiction
then ( A \/ B c= Q & Q c= Q \/ P ) by XBOOLE_1:7, XBOOLE_1:8;
then Q \/ P = Q by A4, XBOOLE_0:def 10;
hence contradiction by A6, A8, XBOOLE_1:7, XBOOLE_1:28; :: thesis: verum

end;

hence contradiction by A1, A2, A4, A5, A9, A10, A11, Th17, XBOOLE_1:7; :: thesis: verum