:: deftheorem Def2 defines OrderSortedRelation OSALG_4:def 2 :
for S being OrderSortedSign
for U1 being OSAlgebra of S
for b₃ being ManySortedRelation of U1 holds
( b₃ is OrderSortedRelation of U1 iff b₃ is os-compatible );