let n be Nat; :: thesis: 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; :: thesis: ((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 Th18
.= ((x1 - y1) + (x2 - y2)) + (x3 - y3) by Th18 ; :: thesis: verum