take (1). G ; :: thesis: (1). G is p -group
thus (1). G is p -group by Th16; :: thesis: verum