let r be Real; :: thesis: ( inside_of_circle (0,0,r) = { p where p is Point of () : |.p.| < r } & ( r > 0 implies circle (0,0,r) = { p2 where p2 is Point of () : |.p2.| = r } ) & outside_of_circle (0,0,r) = { p3 where p3 is Point of () : |.p3.| > r } & closed_inside_of_circle (0,0,r) = { q where q is Point of () : |.q.| <= r } & closed_outside_of_circle (0,0,r) = { q2 where q2 is Point of () : |.q2.| >= r } )
defpred S1[ Point of ()] means |.(\$1 - ).| < r;
defpred S2[ Point of ()] means |.\$1.| < r;
deffunc H1( set ) -> set = \$1;
A1: for p being Point of () holds
( S1[p] iff S2[p] ) by ;
inside_of_circle (0,0,r) = { H1(p) where p is Point of () : S1[p] }
.= { H1(p2) where p2 is Point of () : S2[p2] } from ;
hence inside_of_circle (0,0,r) = { p where p is Point of () : |.p.| < r } ; :: thesis: ( ( r > 0 implies circle (0,0,r) = { p2 where p2 is Point of () : |.p2.| = r } ) & outside_of_circle (0,0,r) = { p3 where p3 is Point of () : |.p3.| > r } & closed_inside_of_circle (0,0,r) = { q where q is Point of () : |.q.| <= r } & closed_outside_of_circle (0,0,r) = { q2 where q2 is Point of () : |.q2.| >= r } )
defpred S3[ Point of ()] means |.(\$1 - ).| = r;
defpred S4[ Point of ()] means |.\$1.| = r;
A2: for p being Point of () holds
( S3[p] iff S4[p] ) by ;
hereby :: thesis: ( outside_of_circle (0,0,r) = { p3 where p3 is Point of () : |.p3.| > r } & closed_inside_of_circle (0,0,r) = { q where q is Point of () : |.q.| <= r } & closed_outside_of_circle (0,0,r) = { q2 where q2 is Point of () : |.q2.| >= r } )
assume r > 0 ; :: thesis: circle (0,0,r) = { p2 where p2 is Point of () : |.p2.| = r }
circle (0,0,r) = { H1(p) where p is Point of () : S3[p] }
.= { H1(p2) where p2 is Point of () : S4[p2] } from ;
hence circle (0,0,r) = { p2 where p2 is Point of () : |.p2.| = r } ; :: thesis: verum
end;
defpred S5[ Point of ()] means |.(\$1 - ).| > r;
defpred S6[ Point of ()] means |.\$1.| > r;
A3: for p being Point of () holds
( S5[p] iff S6[p] ) by ;
outside_of_circle (0,0,r) = { H1(p) where p is Point of () : S5[p] }
.= { H1(p2) where p2 is Point of () : S6[p2] } from ;
hence outside_of_circle (0,0,r) = { p3 where p3 is Point of () : |.p3.| > r } ; :: thesis: ( closed_inside_of_circle (0,0,r) = { q where q is Point of () : |.q.| <= r } & closed_outside_of_circle (0,0,r) = { q2 where q2 is Point of () : |.q2.| >= r } )
defpred S7[ Point of ()] means |.(\$1 - ).| <= r;
defpred S8[ Point of ()] means |.\$1.| <= r;
A4: for p being Point of () holds
( S7[p] iff S8[p] ) by ;
closed_inside_of_circle (0,0,r) = { H1(p) where p is Point of () : S7[p] }
.= { H1(p2) where p2 is Point of () : S8[p2] } from ;
hence closed_inside_of_circle (0,0,r) = { p where p is Point of () : |.p.| <= r } ; :: thesis: closed_outside_of_circle (0,0,r) = { q2 where q2 is Point of () : |.q2.| >= r }
defpred S9[ Point of ()] means |.(\$1 - ).| >= r;
defpred S10[ Point of ()] means |.\$1.| >= r;
A5: for p being Point of () holds
( S9[p] iff S10[p] ) by ;
closed_outside_of_circle (0,0,r) = { H1(p) where p is Point of () : S9[p] }
.= { H1(p2) where p2 is Point of () : S10[p2] } from ;
hence closed_outside_of_circle (0,0,r) = { q2 where q2 is Point of () : |.q2.| >= r } ; :: thesis: verum