theorem :: GLIBPRE0:11

for X being set
for R being Relation of X holds
( R is irreflexive iff id X misses R )