theorem :: EUCLID_6:52

for n being Element of NAT
for q1 being Point of (TOP-REAL n) ex f being Function of (TOP-REAL n),R^1 st
( ( for q being Point of (TOP-REAL n) holds f . q = |.(q - q1).| ) & f is continuous ) by Lm21;