:: deftheorem defines < ORDERS_2:def 6 :
for A being RelStr
for a1, a2 being Element of A holds
( a1 < a2 iff ( a1 <= a2 & a1 <> a2 ) );