reconsider G9 = HGrWOpStr(# the carrier of G, the multF of G, the action of G #) as strict StableSubgroup of G by Lm3;

consider H9 being strict StableSubgroup of H such that

A1: the carrier of H9 = g .: the carrier of G9 by Lm16;

take H9 ; :: thesis: the carrier of H9 = g .: the carrier of G

thus the carrier of H9 = g .: the carrier of G by A1; :: thesis: verum

consider H9 being strict StableSubgroup of H such that

A1: the carrier of H9 = g .: the carrier of G9 by Lm16;

take H9 ; :: thesis: the carrier of H9 = g .: the carrier of G

thus the carrier of H9 = g .: the carrier of G by A1; :: thesis: verum