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 by STRUCT_0:def 5;
hence 1_ G in H by Th53; :: thesis: verum