let P, Q be Element of (TOP-REAL 2); :: thesis: for r being Real holds
( P in Sphere (Q,r) iff P in circle ((Q . 1),(Q . 2),r) )
let r be Real; :: thesis: ( P in Sphere (Q,r) iff P in circle ((Q . 1),(Q . 2),r) )

hereby :: thesis: ( P in circle ((Q . 1),(Q . 2),r) implies P in Sphere (Q,r) )

assume P in Sphere (Q,r) ; :: thesis: P in circle ((Q . 1),(Q . 2),r)
then P in Sphere (|[(Q `1),(Q `2)]|,r) by EUCLID:53;
then P in Sphere (|[(Q . 1),(Q `2)]|,r) by EUCLID:def 9;
then P in Sphere (|[(Q . 1),(Q . 2)]|,r) by EUCLID:def 10;
hence P in circle ((Q . 1),(Q . 2),r) by TOPREAL9:52; :: thesis: verum

end;

assume P in circle ((Q . 1),(Q . 2),r) ; :: thesis: P in Sphere (Q,r)
then P in Sphere (|[(Q . 1),(Q . 2)]|,r) by TOPREAL9:52;
then P in Sphere (|[(Q `1),(Q . 2)]|,r) by EUCLID:def 9;
then P in Sphere (|[(Q `1),(Q `2)]|,r) by EUCLID:def 10;
hence P in Sphere (Q,r) by EUCLID:53; :: thesis: verum