let p1, p2 be Point of (TOP-REAL 2); :: thesis: euc2cpx (p1 - p2) = (euc2cpx p1) - (euc2cpx p2)
thus euc2cpx (p1 - p2) = (euc2cpx p1) + (euc2cpx (- p2)) by Th9
.= (euc2cpx p1) + (- (euc2cpx p2)) by Th13
.= (euc2cpx p1) - (euc2cpx p2) ; :: thesis: verum