:: deftheorem Def1 defines is_reflexive_in RELAT_2:def 1 :
for R being Relation
for X being set holds
( R is_reflexive_in X iff for x being object st x in X holds
[x,x] in R );