theorem Th15: :: MSUALG_2:15

for S being non empty non void ManySortedSign
for U0 being MSAlgebra over S
for A being MSSubset of U0 holds (Constants U0) (\/) A c= MSSubSort A