theorem Th3: :: JORDAN:3

for p1, p2 being Point of (TOP-REAL 2) st p1 `2 < p2 `2 holds
((1 / 2) * (p1 + p2)) `2 < p2 `2