let O be set ; :: thesis: for G being GroupWithOperators of O
for H1 being StableSubgroup of G holds (1). G is StableSubgroup of H1
let G be GroupWithOperators of O; :: thesis: for H1 being StableSubgroup of G holds (1). G is StableSubgroup of H1
let H1 be StableSubgroup of G; :: thesis: (1). G is StableSubgroup of H1
(1). G = (1). H1 by Th15;
hence (1). G is StableSubgroup of H1 ; :: thesis: verum