let G be addGroup; :: thesis: for H being Subgroup of G holds 0_ G in H
let H be Subgroup of G; :: thesis: 0_ G in H
0_ H in H ;
hence 0_ G in H by Th44; :: thesis: verum