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