let P, Q be Subset of (TOP-REAL 2); :: thesis: for p1, p2 being Point of (TOP-REAL 2) st P is_an_arc_of p1,p2 & P meets Q & P /\ Q is closed holds

( First_Point (P,p1,p2,Q) = Last_Point (P,p2,p1,Q) & Last_Point (P,p1,p2,Q) = First_Point (P,p2,p1,Q) )

let p1, p2 be Point of (TOP-REAL 2); :: thesis: ( P is_an_arc_of p1,p2 & P meets Q & P /\ Q is closed implies ( First_Point (P,p1,p2,Q) = Last_Point (P,p2,p1,Q) & Last_Point (P,p1,p2,Q) = First_Point (P,p2,p1,Q) ) )

assume that

A1: P is_an_arc_of p1,p2 and

A2: P /\ Q <> {} and

A3: P /\ Q is closed ; :: according to XBOOLE_0:def 7 :: thesis: ( First_Point (P,p1,p2,Q) = Last_Point (P,p2,p1,Q) & Last_Point (P,p1,p2,Q) = First_Point (P,p2,p1,Q) )

reconsider P = P as non empty Subset of (TOP-REAL 2) by A2;

A4: P meets Q by A2;

A5: P is_an_arc_of p2,p1 by A1, JORDAN5B:14;

A6: for g being Function of I[01],((TOP-REAL 2) | P)

for s2 being Real st g is being_homeomorphism & g . 0 = p1 & g . 1 = p2 & g . s2 = Last_Point (P,p2,p1,Q) & 0 <= s2 & s2 <= 1 holds

for t being Real st 0 <= t & t < s2 holds

not g . t in Q

for s2 being Real st g is being_homeomorphism & g . 0 = p1 & g . 1 = p2 & g . s2 = First_Point (P,p2,p1,Q) & 0 <= s2 & s2 <= 1 holds

for t being Real st 1 >= t & t > s2 holds

not g . t in Q

hence ( First_Point (P,p1,p2,Q) = Last_Point (P,p2,p1,Q) & Last_Point (P,p1,p2,Q) = First_Point (P,p2,p1,Q) ) by A1, A3, A4, A6, A27, Def1, Def2; :: thesis: verum

( First_Point (P,p1,p2,Q) = Last_Point (P,p2,p1,Q) & Last_Point (P,p1,p2,Q) = First_Point (P,p2,p1,Q) )

let p1, p2 be Point of (TOP-REAL 2); :: thesis: ( P is_an_arc_of p1,p2 & P meets Q & P /\ Q is closed implies ( First_Point (P,p1,p2,Q) = Last_Point (P,p2,p1,Q) & Last_Point (P,p1,p2,Q) = First_Point (P,p2,p1,Q) ) )

assume that

A1: P is_an_arc_of p1,p2 and

A2: P /\ Q <> {} and

A3: P /\ Q is closed ; :: according to XBOOLE_0:def 7 :: thesis: ( First_Point (P,p1,p2,Q) = Last_Point (P,p2,p1,Q) & Last_Point (P,p1,p2,Q) = First_Point (P,p2,p1,Q) )

reconsider P = P as non empty Subset of (TOP-REAL 2) by A2;

A4: P meets Q by A2;

A5: P is_an_arc_of p2,p1 by A1, JORDAN5B:14;

A6: for g being Function of I[01],((TOP-REAL 2) | P)

for s2 being Real st g is being_homeomorphism & g . 0 = p1 & g . 1 = p2 & g . s2 = Last_Point (P,p2,p1,Q) & 0 <= s2 & s2 <= 1 holds

for t being Real st 0 <= t & t < s2 holds

not g . t in Q

proof

