let G be Group; :: thesis: for g being Element of G

for H being Subgroup of G st g in H holds

g " in H

let g be Element of G; :: thesis: for H being Subgroup of G st g in H holds

g " in H

let H be Subgroup of G; :: thesis: ( g in H implies g " in H )

assume g in H ; :: thesis: g " in H

then reconsider h = g as Element of H ;

h " in H ;

hence g " in H by Th48; :: thesis: verum

for H being Subgroup of G st g in H holds

g " in H

let g be Element of G; :: thesis: for H being Subgroup of G st g in H holds

g " in H

let H be Subgroup of G; :: thesis: ( g in H implies g " in H )

assume g in H ; :: thesis: g " in H

then reconsider h = g as Element of H ;

h " in H ;

hence g " in H by Th48; :: thesis: verum