let p1, p2, q1, q2 be Element of REAL 3; :: thesis: (p1 + p2) - (q1 + q2) = (p1 - q1) + (p2 - q2)
thus (p1 + p2) - (q1 + q2) = ((p1 + p2) - q1) - q2 by RVSUM_1:39
.= (p1 + p2) + ((- q1) + (- q2)) by RVSUM_1:15
.= (p1 - q1) + (p2 - q2) by Lm9 ; :: thesis: verum