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