consider S being non void Signature, A being feasible MSAlgebra of S;
take A ; :: thesis: ex S being non void Signature st A is feasible MSAlgebra of S
take S ; :: thesis: A is feasible MSAlgebra of S
thus A is feasible MSAlgebra of S ; :: thesis: verum