let FT be non empty RelStr ; :: thesis: for A, B being Subset of FT st FT is symmetric & A is connected & B is connected & not A,B are_separated holds
A \/ B is connected
let A, B be Subset of FT; :: thesis: ( FT is symmetric & A is connected & B is connected & not A,B are_separated implies A \/ B is connected )
assume that
A1: FT is symmetric and
A2: A is connected and
A3: B is connected and
A4: not A,B are_separated ; :: thesis: A \/ B is connected
given P, Q being Subset of FT such that A5: A \/ B = P \/ Q and
A6: P <> {} and
A7: Q <> {} and
A8: P misses Q and
A9: P ^b misses Q ; :: according to FIN_TOPO:def 18 :: thesis: contradiction
A10: Q ^b misses P by A1, A9, Th6;

A11: now

assume A12: ( A c= P & B c= Q ) ; :: thesis: contradiction
then A13: A ^b c= P ^b by FIN_TOPO:19;

per cases ( A ^b meets B or A meets B ^b ) by A4, FINTOPO4:def 1;

suppose A ^b meets B ; :: thesis: contradiction

hence contradiction by A9, A12, A13, XBOOLE_1:64; :: thesis: verum

end;

suppose A meets B ^b ; :: thesis: contradiction

then not A ^b misses B by A1, Th6;
hence contradiction by A9, A12, A13, XBOOLE_1:64; :: thesis: verum

end;

end;

end;

A14: now

assume A15: ( A c= Q & B c= P ) ; :: thesis: contradiction

per cases ( A ^b meets B or A meets B ^b ) by A4, FINTOPO4:def 1;

suppose A ^b meets B ; :: thesis: contradiction

then Q ^b meets B by A15, FIN_TOPO:19, XBOOLE_1:63;
hence contradiction by A10, A15, XBOOLE_1:63; :: thesis: verum

end;

suppose A meets B ^b ; :: thesis: contradiction

then not A ^b misses B by A1, Th6;
then Q ^b meets B by A15, FIN_TOPO:19, XBOOLE_1:63;
hence contradiction by A10, A15, XBOOLE_1:63; :: thesis: verum

end;

end;

end;

A16: now

assume A17: A /\ P = {} ; :: thesis: contradiction
then A18: A /\ Q = (A /\ P) \/ (A /\ Q)
.= A /\ (P \/ Q) by XBOOLE_1:23
.= A by A5, XBOOLE_1:21 ;
A19: B /\ P = (A /\ P) \/ (B /\ P) by A17
.= (A \/ B) /\ P by XBOOLE_1:23
.= P by A5, XBOOLE_1:21 ;

A20: now

assume B /\ Q = {} ; :: thesis: contradiction
then B /\ P = (B /\ Q) \/ (B /\ P)
.= B /\ (Q \/ P) by XBOOLE_1:23
.= B by A5, XBOOLE_1:21 ;
hence contradiction by A14, A18, XBOOLE_1:18; :: thesis: verum

end;

set P3 = B /\ P;
set Q3 = B /\ Q;
A21: (B /\ P) \/ (B /\ Q) = B /\ (P \/ Q) by XBOOLE_1:23
.= B by A5, XBOOLE_1:21 ;
A22: B /\ P misses B /\ Q by A8, XBOOLE_1:76;
A23: (B /\ P) ^b c= P ^b by FIN_TOPO:19, XBOOLE_1:17;
B /\ Q c= Q by XBOOLE_1:17;
then (B /\ P) ^b misses B /\ Q by A9, A23, XBOOLE_1:64;
hence contradiction by A3, A6, A19, A20, A21, A22, FIN_TOPO:def 18; :: thesis: verum

end;

A24: now

assume A25: A /\ Q = {} ; :: thesis: contradiction
then A26: A /\ P = (A /\ Q) \/ (A /\ P)
.= A /\ (Q \/ P) by XBOOLE_1:23
.= A by A5, XBOOLE_1:21 ;
A27: B /\ Q = (A /\ Q) \/ (B /\ Q) by A25
.= (A \/ B) /\ Q by XBOOLE_1:23
.= Q by A5, XBOOLE_1:21 ;

A28: now

assume B /\ P = {} ; :: thesis: contradiction
then B /\ Q = (B /\ P) \/ (B /\ Q)
.= B /\ (P \/ Q) by XBOOLE_1:23
.= B by A5, XBOOLE_1:21 ;
hence contradiction by A11, A26, XBOOLE_1:18; :: thesis: verum

end;

set P3 = B /\ Q;
set Q3 = B /\ P;
A29: (B /\ P) \/ (B /\ Q) = B /\ (P \/ Q) by XBOOLE_1:23
.= B by A5, XBOOLE_1:21 ;
A30: B /\ Q misses B /\ P by A8, XBOOLE_1:76;
A31: (B /\ Q) ^b c= Q ^b by FIN_TOPO:19, XBOOLE_1:17;
B /\ P c= P by XBOOLE_1:17;
then (B /\ Q) ^b misses B /\ P by A10, A31, XBOOLE_1:64;
hence contradiction by A3, A7, A27, A28, A29, A30, FIN_TOPO:def 18; :: thesis: verum

end;

set P2 = A /\ P;
set Q2 = A /\ Q;
A32: (A /\ P) \/ (A /\ Q) = A /\ (P \/ Q) by XBOOLE_1:23
.= A by A5, XBOOLE_1:21 ;
A33: A /\ P misses A /\ Q by A8, XBOOLE_1:76;
A34: (A /\ P) ^b c= P ^b by FIN_TOPO:19, XBOOLE_1:17;
A /\ Q c= Q by XBOOLE_1:17;
then (A /\ P) ^b misses A /\ Q by A9, A34, XBOOLE_1:64;
hence contradiction by A2, A16, A24, A32, A33, FIN_TOPO:def 18; :: thesis: verum