A1: P is_irreflexive_in field P by Def10;
let a be object ; :: according to RELAT_2:def 2,RELAT_2:def 10 :: thesis: ( a in field (P \ R) implies not [a,a] in P \ R )
A2: now :: thesis: ( a in dom (P \ R) implies not [a,a] in P )
assume a in dom (P \ R) ; :: thesis: not [a,a] in P
then consider b being object such that
A3: [a,b] in P \ R by XTUPLE_0:def 12;
[a,b] in P by A3, XBOOLE_0:def 5;
then a in field P by RELAT_1:15;
hence not [a,a] in P by A1; :: thesis: verum
end;
now :: thesis: ( a in rng (P \ R) implies not [a,a] in P )
assume a in rng (P \ R) ; :: thesis: not [a,a] in P
then consider b being object such that
A4: [b,a] in P \ R by XTUPLE_0:def 13;
[b,a] in P by A4, XBOOLE_0:def 5;
then a in field P by RELAT_1:15;
hence not [a,a] in P by A1; :: thesis: verum
end;
hence ( a in field (P \ R) implies not [a,a] in P \ R ) by A2, XBOOLE_0:def 3, XBOOLE_0:def 5; :: thesis: verum