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

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