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