let A be Universal_Algebra; :: thesis: for B being Subset of A
for G being GeneratorSet of A st G c= B holds
B is GeneratorSet of A
let B be Subset of A; :: thesis: for G being GeneratorSet of A st G c= B holds
B is GeneratorSet of A
let G be GeneratorSet of A; :: thesis: ( G c= B implies B is GeneratorSet of A )
assume A1: G c= B ; :: thesis: B is GeneratorSet of A
now :: thesis: for a being Element of A ex n being Nat st a in B |^ n
let a be Element of A; :: thesis: ex n being Nat st a in B |^ n
consider n being Nat such that
A2: a in G |^ n by Th30;
take n = n; :: thesis: a in B |^ n
G |^ n c= B |^ n by A1, Th22;
hence a in B |^ n by A2; :: thesis: verum
end;
hence B is GeneratorSet of A by Th30; :: thesis: verum