let A, B, C be Point of (TOP-REAL 2); :: thesis: ( angle (A,B,C) = 0 & A,B,C are_mutually_distinct & not angle (B,C,A) = PI implies angle (B,A,C) = PI )
set z1 = euc2cpx A;
set z2 = euc2cpx B;
set z3 = euc2cpx C;
assume that
A1: angle (A,B,C) = 0 and
A2: A,B,C are_mutually_distinct ; :: thesis: ( angle (B,C,A) = PI or angle (B,A,C) = PI )
( A <> B & A <> C & B <> C ) by A2, ZFMISC_1:def 5;
then A3: ( euc2cpx A <> euc2cpx B & euc2cpx A <> euc2cpx C & euc2cpx B <> euc2cpx C ) by EUCLID_3:4;