let O be set ; :: thesis: for G being GroupWithOperators of O
for H1 being StableSubgroup of G
for x being object st x in H1 holds
x in G
let G be GroupWithOperators of O; :: thesis: for H1 being StableSubgroup of G
for x being object st x in H1 holds
x in G
let H1 be StableSubgroup of G; :: thesis: for x being object st x in H1 holds
x in G
let x be object ; :: thesis: ( x in H1 implies x in G )
assume A1: x in H1 ; :: thesis: x in G
H1 is Subgroup of G by Def7;
hence x in G by A1, GROUP_2:40; :: thesis: verum