let FT be non empty RelStr ; :: thesis: 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; :: thesis: ( 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 ; :: thesis: ( A c= B or A c= C )
assume ( not A c= B & not A c= C ) ; :: thesis: contradiction
then ( A meets B & A meets C ) by A3, XBOOLE_1:73;
then A5: ( A /\ B <> {} & A /\ C <> {} ) by XBOOLE_0:def 7;
A6: {} FT = {} ;
A7: ( A /\ B c= B & A /\ C c= C ) by XBOOLE_1:17;
then A8: A /\ B misses A /\ C by A1, A4, Th29, FINTOPO4:6;
(A /\ B) \/ (A /\ C) = A /\ (B \/ C) by XBOOLE_1:23
.= A by A3, XBOOLE_1:28 ;
hence contradiction by A2, A4, A5, A6, A7, A8, Th4, Th29; :: thesis: verum