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 16 :: thesis: contradiction
set P2 = A /\ P;
set Q2 = A /\ Q;
A10: A /\ P misses A /\ Q by A8, XBOOLE_1:76;
A11: Q ^b misses P by A1, A9, Th5;

A12: now :: thesis: ( A c= Q implies not B c= P )

assume that
A13: A c= Q and
A14: 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 A13, FIN_TOPO:14, XBOOLE_1:63;
hence contradiction by A11, A14, XBOOLE_1:63; :: thesis: verum

end;

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

then not A ^b misses B by A1, Th5;
then Q ^b meets B by A13, FIN_TOPO:14, XBOOLE_1:63;
hence contradiction by A11, A14, XBOOLE_1:63; :: thesis: verum

end;

end;

end;

A15: now :: thesis: not A /\ P = {}

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

A18: now :: thesis: not B /\ Q = {}

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 A12, A17, XBOOLE_1:18; :: thesis: verum

end;

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

end;

A22: now :: thesis: ( A c= P implies not B c= Q )

assume that
A23: A c= P and
A24: B c= Q ; :: thesis: contradiction
A25: A ^b c= P ^b by A23, FIN_TOPO:14;

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, A24, A25, XBOOLE_1:64; :: thesis: verum

end;

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

then not A ^b misses B by A1, Th5;
hence contradiction by A9, A24, A25, XBOOLE_1:64; :: thesis: verum

end;

end;

end;

A26: now :: thesis: not A /\ Q = {}

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

A29: now :: thesis: not B /\ P = {}

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 A22, A28, XBOOLE_1:18; :: thesis: verum

end;

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

end;

( (A /\ P) ^b c= P ^b & A /\ Q c= Q ) by FIN_TOPO:14, XBOOLE_1:17;
then A33: (A /\ P) ^b misses A /\ Q by A9, XBOOLE_1:64;
(A /\ P) \/ (A /\ Q) = A /\ (P \/ Q) by XBOOLE_1:23
.= A by A5, XBOOLE_1:21 ;
hence contradiction by A2, A15, A26, A10, A33; :: thesis: verum