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 )

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

now :: thesis: ( a in rng (P \ R) implies not [a,a] in P )

hence
( a in field (P \ R) implies not [a,a] in P \ R )
by A2, XBOOLE_0:def 3, XBOOLE_0:def 5; :: thesis: verumassume
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;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