let A, B, C be Point of (TOP-REAL 2); ( A,B,C is_a_triangle implies the_radius_of_the_circumcircle (A,B,C) > 0 )
assume A1:
A,B,C is_a_triangle
; 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
; 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; verum