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