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