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

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