for G being finite Group
for p being prime Nat holds
( ( for H being Subgroup of G st H is p -group holds
ex P being Subgroup of G st
( P is_Sylow_p-subgroup_of_prime p & H is Subgroup of P ) ) & ( for P1, P2 being Subgroup of G st P1 is_Sylow_p-subgroup_of_prime p & P2 is_Sylow_p-subgroup_of_prime p holds
P1,P2 are_conjugated ) )