let R be Relation; :: thesis: ( R is antisymmetric iff for x, y being object st [x,y] in R & [y,x] in R holds
x = y )
thus ( R is antisymmetric implies for x, y being object st [x,y] in R & [y,x] in R holds
x = y ) :: thesis: ( ( for x, y being object 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 object 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 object ; :: thesis: ( [x,y] in R & [y,x] in R implies x = y )
assume that
A2: [x,y] in R and
A3: [y,x] in R ; :: thesis: x = y
( x in field R & y in field R ) by A2, RELAT_1:15;
hence x = y by A1, A2, A3, RELAT_2:def 4; :: thesis: verum

end;

assume for x, y being object st [x,y] in R & [y,x] in R holds
x = y ; :: thesis: R is antisymmetric
then for x, y being object 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