let a, b, z be Real; 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); ( 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*> )
; ( ( 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.] )
( 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.]
;
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
a <> b
;
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;
verum end; end;
end;
assume
x in [.p,q.]
; ( ( 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
;
hence
( ( a <= b implies z in [.a,b.] ) & ( a >= b implies z in [.b,a.] ) )
by B5; verum