let R be Relation; :: thesis: ( R is irreflexive iff id (field R) misses R )

A1: now

assume R is irreflexive ; :: thesis: id (field R) misses R
then A2: R is_irreflexive_in field R by Def10;

now

let a, b be set ; :: thesis: not [a,b] in (id (field R)) /\ R
assume [a,b] in (id (field R)) /\ R ; :: thesis: contradiction
then ( [a,b] in id (field R) & [a,b] in R ) by XBOOLE_0:def 4;
then ( a in field R & a = b & [a,b] in R ) by RELAT_1:def 10;
hence contradiction by A2, Def2; :: thesis: verum

end;

then (id (field R)) /\ R = {} by RELAT_1:56;
hence id (field R) misses R by XBOOLE_0:def 7; :: thesis: verum

end;

now

assume A3: id (field R) misses R ; :: thesis: R is irreflexive

now

let a be set ; :: thesis: ( a in field R implies not [a,a] in R )
assume a in field R ; :: thesis: not [a,a] in R
then [a,a] in id (field R) by RELAT_1:def 10;
hence not [a,a] in R by A3, XBOOLE_0:3; :: thesis: verum

end;

then R is_irreflexive_in field R by Def2;
hence R is irreflexive by Def10; :: thesis: verum

end;

hence ( R is irreflexive iff id (field R) misses R ) by A1; :: thesis: verum