for S, S9 being non void Signature
for A being non-empty disjoint_valued MSAlgebra over S st A is Algebra of S9 holds
S is Extension of S9