let a, b be Real; :: thesis: for p, q being Point of (REAL-NS 1)

for I being Function of REAL,(REAL-NS 1) st p = <*a*> & q = <*b*> & I = (proj (1,1)) " holds

( ( a <= b implies I .: [.a,b.] = [.p,q.] ) & ( a < b implies I .: ].a,b.[ = ].p,q.[ ) )

let p, q be Point of (REAL-NS 1); :: thesis: for I being Function of REAL,(REAL-NS 1) st p = <*a*> & q = <*b*> & I = (proj (1,1)) " holds

( ( a <= b implies I .: [.a,b.] = [.p,q.] ) & ( a < b implies I .: ].a,b.[ = ].p,q.[ ) )

let I be Function of REAL,(REAL-NS 1); :: thesis: ( p = <*a*> & q = <*b*> & I = (proj (1,1)) " implies ( ( a <= b implies I .: [.a,b.] = [.p,q.] ) & ( a < b implies I .: ].a,b.[ = ].p,q.[ ) ) )

assume that

A1: ( p = <*a*> & q = <*b*> ) and

A2: I = (proj (1,1)) " ; :: thesis: ( ( a <= b implies I .: [.a,b.] = [.p,q.] ) & ( a < b implies I .: ].a,b.[ = ].p,q.[ ) )

reconsider J = proj (1,1) as Function of (REAL-NS 1),REAL by Lm1;

A7: ( J . p = a & J . q = b ) by A1, PDIFF_1:1;

hence I .: ].a,b.[ = ].p,q.[ by B6, XBOOLE_0:def 10; :: thesis: verum

for I being Function of REAL,(REAL-NS 1) st p = <*a*> & q = <*b*> & I = (proj (1,1)) " holds

( ( a <= b implies I .: [.a,b.] = [.p,q.] ) & ( a < b implies I .: ].a,b.[ = ].p,q.[ ) )

let p, q be Point of (REAL-NS 1); :: thesis: for I being Function of REAL,(REAL-NS 1) st p = <*a*> & q = <*b*> & I = (proj (1,1)) " holds

( ( a <= b implies I .: [.a,b.] = [.p,q.] ) & ( a < b implies I .: ].a,b.[ = ].p,q.[ ) )

let I be Function of REAL,(REAL-NS 1); :: thesis: ( p = <*a*> & q = <*b*> & I = (proj (1,1)) " implies ( ( a <= b implies I .: [.a,b.] = [.p,q.] ) & ( a < b implies I .: ].a,b.[ = ].p,q.[ ) ) )

assume that

A1: ( p = <*a*> & q = <*b*> ) and

A2: I = (proj (1,1)) " ; :: thesis: ( ( a <= b implies I .: [.a,b.] = [.p,q.] ) & ( a < b implies I .: ].a,b.[ = ].p,q.[ ) )

hereby :: thesis: ( a < b implies I .: ].a,b.[ = ].p,q.[ )

assume X2:
a < b
; :: thesis: I .: ].a,b.[ = ].p,q.[assume X1:
a <= b
; :: thesis: I .: [.a,b.] = [.p,q.]

reconsider J = proj (1,1) as Function of (REAL-NS 1),REAL by Lm1;

A7: ( J . p = a & J . q = b ) by A1, PDIFF_1:1;

hence I .: [.a,b.] = [.p,q.] by A6, XBOOLE_0:def 10; :: thesis: verum

end;now :: thesis: for y being object st y in I .: [.a,b.] holds

y in [.p,q.]

then A6:
I .: [.a,b.] c= [.p,q.]
;y in [.p,q.]

let y be object ; :: thesis: ( y in I .: [.a,b.] implies y in [.p,q.] )

assume y in I .: [.a,b.] ; :: thesis: y in [.p,q.]

then consider x being object such that

A3: ( x in dom I & [x,y] in I & x in [.a,b.] ) by RELAT_1:110;

reconsider x = x as Element of REAL by A3;

I . x = <*x*> by A2, PDIFF_1:1;

then I . x in [.p,q.] by A1, A3, LM519C1;

hence y in [.p,q.] by A3, FUNCT_1:1; :: thesis: verum

end;assume y in I .: [.a,b.] ; :: thesis: y in [.p,q.]

then consider x being object such that

A3: ( x in dom I & [x,y] in I & x in [.a,b.] ) by RELAT_1:110;

reconsider x = x as Element of REAL by A3;

I . x = <*x*> by A2, PDIFF_1:1;

then I . x in [.p,q.] by A1, A3, LM519C1;

hence y in [.p,q.] by A3, FUNCT_1:1; :: thesis: verum

reconsider J = proj (1,1) as Function of (REAL-NS 1),REAL by Lm1;

A7: ( J . p = a & J . q = b ) by A1, PDIFF_1:1;

now :: thesis: for x being object st x in [.p,q.] holds

x in I .: [.a,b.]

then
[.p,q.] c= I .: [.a,b.]
;x in I .: [.a,b.]

let x be object ; :: thesis: ( x in [.p,q.] implies x in I .: [.a,b.] )

assume B0: x in [.p,q.] ; :: thesis: x in I .: [.a,b.]

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 ) ;

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 ;

then ( a <= J . x & J . x <= b ) by A7, X1, XREAL_1:171, XREAL_1:172, B2;

then B5: J . x in [.a,b.] ;

then reconsider z = J . x as Element of REAL ;

set z1 = I . z;

[z,(I . z)] in I by A2, PDIFF_1:2, FUNCT_1:1;

then B9: I . z in I .: [.a,b.] by B5, A2, PDIFF_1:2, RELAT_1:110;

I * J = id (rng I) by PDIFF_1:2, A2, Lm2, FUNCT_1:39;

then J = I " by A2, PDIFF_1:2, Lm2, FUNCT_1:42;

hence x in I .: [.a,b.] by B9, FUNCT_1:35, Lm1, A2, PDIFF_1:2, B0; :: thesis: verum

end;assume B0: x in [.p,q.] ; :: thesis: x in I .: [.a,b.]

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 ) ;

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 ;

