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;
[#] 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 A11: GPQ is compact by COMPTS_1:2;
then A12: [#] GPQ is real-bounded by WEIERSTR:11;
set Ex = lower_bound ([#] GPQ);
reconsider f1 = f as Function ;
take f . (lower_bound ([#] GPQ)) ; :: thesis:
A13: 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 lower_bound ([#] GPQ) in [#] GPQ by A11, A12, RCOMP_1:13, WEIERSTR:12;
then A14: lower_bound ([#] GPQ) in GPQ by WEIERSTR:def 1;
then A15: lower_bound ([#] GPQ) <= 1 by BORSUK_1:43;
A16: dom f = the carrier of I[01] by FUNCT_2:def 1;
A17: for t being Real st 0 <= t & t < lower_bound ([#] GPQ) holds
not f . t in Q

proof

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

end;

A24: 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 A24, TOPS_2:def 4;
then A25: f = g1 " by A10, A6, TOPS_2:51;
A26: ( ex pq being object st
( pq in dom (f ") & pq in PQ & lower_bound ([#] GPQ) = (f ") . pq ) & 0 <= lower_bound ([#] GPQ) ) by A14, BORSUK_1:43, FUNCT_1:def 6;
f " is one-to-one by A10, A6, TOPS_2:50;
hence ( f . (lower_bound ([#] GPQ)) is Point of (TOP-REAL 2) & f . (lower_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 . (lower_bound ([#] GPQ)) & 0 <= s2 & s2 <= 1 & ( for t being Real st 0 <= t & t < s2 holds
not g . t in Q ) ) ) by A4, A5, A25, A26, A15, A17, FUNCT_1:34; :: thesis: