let p be Prime; :: thesis: for G being finite strict Group st card G = p holds
G is p -commutative-group
let G be finite strict Group; :: thesis: ( card G = p implies G is p -commutative-group )
assume A1: card G = p ; :: thesis: G is p -commutative-group
p = p |^ 1 ;
then A2: G is p -group by A1;
G is cyclic Group by A1, GR_CY_1:21;
hence G is p -commutative-group by A2; :: thesis: verum