theorem ThCarrG: :: GROUP_23:97

for G being Group
for I being non empty set
for F being componentwise_strict Subgroup-Family of I,G
for Fam being Subset of (Subgroups G) st Fam = rng F holds
union { A where A is Subset of G : ex H being strict Subgroup of G st
( H in Fam & A = the carrier of H ) } = Union (Carrier F)