theorem :: PARTIT_2:31

for X being non empty set
for R being Relation of X st R is_irreflexive_in X holds
R is irreflexive