let G be Group; :: thesis: for a, b being Element of G st b in gr {a} holds
gr {b} is strict Subgroup of gr {a}
let a, b be Element of G; :: thesis: ( b in gr {a} implies gr {b} is strict Subgroup of gr {a} )
assume b in gr {a} ; :: thesis: gr {b} is strict Subgroup of gr {a}
then reconsider b0 = b as Element of (gr {a}) ;
gr {b0} = gr {b} by GR_CY_2:3;
hence gr {b} is strict Subgroup of gr {a} ; :: thesis: verum