let P, Q be Element of (TOP-REAL 2); for r being Real holds
( P in Sphere (Q,r) iff P in circle ((Q . 1),(Q . 2),r) )
let r be Real; ( P in Sphere (Q,r) iff P in circle ((Q . 1),(Q . 2),r) )
hereby ( P in circle ((Q . 1),(Q . 2),r) implies P in Sphere (Q,r) )
assume
P in Sphere (
Q,
r)
;
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;
verum
end;
assume
P in circle ((Q . 1),(Q . 2),r)
; 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; verum