consider A being non-empty MSAlgebra of S;
take A ; :: thesis: A is non-empty
thus A is non-empty ; :: thesis: verum