let A be Point of (TOP-REAL 2); for a, b being Real
for r being positive Real st A in circle (a,b,r) holds
A <> |[a,b]|
let a, b be Real; for r being positive Real st A in circle (a,b,r) holds
A <> |[a,b]|
let r be positive Real; ( A in circle (a,b,r) implies A <> |[a,b]| )
assume A1:
A in circle (a,b,r)
; A <> |[a,b]|
circle (a,b,r) = { p where p is Point of (TOP-REAL 2) : |.(p - |[a,b]|).| = r }
by JGRAPH_6:def 5;
then consider p0 being Point of (TOP-REAL 2) such that
A2:
A = p0
and
A3:
|.(p0 - |[a,b]|).| = r
by A1;
thus
A <> |[a,b]|
by A2, A3, EUCLID_6:42; verum