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

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