reconsider H' = H as Subgroup of G by Def7;
carr H' is Subset of ;
hence the carrier of H is Subset of ; :: thesis: verum