theorem Th39: :: ANPROJ_8:45

for p, q being Point of (TOP-REAL 3) holds |(p,(q <X> p))| = 0