let P, Q be Subset of (TOP-REAL 2); :: thesis:
let p1, p2 be Point of (TOP-REAL 2); :: thesis:
assume that
A1: P meets Q and
A2: P /\ Q is closed and
A3: P is_an_arc_of p1,p2 ; :: thesis:
P /\ Q <> {} by A1;
then reconsider P = P as non empty Subset of (TOP-REAL 2) ;
consider f being Function of I[01],((TOP-REAL 2) | P) such that
A4: f is being_homeomorphism and
A5: ( f . 0 = p1 & f . 1 = p2 ) by A3, TOPREAL1:def 1;
A6: f is one-to-one by A4, TOPS_2:def 5;
[#] ((TOP-REAL 2) | P) = P by PRE_TOPC:def 5;
then reconsider PQ = P /\ Q as non empty Subset of ((TOP-REAL 2) | P) by A1, XBOOLE_1:17;
reconsider P1 = P, Q1 = Q as non empty Subset of (TOP-REAL 2) by A1;
consider OO being object such that
A7: OO in PQ by XBOOLE_0:def 1;
reconsider PP = P as Subset of (TOP-REAL 2) ;
PP is compact by A3, Th1;
then A8: P /\ Q is compact by A2, COMPTS_1:9, XBOOLE_1:17;
PQ <> {} ((TOP-REAL 2) | P) ;
then reconsider PQ1 = P /\ Q as non empty Subset of ((TOP-REAL 2) | P1) ;
(TOP-REAL 2) | (P1 /\ Q1) = ((TOP-REAL 2) | P1) | PQ1 by GOBOARD9:2;
then A9: PQ is compact by A8, COMPTS_1:3;
set g = f " ;
reconsider g1 = f " as Function ;
A10: rng f = [#] ((TOP-REAL 2) | P) by A4, TOPS_2:def 5;
A11: f " is one-to-one by A10, A6, TOPS_2:50;
f " is being_homeomorphism by A4, TOPS_2:56;
then rng (f ") = [#] I[01] by TOPS_2:def 5;
then f " is onto by FUNCT_2:def 3;
then (f ") " = g1 " by A11, TOPS_2:def 4;
then A12: f = g1 " by A10, A6, TOPS_2:51;
[#] I[01] c= [#] R^1 by PRE_TOPC:def 4;
then reconsider GPQ = (f ") .: PQ as Subset of R^1 by XBOOLE_1:1;
f " is continuous by A4, TOPS_2:def 5;
then ( (f ") .: PQ c= [#] I[01] & ( for P being Subset of I[01] st P = GPQ holds
P is compact ) ) by A9, WEIERSTR:8;
then A13: GPQ is compact by COMPTS_1:2;
then A14: [#] GPQ is real-bounded by WEIERSTR:11;
set Ex = upper_bound ([#] GPQ);
reconsider f1 = f as Function ;
take f . (upper_bound ([#] GPQ)) ; :: thesis:
A15: dom (f ") = the carrier of ((TOP-REAL 2) | P) by FUNCT_2:def 1;
dom (f ") = the carrier of ((TOP-REAL 2) | P) by FUNCT_2:def 1;
then (f ") . OO in GPQ by A7, FUNCT_1:def 6;
then [#] GPQ <> {} by WEIERSTR:def 1;
then upper_bound ([#] GPQ) in [#] GPQ by A13, A14, RCOMP_1:12, WEIERSTR:12;
then A16: upper_bound ([#] GPQ) in GPQ by WEIERSTR:def 1;
then A17: 0 <= upper_bound ([#] GPQ) by BORSUK_1:43;
A18: dom f = the carrier of I[01] by FUNCT_2:def 1;
A19: for t being Real st 1 >= t & t > upper_bound ([#] GPQ) holds
not f . t in Q

proof

let t be Real; :: thesis:
assume that
A20: 1 >= t and
A21: t > upper_bound ([#] GPQ) ; :: thesis:
t in the carrier of I[01] by A17, A20, A21, BORSUK_1:43;
then f . t in the carrier of ((TOP-REAL 2) | P) by FUNCT_2:5;
then A22: f . t in P by PRE_TOPC:8;
f is onto by A10, FUNCT_2:def 3;
then A23: f " = f1 " by A6, TOPS_2:def 4;
assume f . t in Q ; :: thesis:
then f . t in PQ by A22, XBOOLE_0:def 4;
then A24: (f ") . (f . t) in GPQ by A15, FUNCT_1:def 6;
t in dom f by A18, A17, A20, A21, BORSUK_1:43;
then (f ") . (f . t) = t by A6, A23, FUNCT_1:34;
then t in [#] GPQ by A24, WEIERSTR:def 1;
hence contradiction by A14, A21, SEQ_4:def 1; :: thesis:

end;

A25: ( ex pq being object st
( pq in dom (f ") & pq in PQ & upper_bound ([#] GPQ) = (f ") . pq ) & upper_bound ([#] GPQ) <= 1 ) by A16, BORSUK_1:43, FUNCT_1:def 6;
f " is one-to-one by A10, A6, TOPS_2:50;
hence ( f . (upper_bound ([#] GPQ)) is Point of (TOP-REAL 2) & f . (upper_bound ([#] GPQ)) in P /\ Q & ex g being Function of I[01],((TOP-REAL 2) | P) ex s2 being Real st
( g is being_homeomorphism & g . 0 = p1 & g . 1 = p2 & g . s2 = f . (upper_bound ([#] GPQ)) & 0 <= s2 & s2 <= 1 & ( for t being Real st 1 >= t & t > s2 holds
not g . t in Q ) ) ) by A4, A5, A12, A17, A25, A19, FUNCT_1:34; :: thesis: