let A, B, C be Point of (TOP-REAL 2); :: thesis: ( A,B,C is_a_triangle implies ( (- 2) * PI < (angle (B,A,C)) - (angle (C,B,A)) & (angle (B,A,C)) - (angle (C,B,A)) < 2 * PI ) )
assume A1: A,B,C is_a_triangle ; :: thesis: ( (- 2) * PI < (angle (B,A,C)) - (angle (C,B,A)) & (angle (B,A,C)) - (angle (C,B,A)) < 2 * PI )
A2: ( 0 <= angle (B,A,C) & angle (B,A,C) < 2 * PI & 0 <= angle (C,B,A) & angle (C,B,A) < 2 * PI ) by EUCLID11:2;
then A3: ( 0 < angle (B,A,C) & angle (B,A,C) < 2 * PI & 0 < angle (C,B,A) & angle (C,B,A) < 2 * PI ) by A1, EUCLID10:30;
0 - (2 * PI) < (angle (B,A,C)) - (angle (C,B,A)) by A3, XREAL_1:14;
hence (- 2) * PI < (angle (B,A,C)) - (angle (C,B,A)) ; :: thesis: (angle (B,A,C)) - (angle (C,B,A)) < 2 * PI
(angle (B,A,C)) - (angle (C,B,A)) < (2 * PI) - 0 by A2, XREAL_1:14;
hence (angle (B,A,C)) - (angle (C,B,A)) < 2 * PI ; :: thesis: verum