theorem :: GRSOLV_1:17

for G being Group
for H being Subgroup of G holds ((Omega). G) /\ H = (Omega). H by Lm286;