now

let x, y be set ; :: thesis: ( x in field (R \~ ) & y in field (R \~ ) & [x,y] in R \~ implies not [y,x] in R \~ )
assume that
x in field (R \~ ) and
y in field (R \~ ) and
A1: [x,y] in R \~ ; :: thesis: not [y,x] in R \~
not [x,y] in R ~ by A1, XBOOLE_0:def 5;
hence not [y,x] in R \~ by RELAT_1:def 7; :: thesis: verum

end;

then R \~ is_asymmetric_in field (R \~ ) by RELAT_2:def 5;
hence R \~ is asymmetric by RELAT_2:def 13; :: thesis: verum