let A, B, C be Point of (TOP-REAL 2); :: thesis: ( A,B,C is_a_triangle & PI < angle (C,B,A) & angle (C,B,A) < 2 * PI implies the_diameter_of_the_circumcircle (A,B,C) < 0 )
assume that
A1: A,B,C is_a_triangle and
A2: ( PI < angle (C,B,A) & angle (C,B,A) < 2 * PI ) ; :: thesis: the_diameter_of_the_circumcircle (A,B,C) < 0
A,B,C are_mutually_distinct by A1, EUCLID_6:20;
then A3: ( |.(C - A).| >= 0 & |.(C - A).| <> 0 ) by EUCLID_6:42;
( PI + ((2 * PI) * 0) < angle (C,B,A) & angle (C,B,A) < (2 * PI) + ((2 * PI) * 0) ) by A2;
then |.(C - A).| / (sin (angle (C,B,A))) < 0 by XREAL_1:142, A3, SIN_COS6:12;
hence the_diameter_of_the_circumcircle (A,B,C) < 0 by A1, EUCLID10:44; :: thesis: verum