A27:
for g being Function of I[01],((TOP-REAL 2) | P)
set Ex = L[01] (((0,1) (#)),((#) (0,1)));

let f be Function of I[01],((TOP-REAL 2) | P); :: thesis: for s2 being Real st f is being_homeomorphism & f . 0 = p1 & f . 1 = p2 & f . s2 = Last_Point (P,p2,p1,Q) & 0 <= s2 & s2 <= 1 holds

for t being Real st 0 <= t & t < s2 holds

not f . t in Q

let s2 be Real; :: thesis: ( f is being_homeomorphism & f . 0 = p1 & f . 1 = p2 & f . s2 = Last_Point (P,p2,p1,Q) & 0 <= s2 & s2 <= 1 implies for t being Real st 0 <= t & t < s2 holds

not f . t in Q )

assume that

A7: f is being_homeomorphism and

A8: f . 0 = p1 and

A9: f . 1 = p2 and

A10: f . s2 = Last_Point (P,p2,p1,Q) and

A11: 0 <= s2 and

A12: s2 <= 1 ; :: thesis: for t being Real st 0 <= t & t < s2 holds

not f . t in Q

set s21 = 1 - s2;

set g = f * (L[01] (((0,1) (#)),((#) (0,1))));

A13: L[01] (((0,1) (#)),((#) (0,1))) is being_homeomorphism by TREAL_1:18;

dom f = [#] I[01] by A7, TOPS_2:def 5;

then rng (L[01] (((0,1) (#)),((#) (0,1)))) = dom f by A13, TOPMETR:20, TOPS_2:def 5;

then dom (f * (L[01] (((0,1) (#)),((#) (0,1))))) = dom (L[01] (((0,1) (#)),((#) (0,1)))) by RELAT_1:27;

then A14: dom (f * (L[01] (((0,1) (#)),((#) (0,1))))) = [#] I[01] by A13, TOPMETR:20, TOPS_2:def 5;

reconsider g = f * (L[01] (((0,1) (#)),((#) (0,1)))) as Function of I[01],((TOP-REAL 2) | P) by TOPMETR:20;

A15: ( 1 - 1 <= 1 - s2 & 1 - s2 <= 1 - 0 ) by A11, A12, XREAL_1:13;

then A16: 1 - s2 in dom g by A14, BORSUK_1:43;

(L[01] (((0,1) (#)),((#) (0,1)))) . ((#) (0,1)) = 1 by BORSUK_1:def 15, TREAL_1:5, TREAL_1:9;

then A17: g . 0 = p2 by A9, A14, BORSUK_1:def 14, FUNCT_1:12, TREAL_1:5;

(L[01] (((0,1) (#)),((#) (0,1)))) . ((0,1) (#)) = 0 by BORSUK_1:def 14, TREAL_1:5, TREAL_1:9;

then A18: g . 1 = p1 by A8, A14, BORSUK_1:def 15, FUNCT_1:12, TREAL_1:5;

let t be Real; :: thesis: ( 0 <= t & t < s2 implies not f . t in Q )

assume that

A19: 0 <= t and

A20: t < s2 ; :: thesis: not f . t in Q

A21: 1 - t <= 1 - 0 by A19, XREAL_1:13;

t <= 1 by A12, A20, XXREAL_0:2;

then A22: 1 - 1 <= 1 - t by XREAL_1:13;

then reconsider r2 = 1 - s2, t9 = 1 - t as Point of (Closed-Interval-TSpace (0,1)) by A15, A21, BORSUK_1:43, TOPMETR:20;

A23: 1 - t in dom g by A14, A22, A21, BORSUK_1:43;

(L[01] (((0,1) (#)),((#) (0,1)))) . r2 = ((1 - (1 - s2)) * 1) + ((1 - s2) * 0) by BORSUK_1:def 14, BORSUK_1:def 15, TREAL_1:5, TREAL_1:def 3

.= s2 ;

then A24: g . (1 - s2) = f . s2 by A16, FUNCT_1:12;

(L[01] (((0,1) (#)),((#) (0,1)))) . t9 = ((1 - (1 - t)) * 1) + ((1 - t) * 0) by BORSUK_1:def 14, BORSUK_1:def 15, TREAL_1:5, TREAL_1:def 3

.= t ;

then A25: g . t9 = f . t by A23, FUNCT_1:12;

A26: 1 - s2 < 1 - t by A20, XREAL_1:15;

g is being_homeomorphism by A7, A13, TOPMETR:20, TOPS_2:57;

hence not f . t in Q by A3, A5, A4, A10, A17, A18, A15, A21, A24, A25, A26, Def2; :: thesis: verum

end;let f be Function of I[01],((TOP-REAL 2) | P); :: thesis: for s2 being Real st f is being_homeomorphism & f . 0 = p1 & f . 1 = p2 & f . s2 = Last_Point (P,p2,p1,Q) & 0 <= s2 & s2 <= 1 holds

for t being Real st 0 <= t & t < s2 holds

not f . t in Q

let s2 be Real; :: thesis: ( f is being_homeomorphism & f . 0 = p1 & f . 1 = p2 & f . s2 = Last_Point (P,p2,p1,Q) & 0 <= s2 & s2 <= 1 implies for t being Real st 0 <= t & t < s2 holds

not f . t in Q )

assume that

A7: f is being_homeomorphism and

A8: f . 0 = p1 and

A9: f . 1 = p2 and

A10: f . s2 = Last_Point (P,p2,p1,Q) and

A11: 0 <= s2 and

A12: s2 <= 1 ; :: thesis: for t being Real st 0 <= t & t < s2 holds

not f . t in Q

set s21 = 1 - s2;

set g = f * (L[01] (((0,1) (#)),((#) (0,1))));

A13: L[01] (((0,1) (#)),((#) (0,1))) is being_homeomorphism by TREAL_1:18;

dom f = [#] I[01] by A7, TOPS_2:def 5;

then rng (L[01] (((0,1) (#)),((#) (0,1)))) = dom f by A13, TOPMETR:20, TOPS_2:def 5;

then dom (f * (L[01] (((0,1) (#)),((#) (0,1))))) = dom (L[01] (((0,1) (#)),((#) (0,1)))) by RELAT_1:27;

then A14: dom (f * (L[01] (((0,1) (#)),((#) (0,1))))) = [#] I[01] by A13, TOPMETR:20, TOPS_2:def 5;

reconsider g = f * (L[01] (((0,1) (#)),((#) (0,1)))) as Function of I[01],((TOP-REAL 2) | P) by TOPMETR:20;

A15: ( 1 - 1 <= 1 - s2 & 1 - s2 <= 1 - 0 ) by A11, A12, XREAL_1:13;

then A16: 1 - s2 in dom g by A14, BORSUK_1:43;

(L[01] (((0,1) (#)),((#) (0,1)))) . ((#) (0,1)) = 1 by BORSUK_1:def 15, TREAL_1:5, TREAL_1:9;

then A17: g . 0 = p2 by A9, A14, BORSUK_1:def 14, FUNCT_1:12, TREAL_1:5;

(L[01] (((0,1) (#)),((#) (0,1)))) . ((0,1) (#)) = 0 by BORSUK_1:def 14, TREAL_1:5, TREAL_1:9;

then A18: g . 1 = p1 by A8, A14, BORSUK_1:def 15, FUNCT_1:12, TREAL_1:5;

let t be Real; :: thesis: ( 0 <= t & t < s2 implies not f . t in Q )

assume that

A19: 0 <= t and

A20: t < s2 ; :: thesis: not f . t in Q

A21: 1 - t <= 1 - 0 by A19, XREAL_1:13;

t <= 1 by A12, A20, XXREAL_0:2;

then A22: 1 - 1 <= 1 - t by XREAL_1:13;

then reconsider r2 = 1 - s2, t9 = 1 - t as Point of (Closed-Interval-TSpace (0,1)) by A15, A21, BORSUK_1:43, TOPMETR:20;

A23: 1 - t in dom g by A14, A22, A21, BORSUK_1:43;

(L[01] (((0,1) (#)),((#) (0,1)))) . r2 = ((1 - (1 - s2)) * 1) + ((1 - s2) * 0) by BORSUK_1:def 14, BORSUK_1:def 15, TREAL_1:5, TREAL_1:def 3

.= s2 ;

then A24: g . (1 - s2) = f . s2 by A16, FUNCT_1:12;

(L[01] (((0,1) (#)),((#) (0,1)))) . t9 = ((1 - (1 - t)) * 1) + ((1 - t) * 0) by BORSUK_1:def 14, BORSUK_1:def 15, TREAL_1:5, TREAL_1:def 3

.= t ;

then A25: g . t9 = f . t by A23, FUNCT_1:12;

A26: 1 - s2 < 1 - t by A20, XREAL_1:15;

g is being_homeomorphism by A7, A13, TOPMETR:20, TOPS_2:57;

hence not f . t in Q by A3, A5, A4, A10, A17, A18, A15, A21, A24, A25, A26, Def2; :: thesis: verum

for s2 being Real st g is being_homeomorphism & g . 0 = p1 & g . 1 = p2 & g . s2 = First_Point (P,p2,p1,Q) & 0 <= s2 & s2 <= 1 holds

for t being Real st 1 >= t & t > s2 holds

not g . t in Q

proof

( Last_Point (P,p2,p1,Q) in P /\ Q & First_Point (P,p2,p1,Q) in P /\ Q )
by A3, A5, A4, Def1, Def2;
set Ex = L[01] (((0,1) (#)),((#) (0,1)));

let f be Function of I[01],((TOP-REAL 2) | P); :: thesis: for s2 being Real st f is being_homeomorphism & f . 0 = p1 & f . 1 = p2 & f . s2 = First_Point (P,p2,p1,Q) & 0 <= s2 & s2 <= 1 holds

for t being Real st 1 >= t & t > s2 holds

not f . t in Q

let s2 be Real; :: thesis: ( f is being_homeomorphism & f . 0 = p1 & f . 1 = p2 & f . s2 = First_Point (P,p2,p1,Q) & 0 <= s2 & s2 <= 1 implies for t being Real st 1 >= t & t > s2 holds

not f . t in Q )

assume that

A28: f is being_homeomorphism and

A29: f . 0 = p1 and

A30: f . 1 = p2 and

A31: f . s2 = First_Point (P,p2,p1,Q) and

A32: 0 <= s2 and

A33: s2 <= 1 ; :: thesis: for t being Real st 1 >= t & t > s2 holds

not f . t in Q

set g = f * (L[01] (((0,1) (#)),((#) (0,1))));

A34: L[01] (((0,1) (#)),((#) (0,1))) is being_homeomorphism by TREAL_1:18;

dom f = [#] I[01] by A28, TOPS_2:def 5;

then rng (L[01] (((0,1) (#)),((#) (0,1)))) = dom f by A34, TOPMETR:20, TOPS_2:def 5;

then dom (f * (L[01] (((0,1) (#)),((#) (0,1))))) = dom (L[01] (((0,1) (#)),((#) (0,1)))) by RELAT_1:27;

then A35: dom (f * (L[01] (((0,1) (#)),((#) (0,1))))) = [#] I[01] by A34, TOPMETR:20, TOPS_2:def 5;

let t be Real; :: thesis: ( 1 >= t & t > s2 implies not f . t in Q )

assume that

A36: 1 >= t and

A37: t > s2 ; :: thesis: not f . t in Q

A38: 1 - s2 > 1 - t by A37, XREAL_1:15;

set s21 = 1 - s2;

A39: 1 - s2 <= 1 - 0 by A32, XREAL_1:13;

reconsider g = f * (L[01] (((0,1) (#)),((#) (0,1)))) as Function of I[01],((TOP-REAL 2) | P) by TOPMETR:20;

A40: 1 - 1 <= 1 - t by A36, XREAL_1:13;

A41: 1 - t <= 1 - 0 by A32, A37, XREAL_1:13;

then A42: 1 - t in dom g by A35, A40, BORSUK_1:43;

A43: 1 - 1 <= 1 - s2 by A33, XREAL_1:13;

then A44: 1 - s2 in dom g by A35, A39, BORSUK_1:43;

reconsider r2 = 1 - s2, t9 = 1 - t as Point of (Closed-Interval-TSpace (0,1)) by A43, A39, A40, A41, BORSUK_1:43, TOPMETR:20;

(L[01] (((0,1) (#)),((#) (0,1)))) . r2 = ((1 - (1 - s2)) * 1) + ((1 - s2) * 0) by BORSUK_1:def 14, BORSUK_1:def 15, TREAL_1:5, TREAL_1:def 3

.= s2 ;

then A45: g . (1 - s2) = f . s2 by A44, FUNCT_1:12;

(L[01] (((0,1) (#)),((#) (0,1)))) . t9 = ((1 - (1 - t)) * 1) + ((1 - t) * 0) by BORSUK_1:def 14, BORSUK_1:def 15, TREAL_1:5, TREAL_1:def 3

.= t ;

then A46: g . t9 = f . t by A42, FUNCT_1:12;

(L[01] (((0,1) (#)),((#) (0,1)))) . ((#) (0,1)) = 1 by BORSUK_1:def 15, TREAL_1:5, TREAL_1:9;

then A47: g . 0 = p2 by A30, A35, BORSUK_1:def 14, FUNCT_1:12, TREAL_1:5;

(L[01] (((0,1) (#)),((#) (0,1)))) . ((0,1) (#)) = 0 by BORSUK_1:def 14, TREAL_1:5, TREAL_1:9;

then A48: g . 1 = p1 by A29, A35, BORSUK_1:def 15, FUNCT_1:12, TREAL_1:5;

g is being_homeomorphism by A28, A34, TOPMETR:20, TOPS_2:57;

hence not f . t in Q by A3, A5, A4, A31, A47, A48, A39, A40, A45, A46, A38, Def1; :: thesis: verum

end;let f be Function of I[01],((TOP-REAL 2) | P); :: thesis: for s2 being Real st f is being_homeomorphism & f . 0 = p1 & f . 1 = p2 & f . s2 = First_Point (P,p2,p1,Q) & 0 <= s2 & s2 <= 1 holds

for t being Real st 1 >= t & t > s2 holds

not f . t in Q

let s2 be Real; :: thesis: ( f is being_homeomorphism & f . 0 = p1 & f . 1 = p2 & f . s2 = First_Point (P,p2,p1,Q) & 0 <= s2 & s2 <= 1 implies for t being Real st 1 >= t & t > s2 holds

not f . t in Q )

assume that

A28: f is being_homeomorphism and

A29: f . 0 = p1 and

A30: f . 1 = p2 and

A31: f . s2 = First_Point (P,p2,p1,Q) and

A32: 0 <= s2 and

A33: s2 <= 1 ; :: thesis: for t being Real st 1 >= t & t > s2 holds

not f . t in Q

set g = f * (L[01] (((0,1) (#)),((#) (0,1))));

A34: L[01] (((0,1) (#)),((#) (0,1))) is being_homeomorphism by TREAL_1:18;

dom f = [#] I[01] by A28, TOPS_2:def 5;

then rng (L[01] (((0,1) (#)),((#) (0,1)))) = dom f by A34, TOPMETR:20, TOPS_2:def 5;

then dom (f * (L[01] (((0,1) (#)),((#) (0,1))))) = dom (L[01] (((0,1) (#)),((#) (0,1)))) by RELAT_1:27;

then A35: dom (f * (L[01] (((0,1) (#)),((#) (0,1))))) = [#] I[01] by A34, TOPMETR:20, TOPS_2:def 5;

let t be Real; :: thesis: ( 1 >= t & t > s2 implies not f . t in Q )

assume that

A36: 1 >= t and

A37: t > s2 ; :: thesis: not f . t in Q

A38: 1 - s2 > 1 - t by A37, XREAL_1:15;

set s21 = 1 - s2;

A39: 1 - s2 <= 1 - 0 by A32, XREAL_1:13;

reconsider g = f * (L[01] (((0,1) (#)),((#) (0,1)))) as Function of I[01],((TOP-REAL 2) | P) by TOPMETR:20;

A40: 1 - 1 <= 1 - t by A36, XREAL_1:13;

A41: 1 - t <= 1 - 0 by A32, A37, XREAL_1:13;

then A42: 1 - t in dom g by A35, A40, BORSUK_1:43;

A43: 1 - 1 <= 1 - s2 by A33, XREAL_1:13;

then A44: 1 - s2 in dom g by A35, A39, BORSUK_1:43;

reconsider r2 = 1 - s2, t9 = 1 - t as Point of (Closed-Interval-TSpace (0,1)) by A43, A39, A40, A41, BORSUK_1:43, TOPMETR:20;

(L[01] (((0,1) (#)),((#) (0,1)))) . r2 = ((1 - (1 - s2)) * 1) + ((1 - s2) * 0) by BORSUK_1:def 14, BORSUK_1:def 15, TREAL_1:5, TREAL_1:def 3

.= s2 ;

then A45: g . (1 - s2) = f . s2 by A44, FUNCT_1:12;

(L[01] (((0,1) (#)),((#) (0,1)))) . t9 = ((1 - (1 - t)) * 1) + ((1 - t) * 0) by BORSUK_1:def 14, BORSUK_1:def 15, TREAL_1:5, TREAL_1:def 3

.= t ;

then A46: g . t9 = f . t by A42, FUNCT_1:12;

(L[01] (((0,1) (#)),((#) (0,1)))) . ((#) (0,1)) = 1 by BORSUK_1:def 15, TREAL_1:5, TREAL_1:9;

then A47: g . 0 = p2 by A30, A35, BORSUK_1:def 14, FUNCT_1:12, TREAL_1:5;

(L[01] (((0,1) (#)),((#) (0,1)))) . ((0,1) (#)) = 0 by BORSUK_1:def 14, TREAL_1:5, TREAL_1:9;

then A48: g . 1 = p1 by A29, A35, BORSUK_1:def 15, FUNCT_1:12, TREAL_1:5;

g is being_homeomorphism by A28, A34, TOPMETR:20, TOPS_2:57;

hence not f . t in Q by A3, A5, A4, A31, A47, A48, A39, A40, A45, A46, A38, Def1; :: thesis: verum

hence ( First_Point (P,p1,p2,Q) = Last_Point (P,p2,p1,Q) & Last_Point (P,p1,p2,Q) = First_Point (P,p2,p1,Q) ) by A1, A3, A4, A6, A27, Def1, Def2; :: thesis: verum