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:15
.= ((p1 + q1) + p2) + q2 by RVSUM_1:15
.= (p1 + q1) + (p2 + q2) by RVSUM_1:15 ; :: thesis: verum