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