let p1, p2, p3 be Point of (TOP-REAL 2); :: thesis: ( p1 <> p2 & p3 <> p2 implies ( |((p1 - p2),(p3 - p2))| = 0 iff ( angle p1,p2,p3 = PI / 2 or angle p1,p2,p3 = (3 / 2) * PI ) ) )
assume that
A1: p1 <> p2 and
A2: p3 <> p2 ; :: thesis: ( |((p1 - p2),(p3 - p2))| = 0 iff ( angle p1,p2,p3 = PI / 2 or angle p1,p2,p3 = (3 / 2) * PI ) )
p1 - p2 <> 0. (TOP-REAL 2) by A1, EUCLID:47;
then A3: euc2cpx (p1 - p2) <> 0c by Th2, Th20;
p3 - p2 <> 0. (TOP-REAL 2) by A2, EUCLID:47;
then A4: euc2cpx (p3 - p2) <> 0c by Th2, Th20;
A5: ( (euc2cpx p1) - (euc2cpx p2) = euc2cpx (p1 - p2) & (euc2cpx p3) - (euc2cpx p2) = euc2cpx (p3 - p2) ) by Th19;

hereby :: thesis: ( ( angle p1,p2,p3 = PI / 2 or angle p1,p2,p3 = (3 / 2) * PI ) implies |((p1 - p2),(p3 - p2))| = 0 )

assume |((p1 - p2),(p3 - p2))| = 0 ; :: thesis: ( angle p1,p2,p3 = PI / 2 or angle p1,p2,p3 = (3 / 2) * PI )
then Re ((euc2cpx (p1 - p2)) .|. (euc2cpx (p3 - p2))) = 0 by Th51;
then ( angle (euc2cpx (p1 - p2)),0c ,(euc2cpx (p3 - p2)) = PI / 2 or angle (euc2cpx (p1 - p2)),0c ,(euc2cpx (p3 - p2)) = (3 / 2) * PI ) by A3, A4, COMPLEX2:89;
hence ( angle p1,p2,p3 = PI / 2 or angle p1,p2,p3 = (3 / 2) * PI ) by A5, COMPLEX2:85; :: thesis: verum

end;

A6: |((p1 - p2),(p3 - p2))| = Re ((euc2cpx (p1 - p2)) .|. (euc2cpx (p3 - p2))) by Th51;
assume ( angle p1,p2,p3 = PI / 2 or angle p1,p2,p3 = (3 / 2) * PI ) ; :: thesis: |((p1 - p2),(p3 - p2))| = 0
then ( angle (euc2cpx (p1 - p2)),0c ,(euc2cpx (p3 - p2)) = PI / 2 or angle (euc2cpx (p1 - p2)),0c ,(euc2cpx (p3 - p2)) = (3 / 2) * PI ) by A5, COMPLEX2:85;
hence |((p1 - p2),(p3 - p2))| = 0 by A6, A3, A4, COMPLEX2:89; :: thesis: verum