set A = the non-empty MSAlgebra over S;
take the non-empty MSAlgebra over S ; :: thesis: the non-empty MSAlgebra over S is non-empty
thus the non-empty MSAlgebra over S is non-empty ; :: thesis: verum