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 that
A2: ( x in field (R ~) & y in field (R ~) ) and
A3: ( [x,y] in R ~ & [y,x] in R ~ ) ; :: thesis: x = y
A4: ( [y,x] in R & [x,y] in R ) by A3, RELAT_1:def 7;
( x in field R & y in field R ) by A2, RELAT_1:21;
hence x = y by A1, A4, Def4; :: thesis: verum

end;

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