theorem Th20: :: SPRECT_2:20

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 )