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

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

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

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

then A1: R is_irreflexive_in field R ;

end;then A1: R is_irreflexive_in field R ;

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

hence
id (field R) misses R
by RELAT_1:37, XBOOLE_0:def 7; :: thesis: verumlet 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;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

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