let G be addGroup; :: 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