let a, b, z be Real; :: thesis:
let p, q, x be Point of (REAL-NS 1); :: thesis:
reconsider I = (proj (1,1)) " as Function of REAL,(REAL 1) by PDIFF_1:2;
reconsider J = proj (1,1) as Function of (REAL-NS 1),REAL by Lm1;
assume P2: ( p = <*a*> & q = <*b*> & x = <*z*> ) ; :: thesis:
A2: ( I . a = p & I . b = q & I . z = x & J . p = a & J . q = b & J . x = z ) by P2, PDIFF_1:1;

assume z in ].a,b.[ ; :: thesis:
then A4: ( a < z & z < b ) by XXREAL_1:4;
then A5: a < b by XXREAL_0:2;
reconsider r = (z - a) / (b - a) as Real ;
A6: ( 0 < z - a & 0 < b - a & z - a < b - a ) by A4, A5, XREAL_1:14, XREAL_1:50;
then C1: ( 0 < r & r < 1 ) by XREAL_1:139, XREAL_1:191;
C3: ((1 - r) * a) + (r * b) = a + (((z - a) / (b - a)) * (b - a))
.= a + (z - a) by A6, XCMPLX_1:87 ;
q - p = I . (b - a) by A2, PDIFF_1:3;
then r * (q - p) = I . (r * (b - a)) by PDIFF_1:3;
then p + (r * (q - p)) = x by A2, C3, PDIFF_1:3;
then x in { (p + (t * (q - p))) where t is Real : ( 0 < t & t < 1 ) } by C1;
hence x in ].p,q.[ by A4, P2, FINSEQ_1:76, NDIFF_5:16; :: thesis:

end;

assume x in ].p,q.[ ; :: thesis:
then X1: ( x in [.p,q.] & not x in {p,q} ) by XBOOLE_0:def 5;
then x in { (((1 - r) * p) + (r * q)) where r is Real : ( 0 <= r & r <= 1 ) } by RLTOPSP1:def 2;
then consider r being Real such that
B1: ( x = ((1 - r) * p) + (r * q) & 0 <= r & r <= 1 ) ;
B2: J . x = (J . ((1 - r) * p)) + (J . (r * q)) by B1, PDIFF_1:4
.= ((1 - r) * (J . p)) + (J . (r * q)) by PDIFF_1:4
.= ((1 - r) * (J . p)) + (r * (J . q)) by PDIFF_1:4 ;
hence a <> b by A2, X1, TARSKI:def 2; :: thesis:

end;

end;

then X4: r < 1 by B1, XXREAL_0:1;
set s = 1 - r;
X5: ( r = 1 - (1 - r) & 0 < 1 - r & 1 - r < 1 ) by X3, B1, X4, XREAL_1:44, XREAL_1:50;

end;