let FT be non empty RelStr ; :: thesis: for A, B, C being Subset of FT st FT is filled & A is connected & A c= B \/ C & B,C are_separated & not A c= B holds

A c= C

let A, B, C be Subset of FT; :: thesis: ( FT is filled & A is connected & A c= B \/ C & B,C are_separated & not A c= B implies A c= C )

assume that

A1: FT is filled and

A2: A is connected and

A3: A c= B \/ C and

A4: B,C are_separated ; :: thesis: ( A c= B or A c= C )

A5: (A /\ B) \/ (A /\ C) = A /\ (B \/ C) by XBOOLE_1:23

.= A by A3, XBOOLE_1:28 ;

assume that

A6: not A c= B and

A7: not A c= C ; :: thesis: contradiction

A meets B by A3, A7, XBOOLE_1:73;

then A8: A /\ B <> {} ;

A meets C by A3, A6, XBOOLE_1:73;

then A9: A /\ C <> {} ;

A10: ( A /\ B c= B & A /\ C c= C ) by XBOOLE_1:17;

then ( {} FT = {} & A /\ B misses A /\ C ) by A1, A4, Th28, FINTOPO4:6;

hence contradiction by A2, A4, A8, A9, A10, A5, Th3, Th28; :: thesis: verum

A c= C

let A, B, C be Subset of FT; :: thesis: ( FT is filled & A is connected & A c= B \/ C & B,C are_separated & not A c= B implies A c= C )

assume that

A1: FT is filled and

A2: A is connected and

A3: A c= B \/ C and

A4: B,C are_separated ; :: thesis: ( A c= B or A c= C )

A5: (A /\ B) \/ (A /\ C) = A /\ (B \/ C) by XBOOLE_1:23

.= A by A3, XBOOLE_1:28 ;

assume that

A6: not A c= B and

A7: not A c= C ; :: thesis: contradiction

A meets B by A3, A7, XBOOLE_1:73;

then A8: A /\ B <> {} ;

A meets C by A3, A6, XBOOLE_1:73;

then A9: A /\ C <> {} ;

A10: ( A /\ B c= B & A /\ C c= C ) by XBOOLE_1:17;

then ( {} FT = {} & A /\ B misses A /\ C ) by A1, A4, Th28, FINTOPO4:6;

hence contradiction by A2, A4, A8, A9, A10, A5, Th3, Th28; :: thesis: verum