reconsider G9 = HGrWOpStr(# the carrier of G, the multF of G, the action of G #) as StableSubgroup of G by Lm3;
take G9 ; :: thesis: G9 is strict
thus G9 is strict ; :: thesis: verum