for S being non empty non void ManySortedSign
for U0 being free feasible MSAlgebra over S
for A being free GeneratorSet of U0
for Z being MSSubset of U0 st Z c= A & GenMSAlg Z is feasible holds
GenMSAlg Z is free