let A, B, C be Point of (TOP-REAL 2); :: thesis: ( angle (C,B,A) < PI implies 0 <= the_diameter_of_the_circumcircle (A,B,C) )
assume angle (C,B,A) < PI ; :: thesis: 0 <= the_diameter_of_the_circumcircle (A,B,C)
then 0 <= the_area_of_polygon3 (A,B,C) by Th5;
hence 0 <= the_diameter_of_the_circumcircle (A,B,C) ; :: thesis: verum