set H = G;
take G ; :: thesis: ( G is Subgroup of G & ( for o being Element of O holds G ^ o = (G ^ o) | the carrier of G ) )
thus ( G is Subgroup of G & ( for o being Element of O holds G ^ o = (G ^ o) | the carrier of G ) ) by GROUP_2:54; :: thesis: verum