:: deftheorem defines the_sylow_p-subgroups_of_prime GROUP_10:def 19 :
for G being Group
for p being Nat holds the_sylow_p-subgroups_of_prime (p,G) = { H where H is Element of Subgroups G : ex P being strict Subgroup of G st
( P = H & P is_Sylow_p-subgroup_of_prime p ) } ;