theorem Th1: :: ORDERS_2:1

for A being non empty reflexive RelStr
for a being Element of A holds a <= a