A1: P is_antisymmetric_in field P by Def12;
let a be set ; :: according to RELAT_2:def 4,RELAT_2:def 12 :: thesis: for y being set 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 set ; :: 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
A6: [a,b] in P \ R and
A7: [b,a] in P \ R ; :: thesis: a = b
A8: [b,a] in P by A7, XBOOLE_0:def 5;
A9: [a,b] in P by A6, XBOOLE_0:def 5;
then ( a in field P & b in field P ) by RELAT_1:15;
hence a = b by A1, A9, A8, Def4; :: thesis: verum