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:59;
A7:
(1 - l1) * p = |[((1 - l1) * (p `1 )),((1 - l1) * (p `2 ))]|
by EUCLID:61;
A8:
l1 * q = |[(l1 * (q `1 )),(l1 * (q `2 ))]|
by EUCLID:61;
p `2 =
(((1 - l1) * p) `2 ) + ((l1 * q) `2 )
by A3, A5, A6, EUCLID:56
.=
((1 - l1) * (p `2 )) + ((l1 * q) `2 )
by A7, EUCLID:56
.=
((1 - l1) * (p `2 )) + (l1 * (q `2 ))
by A8, EUCLID:56
;
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, EUCLID:33
.=
p + (0. (TOP-REAL 2))
by EUCLID:33
.=
p
by EUCLID:31
;
hence
contradiction
by A4; verum