take 1_ G ; :: thesis: 1_ G is m -element
thus 1_ G is m -element by Th13; :: thesis: verum