for S1 being OrderSortedSign
for OU0 being OSAlgebra of S1
for s being SortSymbol of S1 holds Constants (OU0,s) c= OSConstants (OU0,s)