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 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 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 A1: ( p = <*a*> & q = <*b*> & x = <*z*> ) ; :: thesis: ( ( z in [.a,b.] implies x in [.p,q.] ) & ( x in [.p,q.] implies ( ( a <= b implies z in [.a,b.] ) & ( a >= b implies z in [.b,a.] ) ) ) )
then A2: ( p = I . a & q = I . b & x = I . z & J . p = a & J . q = b & J . x = z ) by PDIFF_1:1;
thus ( z in [.a,b.] implies x in [.p,q.] ) :: thesis: ( x in [.p,q.] implies ( ( a <= b implies z in [.a,b.] ) & ( a >= b implies z in [.b,a.] ) ) )
proof
assume z in [.a,b.] ; :: thesis: x in [.p,q.]
then A5: ( a <= z & z <= b ) by XXREAL_1:1;
then A6: a <= b by XXREAL_0:2;
per cases ( a = b or a <> b ) ;
suppose Z1: a = b ; :: thesis: x in [.p,q.]
reconsider r = 0 as Real ;
Z2: z = ((1 - r) * a) + (r * b) by Z1, A5, XXREAL_0:1;
( (1 - r) * p = I . ((1 - r) * a) & r * q = I . (r * b) ) by A2, PDIFF_1:3;
then I . z = ((1 - r) * p) + (r * q) by Z2, PDIFF_1:3;
then x = ((1 - r) * p) + (r * q) by A1, PDIFF_1:1;
then x in { (((1 - r) * p) + (r * q)) where r is Real : ( 0 <= r & r <= 1 ) } ;
hence x in [.p,q.] by RLTOPSP1:def 2; :: thesis: verum
end;
suppose a <> b ; :: thesis: x in [.p,q.]
then X2: a < b by A6, XXREAL_0:1;
reconsider r = (z - a) / (b - a) as Real ;
A7: ( 0 <= z - a & 0 <= b - a ) by A5, A6, XREAL_1:48;
z - a <= b - a by A5, XREAL_1:13;
then C2: r <= 1 by A7, XREAL_1:185;
A8: 0 < b - a by X2, XREAL_1:50;
C3: ((1 - r) * a) + (r * b) = a + (((z - a) / (b - a)) * (b - a))
.= a + (z - a) by A8, XCMPLX_1:87 ;
( (1 - r) * p = I . ((1 - r) * a) & r * q = I . (r * b) ) by A2, PDIFF_1:3;
then ((1 - r) * p) + (r * q) = I . z by C3, PDIFF_1:3
.= x by A1, PDIFF_1:1 ;
then x in { (((1 - r) * p) + (r * q)) where r is Real : ( 0 <= r & r <= 1 ) } by A7, C2;
hence x in [.p,q.] by RLTOPSP1:def 2; :: thesis: verum
end;
end;
end;
assume x in [.p,q.] ; :: thesis: ( ( a <= b implies z in [.a,b.] ) & ( a >= b implies z in [.b,a.] ) )
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
B2: ( x = ((1 - r) * p) + (r * q) & 0 <= r & r <= 1 ) ;
B4: J . x = (J . ((1 - r) * p)) + (J . (r * q)) by B2, 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 ;
B5: now :: thesis: ( a <= b implies z in [.a,b.] )
assume a <= b ; :: thesis: z in [.a,b.]
then ( a <= z & z <= b ) by A2, XREAL_1:171, XREAL_1:172, B2, B4;
hence z in [.a,b.] ; :: thesis: verum
end;
now :: thesis: ( a >= b implies z in [.b,a.] )
assume B6: a >= b ; :: thesis: z in [.b,a.]
set s = 1 - r;
( 0 <= 1 - r & 1 - r <= 1 & J . x = ((1 - r) * (J . p)) + ((1 - (1 - r)) * (J . q)) ) by B2, B4, XREAL_1:43, XREAL_1:48;
then ( b <= z & z <= a ) by A2, XREAL_1:171, XREAL_1:172, B6;
hence z in [.b,a.] ; :: thesis: verum
end;
hence ( ( a <= b implies z in [.a,b.] ) & ( a >= b implies z in [.b,a.] ) ) by B5; :: thesis: verum