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