theorem :: EUCLID_3:43

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