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