for S1 being OrderSortedSign
for OU0 being OSAlgebra of S1 holds Constants OU0 c= OSConstants OU0