theorem :: EUCLID_3:45

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