let A be Point of (TOP-REAL 2); :: thesis: 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; :: thesis: for r being positive Real st A in circle (a,b,r) holds
A <> |[a,b]|
let r be positive Real; :: thesis: ( A in circle (a,b,r) implies A <> |[a,b]| )
assume A1: A in circle (a,b,r) ; :: thesis: 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; :: thesis: verum