theorem Th36: :: GROUP_9:36

for O being set
for G being GroupWithOperators of O
for H1 being StableSubgroup of G
for H2 being strict StableSubgroup of G holds
( H1 is StableSubgroup of H2 iff H1 "\/" H2 = H2 )