let R be non empty reflexive RelStr ; id the carrier of R c= the InternalRel of R /\ the InternalRel of (R ~)
let a be object ; TARSKI:def 3 ( not a in id the carrier of R or a in the InternalRel of R /\ the InternalRel of (R ~) )
assume A1:
a in id the carrier of R
; a in the InternalRel of R /\ the InternalRel of (R ~)
then consider y, z being object such that
A2:
a = [y,z]
by RELAT_1:def 1;
reconsider y = y, z = z as Element of R by A1, A2, ZFMISC_1:87;
y <= z
by A1, A2, RELAT_1:def 10;
then A3:
a in the InternalRel of R
by A2, ORDERS_2:def 5;
y = z
by A1, A2, RELAT_1:def 10;
then
a in the InternalRel of (R ~)
by A2, A3, RELAT_1:def 7;
hence
a in the InternalRel of R /\ the InternalRel of (R ~)
by A3, XBOOLE_0:def 4; verum