A1:
P is_antisymmetric_in field P
by Def12;
let a be object ; RELAT_2:def 4,RELAT_2:def 12 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 ; ( 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
; 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; verum