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