let S be non empty non void ManySortedSign ; for A being MSAlgebra over 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 over S; 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; for B being MSSubset of A st G c= B holds
B is GeneratorSet of A
let B be MSSubset of A; ( G c= B implies B is GeneratorSet of A )
B is MSSubset of (GenMSAlg B)
by MSUALG_2:def 17;
then A1:
B c= the Sorts of (GenMSAlg B)
by PBOOLE:def 18;
assume
G c= B
; B is GeneratorSet of A
then
G c= the Sorts of (GenMSAlg B)
by A1, PBOOLE:13;
then
G is MSSubset of (GenMSAlg B)
by PBOOLE:def 18;
then
GenMSAlg G is MSSubAlgebra of GenMSAlg B
by MSUALG_2:def 17;
then
the Sorts of (GenMSAlg G) is MSSubset of (GenMSAlg B)
by MSUALG_2:def 9;
then A2:
the Sorts of (GenMSAlg G) c= the Sorts of (GenMSAlg B)
by PBOOLE:def 18;
A3:
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 9;
then
the Sorts of (GenMSAlg B) c= the Sorts of (GenMSAlg G)
by PBOOLE:def 18;
hence
the Sorts of (GenMSAlg B) = the Sorts of A
by A3, A2, PBOOLE:146; MSAFREE:def 4 verum