:: deftheorem defines reflexive YELLOW_0:def 1 :
for A being non empty RelStr holds
( A is reflexive iff for x being Element of A holds x <= x );