let G be Group; :: thesis: for a being Element of G
for A being Subset of G st a in A holds
a in gr A
let a be Element of G; :: thesis: for A being Subset of G st a in A holds
a in gr A
let A be Subset of G; :: thesis: ( a in A implies a in gr A )
assume A1: a in A ; :: thesis: a in gr A
A c= the carrier of (gr A) by Def4;
hence a in gr A by A1, STRUCT_0:def 5; :: thesis: verum