let G be Group; :: thesis: for I being set
for F being Subgroup-Family of I,G
for J being set st J c= I holds
F | J is Subgroup-Family of J,G
let I be set ; :: thesis: for F being Subgroup-Family of I,G
for J being set st J c= I holds
F | J is Subgroup-Family of J,G
let F be Subgroup-Family of I,G; :: thesis: for J being set st J c= I holds
F | J is Subgroup-Family of J,G
let J be set ; :: thesis: ( J c= I implies F | J is Subgroup-Family of J,G )
assume A1: J c= I ; :: thesis: F | J is Subgroup-Family of J,G
for j being object st j in J holds
(F | J) . j is Subgroup of G

proof

let j be object ; :: thesis: ( j in J implies (F | J) . j is Subgroup of G )
assume A2: j in J ; :: thesis: (F | J) . j is Subgroup of G
then F . j is Subgroup of G by A1, GROUP_20:def 1;
hence (F | J) . j is Subgroup of G by A2, FUNCT_1:49; :: thesis: verum

end;

hence F | J is Subgroup-Family of J,G by A1, GROUP_20:def 1; :: thesis: verum