let A be Universal_Algebra; :: thesis: ( Constants A = {} implies for G being GeneratorSet of A holds G <> {} )
assume A1: Constants A = {} ; :: thesis: for G being GeneratorSet of A holds G <> {}
let G be GeneratorSet of A; :: thesis: G <> {}
assume A2: G = {} ; :: thesis: contradiction
then G = {} A ;
then G is opers_closed by A1, Th28;
hence contradiction by A2, FREEALG:def 4; :: thesis: verum