:: deftheorem Def25 defines /\ GROUP_9:def 25 :
for O being set
for G being GroupWithOperators of O
for H1, H2 being StableSubgroup of G
for b₅ being strict StableSubgroup of G holds
( b₅ = H1 /\ H2 iff the carrier of b₅ = (carr H1) /\ (carr H2) );