let A be Universal_Algebra; :: thesis: for B being strict non-empty MSSubAlgebra of MSAlg A st the carrier of (MSSign A) = {0} holds
1-Alg B is SubAlgebra of A
let B be strict non-empty MSSubAlgebra of MSAlg A; :: thesis: ( the carrier of (MSSign A) = {0} implies 1-Alg B is SubAlgebra of A )
assume the carrier of (MSSign A) = {0} ; :: thesis: 1-Alg B is SubAlgebra of A
then MSAlg (1-Alg B) = MSAlgebra(# the Sorts of B, the Charact of B #) by Th26;
hence 1-Alg B is SubAlgebra of A by Th16; :: thesis: verum