:: deftheorem defines <= ORDERS_2:def 5 :
for A being RelStr
for a1, a2 being Element of A holds
( a1 <= a2 iff [a1,a2] in the InternalRel of A );