let FT be non empty RelStr ; :: thesis: for A, B, C being Subset of FT st FT is filled & 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 filled & 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 filled & 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;
now :: thesis: for P, Q being Subset of FT st A \/ B = P \/ Q & P misses Q & P,Q are_separated & not P = {} FT holds
Q = {} FT
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
.= (P \/ Q) \/ C by ;
A10: now :: thesis: ( not A c= Q or P = {} FT or Q = {} FT )
A11: [#] FT = P \/ (Q \/ C) by ;
assume A c= Q ; :: thesis: ( P = {} FT or Q = {} FT )
then P misses A by ;
then P c= B by ;
then A12: P,C are_separated by ;
then P misses Q \/ C by ;
hence ( P = {} FT or Q = {} FT ) by A6, A8, A12, A11, Th3, Th29; :: thesis: verum
end;
now :: thesis: ( not A c= P or P = {} FT or Q = {} FT )
A13: [#] FT = Q \/ (P \/ C) by ;
assume A c= P ; :: thesis: ( P = {} FT or Q = {} FT )
then Q misses A by ;
then Q c= B by ;
then A14: Q,C are_separated by ;
then Q misses P \/ C by ;
hence ( P = {} FT or Q = {} FT ) by A6, A8, A14, A13, Th3, Th29; :: thesis: verum
end;
hence ( P = {} FT or Q = {} FT ) by ; :: thesis: verum
end;
hence A \/ B is connected by ; :: thesis: verum