:: deftheorem defines OSConstants OSALG_2:def 3 :
for S1 being OrderSortedSign
for OU0 being OSAlgebra of S1
for s being SortSymbol of S1 holds OSConstants (OU0,s) = union { (Constants (OU0,s2)) where s2 is SortSymbol of S1 : s2 <= s } ;