let R be RelStr ; :: thesis: ( R is asymmetric implies the InternalRel of R misses the InternalRel of R ~ )
assume A1: R is asymmetric ; :: thesis: the InternalRel of R misses the InternalRel of R ~
assume the InternalRel of R meets the InternalRel of R ~ ; :: thesis: contradiction
then consider x being set such that
A2: x in the InternalRel of R and
A3: x in the InternalRel of R ~ by XBOOLE_0:3;
consider y, z being set such that
A4: x = [y,z] by A3, RELAT_1:def 1;
A5: [z,y] in the InternalRel of R by A3, A4, RELAT_1:def 7;
the InternalRel of R is asymmetric by A1, Def5;
then A6: the InternalRel of R is_asymmetric_in field the InternalRel of R by RELAT_2:def 13;
( y in field the InternalRel of R & z in field the InternalRel of R ) by A2, A4, RELAT_1:30;
hence contradiction by A2, A4, A5, A6, RELAT_2:def 5; :: thesis: verum