let G be Group; :: thesis: for a being Element of
for A being Subset of st a in A holds
a in gr A
let a be Element of ; :: thesis: for A being Subset of st a in A holds
a in gr A
let A be Subset of ; :: 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 Def5;
hence a in gr A by A1, STRUCT_0:def 5; :: thesis: verum