let r be real number ; :: thesis: for s being Point of (TOP-REAL 2) st s in Sphere (0. (TOP-REAL 2)),r holds
((s `1 ) ^2 ) + ((s `2 ) ^2 ) = r ^2
let s be Point of (TOP-REAL 2); :: thesis: ( s in Sphere (0. (TOP-REAL 2)),r implies ((s `1 ) ^2 ) + ((s `2 ) ^2 ) = r ^2 )
assume s in Sphere (0. (TOP-REAL 2)),r ; :: thesis: ((s `1 ) ^2 ) + ((s `2 ) ^2 ) = r ^2
then |.(s - (0. (TOP-REAL 2))).| = r by Th9;
then |.s.| = r by RLVECT_1:26;
hence ((s `1 ) ^2 ) + ((s `2 ) ^2 ) = r ^2 by JGRAPH_1:46; :: thesis: verum