let G be non empty addMagma ; :: thesis: for A being Subset of G
for g, h being Element of G st G is add-associative holds
(A + g) + h = A + (g + h)
let A be Subset of G; :: thesis: for g, h being Element of G st G is add-associative holds
(A + g) + h = A + (g + h)
let g, h be Element of G; :: thesis: ( G is add-associative implies (A + g) + h = A + (g + h) )
assume G is add-associative ; :: thesis: (A + g) + h = A + (g + h)
hence (A + g) + h = A + ({g} + {h}) by Th10
.= A + (g + h) by Th18 ;
:: thesis: verum