let O be set ; :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: ( X = X9 & Y = Y9 implies X9 /\ Y9 = X /\ Y )
assume A1: ( X = X9 & Y = Y9 ) ; :: thesis: 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 ; :: thesis: verum