let x be object ; :: thesis: for G being non empty addGroup-like addMagma
for H being Subgroup of G st x in H holds
x in G
let G be non empty addGroup-like addMagma ; :: 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 A1: x in H ; :: thesis: x in G
the carrier of H c= the carrier of G by DefA5;
hence x in G by A1; :: thesis: verum