let A, B, C be Point of (TOP-REAL 2); :: thesis: ( A,B,C is_a_triangle implies angle (A,B,C) <> 0 )
assume A1: A,B,C is_a_triangle ; :: thesis: angle (A,B,C) <> 0
then A2: A,B,C are_mutually_distinct by EUCLID_6:20;
now :: thesis: not angle (A,B,C) = 0
assume angle (A,B,C) = 0 ; :: thesis: contradiction
then ( angle (B,C,A) = PI or angle (B,A,C) = PI ) by A2, MENELAUS:8;
then ( C in LSeg (B,A) or A in LSeg (B,C) ) by EUCLID_6:11;
hence contradiction by A1, TOPREAL9:67; :: thesis: verum
end;
hence angle (A,B,C) <> 0 ; :: thesis: verum