theorem :: ALGSPEC1:56

for S being Signature
for E being Extension of S
for A being Algebra of E holds A is Algebra of S