for G being finite Group
for p being prime Nat ex P being strict Subgroup of G st P is_Sylow_p-subgroup_of_prime p