let GX be TopSpace; 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; ( 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
; A \/ B is connected
assume
not A \/ B is connected
; 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 ( A c= P implies not B c= P )end;
A14:
now ( A c= Q implies not B c= Q )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; verum