let p1, p2, p3 be Point of (TOP-REAL 2); :: thesis: ( angle (p1,p2,p3) = 0 implies ( Arg (p1 - p2) = Arg (p3 - p2) & angle (p3,p2,p1) = 0 ) )
assume A1: angle (p1,p2,p3) = 0 ; :: thesis: ( Arg (p1 - p2) = Arg (p3 - p2) & angle (p3,p2,p1) = 0 )
( (euc2cpx p1) - (euc2cpx p2) = euc2cpx (p1 - p2) & (euc2cpx p3) - (euc2cpx p2) = euc2cpx (p3 - p2) ) by Th15;
hence ( Arg (p1 - p2) = Arg (p3 - p2) & angle (p3,p2,p1) = 0 ) by A1, COMPLEX2:74; :: thesis: verum