let x be object ; :: 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 A1: x in the carrier of H ;

the carrier of H c= the carrier of G by Def5;

hence x in G by A1; :: thesis: verum

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 A1: x in the carrier of H ;

the carrier of H c= the carrier of G by Def5;

hence x in G by A1; :: thesis: verum