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

per cases then ( ( angle ((euc2cpx B),(euc2cpx C),(euc2cpx A)) = 0 & angle ((euc2cpx C),(euc2cpx A),(euc2cpx B)) = PI ) or ( angle ((euc2cpx B),(euc2cpx C),(euc2cpx A)) = PI & angle ((euc2cpx C),(euc2cpx A),(euc2cpx B)) = 0 ) ) by COMPLEX2:87;

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

hence ( ( angle (B,C,A) = 0 & angle (C,A,B) = PI ) or ( angle (B,C,A) = PI & angle (C,A,B) = 0 & ((angle (A,B,C)) + (angle (B,C,A))) + (angle (C,A,B)) = PI ) ) by EUCLID_3:def 4; :: thesis: verum

end;

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

then ( angle (B,C,A) = PI & angle (C,A,B) = 0 ) by EUCLID_3:def 4;
hence ( ( angle (B,C,A) = 0 & angle (C,A,B) = PI ) or ( angle (B,C,A) = PI & angle (C,A,B) = 0 & ((angle (A,B,C)) + (angle (B,C,A))) + (angle (C,A,B)) = PI ) ) by A2; :: thesis: verum

end;

end;