let P, Q be Subset of (TOP-REAL 2); for p1, p2 being Point of (TOP-REAL 2) st P meets Q & P /\ Q is closed & P is_an_arc_of p1,p2 holds
ex EX being Point of (TOP-REAL 2) st
( 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 ) ) )
let p1, p2 be Point of (TOP-REAL 2); ( P meets Q & P /\ Q is closed & P is_an_arc_of p1,p2 implies ex EX being Point of (TOP-REAL 2) st
( 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 ) ) ) )
assume that
A1:
P meets Q
and
A2:
P /\ Q is closed
and
A3:
P is_an_arc_of p1,p2
; ex EX being Point of (TOP-REAL 2) st
( 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 ) ) )
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))
; ( 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 ) ) )
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;
( 0 <= t & t < lower_bound ([#] GPQ) implies not f . t in Q )
assume that A18:
0 <= t
and A19:
t < lower_bound ([#] GPQ)
;
not f . t in Q
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
;
contradiction
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;
verum
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; verum