for O being set
for G being GroupWithOperators of O
for H1 being StableSubgroup of G holds
( ((1). G) /\ H1 = (1). G & H1 /\ ((1). G) = (1). G )