let FT be non empty RelStr ; 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; ( 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
; ( 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
; 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; verum