let n be Nat; for x1, x2, x3, y1, y2, y3 being Element of REAL n holds ((x1 + x2) + x3) + ((y1 + y2) + y3) = ((x1 + y1) + (x2 + y2)) + (x3 + y3)
let x1, x2, x3, y1, y2, y3 be Element of REAL n; ((x1 + x2) + x3) + ((y1 + y2) + y3) = ((x1 + y1) + (x2 + y2)) + (x3 + y3)
thus ((x1 + x2) + x3) + ((y1 + y2) + y3) =
((x1 + x2) + (y1 + y2)) + (x3 + y3)
by Th16
.=
((x1 + y1) + (x2 + y2)) + (x3 + y3)
by Th16
; verum