theorem Th23: :: MSUALG_2:23

for S being non empty non void ManySortedSign
for U0 being non-empty MSAlgebra over S
for U1 being MSSubAlgebra of U0 holds (GenMSAlg (Constants U0)) /\ U1 = GenMSAlg (Constants U0)