let A, B be Point of (TOP-REAL 2); :: thesis: for a, b being Real
for r being positive Real st A,B,|[a,b]| are_mutually_distinct & A in circle (a,b,r) & B in circle (a,b,r) & |[a,b]| in LSeg (A,B) holds
|.(A - B).| = 2 * r
let a, b be Real; :: thesis: for r being positive Real st A,B,|[a,b]| are_mutually_distinct & A in circle (a,b,r) & B in circle (a,b,r) & |[a,b]| in LSeg (A,B) holds
|.(A - B).| = 2 * r
let r be positive Real; :: thesis: ( A,B,|[a,b]| are_mutually_distinct & A in circle (a,b,r) & B in circle (a,b,r) & |[a,b]| in LSeg (A,B) implies |.(A - B).| = 2 * r )
assume that
A1: A,B,|[a,b]| are_mutually_distinct and
A2: ( A in circle (a,b,r) & B in circle (a,b,r) ) and
A3: |[a,b]| in LSeg (A,B) ; :: thesis: |.(A - B).| = 2 * r
A4: circle (a,b,r) = { p where p is Point of (TOP-REAL 2) : |.(p - |[a,b]|).| = r } by JGRAPH_6:def 5;
consider JA being Point of (TOP-REAL 2) such that
A5: A = JA and
A6: |.(JA - |[a,b]|).| = r by A2, A4;
consider JB being Point of (TOP-REAL 2) such that
A7: B = JB and
A8: |.(JB - |[a,b]|).| = r by A2, A4;
|.(A - B).| = |.(A - |[a,b]|).| + |.(|[a,b]| - B).| by A1, A3, Thm37
.= r + r by A5, A6, A7, A8, EUCLID_6:43 ;
hence |.(A - B).| = 2 * r ; :: thesis: verum