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

for H being Subgroup of G st g in carr H holds

g " in carr H

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

g " in carr H

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

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

then g in H ;

then g " in H by Th51;

hence g " in carr H ; :: thesis: verum

for H being Subgroup of G st g in carr H holds

g " in carr H

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

g " in carr H

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

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

then g in H ;

then g " in H by Th51;

hence g " in carr H ; :: thesis: verum