let R be non empty reflexive RelStr ; :: thesis: id the carrier of R c= the InternalRel of R /\ the InternalRel of (R ~ )
let a be set ; :: according to TARSKI:def 3 :: thesis: ( 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 ; :: thesis: a in the InternalRel of R /\ the InternalRel of (R ~ )
then consider y, z being set 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:106;
A3: y = z by A1, A2, RELAT_1:def 10;
y <= z by A1, A2, RELAT_1:def 10;
then A4: a in the InternalRel of R by A2, ORDERS_2:def 9;
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 A4, XBOOLE_0:def 4; :: thesis: verum