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

hereby :: thesis: ( id (field R) misses R implies R is irreflexive )

assume R is irreflexive ; :: thesis: id (field R) misses R
then A1: R is_irreflexive_in field R ;

now :: thesis: for a, b being object holds not [a,b] in (id (field R)) /\ R

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

end;

hence id (field R) misses R by RELAT_1:37, XBOOLE_0:def 7; :: thesis: verum

end;

assume A4: id (field R) misses R ; :: thesis: R is irreflexive
let a be object ; :: according to RELAT_2:def 2,RELAT_2:def 10 :: 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 A4, XBOOLE_0:3; :: thesis: verum