:: deftheorem Def2 defines OSSubset OSALG_2:def 2 :
for S being OrderSortedSign
for U0 being OSAlgebra of S
for b₃ being ManySortedSubset of the Sorts of U0 holds
( b₃ is OSSubset of U0 iff b₃ is OrderSortedSet of S );