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