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;

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

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

end;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;

end;

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;hence contradiction by A11, A14, XBOOLE_1:63; :: thesis: verum

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;then Q ^b meets B by A13, FIN_TOPO:14, XBOOLE_1:63;

hence contradiction by A11, A14, XBOOLE_1:63; :: thesis: verum

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 ;

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;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 = {}

set P3 = B /\ P;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;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

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

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;

end;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;

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

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

( (A /\ P) ^b c= P ^b & A /\ Q c= Q )
by FIN_TOPO:14, XBOOLE_1:17;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 ;

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;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 = {}

set P3 = B /\ Q;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;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

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

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