theorem Th1: :: EUCLID_5:1

for p being Point of (TOP-REAL 3) ex x, y, z being Real st p = <*x,y,z*>