theorem :: GROUP_9:68

for O being set
for G being GroupWithOperators of O
for H1 being StableSubgroup of G holds multMagma(# the carrier of H1, the multF of H1 #) is strict Subgroup of G by Lm15;