for S, X being non empty set
for R being Relation of X st R is irreflexive & field R c= S holds
R is_irreflexive_in S