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 A1A: B,A,C are_mutually_distinct by EUCLID_6:20;
assume A2: (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 A3: ( 0 <= angle (B,A,C) & angle (B,A,C) < PI ) ; :: thesis: contradiction

(angle (B,A,C)) - PI = angle (C,B,A) by A2;
hence contradiction by A3, XREAL_1:49, EUCLID11:2; :: thesis: verum

end;

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

then angle (C,B,A) = 0 by A2;
hence contradiction by A1, EUCLID10:30; :: thesis: verum

end;

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

then (angle (B,A,C)) - PI < (2 * PI) - PI by XREAL_1:14;
hence contradiction by A1A, A2, A4, EUCLID11:8; :: thesis: verum

end;

end;