theorem :: EUCLID_3:36

for p1, p2, p3 being Point of (TOP-REAL 2) st angle (p1,p2,p3) = 0 holds
( Arg (p1 - p2) = Arg (p3 - p2) & angle (p3,p2,p1) = 0 )