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