let A, B, C be Point of (TOP-REAL 2); :: thesis: ( A,B,C is_a_triangle & 0 < angle (C,B,A) & angle (C,B,A) < PI implies the_diameter_of_the_circumcircle (A,B,C) > 0 )
assume that
A1: A,B,C is_a_triangle and
A2: ( 0 < angle (C,B,A) & angle (C,B,A) < 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;
( (2 * PI) * 0 < angle (C,B,A) & angle (C,B,A) < PI + ((2 * PI) * 0) ) by A2;
then ( sin (angle (C,B,A)) > 0 & |.(C - A).| > 0 ) by A3, SIN_COS6:11;
then |.(C - A).| / (sin (angle (C,B,A))) > 0 by XREAL_1:139;
hence the_diameter_of_the_circumcircle (A,B,C) > 0 by A1, EUCLID10:44; :: thesis: verum