:: deftheorem Def5 defines OSConstants OSALG_2:def 5 :
for S1 being OrderSortedSign
for OU0 being OSAlgebra of S1
for b₃ being OSSubset of OU0 holds
( b₃ = OSConstants OU0 iff for s being SortSymbol of S1 holds b₃ . s = OSConstants (OU0,s) );