let r be real number ; :: 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₁[ Point of (TOP-REAL 2)] means |.($1 - |[0,0]|).| < r;
defpred S₂[ Point of (TOP-REAL 2)] means |.$1.| < r;
deffunc H₁( set ) -> set = $1;
A1: for p being Point of (TOP-REAL 2) holds
( S₁[p] iff S₂[p] ) by EUCLID:58, RLVECT_1:26;
inside_of_circle (0,0,r) = { H₁(p) where p is Point of (TOP-REAL 2) : S₁[p] }
.= { H₁(p2) where p2 is Point of (TOP-REAL 2) : S₂[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₃[ Point of (TOP-REAL 2)] means |.($1 - |[0,0]|).| = r;
defpred S₄[ Point of (TOP-REAL 2)] means |.$1.| = r;
A2: for p being Point of (TOP-REAL 2) holds
( S₃[p] iff S₄[p] ) by EUCLID:58, RLVECT_1:26;

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 } )

assume r > 0 ; :: thesis: circle (0,0,r) = { p2 where p2 is Point of (TOP-REAL 2) : |.p2.| = r }
circle (0,0,r) = { H₁(p) where p is Point of (TOP-REAL 2) : S₃[p] }
.= { H₁(p2) where p2 is Point of (TOP-REAL 2) : S₄[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;

defpred S₅[ Point of (TOP-REAL 2)] means |.($1 - |[0,0]|).| > r;
defpred S₆[ Point of (TOP-REAL 2)] means |.$1.| > r;
A3: for p being Point of (TOP-REAL 2) holds
( S₅[p] iff S₆[p] ) by EUCLID:58, RLVECT_1:26;
outside_of_circle (0,0,r) = { H₁(p) where p is Point of (TOP-REAL 2) : S₅[p] }
.= { H₁(p2) where p2 is Point of (TOP-REAL 2) : S₆[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₇[ Point of (TOP-REAL 2)] means |.($1 - |[0,0]|).| <= r;
defpred S₈[ Point of (TOP-REAL 2)] means |.$1.| <= r;
A4: for p being Point of (TOP-REAL 2) holds
( S₇[p] iff S₈[p] ) by EUCLID:58, RLVECT_1:26;
closed_inside_of_circle (0,0,r) = { H₁(p) where p is Point of (TOP-REAL 2) : S₇[p] }
.= { H₁(p2) where p2 is Point of (TOP-REAL 2) : S₈[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₉[ Point of (TOP-REAL 2)] means |.($1 - |[0,0]|).| >= r;
defpred S₁₀[ Point of (TOP-REAL 2)] means |.$1.| >= r;
A5: for p being Point of (TOP-REAL 2) holds
( S₉[p] iff S₁₀[p] ) by EUCLID:58, RLVECT_1:26;
closed_outside_of_circle (0,0,r) = { H₁(p) where p is Point of (TOP-REAL 2) : S₉[p] }
.= { H₁(p2) where p2 is Point of (TOP-REAL 2) : S₁₀[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