for O being set
for G being GroupWithOperators of O
for H1, H2, H3 being StableSubgroup of G holds (H1 /\ H2) /\ H3 = H1 /\ (H2 /\ H3)