let n be Element of NAT ; :: thesis: for p1, p2, q1, q2 being Point of (TOP-REAL n) st LSeg q1,q2 c= LSeg p1,p2 & p1 in LSeg q1,q2 & not p1 = q1 holds
p1 = q2
let p1, p2, q1, q2 be Point of (TOP-REAL n); :: thesis: ( LSeg q1,q2 c= LSeg p1,p2 & p1 in LSeg q1,q2 & not p1 = q1 implies p1 = q2 )
assume A1: LSeg q1,q2 c= LSeg p1,p2 ; :: thesis: ( not p1 in LSeg q1,q2 or p1 = q1 or p1 = q2 )
assume p1 in LSeg q1,q2 ; :: thesis: ( p1 = q1 or p1 = q2 )
then consider r1 being Real such that
A2: ( p1 = ((1 - r1) * q1) + (r1 * q2) & 0 <= r1 & r1 <= 1 ) ;
A3: ( q1 in LSeg q1,q2 & q2 in LSeg q1,q2 ) by RLTOPSP1:69;
then q1 in LSeg p1,p2 by A1;
then consider s1 being Real such that
A4: ( q1 = ((1 - s1) * p1) + (s1 * p2) & 0 <= s1 & s1 <= 1 ) ;
q2 in LSeg p1,p2 by A1, A3;
then consider s2 being Real such that
A5: ( q2 = ((1 - s2) * p1) + (s2 * p2) & 0 <= s2 & s2 <= 1 ) ;
p1 = ((1 - r1) * (((1 - s1) * p1) + (s1 * p2))) + ((r1 * ((1 - s2) * p1)) + (r1 * (s2 * p2))) by A2, A4, A5, EUCLID:36
.= (((1 - r1) * ((1 - s1) * p1)) + ((1 - r1) * (s1 * p2))) + ((r1 * ((1 - s2) * p1)) + (r1 * (s2 * p2))) by EUCLID:36
.= ((((1 - r1) * ((1 - s1) * p1)) + ((1 - r1) * (s1 * p2))) + (r1 * ((1 - s2) * p1))) + (r1 * (s2 * p2)) by EUCLID:30
.= (((((1 - r1) * (1 - s1)) * p1) + ((1 - r1) * (s1 * p2))) + (r1 * ((1 - s2) * p1))) + (r1 * (s2 * p2)) by EUCLID:34
.= (((((1 - r1) * (1 - s1)) * p1) + (((1 - r1) * s1) * p2)) + (r1 * ((1 - s2) * p1))) + (r1 * (s2 * p2)) by EUCLID:34
.= (((((1 - r1) * (1 - s1)) * p1) + (((1 - r1) * s1) * p2)) + ((r1 * (1 - s2)) * p1)) + (r1 * (s2 * p2)) by EUCLID:34
.= (((((1 - r1) * (1 - s1)) * p1) + (((1 - r1) * s1) * p2)) + ((r1 * (1 - s2)) * p1)) + ((r1 * s2) * p2) by EUCLID:34
.= (((r1 * s2) * p2) + ((((1 - r1) * s1) * p2) + (((1 - r1) * (1 - s1)) * p1))) + ((r1 * (1 - s2)) * p1) by EUCLID:30
.= ((((r1 * s2) * p2) + (((1 - r1) * s1) * p2)) + (((1 - r1) * (1 - s1)) * p1)) + ((r1 * (1 - s2)) * p1) by EUCLID:30
.= ((((r1 * s2) + ((1 - r1) * s1)) * p2) + (((1 - r1) * (1 - s1)) * p1)) + ((r1 * (1 - s2)) * p1) by EUCLID:37
.= (((r1 * s2) + ((1 - r1) * s1)) * p2) + ((((1 - r1) * (1 - s1)) * p1) + ((r1 * (1 - s2)) * p1)) by EUCLID:30
.= (((r1 * s2) + ((1 - r1) * s1)) * p2) + ((((1 - r1) * (1 - s1)) + (r1 * (1 - s2))) * p1) by EUCLID:37 ;
then 0. (TOP-REAL n) = ((((r1 * s2) + ((1 - r1) * s1)) * p2) + ((((1 - r1) * (1 - s1)) + (r1 * (1 - s2))) * p1)) - p1 by EUCLID:46
.= (((r1 * s2) + ((1 - r1) * s1)) * p2) + (((((1 - r1) * (1 - s1)) + (r1 * (1 - s2))) * p1) - p1) by EUCLID:49
.= (((r1 * s2) + ((1 - r1) * s1)) * p2) + (((((1 - r1) * (1 - s1)) + (r1 * (1 - s2))) * p1) - (1 * p1)) by EUCLID:33
.= (((((1 - r1) * (1 - s1)) + (r1 * (1 - s2))) - 1) * p1) + (((r1 * s2) + ((1 - r1) * s1)) * p2) by EUCLID:54
.= (((((1 - r1) * (1 - s1)) + (r1 * (1 - s2))) - 1) * p1) - (- (((r1 * s2) + ((1 - r1) * s1)) * p2)) by EUCLID:39 ;
then ((((1 - r1) * (1 - s1)) + (r1 * (1 - s2))) - 1) * p1 = - (((r1 * s2) + ((1 - r1) * s1)) * p2) by EUCLID:47;
then ((((1 - r1) * (1 - s1)) + (r1 * (1 - s2))) - 1) * p1 = (- ((r1 * s2) + ((1 - r1) * s1))) * p2 by EUCLID:44;
then A6: ( - ((r1 * s2) + ((1 - r1) * s1)) = - 0 or p1 = p2 ) by EUCLID:38;

