let S be non empty non void ManySortedSign ; :: thesis: for U0 being strict non-empty MSAlgebra over S
for A being MSSubset of U0 holds
( A is GeneratorSet of U0 iff GenMSAlg A = U0 )
let U0 be strict non-empty MSAlgebra over S; :: thesis: for A being MSSubset of U0 holds
( A is GeneratorSet of U0 iff GenMSAlg A = U0 )
let A be MSSubset of U0; :: thesis: ( A is GeneratorSet of U0 iff GenMSAlg A = U0 )
thus ( A is GeneratorSet of U0 implies GenMSAlg A = U0 ) :: thesis: ( GenMSAlg A = U0 implies A is GeneratorSet of U0 )

proof

reconsider U1 = U0 as MSSubAlgebra of U0 by MSUALG_2:5;
assume A is GeneratorSet of U0 ; :: thesis: GenMSAlg A = U0
then the Sorts of (GenMSAlg A) = the Sorts of U1 by Def4;
hence GenMSAlg A = U0 by MSUALG_2:9; :: thesis: verum

end;

assume GenMSAlg A = U0 ; :: thesis: A is GeneratorSet of U0
hence A is GeneratorSet of U0 by Def4; :: thesis: verum