let G be Group; :: thesis: for A being non empty Subset of G

for N, H being Subgroup of G st N is Subgroup of H holds

H ` A c= N ` A

let A be non empty Subset of G; :: thesis: for N, H being Subgroup of G st N is Subgroup of H holds

H ` A c= N ` A

let N, H be Subgroup of G; :: thesis: ( N is Subgroup of H implies H ` A c= N ` A )

assume A1: N is Subgroup of H ; :: thesis: H ` A c= N ` A

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in H ` A or x in N ` A )

assume A2: x in H ` A ; :: thesis: x in N ` A

then reconsider x = x as Element of G ;

A3: x * N c= x * H by A1, GROUP_3:6;

x * H c= A by A2, Th12;

then x * N c= A by A3;

hence x in N ` A ; :: thesis: verum

for N, H being Subgroup of G st N is Subgroup of H holds

H ` A c= N ` A

let A be non empty Subset of G; :: thesis: for N, H being Subgroup of G st N is Subgroup of H holds

H ` A c= N ` A

let N, H be Subgroup of G; :: thesis: ( N is Subgroup of H implies H ` A c= N ` A )

assume A1: N is Subgroup of H ; :: thesis: H ` A c= N ` A

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in H ` A or x in N ` A )

assume A2: x in H ` A ; :: thesis: x in N ` A

then reconsider x = x as Element of G ;

A3: x * N c= x * H by A1, GROUP_3:6;

x * H c= A by A2, Th12;

then x * N c= A by A3;

hence x in N ` A ; :: thesis: verum