let G be non empty Abelian add-associative addLoopStr ; :: thesis: for u, v, w being Element of G holds (u - v) - w = (u - w) - v
let u, v, w be Element of G; :: thesis: (u - v) - w = (u - w) - v
thus (u - v) - w = (u + (- v)) + (- w)
.= (u + (- w)) + (- v) by RLVECT_1:def 3
.= (u - w) - v ; :: thesis: verum