let A, B, C be Point of (TOP-REAL 2); :: thesis: ( A,B,C is_a_triangle implies (angle (B,A,C)) - (angle (C,B,A)) <> - PI )
assume A1: A,B,C is_a_triangle ; :: thesis: (angle (B,A,C)) - (angle (C,B,A)) <> - PI
then B,A,C is_a_triangle by MENELAUS:15;
then A2: B,A,C are_mutually_distinct by EUCLID_6:20;
assume A3: (angle (B,A,C)) - (angle (C,B,A)) = - PI ; :: thesis: contradiction

per cases ( ( 0 <= angle (B,A,C) & angle (B,A,C) < PI ) or angle (B,A,C) = PI or ( PI < angle (B,A,C) & angle (B,A,C) < 2 * PI ) ) by EUCLID11:3;

suppose ( 0 <= angle (B,A,C) & angle (B,A,C) < PI ) ; :: thesis: contradiction

then A4: ( 0 < angle (B,A,C) & angle (B,A,C) < PI ) by A1, EUCLID10:30;
then 0 + PI < (angle (B,A,C)) + PI by XREAL_1:8;
hence contradiction by A3, A4, A2, EUCLID11:5; :: thesis: verum

end;

suppose angle (B,A,C) = PI ; :: thesis: contradiction

hence contradiction by A3, EUCLID11:2; :: thesis: verum

end;

suppose ( PI < angle (B,A,C) & angle (B,A,C) < 2 * PI ) ; :: thesis: contradiction

then PI + PI < (angle (B,A,C)) + PI by XREAL_1:8;
hence contradiction by A3, EUCLID11:2; :: thesis: verum

end;

end;