let A, B, C be Point of (TOP-REAL 2); :: thesis: ( A,B,C is_a_triangle implies the_radius_of_the_circumcircle (A,B,C) > 0 )
assume A1: A,B,C is_a_triangle ; :: thesis: the_radius_of_the_circumcircle (A,B,C) > 0
then A2: A,B,C are_mutually_distinct by EUCLID_6:20;
assume A3: the_radius_of_the_circumcircle (A,B,C) <= 0 ; :: thesis: contradiction
A4: |.((the_circumcenter (A,B,C)) - A).| = 0 by A1, A3, Def4;
consider a, b, r being Real such that
A5: ( A in circle (a,b,r) & B in circle (a,b,r) & C in circle (a,b,r) ) by A1, Th48;
A6: r = 0 by A1, A4, A5, Th49;
circle (a,b,0) = {|[a,b]|} by EUCLID10:36;
then ( A = |[a,b]| & B = |[a,b]| & C = |[a,b]| ) by A5, A6, TARSKI:def 1;
hence contradiction by A2; :: thesis: verum