let G be Group; :: thesis: (1). G is trivial
the carrier of ((1). G) = {(1_ G)} by GROUP_2:def 7;
hence (1). G is trivial by Def2; :: thesis: verum