theorem Th2: :: JORDAN:2

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