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 ; :: 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

A3: ( a in field (P /\ R) & b in field (P /\ R) ) and

A4: [a,b] in P /\ R ; :: thesis: 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; :: thesis: verum

A2: field (P /\ R) c= (field P) /\ (field R) by RELAT_1:19;

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

A3: ( a in field (P /\ R) & b in field (P /\ R) ) and

A4: [a,b] in P /\ R ; :: thesis: 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; :: thesis: verum