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