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 Th19;
hence ( Arg (p1 - p2) = Arg (p3 - p2) & angle p3,p2,p1 = 0 ) by A1, COMPLEX2:88; :: thesis: verum