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

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