:: deftheorem Def9 defines reflexive RELAT_2:def 9 :
for R being Relation holds
( R is reflexive iff R is_reflexive_in field R );