let G be Group; :: thesis: not 1_ G is generating
let A be Subset of G; :: according to GROUP_4:def 5 :: thesis: ( gr A = multMagma(# the carrier of G, the multF of G #) implies gr (A \ {(1_ G)}) = multMagma(# the carrier of G, the multF of G #) )
assume gr A = multMagma(# the carrier of G, the multF of G #) ; :: thesis: gr (A \ {(1_ G)}) = multMagma(# the carrier of G, the multF of G #)
hence gr (A \ {(1_ G)}) = multMagma(# the carrier of G, the multF of G #) by Th44; :: thesis: verum