:: deftheorem defines is_Sylow_p-subgroup_of_prime GROUP_10:def 18 :
for p being Nat
for G being Group
for P being Subgroup of G holds
( P is_Sylow_p-subgroup_of_prime p iff ( P is p -group & not p divides index P ) );