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;

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

hence
A \/ B is connected
by A1, Th6; :: thesis: verumQ = {} 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 A4, XBOOLE_1:45

.= (P \/ Q) \/ C by A7, XBOOLE_1:4 ;

end;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 :: thesis: ( not A c= Q or P = {} FT or Q = {} FT )

A11:
[#] FT = P \/ (Q \/ C)
by A9, XBOOLE_1:4;

assume A c= Q ; :: thesis: ( P = {} FT or Q = {} FT )

then P misses A by A1, A8, Th28, FINTOPO4:6;

then P c= B by A7, XBOOLE_1:7, XBOOLE_1:73;

then A12: P,C are_separated by A5, Th28;

then P misses Q \/ C by A1, A8, Th29, FINTOPO4:6;

hence ( P = {} FT or Q = {} FT ) by A6, A8, A12, A11, Th3, Th29; :: thesis: verum

end;assume A c= Q ; :: thesis: ( P = {} FT or Q = {} FT )

then P misses A by A1, A8, Th28, FINTOPO4:6;

then P c= B by A7, XBOOLE_1:7, XBOOLE_1:73;

then A12: P,C are_separated by A5, Th28;

then P misses Q \/ C by A1, A8, Th29, FINTOPO4:6;

hence ( P = {} FT or Q = {} FT ) by A6, A8, A12, A11, Th3, Th29; :: thesis: verum

now :: thesis: ( not A c= P or P = {} FT or Q = {} FT )

hence
( P = {} FT or Q = {} FT )
by A1, A3, A7, A8, A10, Th32, XBOOLE_1:7; :: thesis: verumA13:
[#] FT = Q \/ (P \/ C)
by A9, XBOOLE_1:4;

assume A c= P ; :: thesis: ( P = {} FT or Q = {} FT )

then Q misses A by A1, A8, Th28, FINTOPO4:6;

then Q c= B by A7, XBOOLE_1:7, XBOOLE_1:73;

then A14: Q,C are_separated by A5, Th28;

then Q misses P \/ C by A1, A8, Th29, FINTOPO4:6;

hence ( P = {} FT or Q = {} FT ) by A6, A8, A14, A13, Th3, Th29; :: thesis: verum

end;assume A c= P ; :: thesis: ( P = {} FT or Q = {} FT )

then Q misses A by A1, A8, Th28, FINTOPO4:6;

then Q c= B by A7, XBOOLE_1:7, XBOOLE_1:73;

then A14: Q,C are_separated by A5, Th28;

then Q misses P \/ C by A1, A8, Th29, FINTOPO4:6;

hence ( P = {} FT or Q = {} FT ) by A6, A8, A14, A13, Th3, Th29; :: thesis: verum