:: deftheorem defines <~ ORDERS_5:def 4 :
for A being RelStr
for a1, a2 being Element of A holds
( a1 <~ a2 iff ( a1 <= a2 & not a2 <= a1 ) );