let p1, p2, p3, p4 be Point of (TOP-REAL 3); :: thesis: (p1 + p2) <X> (p3 + p4) = (((p1 <X> p3) + (p1 <X> p4)) + (p2 <X> p3)) + (p2 <X> p4)
(p1 + p2) <X> (p3 + p4) = (p1 <X> (p3 + p4)) + (p2 <X> (p3 + p4)) by Th24
.= ((p1 <X> p3) + (p1 <X> p4)) + (p2 <X> (p3 + p4)) by Th23
.= ((p1 <X> p3) + (p1 <X> p4)) + ((p2 <X> p3) + (p2 <X> p4)) by Th23 ;
hence (p1 + p2) <X> (p3 + p4) = (((p1 <X> p3) + (p1 <X> p4)) + (p2 <X> p3)) + (p2 <X> p4) by RLVECT_1:def 3; :: thesis: verum