let P, Q be Subset of (TOP-REAL 2); :: thesis:
let p1, p2 be Point of (TOP-REAL 2); :: thesis:
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:
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

set Ex = L[01] (((0,1) (#)),((#) (0,1)));
let f be Function of I[01],((TOP-REAL 2) | P); :: thesis:
let s2 be Real; :: thesis:
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:
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:
assume that
A19: 0 <= t and
A20: t < s2 ; :: thesis:
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:

end;

A27: 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 = 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

set Ex = L[01] (((0,1) (#)),((#) (0,1)));
let f be Function of I[01],((TOP-REAL 2) | P); :: thesis:
let s2 be Real; :: thesis:
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:
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:
assume that
A36: 1 >= t and
A37: t > s2 ; :: thesis:
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:

end;

( Last_Point (P,p2,p1,Q) in P /\ Q & First_Point (P,p2,p1,Q) in P /\ Q ) by A3, A5, A4, Def1, Def2;
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: