let n be 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 )
q2 in LSeg (q1,q2) by RLTOPSP1:68;
then q2 in LSeg (p1,p2) by A1;
then consider s2 being Real such that
A2: q2 = ((1 - s2) * p1) + (s2 * p2) and
A3: 0 <= s2 and
s2 <= 1 ;
assume p1 in LSeg (q1,q2) ; :: thesis: ( p1 = q1 or p1 = q2 )
then consider r1 being Real such that
A4: p1 = ((1 - r1) * q1) + (r1 * q2) and
A5: ( 0 <= r1 & r1 <= 1 ) ;
A6: q1 in LSeg (q1,q2) by RLTOPSP1:68;
then q1 in LSeg (p1,p2) by A1;
then consider s1 being Real such that
A7: q1 = ((1 - s1) * p1) + (s1 * p2) and
A8: 0 <= s1 and
s1 <= 1 ;
p1 = ((1 - r1) * (((1 - s1) * p1) + (s1 * p2))) + ((r1 * ((1 - s2) * p1)) + (r1 * (s2 * p2))) by A4, A7, A2, RLVECT_1:def 5
.= (((1 - r1) * ((1 - s1) * p1)) + ((1 - r1) * (s1 * p2))) + ((r1 * ((1 - s2) * p1)) + (r1 * (s2 * p2))) by RLVECT_1:def 5
.= ((((1 - r1) * ((1 - s1) * p1)) + ((1 - r1) * (s1 * p2))) + (r1 * ((1 - s2) * p1))) + (r1 * (s2 * p2)) by RLVECT_1:def 3
.= (((((1 - r1) * (1 - s1)) * p1) + ((1 - r1) * (s1 * p2))) + (r1 * ((1 - s2) * p1))) + (r1 * (s2 * p2)) by RLVECT_1:def 7
.= (((((1 - r1) * (1 - s1)) * p1) + (((1 - r1) * s1) * p2)) + (r1 * ((1 - s2) * p1))) + (r1 * (s2 * p2)) by RLVECT_1:def 7
.= (((((1 - r1) * (1 - s1)) * p1) + (((1 - r1) * s1) * p2)) + ((r1 * (1 - s2)) * p1)) + (r1 * (s2 * p2)) by RLVECT_1:def 7
.= (((((1 - r1) * (1 - s1)) * p1) + (((1 - r1) * s1) * p2)) + ((r1 * (1 - s2)) * p1)) + ((r1 * s2) * p2) by RLVECT_1:def 7
.= (((r1 * s2) * p2) + ((((1 - r1) * s1) * p2) + (((1 - r1) * (1 - s1)) * p1))) + ((r1 * (1 - s2)) * p1) by RLVECT_1:def 3
.= ((((r1 * s2) * p2) + (((1 - r1) * s1) * p2)) + (((1 - r1) * (1 - s1)) * p1)) + ((r1 * (1 - s2)) * p1) by RLVECT_1:def 3
.= ((((r1 * s2) + ((1 - r1) * s1)) * p2) + (((1 - r1) * (1 - s1)) * p1)) + ((r1 * (1 - s2)) * p1) by RLVECT_1:def 6
.= (((r1 * s2) + ((1 - r1) * s1)) * p2) + ((((1 - r1) * (1 - s1)) * p1) + ((r1 * (1 - s2)) * p1)) by RLVECT_1:def 3
.= (((r1 * s2) + ((1 - r1) * s1)) * p2) + ((((1 - r1) * (1 - s1)) + (r1 * (1 - s2))) * p1) by RLVECT_1:def 6 ;
then 0. (TOP-REAL n) = ((((r1 * s2) + ((1 - r1) * s1)) * p2) + ((((1 - r1) * (1 - s1)) + (r1 * (1 - s2))) * p1)) - p1 by RLVECT_1:5
.= (((r1 * s2) + ((1 - r1) * s1)) * p2) + (((((1 - r1) * (1 - s1)) + (r1 * (1 - s2))) * p1) - p1) by RLVECT_1:def 3
.= (((r1 * s2) + ((1 - r1) * s1)) * p2) + (((((1 - r1) * (1 - s1)) + (r1 * (1 - s2))) * p1) - (1 * p1)) by RLVECT_1:def 8
.= (((((1 - r1) * (1 - s1)) + (r1 * (1 - s2))) - 1) * p1) + (((r1 * s2) + ((1 - r1) * s1)) * p2) by RLVECT_1:35
.= (((((1 - r1) * (1 - s1)) + (r1 * (1 - s2))) - 1) * p1) - (- (((r1 * s2) + ((1 - r1) * s1)) * p2)) ;
then ((((1 - r1) * (1 - s1)) + (r1 * (1 - s2))) - 1) * p1 = - (((r1 * s2) + ((1 - r1) * s1)) * p2) by RLVECT_1:21;
then ((((1 - r1) * (1 - s1)) + (r1 * (1 - s2))) - 1) * p1 = (- ((r1 * s2) + ((1 - r1) * s1))) * p2 by RLVECT_1:79;
then A9: ( - ((r1 * s2) + ((1 - r1) * s1)) = - 0 or p1 = p2 ) by RLVECT_1:36;

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

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

now :: thesis: ( p1 = q1 or p1 = q2 )

per cases ( ( r1 = 0 & s1 = 0 ) or ( r1 = 1 & s2 = 0 ) or ( s2 = 0 & s1 = 0 ) ) by A5, A8, A3, A10, XREAL_1:170;

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

then p1 = (1 * q1) + (0. (TOP-REAL n)) by A4, RLVECT_1:10
.= q1 + (0. (TOP-REAL n)) by RLVECT_1:def 8
.= q1 by RLVECT_1:4 ;
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 A4, RLVECT_1:10
.= 1 * q2 by RLVECT_1:4
.= q2 by RLVECT_1:def 8 ;
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 A7, RLVECT_1:10
.= p1 + (0. (TOP-REAL n)) by RLVECT_1:def 8
.= p1 by RLVECT_1:4 ;
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:70;
hence ( p1 = q1 or p1 = q2 ) by A6, TARSKI:def 1; :: thesis: verum

end;

end;