for S being non empty non void ManySortedSign
for U0 being MSAlgebra over S
for U1 being MSSubAlgebra of U0 holds Constants U0 is MSSubset of U1