let S be non empty non void ManySortedSign ; :: thesis: for A being MSAlgebra of S
for G being GeneratorSet of A
for B being MSSubset of A st G c= B holds
B is GeneratorSet of A
let A be MSAlgebra of S; :: thesis: for G being GeneratorSet of A
for B being MSSubset of A st G c= B holds
B is GeneratorSet of A
let G be GeneratorSet of A; :: thesis: for B being MSSubset of A st G c= B holds
B is GeneratorSet of A
let B be MSSubset of A; :: thesis: ( G c= B implies B is GeneratorSet of A )
assume A1: G c= B ; :: thesis: B is GeneratorSet of A
A2: the Sorts of (GenMSAlg G) = the Sorts of A by MSAFREE:def 4;
then the Sorts of (GenMSAlg B) is MSSubset of (GenMSAlg G) by MSUALG_2:def 10;
then A3: the Sorts of (GenMSAlg B) c= the Sorts of (GenMSAlg G) by PBOOLE:def 23;
B is MSSubset of (GenMSAlg B) by MSUALG_2:def 18;
then B c= the Sorts of (GenMSAlg B) by PBOOLE:def 23;
then G c= the Sorts of (GenMSAlg B) by A1, PBOOLE:15;
then G is MSSubset of (GenMSAlg B) by PBOOLE:def 23;
then GenMSAlg G is MSSubAlgebra of GenMSAlg B by MSUALG_2:def 18;
then the Sorts of (GenMSAlg G) is MSSubset of (GenMSAlg B) by MSUALG_2:def 10;
then the Sorts of (GenMSAlg G) c= the Sorts of (GenMSAlg B) by PBOOLE:def 23;
hence the Sorts of (GenMSAlg B) = the Sorts of A by A2, A3, PBOOLE:def 13; :: according to MSAFREE:def 4 :: thesis: verum