let FT be non empty RelStr ; for A, B, C being Subset of FT st FT is reflexive & 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 reflexive & A is connected & A c= B \/ C & B,C are_separated & not A c= B implies A c= C )
assume that
A1:
FT is reflexive
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 <> {}
by XBOOLE_0:def 7;
A meets C
by A3, A6, XBOOLE_1:73;
then A9:
A /\ C <> {}
by XBOOLE_0:def 7;
A10:
( A /\ B c= B & A /\ C c= C )
by XBOOLE_1:17;
then
( {} FT = {} & A /\ B misses A /\ C )
by A1, A4, Th29, FINTOPO4:6;
hence
contradiction
by A2, A4, A8, A9, A10, A5, Th4, Th29; verum