now :: thesis: for x, y being object st x in field (R \~) & y in field (R \~) & [x,y] in R \~ holds
not [y,x] in R \~

let x, y be object ; :: 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 \~) ;
hence R \~ is asymmetric ; :: thesis: verum