let p, q, p1 be Point of (TOP-REAL 2); ( p `2 <> q `2 & p1 in LSeg (p,q) & p1 `2 = p `2 implies p1 = p )
assume that
A1:
p `2 <> q `2
and
A2:
p1 in LSeg (p,q)
; ( not p1 `2 = p `2 or p1 = p )
assume A3:
p1 `2 = p `2
; p1 = p
assume A4:
p1 <> p
; contradiction
consider l1 being Real such that
A5:
p1 = ((1 - l1) * p) + (l1 * q)
and
0 <= l1
and
l1 <= 1
by A2;
A6:
((1 - l1) * p) + (l1 * q) = |[((((1 - l1) * p) `1) + ((l1 * q) `1)),((((1 - l1) * p) `2) + ((l1 * q) `2))]|
by EUCLID:55;
A7:
(1 - l1) * p = |[((1 - l1) * (p `1)),((1 - l1) * (p `2))]|
by EUCLID:57;
A8:
l1 * q = |[(l1 * (q `1)),(l1 * (q `2))]|
by EUCLID:57;
p `2 =
(((1 - l1) * p) `2) + ((l1 * q) `2)
by A3, A5, A6, EUCLID:52
.=
((1 - l1) * (p `2)) + ((l1 * q) `2)
by A7, EUCLID:52
.=
((1 - l1) * (p `2)) + (l1 * (q `2))
by A8, EUCLID:52
;
then
(1 - (1 - l1)) * (p `2) = l1 * (q `2)
;
then
l1 = 0
by A1, XCMPLX_1:5;
then p1 =
(1 * p) + (0. (TOP-REAL 2))
by A5, RLVECT_1:10
.=
p + (0. (TOP-REAL 2))
by RLVECT_1:def 8
.=
p
by RLVECT_1:4
;
hence
contradiction
by A4; verum