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

proof

let t be Real; :: thesis:
assume A23: ( 0 <= t & t < lower_bound ([#] GPQ) ) ; :: thesis:
then A24: t <= 1 by A22, XXREAL_0:2;
then A25: t in the carrier of I[01] by A23, BORSUK_1:86;
A26: t in dom f by A6, A23, A24, BORSUK_1:86;
assume A27: f . t in Q ; :: thesis:
f . t in the carrier of ((TOP-REAL 2) | P) by A25, FUNCT_2:7;
then f . t in P by PRE_TOPC:29;
then f . t in PQ by A27, XBOOLE_0:def 4;
then A28: (f " ) . (f . t) in GPQ by A19, FUNCT_1:def 12;
f " = f1 " by A7, TOPS_2:def 4;
then (f " ) . (f . t) = t by A7, A26, FUNCT_1:56;
then t in [#] GPQ by A28, WEIERSTR:def 3;
hence contradiction by A14, A23, SEQ_4:def 5; :: thesis:

end;

hence ( EX is Point of (TOP-REAL 2) & EX 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 = EX & 0 <= s2 & s2 <= 1 & ( for t being Real st 0 <= t & t < s2 holds
not g . t in Q ) ) ) by A20, A21, A22, FUNCT_1:56; :: thesis: