let R be Relation; :: thesis: ( R is antisymmetric iff for x, y being set st [x,y] in R & [y,x] in R holds
x = y )
thus ( R is antisymmetric implies for x, y being set st [x,y] in R & [y,x] in R holds
x = y ) :: thesis: ( ( for x, y being set st [x,y] in R & [y,x] in R holds
x = y ) implies R is antisymmetric )

proof

assume R is antisymmetric ; :: thesis: for x, y being set st [x,y] in R & [y,x] in R holds
x = y
then A1: R is_antisymmetric_in field R by RELAT_2:def 12;
let x, y be set ; :: thesis: ( [x,y] in R & [y,x] in R implies x = y )
assume A2: ( [x,y] in R & [y,x] in R ) ; :: thesis: x = y
then ( x in field R & y in field R ) by RELAT_1:30;
hence x = y by A1, A2, RELAT_2:def 4; :: thesis: verum

end;

assume for x, y being set st [x,y] in R & [y,x] in R holds
x = y ; :: thesis: R is antisymmetric
then for x, y being set st x in field R & y in field R & [x,y] in R & [y,x] in R holds
x = y ;
then R is_antisymmetric_in field R by RELAT_2:def 4;
hence R is antisymmetric by RELAT_2:def 12; :: thesis: verum