let P, R be Relation; :: thesis: ( P is irreflexive implies P \ R is irreflexive )
assume P is irreflexive ; :: thesis: P \ R is irreflexive
then A1: P is_irreflexive_in field P by Def10;

now

let a be set ; :: thesis: ( a in field (P \ R) implies not [a,a] in P \ R )

A2: now

assume a in dom (P \ R) ; :: thesis: not [a,a] in P
then consider b being set such that
A3: [a,b] in P \ R by RELAT_1:def 4;
[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, Def2; :: thesis: verum

end;

A4: now

assume a in rng (P \ R) ; :: thesis: not [a,a] in P
then consider b being set such that
A5: [b,a] in P \ R by RELAT_1:def 5;
[b,a] in P by A5, XBOOLE_0:def 5;
then a in field P by RELAT_1:15;
hence not [a,a] in P by A1, Def2; :: thesis: verum

end;

assume a in field (P \ R) ; :: thesis: not [a,a] in P \ R
then a in (dom (P \ R)) \/ (rng (P \ R)) by RELAT_1:def 6;
hence not [a,a] in P \ R by A2, A4, XBOOLE_0:def 3, XBOOLE_0:def 5; :: thesis: verum

end;

then P \ R is_irreflexive_in field (P \ R) by Def2;
hence P \ R is irreflexive by Def10; :: thesis: verum