let R be Relation; :: thesis: ( R is asymmetric iff for x, y being object st [x,y] in R holds
not [y,x] in R )
A1: ( R is asymmetric implies for x, y being object st [x,y] in R holds
not [y,x] in R )

proof

assume Z0: R is asymmetric ; :: thesis: for x, y being object st [x,y] in R holds
not [y,x] in R
let x, y be object ; :: thesis: ( [x,y] in R implies not [y,x] in R )
assume B1: [x,y] in R ; :: thesis: 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 Z0, RELAT_2:def 5, RELAT_2:def 13, B1; :: thesis: verum

end;

( ( for x, y being object st [x,y] in R holds
not [y,x] in R ) implies R is asymmetric )

proof

assume Z1: for x, y being object st [x,y] in R holds
not [y,x] in R ; :: thesis: R is asymmetric
set X = field R;
for x, y being object st x in field R & y in field R & [x,y] in R holds
not [y,x] in R by Z1;
hence R is asymmetric by RELAT_2:def 13, RELAT_2:def 5; :: thesis: verum

end;

hence ( R is asymmetric iff for x, y being object st [x,y] in R holds
not [y,x] in R ) by A1; :: thesis: verum