theorem Th18: :: SPRECT_2:18

for a, b, c being Point of (TOP-REAL 2) st b in LSeg (a,c) & a `2 <= b `2 & c `2 <= b `2 & not a = b & not b = c holds
( a `2 = b `2 & c `2 = b `2 )