let p, q, p1 be Point of (TOP-REAL 2); :: thesis: ( p `1 <> q `1 & p1 in LSeg p,q & p1 `1 = p `1 implies p1 = p )
assume A1: ( p `1 <> q `1 & p1 in LSeg p,q ) ; :: thesis: ( not p1 `1 = p `1 or p1 = p )
assume A2: p1 `1 = p `1 ; :: thesis: p1 = p
assume A3: p1 <> p ; :: thesis: contradiction
p1 in { (((1 - l) * p) + (l * q)) where l is Real : ( 0 <= l & l <= 1 ) } by A1;
then consider l1 being Real such that
A4: ( p1 = ((1 - l1) * p) + (l1 * q) & 0 <= l1 & l1 <= 1 ) ;
A5: ((1 - l1) * p) + (l1 * q) = |[((((1 - l1) * p) `1 ) + ((l1 * q) `1 )),((((1 - l1) * p) `2 ) + ((l1 * q) `2 ))]| by EUCLID:59;
A6: ( (1 - l1) * p = |[((1 - l1) * (p `1 )),((1 - l1) * (p `2 ))]| & l1 * q = |[(l1 * (q `1 )),(l1 * (q `2 ))]| ) by EUCLID:61;
p `1 = (((1 - l1) * p) `1 ) + ((l1 * q) `1 ) by A2, A4, A5, EUCLID:56
.= ((1 - l1) * (p `1 )) + ((l1 * q) `1 ) by A6, EUCLID:56
.= ((1 - l1) * (p `1 )) + (l1 * (q `1 )) by A6, EUCLID:56 ;
then (1 - (1 - l1)) * (p `1 ) = l1 * (q `1 ) ;
then l1 = 0 by A1, XCMPLX_1:5;
then p1 = (1 * p) + (0. (TOP-REAL 2)) by A4, EUCLID:33
.= p + (0. (TOP-REAL 2)) by EUCLID:33
.= p by EUCLID:31 ;
hence contradiction by A3; :: thesis: verum