let R be Relation; :: thesis: ( R is asymmetric implies R ~ is asymmetric )
assume R is asymmetric ; :: thesis: R ~ is asymmetric
then A1: R is_asymmetric_in field R by Def13;

now

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

end;

then R ~ is_asymmetric_in field (R ~ ) by Def5;
hence R ~ is asymmetric by Def13; :: thesis: verum