let R be RelStr ; ( R is asymmetric implies the InternalRel of R misses the InternalRel of R ~ )
assume
R is asymmetric
; 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 ~
; 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; verum