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

now

let a, b be set ; :: thesis: ( a in field (P \ R) & b in field (P \ R) & [a,b] in P \ R implies not [b,a] in P \ R )
assume that
a in field (P \ R) and
b in field (P \ R) and
A2: [a,b] in P \ R ; :: thesis: not [b,a] in P \ R
A3: [a,b] in P by A2, XBOOLE_0:def 5;
then ( a in field P & b in field P ) by RELAT_1:15;
then not [b,a] in P by A1, A3, Def5;
hence not [b,a] in P \ R by XBOOLE_0:def 5; :: thesis: verum

end;

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