let G, H be finite Group; :: thesis: for p being prime Nat
for I being Subgroup of G
for P being Subgroup of H st I = P & I is_Sylow_p-subgroup_of_prime p & H is Subgroup of G holds
P is_Sylow_p-subgroup_of_prime p
let p be prime Nat; :: thesis: for I being Subgroup of G
for P being Subgroup of H st I = P & I is_Sylow_p-subgroup_of_prime p & H is Subgroup of G holds
P is_Sylow_p-subgroup_of_prime p
let I be Subgroup of G; :: thesis: for P being Subgroup of H st I = P & I is_Sylow_p-subgroup_of_prime p & H is Subgroup of G holds
P is_Sylow_p-subgroup_of_prime p
let P be Subgroup of H; :: thesis: ( I = P & I is_Sylow_p-subgroup_of_prime p & H is Subgroup of G implies P is_Sylow_p-subgroup_of_prime p )
assume A1: I = P ; :: thesis: ( not I is_Sylow_p-subgroup_of_prime p or not H is Subgroup of G or P is_Sylow_p-subgroup_of_prime p )
assume A2: I is_Sylow_p-subgroup_of_prime p ; :: thesis: ( not H is Subgroup of G or P is_Sylow_p-subgroup_of_prime p )
then A3: I is p -group ;
assume H is Subgroup of G ; :: thesis: P is_Sylow_p-subgroup_of_prime p
then reconsider H9 = H as Subgroup of G ;
A4: index I = (index P) * (index H9) by A1, GROUP_2:149;
not p divides index I by A2;
then not p divides index P by A4, NAT_D:9;
hence P is_Sylow_p-subgroup_of_prime p by A1, A3; :: thesis: verum