let A, B, C be 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 )
let p, q, r be Element of (Euclid 2); ( 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 )
; ( A in LSeg (B,C) iff p is_between q,r )
hereby ( p is_between q,r implies A in LSeg (B,C) )
assume A3:
A in LSeg (
B,
C)
;
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;
verum
end;
assume
p is_between q,r
; 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; verum