for X being non empty set
for R being Relation of X st R is_reflexive_in X holds
( R is reflexive & field R = X ) by Th9;