reconsider e = x as Point of (Euclid n) by TOPREAL3:8;

per cases ( r = 0 or r > 0 ) ;

suppose r = 0 ; :: thesis: not Sphere (x,r) is empty

then Sphere (e,r) = {e} by TOPREAL6:54;
hence not Sphere (x,r) is empty by Th13; :: thesis: verum

end;

suppose r > 0 ; :: thesis: not Sphere (x,r) is empty

then reconsider r = r as positive Real ;
consider s being Point of (TOP-REAL n) such that
A1: s in Ball (x,r) by SUBSET_1:4;
reconsider S = s, T = s + (1.REAL n), XX = x as Element of REAL n by EUCLID:22;
set a = ((- (2 * |(((s + (1.REAL n)) - s),(s - x))|)) + (sqrt (delta ((Sum (sqr (T - S))),(2 * |(((s + (1.REAL n)) - s),(s - x))|),((Sum (sqr (S - XX))) - (r ^2)))))) / (2 * (Sum (sqr (T - S))));
s <> s + (1.REAL n) by Th1;
then ex e being Point of (TOP-REAL n) st
( {e} = (halfline (s,(s + (1.REAL n)))) /\ (Sphere (x,r)) & e = ((1 - (((- (2 * |(((s + (1.REAL n)) - s),(s - x))|)) + (sqrt (delta ((Sum (sqr (T - S))),(2 * |(((s + (1.REAL n)) - s),(s - x))|),((Sum (sqr (S - XX))) - (r ^2)))))) / (2 * (Sum (sqr (T - S)))))) * s) + ((((- (2 * |(((s + (1.REAL n)) - s),(s - x))|)) + (sqrt (delta ((Sum (sqr (T - S))),(2 * |(((s + (1.REAL n)) - s),(s - x))|),((Sum (sqr (S - XX))) - (r ^2)))))) / (2 * (Sum (sqr (T - S))))) * (s + (1.REAL n))) ) by A1, Th35;
hence not Sphere (x,r) is empty ; :: thesis: verum

end;

end;