let P, R be Relation; :: thesis: ( P is asymmetric & R is asymmetric implies P /\ R is asymmetric )
assume that
P is asymmetric and
A1: R is asymmetric ; :: thesis: P /\ R is asymmetric
A2: R is_asymmetric_in field R by A1, Def13;
A3: field (P /\ R) c= (field P) /\ (field R) by RELAT_1:34;

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 A4: ( a in field (P /\ R) & b in field (P /\ R) & [a,b] in P /\ R ) ; :: thesis: not [b,a] in P /\ R
then A5: ( a in field P & a in field R ) by A3, XBOOLE_0:def 4;
A6: ( b in field P & b in field R ) by A3, A4, XBOOLE_0:def 4;
( [a,b] in P & [a,b] in R ) by A4, XBOOLE_0:def 4;
then not [b,a] in R by A2, A5, A6, Def5;
hence not [b,a] in P /\ R by XBOOLE_0:def 4; :: thesis: verum

end;

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