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 by STRUCT_0:def 5;
then g " in H by Th60;
hence g " in carr H by STRUCT_0:def 5; :: thesis: verum