let x be set ; :: thesis: for G being non empty Group-like multMagma
for H being Subgroup of G st x in H holds
x in G
let G be non empty Group-like multMagma ; :: thesis: for H being Subgroup of G st x in H holds
x in G
let H be Subgroup of G; :: thesis: ( x in H implies x in G )
assume x in H ; :: thesis: x in G
then ( x in the carrier of H & the carrier of H c= the carrier of G ) by Def5, STRUCT_0:def 5;
hence x in G by STRUCT_0:def 5; :: thesis: verum