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