theorem Th39: :: GROUP_9:39

for O being set
for G being GroupWithOperators of O
for H1 being StableSubgroup of G
for X, Y being StableSubgroup of H1
for X9, Y9 being StableSubgroup of G st X = X9 & Y = Y9 holds
X9 /\ Y9 = X /\ Y