take (1). G ; :: thesis: ( (1). G is p -commutative-group & (1). G is finite )
( (1). G is p -commutative-group-like & (1). G is p -group ) by Th16, Th27;
hence ( (1). G is p -commutative-group & (1). G is finite ) ; :: thesis: verum