let G be non empty Group-like multMagma ; :: thesis: for H being Subgroup of G
for h being Element of H holds h in G
let H be Subgroup of G; :: thesis: for h being Element of H holds h in G
let h be Element of H; :: thesis: h in G
h in H by STRUCT_0:def 5;
hence h in G by Th49; :: thesis: verum