theorem Th10: :: OSALG_2:10
for S1 being OrderSortedSign
for OU0 being OSAlgebra of S1 holds Constants OU0 c= OSConstants OU0