let A, B, C be Point of (TOP-REAL 2); ( A <> B & B <> C & |((B - A),(B - C))| = 0 & not angle (A,B,C) = PI / 2 implies angle (A,B,C) = (3 / 2) * PI )
assume that
A1:
A <> B
and
A2:
B <> C
and
A3:
|((B - A),(B - C))| = 0
; ( angle (A,B,C) = PI / 2 or angle (A,B,C) = (3 / 2) * PI )
|((A - B),(C - B))| =
|((- (A - B)),(- (C - B)))|
by EUCLID_2:23
.=
|((B - A),(- (C - B)))|
by RVSUM_1:35
.=
0
by A3, RVSUM_1:35
;
hence
( angle (A,B,C) = PI / 2 or angle (A,B,C) = (3 / 2) * PI )
by A1, A2, EUCLID_3:45; verum