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