let A, B, C be Point of (TOP-REAL 2); :: thesis: ( 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 ; :: thesis: ( 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; :: thesis: verum