for O being set
for G being GroupWithOperators of O
for H1, H2 being StableSubgroup of G holds
( ( for H being StableSubgroup of G st H = H1 /\ H2 holds
the carrier of H = the carrier of H1 /\ the carrier of H2 ) & ( for H being strict StableSubgroup of G st the carrier of H = the carrier of H1 /\ the carrier of H2 holds
H = H1 /\ H2 ) )