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