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 by Th18;
hence H1 /\ H2 is StableSubgroup of H1 by Lm20, XBOOLE_1:17; :: thesis: verum