:: deftheorem Def2 defines reflexive ORDERS_2:def 2 :
for A being RelStr holds
( A is reflexive iff the InternalRel of A is_reflexive_in the carrier of A );