for O being set
for G being GroupWithOperators of O
for H1, H2 being StableSubgroup of G holds
( H1 is StableSubgroup of H1 "\/" H2 & H2 is StableSubgroup of H1 "\/" H2 )