A1:
P is_antisymmetric_in field P
by Def12;

let a be object ; :: according to RELAT_2:def 4,RELAT_2:def 12 :: thesis: for y being object st a in field (P /\ R) & y in field (P /\ R) & [a,y] in P /\ R & [y,a] in P /\ R holds

a = y

let b be object ; :: thesis: ( a in field (P /\ R) & b in field (P /\ R) & [a,b] in P /\ R & [b,a] in P /\ R implies a = b )

assume that

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

A2: [a,b] in P /\ R and

A3: [b,a] in P /\ R ; :: thesis: a = b

A4: [b,a] in P by A3, XBOOLE_0:def 4;

A5: [a,b] in P by A2, XBOOLE_0:def 4;

then ( a in field P & b in field P ) by RELAT_1:15;

hence a = b by A1, A5, A4; :: thesis: verum

let a be object ; :: according to RELAT_2:def 4,RELAT_2:def 12 :: thesis: for y being object st a in field (P /\ R) & y in field (P /\ R) & [a,y] in P /\ R & [y,a] in P /\ R holds

a = y

let b be object ; :: thesis: ( a in field (P /\ R) & b in field (P /\ R) & [a,b] in P /\ R & [b,a] in P /\ R implies a = b )

assume that

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

A2: [a,b] in P /\ R and

A3: [b,a] in P /\ R ; :: thesis: a = b

A4: [b,a] in P by A3, XBOOLE_0:def 4;

A5: [a,b] in P by A2, XBOOLE_0:def 4;

then ( a in field P & b in field P ) by RELAT_1:15;

hence a = b by A1, A5, A4; :: thesis: verum