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:61;
hence ( (p - q) `1 = (p `1) - (q `1) & (p - q) `2 = (p `2) - (q `2) ) by EUCLID:52; :: thesis: verum