theorem Th22: :: JORDAN1K:22
for p, q being Point of (TOP-REAL 2) st p <> q holds
dist (p,q) > 0