let R be antisymmetric RelStr ; :: thesis: the InternalRel of R /\ the InternalRel of (R ~ ) c= id the carrier of R
let a be set ; :: according to TARSKI:def 3 :: thesis: ( 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 ~ ) ; :: thesis: a in id the carrier of R
then A2: a in the InternalRel of R by XBOOLE_0:def 4;
consider y, z being set such that
A3: a = [y,z] by A1, RELAT_1:def 1;
A4: ( y in the carrier of R & z in the carrier of R ) by A1, A3, ZFMISC_1:106;
reconsider y = y, z = z as Element of R by A1, A3, ZFMISC_1:106;
A5: y <= z by A2, A3, ORDERS_2:def 9;
a in the InternalRel of (R ~ ) by A1, XBOOLE_0:def 4;
then [z,y] in the InternalRel of R by A3, RELAT_1:def 7;
then z <= y by ORDERS_2:def 9;
then y = z by A5, ORDERS_2:25;
hence a in id the carrier of R by A3, A4, RELAT_1:def 10; :: thesis: verum