let R be Relation; :: thesis: ( R is antisymmetric implies R ~ is antisymmetric )
assume R is antisymmetric ; :: thesis: R ~ is antisymmetric
then A1: R is_antisymmetric_in field R by Def12;

now

let x, y be set ; :: thesis: ( x in field (R ~ ) & y in field (R ~ ) & [x,y] in R ~ & [y,x] in R ~ implies x = y )
assume ( x in field (R ~ ) & y in field (R ~ ) & [x,y] in R ~ & [y,x] in R ~ ) ; :: thesis: x = y
then ( x in field R & y in field R & [y,x] in R & [x,y] in R ) by RELAT_1:38, RELAT_1:def 7;
hence x = y by A1, Def4; :: thesis: verum

end;

then R ~ is_antisymmetric_in field (R ~ ) by Def4;
hence R ~ is antisymmetric by Def12; :: thesis: verum