A1:
R is_asymmetric_in field R
by Def13;
A2:
field (P /\ R) c= (field P) /\ (field R)
by RELAT_1:19;
let a be object ; RELAT_2:def 5,RELAT_2:def 13 for y being object st a in field (P /\ R) & y in field (P /\ R) & [a,y] in P /\ R holds
not [y,a] in P /\ R
let b be object ; ( a in field (P /\ R) & b in field (P /\ R) & [a,b] in P /\ R implies not [b,a] in P /\ R )
assume that
A3:
( a in field (P /\ R) & b in field (P /\ R) )
and
A4:
[a,b] in P /\ R
; not [b,a] in P /\ R
A5:
[a,b] in R
by A4, XBOOLE_0:def 4;
( a in field R & b in field R )
by A2, A3, XBOOLE_0:def 4;
then
not [b,a] in R
by A1, A5;
hence
not [b,a] in P /\ R
by XBOOLE_0:def 4; verum