let n be Nat; for p1, p2, q1, q2 being Point of (TOP-REAL n) holds |((p1 - p2),(q1 - q2))| = ((|(p1,q1)| - |(p1,q2)|) - |(p2,q1)|) + |(p2,q2)|
let p1, p2, q1, q2 be Point of (TOP-REAL n); |((p1 - p2),(q1 - q2))| = ((|(p1,q1)| - |(p1,q2)|) - |(p2,q1)|) + |(p2,q2)|
A1:
( |(p1,(q1 - q2))| = |(p1,q1)| - |(p1,q2)| & |(p2,(q1 - q2))| = |(p2,q1)| - |(p2,q2)| )
by Th22;
|((p1 - p2),(q1 - q2))| =
|(p1,(q1 - q2))| - |(p2,(q1 - q2))|
by Th22
.=
((|(p1,q1)| - |(p1,q2)|) - |(p2,q1)|) + |(p2,q2)|
by A1
;
hence
|((p1 - p2),(q1 - q2))| = ((|(p1,q1)| - |(p1,q2)|) - |(p2,q1)|) + |(p2,q2)|
; verum