let a, b, z be Real; :: thesis: for p, q, x being Point of () st p = <*a*> & q = <*b*> & x = <*z*> holds
( ( z in ].a,b.[ implies x in ].p,q.[ ) & ( x in ].p,q.[ implies ( a <> b & ( a < b implies z in ].a,b.[ ) & ( a > b implies z in ].b,a.[ ) ) ) )

let p, q, x be Point of (); :: thesis: ( p = <*a*> & q = <*b*> & x = <*z*> implies ( ( z in ].a,b.[ implies x in ].p,q.[ ) & ( x in ].p,q.[ implies ( a <> b & ( a < b implies z in ].a,b.[ ) & ( a > b implies z in ].b,a.[ ) ) ) ) )
reconsider I = (proj (1,1)) " as Function of REAL,(REAL 1) by PDIFF_1:2;
reconsider J = proj (1,1) as Function of (),REAL by Lm1;
assume P2: ( p = <*a*> & q = <*b*> & x = <*z*> ) ; :: thesis: ( ( z in ].a,b.[ implies x in ].p,q.[ ) & ( x in ].p,q.[ implies ( a <> b & ( a < b implies z in ].a,b.[ ) & ( a > b implies z in ].b,a.[ ) ) ) )
A2: ( I . a = p & I . b = q & I . z = x & J . p = a & J . q = b & J . x = z ) by ;
hereby :: thesis: ( x in ].p,q.[ implies ( a <> b & ( a < b implies z in ].a,b.[ ) & ( a > b implies z in ].b,a.[ ) ) )
assume z in ].a,b.[ ; :: thesis: x in ].p,q.[
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 ;
then C1: ( 0 < r & r < 1 ) by ;
C3: ((1 - r) * a) + (r * b) = a + (((z - a) / (b - a)) * (b - a))
.= a + (z - a) by ;
q - p = I . (b - a) by ;
then r * (q - p) = I . (r * (b - a)) by PDIFF_1:3;
then p + (r * (q - p)) = x by ;
then x in { (p + (t * (q - p))) where t is Real : ( 0 < t & t < 1 ) } by C1;
hence x in ].p,q.[ by ; :: thesis: verum
end;
assume x in ].p,q.[ ; :: thesis: ( a <> b & ( a < b implies z in ].a,b.[ ) & ( a > b implies z in ].b,a.[ ) )
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
.= ((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 ; :: thesis: ( ( a < b implies z in ].a,b.[ ) & ( a > b implies z in ].b,a.[ ) )
X3: now :: thesis: not r = 0
assume r = 0 ; :: thesis: contradiction
then x = p + (0 * q) by
.= p + (0. ()) by RLVECT_1:10 ;
hence contradiction by X1, TARSKI:def 2; :: thesis: verum
end;
now :: thesis: not r = 1
assume r = 1 ; :: thesis: contradiction
then x = (0 * p) + q by
.= (0. ()) + q by RLVECT_1:10 ;
hence contradiction by X1, TARSKI:def 2; :: thesis: verum
end;
then X4: r < 1 by ;
set s = 1 - r;
X5: ( r = 1 - (1 - r) & 0 < 1 - r & 1 - r < 1 ) by ;
hereby :: thesis: ( a > b implies z in ].b,a.[ )
assume a < b ; :: thesis: z in ].a,b.[
then ( a < z & z < b ) by ;
hence z in ].a,b.[ ; :: thesis: verum
end;
assume a > b ; :: thesis: z in ].b,a.[
then ( b < z & z < a ) by ;
hence z in ].b,a.[ ; :: thesis: verum