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 )

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

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

assume
GenMSAlg A = U0
; :: thesis: A is GeneratorSet of U0
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 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

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