let G be Group; :: thesis: for H being strict Subgroup of G
for g being Element of G st g in (carr G) . H holds
g " in (carr G) . H
let H be strict Subgroup of G; :: thesis: for g being Element of G st g in (carr G) . H holds
g " in (carr G) . H
let g be Element of G; :: thesis: ( g in (carr G) . H implies g " in (carr G) . H )
assume g in (carr G) . H ; :: thesis: g " in (carr G) . H
then g in H by Th18;
then g " in H by GROUP_2:60;
hence g " in (carr G) . H by Th18; :: thesis: verum