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 set ; :: 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, XBOOLE_1:1;
hence x in N ` A ; :: thesis: verum