for S being non empty non void all-with_const_op ManySortedSign
for U0 being non-empty MSAlgebra over S
for U1 being non-empty MSSubAlgebra of U0 holds Constants U0 is V8() MSSubset of U1 by Th10;