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
.= a + (H + A) by Th97 ; :: thesis: verum