let G be addGroup; :: thesis: for a being Element of G
for A being Subset of G
for H being Subgroup of G holds (A + H) + a = A + (H + a)
let a be Element of G; :: thesis: for A being Subset of G
for H being Subgroup of G holds (A + H) + a = A + (H + a)
let A be Subset of G; :: thesis: for H being Subgroup of G holds (A + H) + a = A + (H + a)
let H be Subgroup of G; :: thesis: (A + H) + a = A + (H + a)
thus (A + H) + a = A + (H + {a}) by Th97
.= A + (H + a) ; :: thesis: verum