:: deftheorem defstr defines strongly_reflexive REALALG1:def 1 :
for X being set
for R being Relation of X holds
( R is strongly_reflexive iff R is_reflexive_in X );