let S, X be non empty set ; for R being Relation of X st R is asymmetric holds
R is_asymmetric_in S
let R be Relation of X; ( R is asymmetric implies R is_asymmetric_in S )
assume
R is asymmetric
; R is_asymmetric_in S
then A1:
R is_asymmetric_in field R
;
let x, y be object ; RELAT_2:def 5 ( not x in S or not y in S or not [x,y] in R or not [y,x] in R )
assume
( x in S & y in S )
; ( not [x,y] in R or not [y,x] in R )
assume A2:
[x,y] in R
; not [y,x] in R
then
( x in field R & y in field R )
by RELAT_1:15;
hence
not [y,x] in R
by A1, A2; verum