then ( a <= J . x & J . x <= b ) by A7, X1, XREAL_1:171, XREAL_1:172, B2;

then B5: J . x in [.a,b.] ;

then reconsider z = J . x as Element of REAL ;

set z1 = I . z;

[z,(I . z)] in I by A2, PDIFF_1:2, FUNCT_1:1;

then B9: I . z in I .: [.a,b.] by B5, A2, PDIFF_1:2, RELAT_1:110;

I * J = id (rng I) by PDIFF_1:2, A2, Lm2, FUNCT_1:39;

then J = I " by A2, PDIFF_1:2, Lm2, FUNCT_1:42;

hence x in I .: [.a,b.] by B9, FUNCT_1:35, Lm1, A2, PDIFF_1:2, B0; :: thesis: verum

hence I .: [.a,b.] = [.p,q.] by A6, XBOOLE_0:def 10; :: thesis: verum

now :: thesis: for y being object st y in I .: ].a,b.[ holds

y in ].p,q.[

then B6:
I .: ].a,b.[ c= ].p,q.[
;y in ].p,q.[

let y be object ; :: thesis: ( y in I .: ].a,b.[ implies y in ].p,q.[ )

assume y in I .: ].a,b.[ ; :: thesis: y in ].p,q.[

then consider x being object such that

B3: ( x in dom I & [x,y] in I & x in ].a,b.[ ) by RELAT_1:110;

reconsider x = x as Element of REAL by B3;

I . x = <*x*> by A2, PDIFF_1:1;

then I . x in ].p,q.[ by A1, B3, LM519B1;

hence y in ].p,q.[ by B3, FUNCT_1:1; :: thesis: verum

end;assume y in I .: ].a,b.[ ; :: thesis: y in ].p,q.[

then consider x being object such that

B3: ( x in dom I & [x,y] in I & x in ].a,b.[ ) by RELAT_1:110;

reconsider x = x as Element of REAL by B3;

I . x = <*x*> by A2, PDIFF_1:1;

then I . x in ].p,q.[ by A1, B3, LM519B1;

hence y in ].p,q.[ by B3, FUNCT_1:1; :: thesis: verum

reconsider J = proj (1,1) as Function of (REAL-NS 1),REAL by Lm1;

A7: ( J . p = a & J . q = b ) by A1, PDIFF_1:1;

now :: thesis: for x being object st x in ].p,q.[ holds

x in I .: ].a,b.[

then
].p,q.[ c= I .: ].a,b.[
;x in I .: ].a,b.[

let x be object ; :: thesis: ( x in ].p,q.[ implies x in I .: ].a,b.[ )

assume B0: x in ].p,q.[ ; :: thesis: x in I .: ].a,b.[

then B0c: ( x in [.p,q.] & not x in {p,q} ) by XBOOLE_0:def 5;

then B0b: ( x <> p & x <> q ) by TARSKI:def 2;

x in { (((1 - r) * p) + (r * q)) where r is Real : ( 0 <= r & r <= 1 ) } by B0c, RLTOPSP1:def 2;

then consider r being Real such that

B1: ( x = ((1 - r) * p) + (r * q) & 0 <= r & r <= 1 ) ;

.= ((1 - r) * (J . p)) + (J . (r * q)) by PDIFF_1:4

.= ((1 - r) * (J . p)) + (r * (J . q)) by PDIFF_1:4 ;

then ( a < J . x & J . x < b ) by A7, X2, XREAL_1:177, XREAL_1:178, B1a, B1, B1b;

then B5: J . x in ].a,b.[ ;

then reconsider z = J . x as Element of REAL ;

set z1 = I . z;

B91: [z,(I . z)] in I by A2, PDIFF_1:2, FUNCT_1:1;

B11: rng I = the carrier of (REAL-NS 1) by A2, REAL_NS1:def 4, PDIFF_1:2;

I * J = id (rng I) by PDIFF_1:2, A2, Lm2, FUNCT_1:39;

then B14: J = I " by A2, PDIFF_1:2, Lm2, FUNCT_1:42;

x = I . (J . x) by A2, B14, FUNCT_1:35, B11, B0;

hence x in I .: ].a,b.[ by B91, B5, A2, PDIFF_1:2, RELAT_1:110; :: thesis: verum

end;assume B0: x in ].p,q.[ ; :: thesis: x in I .: ].a,b.[

then B0c: ( x in [.p,q.] & not x in {p,q} ) by XBOOLE_0:def 5;

then B0b: ( x <> p & x <> q ) by TARSKI:def 2;

x in { (((1 - r) * p) + (r * q)) where r is Real : ( 0 <= r & r <= 1 ) } by B0c, RLTOPSP1:def 2;

then consider r being Real such that

B1: ( x = ((1 - r) * p) + (r * q) & 0 <= r & r <= 1 ) ;

now :: thesis: not r = 1

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

then x = (0. (REAL-NS 1)) + (1 * q) by B1, RLVECT_1:10;

hence contradiction by B0b, RLVECT_1:def 8; :: thesis: verum

end;then x = (0. (REAL-NS 1)) + (1 * q) by B1, RLVECT_1:10;

hence contradiction by B0b, RLVECT_1:def 8; :: thesis: verum

B1b: now :: thesis: not r = 0

J . x =
(J . ((1 - r) * p)) + (J . (r * q))
by B1, PDIFF_1:4
assume
r = 0
; :: thesis: contradiction

then x = (1 * p) + (0. (REAL-NS 1)) by B1, RLVECT_1:10;

hence contradiction by B0b, RLVECT_1:def 8; :: thesis: verum

end;then x = (1 * p) + (0. (REAL-NS 1)) by B1, RLVECT_1:10;

hence contradiction by B0b, RLVECT_1:def 8; :: thesis: verum

.= ((1 - r) * (J . p)) + (J . (r * q)) by PDIFF_1:4

.= ((1 - r) * (J . p)) + (r * (J . q)) by PDIFF_1:4 ;

then ( a < J . x & J . x < b ) by A7, X2, XREAL_1:177, XREAL_1:178, B1a, B1, B1b;

then B5: J . x in ].a,b.[ ;

then reconsider z = J . x as Element of REAL ;

set z1 = I . z;

B91: [z,(I . z)] in I by A2, PDIFF_1:2, FUNCT_1:1;

B11: rng I = the carrier of (REAL-NS 1) by A2, REAL_NS1:def 4, PDIFF_1:2;

I * J = id (rng I) by PDIFF_1:2, A2, Lm2, FUNCT_1:39;

then B14: J = I " by A2, PDIFF_1:2, Lm2, FUNCT_1:42;

x = I . (J . x) by A2, B14, FUNCT_1:35, B11, B0;

hence x in I .: ].a,b.[ by B91, B5, A2, PDIFF_1:2, RELAT_1:110; :: thesis: verum

hence I .: ].a,b.[ = ].p,q.[ by B6, XBOOLE_0:def 10; :: thesis: verum