let G be addGroup; :: thesis: for g, h being Element of G ex f being Element of G st g + f = h
let g, h be Element of G; :: thesis: ex f being Element of G st g + f = h
take (- g) + h ; :: thesis: g + ((- g) + h) = h
thus g + ((- g) + h) = h by Th12; :: thesis: verum