Description: The predicate "is a group." (This theorem demonstrates the use of symbols as variable names, first proposed by FL in 2010.) (Contributed by NM, 17-Oct-2012) (Revised by Mario Carneiro, 6-Jan-2015)