theorem Th10: :: GROUP_10:10
for G being finite Group
for p being Prime ex P being strict Subgroup of G st P is_Sylow_p-subgroup_of_prime p