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

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