let O be set ; :: thesis: for G being GroupWithOperators of O
for H1 being StableSubgroup of G
for h1 being Element of H1 holds h1 is Element of G
let G be GroupWithOperators of O; :: thesis: for H1 being StableSubgroup of G
for h1 being Element of H1 holds h1 is Element of G
let H1 be StableSubgroup of G; :: thesis: for h1 being Element of H1 holds h1 is Element of G
let h1 be Element of H1; :: thesis: h1 is Element of G
H1 is Subgroup of G by Def7;
hence h1 is Element of G by GROUP_2:42; :: thesis: verum