let p1, p2, p3, p be Point of (TOP-REAL 2); ( p in LSeg (p1,p2) & p <> p2 implies ( |((p3 - p),(p2 - p1))| = 0 iff |((p3 - p),(p2 - p))| = 0 ) )
assume
p in LSeg (p1,p2)
; ( not p <> p2 or ( |((p3 - p),(p2 - p1))| = 0 iff |((p3 - p),(p2 - p))| = 0 ) )
then
p in LSeg (p2,p1)
;
then consider l being Real such that
A1:
p = ((1 - l) * p2) + (l * p1)
and
0 <= l
and
l <= 1
;
assume A2:
p <> p2
; ( |((p3 - p),(p2 - p1))| = 0 iff |((p3 - p),(p2 - p))| = 0 )
A3: p2 - p =
(p2 - ((1 - l) * p2)) - (l * p1)
by A1, RLVECT_1:27
.=
(p2 - ((1 * p2) - (l * p2))) - (l * p1)
by RLVECT_1:35
.=
(p2 - (p2 - (l * p2))) - (l * p1)
by RLVECT_1:def 8
.=
((p2 - p2) + (l * p2)) - (l * p1)
by RLVECT_1:29
.=
((0. (TOP-REAL 2)) + (l * p2)) - (l * p1)
by RLVECT_1:5
.=
(l * p2) - (l * p1)
by RLVECT_1:4
.=
l * (p2 - p1)
by RLVECT_1:34
;
assume
|((p3 - p),(p2 - p))| = 0
; |((p3 - p),(p2 - p1))| = 0
then A5:
l * |((p3 - p),(p2 - p1))| = 0
by A3, EUCLID_2:20;