let FT be non empty RelStr ; :: thesis: for A, B, C being Subset of FT st FT is reflexive & FT is symmetric & FT is connected & A is connected & ([#] FT) \ A = B \/ C & B,C are_separated holds
A \/ B is connected
let A, B, C be Subset of FT; :: thesis: ( FT is reflexive & FT is symmetric & FT is connected & A is connected & ([#] FT) \ A = B \/ C & B,C are_separated implies A \/ B is connected )
assume that
A1: ( FT is reflexive & FT is symmetric ) and
A2: FT is connected and
A3: A is connected and
A4: ([#] FT) \ A = B \/ C and
A5: B,C are_separated ; :: thesis: A \/ B is connected
A6: [#] FT is connected by A2, Def1;

now

let P, Q be Subset of FT; :: thesis: ( A \/ B = P \/ Q & P misses Q & P,Q are_separated & not P = {} FT implies Q = {} FT )
assume that
A7: A \/ B = P \/ Q and
P misses Q and
A8: P,Q are_separated ; :: thesis: ( P = {} FT or Q = {} FT )
A9: [#] FT = A \/ (B \/ C) by A4, XBOOLE_1:45
.= (P \/ Q) \/ C by A7, XBOOLE_1:4 ;

A10: now

assume A c= P ; :: thesis: ( P = {} FT or Q = {} FT )
then Q misses A by A1, A8, Th29, FINTOPO4:6;
then Q c= B by A7, XBOOLE_1:7, XBOOLE_1:73;
then A11: Q,C are_separated by A5, Th29;
then A12: Q misses P \/ C by A1, A8, Th30, FINTOPO4:6;
[#] FT = Q \/ (P \/ C) by A9, XBOOLE_1:4;
then ( Q = {} FT or P \/ C = {} FT ) by A6, A8, A11, A12, Th4, Th30;
hence ( P = {} FT or Q = {} FT ) ; :: thesis: verum

end;

now

assume A c= Q ; :: thesis: ( P = {} FT or Q = {} FT )
then P misses A by A1, A8, Th29, FINTOPO4:6;
then P c= B by A7, XBOOLE_1:7, XBOOLE_1:73;
then A13: P,C are_separated by A5, Th29;
then A14: P misses Q \/ C by A1, A8, Th30, FINTOPO4:6;
[#] FT = P \/ (Q \/ C) by A9, XBOOLE_1:4;
then ( P = {} FT or Q \/ C = {} FT ) by A6, A8, A13, A14, Th4, Th30;
hence ( P = {} FT or Q = {} FT ) ; :: thesis: verum

end;

hence ( P = {} FT or Q = {} FT ) by A1, A3, A7, A8, A10, Th33, XBOOLE_1:7; :: thesis: verum

end;

hence A \/ B is connected by A1, Th7; :: thesis: verum