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