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

for N being Subgroup of G holds N ` (N ` A) c= N ~ (N ~ A)

let A be non empty Subset of G; :: thesis: for N being Subgroup of G holds N ` (N ` A) c= N ~ (N ~ A)

let N be Subgroup of G; :: thesis: N ` (N ` A) c= N ~ (N ~ A)

N ` A c= N ~ A by Th18;

then N ` (N ` A) c= N ~ A by Th34;

hence N ` (N ` A) c= N ~ (N ~ A) by Th35; :: thesis: verum

for N being Subgroup of G holds N ` (N ` A) c= N ~ (N ~ A)

let A be non empty Subset of G; :: thesis: for N being Subgroup of G holds N ` (N ` A) c= N ~ (N ~ A)

let N be Subgroup of G; :: thesis: N ` (N ` A) c= N ~ (N ~ A)

N ` A c= N ~ A by Th18;

then N ` (N ` A) c= N ~ A by Th34;

hence N ` (N ` A) c= N ~ (N ~ A) by Th35; :: thesis: verum