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;

( 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) )

hence
( A in circle (a,b,r) & B in circle (a,b,r) & C in circle (a,b,r) )
; :: thesis: verum
|.(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) 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