for L being non empty 1-sorted
for R being total Relation of the carrier of L holds
( R is reflexive iff for x being Element of L holds [x,x] in R )