consider P being strict Subgroup of G such that
A1: P is_Sylow_p-subgroup_of_prime p by Th10;
reconsider H9 = (Omega). P as Element of Subgroups G by GROUP_3:def 1;
H9 in the_sylow_p-subgroups_of_prime (p,G) by A1;
hence ( not the_sylow_p-subgroups_of_prime (p,G) is empty & the_sylow_p-subgroups_of_prime (p,G) is finite ) by FINSET_1:1, GROUP_3:15; :: thesis: verum