let r be Real; :: thesis: ( inside_of_circle (0,0,r) = { p where p is Point of (TOP-REAL 2) : |.p.| < r } & ( r > 0 implies circle (0,0,r) = { p2 where p2 is Point of (TOP-REAL 2) : |.p2.| = r } ) & outside_of_circle (0,0,r) = { p3 where p3 is Point of (TOP-REAL 2) : |.p3.| > r } & closed_inside_of_circle (0,0,r) = { q where q is Point of (TOP-REAL 2) : |.q.| <= r } & closed_outside_of_circle (0,0,r) = { q2 where q2 is Point of (TOP-REAL 2) : |.q2.| >= r } )

defpred S_{1}[ Point of (TOP-REAL 2)] means |.($1 - |[0,0]|).| < r;

defpred S_{2}[ Point of (TOP-REAL 2)] means |.$1.| < r;

deffunc H_{1}( set ) -> set = $1;

A1: for p being Point of (TOP-REAL 2) holds

( S_{1}[p] iff S_{2}[p] )
by EUCLID:54, RLVECT_1:13;

inside_of_circle (0,0,r) = { H_{1}(p) where p is Point of (TOP-REAL 2) : S_{1}[p] }

.= { H_{1}(p2) where p2 is Point of (TOP-REAL 2) : S_{2}[p2] }
from FRAENKEL:sch 3(A1)
;

hence inside_of_circle (0,0,r) = { p where p is Point of (TOP-REAL 2) : |.p.| < r } ; :: thesis: ( ( r > 0 implies circle (0,0,r) = { p2 where p2 is Point of (TOP-REAL 2) : |.p2.| = r } ) & outside_of_circle (0,0,r) = { p3 where p3 is Point of (TOP-REAL 2) : |.p3.| > r } & closed_inside_of_circle (0,0,r) = { q where q is Point of (TOP-REAL 2) : |.q.| <= r } & closed_outside_of_circle (0,0,r) = { q2 where q2 is Point of (TOP-REAL 2) : |.q2.| >= r } )

defpred S_{3}[ Point of (TOP-REAL 2)] means |.($1 - |[0,0]|).| = r;

defpred S_{4}[ Point of (TOP-REAL 2)] means |.$1.| = r;

A2: for p being Point of (TOP-REAL 2) holds

( S_{3}[p] iff S_{4}[p] )
by EUCLID:54, RLVECT_1:13;

_{5}[ Point of (TOP-REAL 2)] means |.($1 - |[0,0]|).| > r;

defpred S_{6}[ Point of (TOP-REAL 2)] means |.$1.| > r;

A3: for p being Point of (TOP-REAL 2) holds

( S_{5}[p] iff S_{6}[p] )
by EUCLID:54, RLVECT_1:13;

outside_of_circle (0,0,r) = { H_{1}(p) where p is Point of (TOP-REAL 2) : S_{5}[p] }

.= { H_{1}(p2) where p2 is Point of (TOP-REAL 2) : S_{6}[p2] }
from FRAENKEL:sch 3(A3)
;

hence outside_of_circle (0,0,r) = { p3 where p3 is Point of (TOP-REAL 2) : |.p3.| > r } ; :: thesis: ( closed_inside_of_circle (0,0,r) = { q where q is Point of (TOP-REAL 2) : |.q.| <= r } & closed_outside_of_circle (0,0,r) = { q2 where q2 is Point of (TOP-REAL 2) : |.q2.| >= r } )

defpred S_{7}[ Point of (TOP-REAL 2)] means |.($1 - |[0,0]|).| <= r;

defpred S_{8}[ Point of (TOP-REAL 2)] means |.$1.| <= r;

A4: for p being Point of (TOP-REAL 2) holds

( S_{7}[p] iff S_{8}[p] )
by EUCLID:54, RLVECT_1:13;

closed_inside_of_circle (0,0,r) = { H_{1}(p) where p is Point of (TOP-REAL 2) : S_{7}[p] }

.= { H_{1}(p2) where p2 is Point of (TOP-REAL 2) : S_{8}[p2] }
from FRAENKEL:sch 3(A4)
;

hence closed_inside_of_circle (0,0,r) = { p where p is Point of (TOP-REAL 2) : |.p.| <= r } ; :: thesis: closed_outside_of_circle (0,0,r) = { q2 where q2 is Point of (TOP-REAL 2) : |.q2.| >= r }

