let G be Group; :: thesis: for Fam being Subset of (Subgroups G) holds
( G is_internal_product_of Fam iff (Omega). G is_internal_product_of Fam )
let Fam be Subset of (Subgroups G); :: thesis: ( G is_internal_product_of Fam iff (Omega). G is_internal_product_of Fam )

hereby :: thesis: ( (Omega). G is_internal_product_of Fam implies G is_internal_product_of Fam )

assume A1: G is_internal_product_of Fam ; :: thesis: (Omega). G is_internal_product_of Fam
for H being strict Subgroup of G st H in Fam holds
H is normal Subgroup of (Omega). G

proof

let H be strict Subgroup of G; :: thesis: ( H in Fam implies H is normal Subgroup of (Omega). G )
assume H in Fam ; :: thesis: H is normal Subgroup of (Omega). G
then H is normal Subgroup of G by A1;
hence H is normal Subgroup of (Omega). G by GROUP_6:8, GROUP_2:57, GROUP_2:def 5; :: thesis: verum

end;

hence (Omega). G is_internal_product_of Fam by A1; :: thesis: verum

end;

assume A2: (Omega). G is_internal_product_of Fam ; :: thesis: G is_internal_product_of Fam
for H being strict Subgroup of G st H in Fam holds
H is normal Subgroup of G

proof

let H be strict Subgroup of G; :: thesis: ( H in Fam implies H is normal Subgroup of G )
assume H in Fam ; :: thesis: H is normal Subgroup of G
then H is normal Subgroup of (Omega). G by A2;
hence H is normal Subgroup of G by ThMinorAnnoyance; :: thesis: verum

end;

hence G is_internal_product_of Fam by A2; :: thesis: verum