A1:
P is_asymmetric_in field P
by Def13;
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
a in field (P \ R)
and
b in field (P \ R)
and
A2:
[a,b] in P \ R
; 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;
hence
not [b,a] in P \ R
by XBOOLE_0:def 5; verum