let R be RelStr ; :: thesis: ( R is asymmetric implies the InternalRel of R misses the InternalRel of R ~ )
assume R is asymmetric ; :: thesis: the InternalRel of R misses the InternalRel of R ~
then the InternalRel of R is asymmetric ;
then A1: the InternalRel of R is_asymmetric_in field the InternalRel of R ;
assume the InternalRel of R meets the InternalRel of R ~ ; :: thesis: contradiction
then consider x being object 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 object such that
A4: x = [y,z] by A3, RELAT_1:def 1;
A5: z in field the InternalRel of R by A2, A4, RELAT_1:15;
( [z,y] in the InternalRel of R & y in field the InternalRel of R ) by A2, A3, A4, RELAT_1:15, RELAT_1:def 7;
hence contradiction by A2, A4, A1, A5; :: thesis: verum