let a be Real; :: thesis: for A, B, C being Point of (TOP-REAL 2)
for b, c, d, r, s being Real st A,B,C is_a_triangle & A in circle (a,b,r) & B in circle (a,b,r) & C in circle (a,b,r) & A in circle (c,d,s) & B in circle (c,d,s) & C in circle (c,d,s) holds
( a = c & b = d & r = s )
let A, B, C be Point of (TOP-REAL 2); :: thesis: for b, c, d, r, s being Real st A,B,C is_a_triangle & A in circle (a,b,r) & B in circle (a,b,r) & C in circle (a,b,r) & A in circle (c,d,s) & B in circle (c,d,s) & C in circle (c,d,s) holds
( a = c & b = d & r = s )
let b, c, d, r, s be Real; :: thesis: ( A,B,C is_a_triangle & A in circle (a,b,r) & B in circle (a,b,r) & C in circle (a,b,r) & A in circle (c,d,s) & B in circle (c,d,s) & C in circle (c,d,s) implies ( a = c & b = d & r = s ) )
assume that
A1: A,B,C is_a_triangle and
A2: A in circle (a,b,r) and
A3: B in circle (a,b,r) and
A4: C in circle (a,b,r) and
A5: A in circle (c,d,s) and
A6: B in circle (c,d,s) and
A7: C in circle (c,d,s) ; :: thesis: ( a = c & b = d & r = s )
A8: ( |[a,b]| = the_circumcenter (A,B,C) & r = |.((the_circumcenter (A,B,C)) - A).| & |[c,d]| = the_circumcenter (A,B,C) & s = |.((the_circumcenter (A,B,C)) - A).| ) by A1, A2, A3, A4, A5, A6, A7, Th49;
( |[a,b]| `1 = a & |[a,b]| `2 = b & |[c,d]| `1 = c & |[c,d]| `2 = d ) by EUCLID:52;
hence ( a = c & b = d & r = s ) by A8; :: thesis: verum