set S = the non void Signature;
set A = the feasible MSAlgebra of the non void Signature;
take the feasible MSAlgebra of the non void Signature ; :: thesis: ex S being non void Signature st the feasible MSAlgebra of the non void Signature is feasible MSAlgebra of S
take the non void Signature ; :: thesis: the feasible MSAlgebra of the non void Signature is feasible MSAlgebra of the non void Signature
thus the feasible MSAlgebra of the non void Signature is feasible MSAlgebra of the non void Signature ; :: thesis: verum