A1:
P is_asymmetric_in field P
by Def13;

let a be object ; :: according to RELAT_2:def 5,RELAT_2:def 13 :: thesis: 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 ; :: 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;

hence not [b,a] in P \ R by XBOOLE_0:def 5; :: thesis: verum

let a be object ; :: according to RELAT_2:def 5,RELAT_2:def 13 :: thesis: 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 ; :: 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;

hence not [b,a] in P \ R by XBOOLE_0:def 5; :: thesis: verum