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, RLVECT_1:21;
then A3: euc2cpx (p1 - p2) <> 0c by Th2, Th16;
p3 - p2 <> 0. (TOP-REAL 2) by A2, RLVECT_1:21;
then A4: euc2cpx (p3 - p2) <> 0c by Th2, Th16;
A5: ( (euc2cpx p1) - (euc2cpx p2) = euc2cpx (p1 - p2) & (euc2cpx p3) - (euc2cpx p2) = euc2cpx (p3 - p2) ) by Th15;

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 Th42;
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:75;
hence ( angle (p1,p2,p3) = PI / 2 or angle (p1,p2,p3) = (3 / 2) * PI ) by A5, COMPLEX2:71; :: thesis: verum

end;

A6: |((p1 - p2),(p3 - p2))| = Re ((euc2cpx (p1 - p2)) .|. (euc2cpx (p3 - p2))) by Th42;
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:71;
hence |((p1 - p2),(p3 - p2))| = 0 by A6, A3, A4, COMPLEX2:75; :: thesis: verum