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 object ; :: 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

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 object ; :: 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