let a, b, z be Real; :: thesis: for p, q, x being Point of (REAL-NS 1) 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 (REAL-NS 1); :: 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-NS 1),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 P2, PDIFF_1:1;

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: ( ( a < b implies z in ].a,b.[ ) & ( a > b implies z in ].b,a.[ ) )

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;

then ( b < z & z < a ) by A2, X5, XREAL_1:177, XREAL_1:178, B2;

hence z in ].b,a.[ ; :: thesis: verum

( ( 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 (REAL-NS 1); :: 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-NS 1),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 P2, PDIFF_1:1;

hereby :: thesis: ( x in ].p,q.[ implies ( a <> b & ( a < b implies z in ].a,b.[ ) & ( a > b implies z in ].b,a.[ ) ) )

assume
x in ].p,q.[
; :: thesis: ( 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 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: verum

end;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: verum

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: ( ( 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 B1, RLVECT_1:def 8

.= p + (0. (REAL-NS 1)) by RLVECT_1:10 ;

hence contradiction by X1, TARSKI:def 2; :: thesis: verum

end;then x = p + (0 * q) by B1, RLVECT_1:def 8

.= p + (0. (REAL-NS 1)) by RLVECT_1:10 ;

hence contradiction by X1, TARSKI:def 2; :: thesis: verum

now :: thesis: not r = 1

then X4:
r < 1
by B1, XXREAL_0:1;assume
r = 1
; :: thesis: contradiction

then x = (0 * p) + q by B1, RLVECT_1:def 8

.= (0. (REAL-NS 1)) + q by RLVECT_1:10 ;

hence contradiction by X1, TARSKI:def 2; :: thesis: verum

end;then x = (0 * p) + q by B1, RLVECT_1:def 8

.= (0. (REAL-NS 1)) + q by RLVECT_1:10 ;

hence contradiction by X1, TARSKI:def 2; :: thesis: verum

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;

hereby :: thesis: ( a > b implies z in ].b,a.[ )

assume
a > b
; :: thesis: z in ].b,a.[assume
a < b
; :: thesis: z in ].a,b.[

then ( a < z & z < b ) by A2, X3, B1, X4, XREAL_1:177, XREAL_1:178, B2;

hence z in ].a,b.[ ; :: thesis: verum

end;then ( a < z & z < b ) by A2, X3, B1, X4, XREAL_1:177, XREAL_1:178, B2;

hence z in ].a,b.[ ; :: thesis: verum

then ( b < z & z < a ) by A2, X5, XREAL_1:177, XREAL_1:178, B2;

hence z in ].b,a.[ ; :: thesis: verum