let A be Universal_Algebra; :: thesis: for G being GeneratorSet of A holds Generators A c= G
let G be GeneratorSet of A; :: thesis: Generators A c= G
let a be object ; :: according to TARSKI:def 3 :: thesis: ( a nin Generators A or not a nin G )
assume A1: a in Generators A ; :: thesis: not a nin G
then A2: a nin union { (rng o) where o is Element of Operations A : verum } by XBOOLE_0:def 5;
reconsider I = a as Element of A by A1;
assume a nin G ; :: thesis: contradiction
then consider o0 being Element of Operations A such that
A3: I in rng o0 by Th32;
rng o0 in { (rng o) where o is Element of Operations A : verum } ;
hence contradiction by A2, A3, TARSKI:def 4; :: thesis: verum