let p1, p2 be Point of (TOP-REAL 2); :: thesis: ( (p1 + p2) `1 = (p1 `1 ) + (p2 `1 ) & (p1 + p2) `2 = (p1 `2 ) + (p2 `2 ) )
p1 + p2 = |[((p1 `1 ) + (p2 `1 )),((p1 `2 ) + (p2 `2 ))]| by EUCLID:59;
hence ( (p1 + p2) `1 = (p1 `1 ) + (p2 `1 ) & (p1 + p2) `2 = (p1 `2 ) + (p2 `2 ) ) by EUCLID:56; :: thesis: verum