let A, B, C be Point of (TOP-REAL 2); :: thesis: 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 )
let p, q, r be Element of (Euclid 2); :: thesis: ( p,q,r are_mutually_distinct & p = A & q = B & r = C implies ( A in LSeg (B,C) iff p is_between q,r ) )
assume that
A1: p,q,r are_mutually_distinct and
A2: ( p = A & q = B & r = C ) ; :: thesis: ( A in LSeg (B,C) iff p is_between q,r )

hereby :: thesis: ( p is_between q,r implies A in LSeg (B,C) )

assume A3: A in LSeg (B,C) ; :: thesis: p is_between q,r
( dist (B,C) = dist (q,r) & dist (B,A) = dist (q,p) & dist (A,C) = dist (p,r) ) by A2, TOPREAL6:def 1;
then dist (q,r) = (dist (q,p)) + (dist (p,r)) by A3, Th10;
hence p is_between q,r by A1, METRIC_1:def 22; :: thesis: verum

end;

assume p is_between q,r ; :: thesis: A in LSeg (B,C)
then A4: dist (q,r) = (dist (q,p)) + (dist (p,r)) by METRIC_1:def 22;
( dist (q,r) = |.(B - C).| & dist (q,p) = |.(B - A).| & dist (p,r) = |.(A - C).| ) by A2, SPPOL_1:39;
hence A in LSeg (B,C) by A4, Th9; :: thesis: verum