let G be Group; :: thesis: for A being non empty Subset of G
for N being Subgroup of G holds N ` A c= A
let A be non empty Subset of G; :: thesis: for N being Subgroup of G holds N ` A c= A
let N be Subgroup of G; :: thesis: N ` A c= A
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in N ` A or x in A )
assume x in N ` A ; :: thesis: x in A
then consider y being Element of G such that
A1: ( y = x & y * N c= A ) ;
y in y * N by GROUP_2:108;
hence x in A by A1; :: thesis: verum