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 )

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

( 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
p is_between q,r
; :: thesis: 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;( 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

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