let G be Group; :: thesis: for A being Subset of G st A = {(1_ G)} holds
gr A = (1). G
let A be Subset of G; :: thesis: ( A = {(1_ G)} implies gr A = (1). G )
assume A = {(1_ G)} ; :: thesis: gr A = (1). G
then A = the carrier of ((1). G) by GROUP_2:def 7;
hence gr A = (1). G by Th3; :: thesis: verum