let O be 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
let G be 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
let H1 be 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
let X, Y be StableSubgroup of H1; for X9, Y9 being StableSubgroup of G st X = X9 & Y = Y9 holds
X9 /\ Y9 = X /\ Y
reconsider Z = X /\ Y as StableSubgroup of G by Th11;
let X9, Y9 be StableSubgroup of G; ( X = X9 & Y = Y9 implies X9 /\ Y9 = X /\ Y )
assume A1:
( X = X9 & Y = Y9 )
; X9 /\ Y9 = X /\ Y
the carrier of (X /\ Y) = (carr X) /\ (carr Y)
by Def25;
then
X9 /\ Y9 = Z
by A1, Th18;
hence
X9 /\ Y9 = X /\ Y
; verum