theorem Th38: :: BORSUK_7:48

for r being Real
for p being Point of (TOP-REAL 3)
for e being Point of (Euclid 3) st p = e & p `3 = 0 holds
product ((1,2,3) --> (].((p `1) - (r / (sqrt 2))),((p `1) + (r / (sqrt 2))).[,].((p `2) - (r / (sqrt 2))),((p `2) + (r / (sqrt 2))).[,{0})) c= Ball (e,r)