let X be set ; :: thesis: for R being Relation of X holds
( R is irreflexive iff id X misses R )
let R be Relation of X; :: thesis: ( R is irreflexive iff id X misses R )

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

assume A1: R is irreflexive ; :: thesis: not id X meets R
assume id X meets R ; :: thesis: contradiction
then (id X) /\ R <> {} by XBOOLE_0:def 7;
then consider z being object such that
A2: z in (id X) /\ R by XBOOLE_0:def 1;
consider x, y being object such that
A3: z = [x,y] by A2, RELAT_1:def 1;
A4: ( [x,y] in id X & [x,y] in R ) by A2, A3, XBOOLE_0:def 4;
then ( x = y & x in field R ) by RELAT_1:def 10, RELAT_1:15;
hence contradiction by A1, A4, RELAT_2:def 2, RELAT_2:def 10; :: thesis: verum

end;

assume A5: id X misses R ; :: thesis: R is irreflexive
field R c= X \/ X by RELSET_1:8;
then id (field R) misses R by A5, FUNCT_4:3, XBOOLE_1:63;
hence R is irreflexive by RELAT_2:2; :: thesis: verum