assume not (LSeg (p1,p)) /\ (LSeg (p,p2)) c= {p} ; :: thesis: contradiction
then consider y being object such that
A4: y in (LSeg (p1,p)) /\ (LSeg (p,p2)) and
A5: not y in {p} ;
reconsider q = y as Point of (TOP-REAL n) by A4;
A6: q in LSeg (p1,p) by A4, XBOOLE_0:def 4;
then consider d being Real such that
A7: q = ((1 - d) * p1) + (d * p) and
0 <= d and
A8: d <= 1 ;
q in LSeg (p,p2) by A4, XBOOLE_0:def 4;
then consider e being Real such that
A9: q = ((1 - e) * p) + (e * p2) and
A10: 0 <= e and
e <= 1 ;
consider a being Real such that
A11: p = ((1 - a) * p1) + (a * p2) and
A12: 0 <= a and
A13: a <= 1 by A2;
A14: 1 - a >= 0 by A13, XREAL_1:48;
then d < 1 by A8, XXREAL_0:1;
then A15: 1 - d > 0 by XREAL_1:50;
then A16: (1 - d) * a > 0 by A12, A15, XREAL_1:129;
set f = ((1 - e) * a) + e;
q = (((1 - e) * ((1 - a) * p1)) + ((1 - e) * (a * p2))) + (e * p2) by A11, A9, RLVECT_1:def 5
.= ((((1 - e) * (1 - a)) * p1) + ((1 - e) * (a * p2))) + (e * p2) by RLVECT_1:def 7
.= ((((1 - e) * (1 - a)) * p1) + (((1 - e) * a) * p2)) + (e * p2) by RLVECT_1:def 7
.= (((1 - e) * (1 - a)) * p1) + ((((1 - e) * a) * p2) + (e * p2)) by RLVECT_1:def 3
.= (((1 - e) * (1 - a)) * p1) + ((((1 - e) * a) + e) * p2) by RLVECT_1:def 6 ;
then A17: p - q = ((((1 - a) * p1) + (a * p2)) - ((1 - (((1 - e) * a) + e)) * p1)) - ((((1 - e) * a) + e) * p2) by A11, RLVECT_1:27
.= ((((1 - a) * p1) - ((1 - (((1 - e) * a) + e)) * p1)) + (a * p2)) - ((((1 - e) * a) + e) * p2) by RLVECT_1:def 3
.= ((((1 - a) - (1 - (((1 - e) * a) + e))) * p1) + (a * p2)) - ((((1 - e) * a) + e) * p2) by RLVECT_1:35
.= ((((((1 - e) * a) + e) - a) * p1) - ((((1 - e) * a) + e) * p2)) + (a * p2) by RLVECT_1:def 3
.= (((((1 - e) * a) + e) - a) * p1) - (((((1 - e) * a) + e) * p2) - (a * p2)) by RLVECT_1:29
.= (((((1 - e) * a) + e) - a) * p1) - (((((1 - e) * a) + e) - a) * p2) by RLVECT_1:35
.= ((((1 - e) * a) + e) - a) * (p1 - p2) by RLVECT_1:34 ;
q = ((1 - d) * p1) + ((d * ((1 - a) * p1)) + (d * (a * p2))) by A11, A7, RLVECT_1:def 5
.= (((1 - d) * p1) + (d * ((1 - a) * p1))) + (d * (a * p2)) by RLVECT_1:def 3
.= (((1 - d) * p1) + ((d * (1 - a)) * p1)) + (d * (a * p2)) by RLVECT_1:def 7
.= (((1 - d) + (d * (1 - a))) * p1) + (d * (a * p2)) by RLVECT_1:def 6
.= ((1 - (d * a)) * p1) + ((d * a) * p2) by RLVECT_1:def 7 ;
then p - q = ((((1 - a) * p1) + (a * p2)) - ((1 - (d * a)) * p1)) - ((d * a) * p2) by A11, RLVECT_1:27
.= ((((1 - a) * p1) - ((1 - (d * a)) * p1)) + (a * p2)) - ((d * a) * p2) by RLVECT_1:def 3
.= ((((1 - a) - (1 - (d * a))) * p1) + (a * p2)) - ((d * a) * p2) by RLVECT_1:35
.= ((((d * a) - a) * p1) - ((d * a) * p2)) + (a * p2) by RLVECT_1:def 3
.= (((d * a) - a) * p1) - (((d * a) * p2) - (a * p2)) by RLVECT_1:29
.= (((d * a) - a) * p1) - (((d * a) - a) * p2) by RLVECT_1:35
.= ((d * a) - a) * (p1 - p2) by RLVECT_1:34 ;
then (((((1 - e) * a) + e) - a) * (p1 - p2)) - (((d * a) - a) * (p1 - p2)) = 0. (TOP-REAL n) by A17, RLVECT_1:5;
then (((((1 - e) * a) + e) - a) - ((d * a) - a)) * (p1 - p2) = 0. (TOP-REAL n) by RLVECT_1:35;
then A18: ( (((1 - e) * a) + e) - (d * a) = 0 or p1 - p2 = 0. (TOP-REAL n) ) by RLVECT_1:11;
(((1 - e) * a) + e) - (d * a) = ((1 - d) * a) + (e * (1 - a)) ;
then p1 = p2 by A10, A18, A16, A14, RLVECT_1:21;
then p in {p1} by A2, RLTOPSP1:70;
then p = p1 by TARSKI:def 1;
hence contradiction by A5, A6, RLTOPSP1:70; :: thesis: verum