defpred S_{9}[ Point of (TOP-REAL 2)] means |.($1 - |[0,0]|).| >= r;

defpred S_{10}[ Point of (TOP-REAL 2)] means |.$1.| >= r;

A5: for p being Point of (TOP-REAL 2) holds

( S_{9}[p] iff S_{10}[p] )
by EUCLID:54, RLVECT_1:13;

closed_outside_of_circle (0,0,r) = { H_{1}(p) where p is Point of (TOP-REAL 2) : S_{9}[p] }

.= { H_{1}(p2) where p2 is Point of (TOP-REAL 2) : S_{10}[p2] }
from FRAENKEL:sch 3(A5)
;

hence closed_outside_of_circle (0,0,r) = { q2 where q2 is Point of (TOP-REAL 2) : |.q2.| >= r } ; :: thesis: verum

defpred S

defpred S

deffunc H

A1: for p being Point of (TOP-REAL 2) holds

( S

inside_of_circle (0,0,r) = { H

.= { H

hence inside_of_circle (0,0,r) = { p where p is Point of (TOP-REAL 2) : |.p.| < r } ; :: thesis: ( ( r > 0 implies circle (0,0,r) = { p2 where p2 is Point of (TOP-REAL 2) : |.p2.| = r } ) & outside_of_circle (0,0,r) = { p3 where p3 is Point of (TOP-REAL 2) : |.p3.| > r } & closed_inside_of_circle (0,0,r) = { q where q is Point of (TOP-REAL 2) : |.q.| <= r } & closed_outside_of_circle (0,0,r) = { q2 where q2 is Point of (TOP-REAL 2) : |.q2.| >= r } )

defpred S

defpred S

A2: for p being Point of (TOP-REAL 2) holds

( S

hereby :: thesis: ( outside_of_circle (0,0,r) = { p3 where p3 is Point of (TOP-REAL 2) : |.p3.| > r } & closed_inside_of_circle (0,0,r) = { q where q is Point of (TOP-REAL 2) : |.q.| <= r } & closed_outside_of_circle (0,0,r) = { q2 where q2 is Point of (TOP-REAL 2) : |.q2.| >= r } )

defpred Sassume
r > 0
; :: thesis: circle (0,0,r) = { p2 where p2 is Point of (TOP-REAL 2) : |.p2.| = r }

circle (0,0,r) = { H_{1}(p) where p is Point of (TOP-REAL 2) : S_{3}[p] }

.= { H_{1}(p2) where p2 is Point of (TOP-REAL 2) : S_{4}[p2] }
from FRAENKEL:sch 3(A2)
;

hence circle (0,0,r) = { p2 where p2 is Point of (TOP-REAL 2) : |.p2.| = r } ; :: thesis: verum

end;circle (0,0,r) = { H

.= { H

hence circle (0,0,r) = { p2 where p2 is Point of (TOP-REAL 2) : |.p2.| = r } ; :: thesis: verum

defpred S

A3: for p being Point of (TOP-REAL 2) holds

( S

outside_of_circle (0,0,r) = { H

.= { H

hence outside_of_circle (0,0,r) = { p3 where p3 is Point of (TOP-REAL 2) : |.p3.| > r } ; :: thesis: ( closed_inside_of_circle (0,0,r) = { q where q is Point of (TOP-REAL 2) : |.q.| <= r } & closed_outside_of_circle (0,0,r) = { q2 where q2 is Point of (TOP-REAL 2) : |.q2.| >= r } )

defpred S

defpred S

A4: for p being Point of (TOP-REAL 2) holds

( S

closed_inside_of_circle (0,0,r) = { H

.= { H

hence closed_inside_of_circle (0,0,r) = { p where p is Point of (TOP-REAL 2) : |.p.| <= r } ; :: thesis: closed_outside_of_circle (0,0,r) = { q2 where q2 is Point of (TOP-REAL 2) : |.q2.| >= r }

defpred S

defpred S

A5: for p being Point of (TOP-REAL 2) holds

( S

closed_outside_of_circle (0,0,r) = { H

.= { H

hence closed_outside_of_circle (0,0,r) = { q2 where q2 is Point of (TOP-REAL 2) : |.q2.| >= r } ; :: thesis: verum