let A, B, C be Point of (TOP-REAL 2); :: thesis: ( A,B,C is_a_triangle implies ex a, b, r being Real st
( A in circle (a,b,r) & B in circle (a,b,r) & C in circle (a,b,r) ) )
assume A,B,C is_a_triangle ; :: thesis: ex a, b, r being Real st
( A in circle (a,b,r) & B in circle (a,b,r) & C in circle (a,b,r) )
then consider D being Point of (TOP-REAL 2) such that
(the_perpendicular_bisector (A,B)) /\ (the_perpendicular_bisector (B,C)) = {D} and
(the_perpendicular_bisector (B,C)) /\ (the_perpendicular_bisector (C,A)) = {D} and
(the_perpendicular_bisector (C,A)) /\ (the_perpendicular_bisector (A,B)) = {D} and
A1: |.(D - A).| = |.(D - B).| and
A2: |.(D - A).| = |.(D - C).| and
|.(D - B).| = |.(D - C).| by Th47;
take a = D `1 ; :: thesis: ex b, r being Real st
( A in circle (a,b,r) & B in circle (a,b,r) & C in circle (a,b,r) )
take b = D `2 ; :: thesis: ex r being Real st
( A in circle (a,b,r) & B in circle (a,b,r) & C in circle (a,b,r) )
take r = |.(D - A).|; :: thesis: ( A in circle (a,b,r) & B in circle (a,b,r) & C in circle (a,b,r) )
A3: D = |[a,b]| by EUCLID:53;

now :: thesis: ( A in circle (a,b,r) & B in circle (a,b,r) & C in circle (a,b,r) )

|.(A - |[a,b]|).| = r by A3, EUCLID_6:43;
hence A in circle (a,b,r) by TOPREAL9:43; :: thesis: ( B in circle (a,b,r) & C in circle (a,b,r) )
|.(B - |[a,b]|).| = r by A1, A3, EUCLID_6:43;
hence B in circle (a,b,r) by TOPREAL9:43; :: thesis: C in circle (a,b,r)
|.(C - |[a,b]|).| = r by A2, A3, EUCLID_6:43;
hence C in circle (a,b,r) by TOPREAL9:43; :: thesis: verum

end;

hence ( A in circle (a,b,r) & B in circle (a,b,r) & C in circle (a,b,r) ) ; :: thesis: verum