let a, b be Real; :: thesis: circle (a,b,0) = {|[a,b]|}
now :: thesis: ( ( for t being object st t in { p where p is Point of (TOP-REAL 2) : |.(p - |[a,b]|).| = 0 } holds
t in {|[a,b]|} ) & ( for t being object st t in {|[a,b]|} holds
t in { p where p is Point of (TOP-REAL 2) : |.(p - |[a,b]|).| = 0 } ) )
hereby :: thesis: for t being object st t in {|[a,b]|} holds
t in { p where p is Point of (TOP-REAL 2) : |.(p - |[a,b]|).| = 0 }
let t be object ; :: thesis: ( t in { p where p is Point of (TOP-REAL 2) : |.(p - |[a,b]|).| = 0 } implies t in {|[a,b]|} )
assume t in { p where p is Point of (TOP-REAL 2) : |.(p - |[a,b]|).| = 0 } ; :: thesis: t in {|[a,b]|}
then consider p0 being Point of (TOP-REAL 2) such that
A1: t = p0 and
A2: |.(p0 - |[a,b]|).| = 0 ;
p0 = |[a,b]| by A2, EUCLID_6:42;
hence t in {|[a,b]|} by A1, TARSKI:def 1; :: thesis: verum
end;
let t be object ; :: thesis: ( t in {|[a,b]|} implies t in { p where p is Point of (TOP-REAL 2) : |.(p - |[a,b]|).| = 0 } )
assume A3: t in {|[a,b]|} ; :: thesis: t in { p where p is Point of (TOP-REAL 2) : |.(p - |[a,b]|).| = 0 }
then A4: t = |[a,b]| by TARSKI:def 1;
reconsider p0 = t as Point of (TOP-REAL 2) by A3, TARSKI:def 1;
|.(p0 - |[a,b]|).| = 0 by A4, EUCLID_6:42;
hence t in { p where p is Point of (TOP-REAL 2) : |.(p - |[a,b]|).| = 0 } ; :: thesis: verum
end;
then ( { p where p is Point of (TOP-REAL 2) : |.(p - |[a,b]|).| = 0 } c= {|[a,b]|} & {|[a,b]|} c= { p where p is Point of (TOP-REAL 2) : |.(p - |[a,b]|).| = 0 } ) ;
hence circle (a,b,0) = {|[a,b]|} by JGRAPH_6:def 5; :: thesis: verum