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

let H be Subgroup of G; :: thesis: 1_ G in H

1_ H in H ;

hence 1_ G in H by Th44; :: thesis: verum