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