let A, B, C be Point of (TOP-REAL 2); :: thesis: ( A,B,C is_a_triangle & angle (B,A,C) < PI implies ( - PI < (angle (B,A,C)) - (angle (C,B,A)) & (angle (B,A,C)) - (angle (C,B,A)) < PI ) )
assume that
A1: A,B,C is_a_triangle and
A2: angle (B,A,C) < PI ; :: thesis: ( - PI < (angle (B,A,C)) - (angle (C,B,A)) & (angle (B,A,C)) - (angle (C,B,A)) < PI )
B,A,C is_a_triangle by A1, MENELAUS:15;
then A3: B,A,C are_mutually_distinct by EUCLID_6:20;
A4: ( 0 <= angle (B,A,C) & not angle (B,A,C) is zero ) by A1, EUCLID10:30, EUCLID11:2;
A5: ( 0 <= angle (B,A,C) & angle (B,A,C) < PI & 0 <= angle (C,B,A) & angle (C,B,A) < PI ) by A2, A4, A3, EUCLID11:5;
A6: ( 0 < angle (B,A,C) & angle (B,A,C) < PI & 0 < angle (C,B,A) & angle (C,B,A) < PI ) by A2, A4, A3, EUCLID11:5;
0 - PI < (angle (B,A,C)) - (angle (C,B,A)) by A6, XREAL_1:14;
hence - PI < (angle (B,A,C)) - (angle (C,B,A)) ; :: thesis: (angle (B,A,C)) - (angle (C,B,A)) < PI
(angle (B,A,C)) - (angle (C,B,A)) < PI - 0 by A5, XREAL_1:14;
hence (angle (B,A,C)) - (angle (C,B,A)) < PI ; :: thesis: verum