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

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