theorem Th11: :: EUCLID12:13

for A, B, C being Point of (TOP-REAL 2)
for p, q, r being Element of (Euclid 2) st p,q,r are_mutually_distinct & p = A & q = B & r = C holds
( A in LSeg (B,C) iff p is_between q,r )