let A, B, C be Point of (TOP-REAL 2); ( 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
; 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 ; 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 ; 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).|; ( 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 ( 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;
( 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;
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;
verum end;
hence
( A in circle (a,b,r) & B in circle (a,b,r) & C in circle (a,b,r) )
; verum