( SingleAlg S is non-empty & SingleAlg S is disjoint_valued ) by Lm1;
hence ex b₁ being MSAlgebra over S st
( b₁ is non-empty & b₁ is disjoint_valued ) ; :: thesis: verum