let O be set ; :: thesis: for G being GroupWithOperators of O
for H1, H2 being StableSubgroup of G holds H1 /\ H2 is StableSubgroup of H1
let G be GroupWithOperators of O; :: thesis: for H1, H2 being StableSubgroup of G holds H1 /\ H2 is StableSubgroup of H1
let H1, H2 be StableSubgroup of G; :: thesis: H1 /\ H2 is StableSubgroup of H1
( the carrier of (H1 /\ H2) = the carrier of H1 /\ the carrier of H2 & the carrier of H1 /\ the carrier of H2 c= the carrier of H1 ) by Th18, XBOOLE_1:17;
hence H1 /\ H2 is StableSubgroup of H1 by Lm21; :: thesis: verum