theorem Th20: :: EUCLID:23

for n being Nat
for p being Point of (TOP-REAL n) holds p is Function of (Seg n),REAL