theorem :: EUCLID_3:46

for p1, p2, p3 being Point of (TOP-REAL 2) st p1 <> p2 & p3 <> p2 & ( angle (p1,p2,p3) = PI / 2 or angle (p1,p2,p3) = (3 / 2) * PI ) holds
(|.(p1 - p2).| ^2) + (|.(p3 - p2).| ^2) = |.(p1 - p3).| ^2