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

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