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;

per cases ( ( angle ((euc2cpx B),(euc2cpx C),(euc2cpx A)) = 0 & angle ((euc2cpx C),(euc2cpx A),(euc2cpx B)) = PI ) or not angle ((euc2cpx B),(euc2cpx C),(euc2cpx A)) = 0 or not angle ((euc2cpx C),(euc2cpx A),(euc2cpx B)) = PI ) ;

suppose ( angle ((euc2cpx B),(euc2cpx C),(euc2cpx A)) = 0 & angle ((euc2cpx C),(euc2cpx A),(euc2cpx B)) = PI ) ; :: thesis: ( angle (B,C,A) = PI or angle (B,A,C) = PI )

hence ( angle (B,C,A) = PI or angle (B,A,C) = PI ) by COMPLEX2:82; :: thesis: verum

end;

suppose ( not angle ((euc2cpx B),(euc2cpx C),(euc2cpx A)) = 0 or not angle ((euc2cpx C),(euc2cpx A),(euc2cpx B)) = PI ) ; :: thesis: ( angle (B,C,A) = PI or angle (B,A,C) = PI )

hence ( angle (B,C,A) = PI or angle (B,A,C) = PI ) by A3, A1, COMPLEX2:87; :: thesis: verum

end;

end;