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

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