theorem Th17: :: SPRECT_2:17

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