for R being Relation holds
( R is irreflexive iff for x being object st x in field R holds
not [x,x] in R ) by RELAT_2:def 10, RELAT_2:def 2;