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:61;
hence ( (p1 - p2) `1 = (p1 `1) - (p2 `1) & (p1 - p2) `2 = (p1 `2) - (p2 `2) ) ; :: thesis: verum