for O being set
for G being GroupWithOperators of O
for H1 being StableSubgroup of G holds (1). G is StableSubgroup of H1