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 = {} ;
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;
A14: now :: thesis: ( A c= Q implies not B c= Q )
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;
( not A c= P or not B c= Q ) by A3, A5, Th7;
hence contradiction by A1, A2, A4, A5, A10, A8, A14, Th16, XBOOLE_1:7; :: thesis: verum