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 S1[ Point of (TOP-REAL 2)] means |.($1 - |[0,0]|).| < r;
defpred S2[ Point of (TOP-REAL 2)] means |.$1.| < r;
deffunc H1( set ) -> set = $1;
A1: for p being Point of (TOP-REAL 2) holds
( S1[p] iff S2[p] ) by EUCLID:54, RLVECT_1:13;
inside_of_circle (0,0,r) = { H1(p) where p is Point of (TOP-REAL 2) : S1[p] }
.= { H1(p2) where p2 is Point of (TOP-REAL 2) : S2[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 S3[ Point of (TOP-REAL 2)] means |.($1 - |[0,0]|).| = r;
defpred S4[ Point of (TOP-REAL 2)] means |.$1.| = r;
A2: for p being Point of (TOP-REAL 2) holds
( S3[p] iff S4[p] ) by EUCLID:54, RLVECT_1:13;
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) = { H1(p) where p is Point of (TOP-REAL 2) : S3[p] }
.= { H1(p2) where p2 is Point of (TOP-REAL 2) : S4[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 S5[ Point of (TOP-REAL 2)] means |.($1 - |[0,0]|).| > r;
defpred S6[ Point of (TOP-REAL 2)] means |.$1.| > r;
A3: for p being Point of (TOP-REAL 2) holds
( S5[p] iff S6[p] ) by EUCLID:54, RLVECT_1:13;
outside_of_circle (0,0,r) = { H1(p) where p is Point of (TOP-REAL 2) : S5[p] }
.= { H1(p2) where p2 is Point of (TOP-REAL 2) : S6[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 S7[ Point of (TOP-REAL 2)] means |.($1 - |[0,0]|).| <= r;
defpred S8[ Point of (TOP-REAL 2)] means |.$1.| <= r;
A4: for p being Point of (TOP-REAL 2) holds
( S7[p] iff S8[p] ) by EUCLID:54, RLVECT_1:13;
closed_inside_of_circle (0,0,r) = { H1(p) where p is Point of (TOP-REAL 2) : S7[p] }
.= { H1(p2) where p2 is Point of (TOP-REAL 2) : S8[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 S9[ Point of (TOP-REAL 2)] means |.($1 - |[0,0]|).| >= r;
defpred S10[ Point of (TOP-REAL 2)] means |.$1.| >= r;
A5: for p being Point of (TOP-REAL 2) holds
( S9[p] iff S10[p] ) by EUCLID:54, RLVECT_1:13;
closed_outside_of_circle (0,0,r) = { H1(p) where p is Point of (TOP-REAL 2) : S9[p] }
.= { H1(p2) where p2 is Point of (TOP-REAL 2) : S10[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