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 )
assume a in field (P \ R) ; :: thesis: not [a,a] in P \ R
then A2: a in (dom (P \ R)) \/ (rng (P \ R)) by RELAT_1:def 6;

A3: now

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

end;

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 & not [b,a] in R ) by A5, XBOOLE_0:def 5;
then a in field P by RELAT_1:30;
hence not [a,a] in P by A1, Def2; :: thesis: verum

end;

hence not [a,a] in P \ R by A2, A3, 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