A1: n in NAT by ORDINAL1:def 13;
reconsider e = x as Point of (Euclid n) by TOPREAL3:13;

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

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

then Sphere e,r = {e} by TOPREAL6:62;
hence not Sphere x,r is empty by A1, Th15; :: thesis: verum

end;

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

then reconsider r = r as real positive number ;
consider s being Point of (TOP-REAL n) such that
A2: s in Ball x,r by SUBSET_1:10;
reconsider S = s, T = s + (1.REAL n), XX = x as Element of REAL n by EUCLID:25;
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 A1, Th3;
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, A2, Th37;
hence not Sphere x,r is empty ; :: thesis: verum

end;

end;