for O being set
for G being GroupWithOperators of O
for H1 being StableSubgroup of G holds 1_ G = 1_ H1