theorem :: RELAT_2:2

for R being Relation holds
( R is irreflexive iff id (field R) misses R )