for X being set
for R being Relation
for Y being Subset of X st R is_irreflexive_in X holds
R is_irreflexive_in Y