let p, q be Point of (TOP-REAL 2); :: thesis: ( (p + q) `1 = (p `1) + (q `1) & (p + q) `2 = (p `2) + (q `2) )
p + q = |[((p `1) + (q `1)),((p `2) + (q `2))]| by EUCLID:55;
hence ( (p + q) `1 = (p `1) + (q `1) & (p + q) `2 = (p `2) + (q `2) ) by EUCLID:52; :: thesis: verum