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