per cases ( (r1 * s2) + ((1 - r1) * s1) = 0 or p1 = p2 ) by A6;

suppose A7: (r1 * s2) + ((1 - r1) * s1) = 0 ; :: thesis: ( p1 = q1 or p1 = q2 )

now

per cases ( ( r1 = 0 & s1 = 0 ) or ( r1 = 1 & s2 = 0 ) or ( s2 = 0 & s1 = 0 ) ) by A2, A4, A5, A7, XREAL_1:172;

suppose ( r1 = 0 & s1 = 0 ) ; :: thesis: ( p1 = q1 or p1 = q2 )

then p1 = (1 * q1) + (0. (TOP-REAL n)) by A2, EUCLID:33
.= q1 + (0. (TOP-REAL n)) by EUCLID:33
.= q1 by EUCLID:31 ;
hence ( p1 = q1 or p1 = q2 ) ; :: thesis: verum

end;

suppose ( r1 = 1 & s2 = 0 ) ; :: thesis: ( p1 = q1 or p1 = q2 )

then p1 = (0. (TOP-REAL n)) + (1 * q2) by A2, EUCLID:33
.= 1 * q2 by EUCLID:31
.= q2 by EUCLID:33 ;
hence ( p1 = q1 or p1 = q2 ) ; :: thesis: verum

end;

suppose ( s2 = 0 & s1 = 0 ) ; :: thesis: ( p1 = q1 or p1 = q2 )

then q1 = (1 * p1) + (0. (TOP-REAL n)) by A4, EUCLID:33
.= p1 + (0. (TOP-REAL n)) by EUCLID:33
.= p1 by EUCLID:31 ;
hence ( p1 = q1 or p1 = q2 ) ; :: thesis: verum

end;

end;

end;

hence ( p1 = q1 or p1 = q2 ) ; :: thesis: verum

end;

suppose p1 = p2 ; :: thesis: ( p1 = q1 or p1 = q2 )

then LSeg q1,q2 c= {p1} by A1, RLTOPSP1:71;
hence ( p1 = q1 or p1 = q2 ) by A3, TARSKI:def 1; :: thesis: verum

end;

end;