let P, Q be non empty Subset of (TOP-REAL 2); :: thesis: for p1, p2, q1, q2 being Point of (TOP-REAL 2) st P is_an_arc_of p1,p2 & Q is_an_arc_of q1,q2 & ( for p being Point of (TOP-REAL 2) st p in P holds

( p1 `1 <= p `1 & p `1 <= p2 `1 ) ) & ( for p being Point of (TOP-REAL 2) st p in Q holds

( p1 `1 <= p `1 & p `1 <= p2 `1 ) ) & ( for p being Point of (TOP-REAL 2) st p in P holds

( q1 `2 <= p `2 & p `2 <= q2 `2 ) ) & ( for p being Point of (TOP-REAL 2) st p in Q holds

( q1 `2 <= p `2 & p `2 <= q2 `2 ) ) holds

P meets Q

let p1, p2, q1, q2 be Point of (TOP-REAL 2); :: thesis: ( P is_an_arc_of p1,p2 & Q is_an_arc_of q1,q2 & ( for p being Point of (TOP-REAL 2) st p in P holds

( p1 `1 <= p `1 & p `1 <= p2 `1 ) ) & ( for p being Point of (TOP-REAL 2) st p in Q holds

( p1 `1 <= p `1 & p `1 <= p2 `1 ) ) & ( for p being Point of (TOP-REAL 2) st p in P holds

( q1 `2 <= p `2 & p `2 <= q2 `2 ) ) & ( for p being Point of (TOP-REAL 2) st p in Q holds

( q1 `2 <= p `2 & p `2 <= q2 `2 ) ) implies P meets Q )

assume that

A1: P is_an_arc_of p1,p2 and

A2: Q is_an_arc_of q1,q2 and

A3: for p being Point of (TOP-REAL 2) st p in P holds

( p1 `1 <= p `1 & p `1 <= p2 `1 ) and

A4: for p being Point of (TOP-REAL 2) st p in Q holds

( p1 `1 <= p `1 & p `1 <= p2 `1 ) and

A5: for p being Point of (TOP-REAL 2) st p in P holds

( q1 `2 <= p `2 & p `2 <= q2 `2 ) and

A6: for p being Point of (TOP-REAL 2) st p in Q holds

( q1 `2 <= p `2 & p `2 <= q2 `2 ) ; :: thesis: P meets Q

consider g being Function of I[01],((TOP-REAL 2) | Q) such that

A7: g is being_homeomorphism and

A8: g . 0 = q1 and

A9: g . 1 = q2 by A2, TOPREAL1:def 1;

A10: TopStruct(# the carrier of (TOP-REAL 2), the topology of (TOP-REAL 2) #) = TopSpaceMetr (Euclid 2) by EUCLID:def 8;

then reconsider P9 = P, Q9 = Q as Subset of (TopSpaceMetr (Euclid 2)) ;

P is compact by A1, JORDAN5A:1;

then A11: P9 is compact by A10, COMPTS_1:23;

Q is compact by A2, JORDAN5A:1;

then A12: Q9 is compact by A10, COMPTS_1:23;

set e = (min_dist_min (P9,Q9)) / 5;

consider f being Function of I[01],((TOP-REAL 2) | P) such that

A13: f is being_homeomorphism and

A14: f . 0 = p1 and

A15: f . 1 = p2 by A1, TOPREAL1:def 1;

consider f1 being Function of I[01],(TOP-REAL 2) such that

A16: f = f1 and

A17: f1 is continuous and

f1 is one-to-one by A13, JORDAN7:15;

consider g1 being Function of I[01],(TOP-REAL 2) such that

A18: g = g1 and

A19: g1 is continuous and

g1 is one-to-one by A7, JORDAN7:15;

assume P /\ Q = {} ; :: according to XBOOLE_0:def 7 :: thesis: contradiction

then P misses Q ;

then A20: min_dist_min (P9,Q9) > 0 by A11, A12, Th37;

then A21: (min_dist_min (P9,Q9)) / 5 > 0 / 5 by XREAL_1:74;

then consider hb being FinSequence of REAL such that

A22: hb . 1 = 0 and

A23: hb . (len hb) = 1 and

A24: 5 <= len hb and

A25: rng hb c= the carrier of I[01] and

A26: hb is increasing and

A27: for i being Nat

for R being Subset of I[01]

for W being Subset of (Euclid 2) st 1 <= i & i < len hb & R = [.(hb /. i),(hb /. (i + 1)).] & W = g1 .: R holds

diameter W < (min_dist_min (P9,Q9)) / 5 by A19, UNIFORM1:13;

consider h being FinSequence of REAL such that

A28: h . 1 = 0 and

A29: h . (len h) = 1 and

A30: 5 <= len h and

A31: rng h c= the carrier of I[01] and

A32: h is increasing and

A33: for i being Nat

for R being Subset of I[01]

for W being Subset of (Euclid 2) st 1 <= i & i < len h & R = [.(h /. i),(h /. (i + 1)).] & W = f1 .: R holds

diameter W < (min_dist_min (P9,Q9)) / 5 by A17, A21, UNIFORM1:13;

deffunc H_{1}( Nat) -> set = f1 . (h . $1);

ex h19 being FinSequence st

( len h19 = len h & ( for i being Nat st i in dom h19 holds

h19 . i = H_{1}(i) ) )
from FINSEQ_1:sch 2();

then consider h19 being FinSequence such that

A34: len h19 = len h and

A35: for i being Nat st i in dom h19 holds

h19 . i = f1 . (h . i) ;

A36: dom g1 = [#] I[01] by A7, A18, TOPS_2:def 5

.= the carrier of I[01] ;

rng h19 c= the carrier of (TOP-REAL 2)

A42: len h1 >= 1 by A30, A34, XXREAL_0:2;

then A43: h1 . 1 = h1 /. 1 by FINSEQ_4:15;

A44: for i being Nat st 1 <= i & i + 1 <= len h1 holds

|.((h1 /. i) - (h1 /. (i + 1))).| < (min_dist_min (P9,Q9)) / 5

( (h1 /. 1) `1 <= (h1 /. i) `1 & (h1 /. i) `1 <= (h1 /. (len h1)) `1 )

( (X_axis h1) . 1 <= (X_axis h1) . i & (X_axis h1) . i <= (X_axis h1) . (len h1) )

A89: for i being Nat st i in dom h1 holds

( q1 `2 <= (h1 /. i) `2 & (h1 /. i) `2 <= q2 `2 )

( q1 `2 <= (Y_axis h1) . i & (Y_axis h1) . i <= q2 `2 )

then consider f2 being FinSequence of (TOP-REAL 2) such that

A95: f2 is special and

A96: f2 . 1 = h1 . 1 and

A97: f2 . (len f2) = h1 . (len h1) and

A98: len f2 >= len h1 and

A99: ( X_axis f2 lies_between (X_axis h1) . 1,(X_axis h1) . (len h1) & Y_axis f2 lies_between q1 `2 ,q2 `2 ) and

A100: for j being Nat st j in dom f2 holds

ex k being Nat st

( k in dom h1 & |.((f2 /. j) - (h1 /. k)).| < (min_dist_min (P9,Q9)) / 5 ) and

A101: for j being Nat st 1 <= j & j + 1 <= len f2 holds

|.((f2 /. j) - (f2 /. (j + 1))).| < (min_dist_min (P9,Q9)) / 5 by A21, A44, A42, A88, Th38;

A102: len f2 >= 1 by A42, A98, XXREAL_0:2;

then A103: f2 . (len f2) = f2 /. (len f2) by FINSEQ_4:15;

deffunc H_{2}( Nat) -> set = g1 . (hb . $1);

ex h29 being FinSequence st

( len h29 = len hb & ( for i being Nat st i in dom h29 holds

h29 . i = H_{2}(i) ) )
from FINSEQ_1:sch 2();

then consider h29 being FinSequence such that

A104: len h29 = len hb and

A105: for i being Nat st i in dom h29 holds

h29 . i = g1 . (hb . i) ;

rng h29 c= the carrier of (TOP-REAL 2)

A111: rng f = [#] ((TOP-REAL 2) | P) by A13, TOPS_2:def 5

.= P by PRE_TOPC:def 5 ;

A112: for i being Nat st 1 <= i & i + 1 <= len h2 holds

|.((h2 /. i) - (h2 /. (i + 1))).| < (min_dist_min (P9,Q9)) / 5

then A147: len hb in dom hb by FINSEQ_3:25;

A148: 1 <= len hb by A24, XXREAL_0:2;

then A149: h2 . (len h2) = h2 /. (len h2) by A104, FINSEQ_4:15;

A150: dom hb = Seg (len hb) by FINSEQ_1:def 3;

A151: for i being Nat st i in dom hb holds

h2 /. i = g1 . (hb . i)

A155: 1 <= len h by A30, XXREAL_0:2;

then 1 in dom h19 by A34, FINSEQ_3:25;

then A156: h1 /. 1 = f1 . (h . 1) by A35, A43;

len h in dom h19 by A34, A155, FINSEQ_3:25;

then A157: f2 /. 1 <> f2 /. (len f2) by A1, A14, A15, A16, A28, A29, A34, A35, A96, A97, A43, A154, A103, A156, JORDAN6:37;

5 <= len f2 by A30, A34, A98, XXREAL_0:2;

then A158: 2 <= len f2 by XXREAL_0:2;

A159: h1 . (len h1) = h1 /. (len h1) by A42, FINSEQ_4:15;

then A160: (X_axis f2) . (len f2) = (h1 /. (len h1)) `1 by A97, A102, A103, Th40

.= (X_axis h1) . (len h1) by A42, Th40 ;

A161: h2 . 1 = h2 /. 1 by A148, A104, FINSEQ_4:15;

A162: len h2 >= 1 by A24, A104, XXREAL_0:2;

A163: for i being Nat st i in dom h2 holds

( (h2 /. 1) `2 <= (h2 /. i) `2 & (h2 /. i) `2 <= (h2 /. (len h2)) `2 )

( (Y_axis h2) . 1 <= (Y_axis h2) . i & (Y_axis h2) . i <= (Y_axis h2) . (len h2) )

A171: for i being Nat st i in dom h2 holds

( p1 `1 <= (h2 /. i) `1 & (h2 /. i) `1 <= p2 `1 )

( p1 `1 <= (X_axis h2) . i & (X_axis h2) . i <= p2 `1 )

then consider g2 being FinSequence of (TOP-REAL 2) such that

A175: g2 is special and

A176: g2 . 1 = h2 . 1 and

A177: g2 . (len g2) = h2 . (len h2) and

A178: len g2 >= len h2 and

A179: ( Y_axis g2 lies_between (Y_axis h2) . 1,(Y_axis h2) . (len h2) & X_axis g2 lies_between p1 `1 ,p2 `1 ) and

A180: for j being Nat st j in dom g2 holds

ex k being Nat st

( k in dom h2 & |.((g2 /. j) - (h2 /. k)).| < (min_dist_min (P9,Q9)) / 5 ) and

A181: for j being Nat st 1 <= j & j + 1 <= len g2 holds

|.((g2 /. j) - (g2 /. (j + 1))).| < (min_dist_min (P9,Q9)) / 5 by A21, A162, A170, A112, Th39;

5 <= len g2 by A24, A104, A178, XXREAL_0:2;

then A182: 2 <= len g2 by XXREAL_0:2;

A183: len g2 >= 1 by A162, A178, XXREAL_0:2;

then g2 . 1 = g2 /. 1 by FINSEQ_4:15;

then A184: (Y_axis g2) . 1 = (h2 /. 1) `2 by A176, A183, A161, Th41

.= (Y_axis h2) . 1 by A162, Th41 ;

1 in dom hb by A146, FINSEQ_3:25;

then h2 /. 1 = g1 . (hb . 1) by A151;

then A185: g2 . 1 <> g2 . (len g2) by A2, A8, A9, A18, A22, A23, A104, A151, A176, A177, A161, A149, A147, JORDAN6:37;

len hb in dom hb by A148, FINSEQ_3:25;

then A186: g2 . (len g2) = q2 by A9, A18, A23, A104, A151, A177, A149;

g2 /. (len g2) = g2 . (len g2) by A183, FINSEQ_4:15;

then A187: (Y_axis g2) . (len g2) = q2 `2 by A183, A186, Th41;

1 in dom hb by A148, FINSEQ_3:25;

then A188: h2 /. 1 = q1 by A8, A18, A22, A151;

A189: rng g = [#] ((TOP-REAL 2) | Q) by A7, TOPS_2:def 5

.= Q by PRE_TOPC:def 5 ;

len h in dom h19 by A34, A42, FINSEQ_3:25;

then h1 /. (len h1) = p2 by A15, A16, A29, A34, A35, A159;

then A190: (X_axis f2) . (len f2) = p2 `1 by A97, A102, A159, A103, Th40;

1 in dom h19 by A42, FINSEQ_3:25;

then h1 . 1 = f1 . (h . 1) by A35;

then A191: (X_axis f2) . 1 = p1 `1 by A14, A16, A28, A96, A102, A154, Th40;

g2 . (len g2) = g2 /. (len g2) by A183, FINSEQ_4:15;

then A192: (Y_axis g2) . (len g2) = (h2 /. (len h2)) `2 by A177, A183, A149, Th41

.= (Y_axis h2) . (len h2) by A162, Th41 ;

g2 /. 1 = g2 . 1 by A183, FINSEQ_4:15;

then A193: (Y_axis g2) . 1 = q1 `2 by A176, A183, A188, A161, Th41;

(X_axis f2) . 1 = (h1 /. 1) `1 by A96, A102, A43, A154, Th40

.= (X_axis h1) . 1 by A42, Th40 ;

then L~ f2 meets L~ g2 by A95, A99, A175, A179, A154, A103, A191, A190, A193, A187, A160, A184, A192, A158, A182, A157, A185, Th26;

then consider s being object such that

A194: s in L~ f2 and

A195: s in L~ g2 by XBOOLE_0:3;

reconsider ps = s as Point of (TOP-REAL 2) by A194;

ps in union { (LSeg (g2,j)) where j is Nat : ( 1 <= j & j + 1 <= len g2 ) } by A195, TOPREAL1:def 4;

then consider y being set such that

A196: ( ps in y & y in { (LSeg (g2,j)) where j is Nat : ( 1 <= j & j + 1 <= len g2 ) } ) by TARSKI:def 4;

ps in union { (LSeg (f2,i)) where i is Nat : ( 1 <= i & i + 1 <= len f2 ) } by A194, TOPREAL1:def 4;

then consider x being set such that

A197: ( ps in x & x in { (LSeg (f2,i)) where i is Nat : ( 1 <= i & i + 1 <= len f2 ) } ) by TARSKI:def 4;

consider i being Nat such that

A198: x = LSeg (f2,i) and

A199: 1 <= i and

A200: i + 1 <= len f2 by A197;

LSeg (f2,i) = LSeg ((f2 /. i),(f2 /. (i + 1))) by A199, A200, TOPREAL1:def 3;

then A201: |.(ps - (f2 /. i)).| <= |.((f2 /. i) - (f2 /. (i + 1))).| by A197, A198, Th35;

i < len f2 by A200, NAT_1:13;

then i in dom f2 by A199, FINSEQ_3:25;

then consider k being Nat such that

A202: k in dom h1 and

A203: |.((f2 /. i) - (h1 /. k)).| < (min_dist_min (P9,Q9)) / 5 by A100;

k in dom h by A34, A202, FINSEQ_3:29;

then A204: h . k in rng h by FUNCT_1:def 3;

reconsider p11 = h1 /. k as Point of (TOP-REAL 2) ;

|.((f2 /. i) - (f2 /. (i + 1))).| < (min_dist_min (P9,Q9)) / 5 by A101, A199, A200;

then |.(ps - (f2 /. i)).| < (min_dist_min (P9,Q9)) / 5 by A201, XXREAL_0:2;

then ( |.(ps - (h1 /. k)).| <= |.(ps - (f2 /. i)).| + |.((f2 /. i) - (h1 /. k)).| & |.(ps - (f2 /. i)).| + |.((f2 /. i) - (h1 /. k)).| < ((min_dist_min (P9,Q9)) / 5) + ((min_dist_min (P9,Q9)) / 5) ) by A203, TOPRNS_1:34, XREAL_1:8;

then |.(ps - (h1 /. k)).| < ((min_dist_min (P9,Q9)) / 5) + ((min_dist_min (P9,Q9)) / 5) by XXREAL_0:2;

then A205: |.(p11 - ps).| < ((min_dist_min (P9,Q9)) / 5) + ((min_dist_min (P9,Q9)) / 5) by TOPRNS_1:27;

k in Seg (len h1) by A202, FINSEQ_1:def 3;

then ( 1 <= k & k <= len h1 ) by FINSEQ_1:1;

then h1 . k = h1 /. k by FINSEQ_4:15;

then A206: h1 /. k = f1 . (h . k) by A35, A202;

consider j being Nat such that

A207: y = LSeg (g2,j) and

A208: 1 <= j and

A209: j + 1 <= len g2 by A196;

LSeg (g2,j) = LSeg ((g2 /. j),(g2 /. (j + 1))) by A208, A209, TOPREAL1:def 3;

then A210: |.(ps - (g2 /. j)).| <= |.((g2 /. j) - (g2 /. (j + 1))).| by A196, A207, Th35;

j < len g2 by A209, NAT_1:13;

then j in Seg (len g2) by A208, FINSEQ_1:1;

then j in dom g2 by FINSEQ_1:def 3;

then consider k9 being Nat such that

A211: k9 in dom h2 and

A212: |.((g2 /. j) - (h2 /. k9)).| < (min_dist_min (P9,Q9)) / 5 by A180;

k9 in Seg (len h2) by A211, FINSEQ_1:def 3;

then A213: k9 in dom hb by A104, FINSEQ_1:def 3;

then A214: hb . k9 in rng hb by FUNCT_1:def 3;

reconsider q11 = h2 /. k9 as Point of (TOP-REAL 2) ;

|.((g2 /. j) - (g2 /. (j + 1))).| < (min_dist_min (P9,Q9)) / 5 by A181, A208, A209;

then |.(ps - (g2 /. j)).| < (min_dist_min (P9,Q9)) / 5 by A210, XXREAL_0:2;

then ( |.(ps - (h2 /. k9)).| <= |.(ps - (g2 /. j)).| + |.((g2 /. j) - (h2 /. k9)).| & |.(ps - (g2 /. j)).| + |.((g2 /. j) - (h2 /. k9)).| < ((min_dist_min (P9,Q9)) / 5) + ((min_dist_min (P9,Q9)) / 5) ) by A212, TOPRNS_1:34, XREAL_1:8;

then |.(ps - (h2 /. k9)).| < ((min_dist_min (P9,Q9)) / 5) + ((min_dist_min (P9,Q9)) / 5) by XXREAL_0:2;

then ( |.(p11 - q11).| <= |.(p11 - ps).| + |.(ps - q11).| & |.(p11 - ps).| + |.(ps - q11).| < (((min_dist_min (P9,Q9)) / 5) + ((min_dist_min (P9,Q9)) / 5)) + (((min_dist_min (P9,Q9)) / 5) + ((min_dist_min (P9,Q9)) / 5)) ) by A205, TOPRNS_1:34, XREAL_1:8;

then A215: |.(p11 - q11).| < ((((min_dist_min (P9,Q9)) / 5) + ((min_dist_min (P9,Q9)) / 5)) + ((min_dist_min (P9,Q9)) / 5)) + ((min_dist_min (P9,Q9)) / 5) by XXREAL_0:2;

h2 /. k9 = g1 . (hb . k9) by A151, A213;

then A216: h2 /. k9 in rng g by A18, A25, A214, A36, FUNCT_1:def 3;

reconsider x1 = p11, x2 = q11 as Point of (Euclid 2) by EUCLID:22;

dom f1 = [#] I[01] by A13, A16, TOPS_2:def 5

.= the carrier of I[01] ;

then h1 /. k in P by A16, A31, A206, A204, A111, FUNCT_1:def 3;

then min_dist_min (P9,Q9) <= dist (x1,x2) by A11, A12, A216, A189, WEIERSTR:34;

then min_dist_min (P9,Q9) <= |.(p11 - q11).| by Th28;

then min_dist_min (P9,Q9) < 4 * ((min_dist_min (P9,Q9)) / 5) by A215, XXREAL_0:2;

then (4 * ((min_dist_min (P9,Q9)) / 5)) - (5 * ((min_dist_min (P9,Q9)) / 5)) > 0 by XREAL_1:50;

then ((4 - 5) * ((min_dist_min (P9,Q9)) / 5)) / ((min_dist_min (P9,Q9)) / 5) > 0 by A21, XREAL_1:139;

then 4 - 5 > 0 by A20;

hence contradiction ; :: thesis: verum

( p1 `1 <= p `1 & p `1 <= p2 `1 ) ) & ( for p being Point of (TOP-REAL 2) st p in Q holds

( p1 `1 <= p `1 & p `1 <= p2 `1 ) ) & ( for p being Point of (TOP-REAL 2) st p in P holds

( q1 `2 <= p `2 & p `2 <= q2 `2 ) ) & ( for p being Point of (TOP-REAL 2) st p in Q holds

( q1 `2 <= p `2 & p `2 <= q2 `2 ) ) holds

P meets Q

let p1, p2, q1, q2 be Point of (TOP-REAL 2); :: thesis: ( P is_an_arc_of p1,p2 & Q is_an_arc_of q1,q2 & ( for p being Point of (TOP-REAL 2) st p in P holds

( p1 `1 <= p `1 & p `1 <= p2 `1 ) ) & ( for p being Point of (TOP-REAL 2) st p in Q holds

( p1 `1 <= p `1 & p `1 <= p2 `1 ) ) & ( for p being Point of (TOP-REAL 2) st p in P holds

( q1 `2 <= p `2 & p `2 <= q2 `2 ) ) & ( for p being Point of (TOP-REAL 2) st p in Q holds

( q1 `2 <= p `2 & p `2 <= q2 `2 ) ) implies P meets Q )

assume that

A1: P is_an_arc_of p1,p2 and

A2: Q is_an_arc_of q1,q2 and

A3: for p being Point of (TOP-REAL 2) st p in P holds

( p1 `1 <= p `1 & p `1 <= p2 `1 ) and

A4: for p being Point of (TOP-REAL 2) st p in Q holds

( p1 `1 <= p `1 & p `1 <= p2 `1 ) and

A5: for p being Point of (TOP-REAL 2) st p in P holds

( q1 `2 <= p `2 & p `2 <= q2 `2 ) and

A6: for p being Point of (TOP-REAL 2) st p in Q holds

( q1 `2 <= p `2 & p `2 <= q2 `2 ) ; :: thesis: P meets Q

consider g being Function of I[01],((TOP-REAL 2) | Q) such that

A7: g is being_homeomorphism and

A8: g . 0 = q1 and

A9: g . 1 = q2 by A2, TOPREAL1:def 1;

A10: TopStruct(# the carrier of (TOP-REAL 2), the topology of (TOP-REAL 2) #) = TopSpaceMetr (Euclid 2) by EUCLID:def 8;

then reconsider P9 = P, Q9 = Q as Subset of (TopSpaceMetr (Euclid 2)) ;

P is compact by A1, JORDAN5A:1;

then A11: P9 is compact by A10, COMPTS_1:23;

Q is compact by A2, JORDAN5A:1;

then A12: Q9 is compact by A10, COMPTS_1:23;

set e = (min_dist_min (P9,Q9)) / 5;

consider f being Function of I[01],((TOP-REAL 2) | P) such that

A13: f is being_homeomorphism and

A14: f . 0 = p1 and

A15: f . 1 = p2 by A1, TOPREAL1:def 1;

consider f1 being Function of I[01],(TOP-REAL 2) such that

A16: f = f1 and

A17: f1 is continuous and

f1 is one-to-one by A13, JORDAN7:15;

consider g1 being Function of I[01],(TOP-REAL 2) such that

A18: g = g1 and

A19: g1 is continuous and

g1 is one-to-one by A7, JORDAN7:15;

assume P /\ Q = {} ; :: according to XBOOLE_0:def 7 :: thesis: contradiction

then P misses Q ;

then A20: min_dist_min (P9,Q9) > 0 by A11, A12, Th37;

then A21: (min_dist_min (P9,Q9)) / 5 > 0 / 5 by XREAL_1:74;

then consider hb being FinSequence of REAL such that

A22: hb . 1 = 0 and

A23: hb . (len hb) = 1 and

A24: 5 <= len hb and

A25: rng hb c= the carrier of I[01] and

A26: hb is increasing and

A27: for i being Nat

for R being Subset of I[01]

for W being Subset of (Euclid 2) st 1 <= i & i < len hb & R = [.(hb /. i),(hb /. (i + 1)).] & W = g1 .: R holds

diameter W < (min_dist_min (P9,Q9)) / 5 by A19, UNIFORM1:13;

consider h being FinSequence of REAL such that

A28: h . 1 = 0 and

A29: h . (len h) = 1 and

A30: 5 <= len h and

A31: rng h c= the carrier of I[01] and

A32: h is increasing and

A33: for i being Nat

for R being Subset of I[01]

for W being Subset of (Euclid 2) st 1 <= i & i < len h & R = [.(h /. i),(h /. (i + 1)).] & W = f1 .: R holds

diameter W < (min_dist_min (P9,Q9)) / 5 by A17, A21, UNIFORM1:13;

deffunc H

ex h19 being FinSequence st

( len h19 = len h & ( for i being Nat st i in dom h19 holds

h19 . i = H

then consider h19 being FinSequence such that

A34: len h19 = len h and

A35: for i being Nat st i in dom h19 holds

h19 . i = f1 . (h . i) ;

A36: dom g1 = [#] I[01] by A7, A18, TOPS_2:def 5

.= the carrier of I[01] ;

rng h19 c= the carrier of (TOP-REAL 2)

proof

then reconsider h1 = h19 as FinSequence of (TOP-REAL 2) by FINSEQ_1:def 4;
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng h19 or y in the carrier of (TOP-REAL 2) )

assume y in rng h19 ; :: thesis: y in the carrier of (TOP-REAL 2)

then consider x being object such that

A37: x in dom h19 and

A38: y = h19 . x by FUNCT_1:def 3;

reconsider i = x as Element of NAT by A37;

dom h19 = Seg (len h19) by FINSEQ_1:def 3;

then i in dom h by A34, A37, FINSEQ_1:def 3;

then A39: h . i in rng h by FUNCT_1:def 3;

A40: dom f1 = [#] I[01] by A13, A16, TOPS_2:def 5

.= the carrier of I[01] ;

A41: rng f = [#] ((TOP-REAL 2) | P) by A13, TOPS_2:def 5

.= P by PRE_TOPC:def 5 ;

h19 . i = f1 . (h . i) by A35, A37;

then h19 . i in rng f by A16, A31, A39, A40, FUNCT_1:def 3;

hence y in the carrier of (TOP-REAL 2) by A38, A41; :: thesis: verum

end;assume y in rng h19 ; :: thesis: y in the carrier of (TOP-REAL 2)

then consider x being object such that

A37: x in dom h19 and

A38: y = h19 . x by FUNCT_1:def 3;

reconsider i = x as Element of NAT by A37;

dom h19 = Seg (len h19) by FINSEQ_1:def 3;

then i in dom h by A34, A37, FINSEQ_1:def 3;

then A39: h . i in rng h by FUNCT_1:def 3;

A40: dom f1 = [#] I[01] by A13, A16, TOPS_2:def 5

.= the carrier of I[01] ;

A41: rng f = [#] ((TOP-REAL 2) | P) by A13, TOPS_2:def 5

.= P by PRE_TOPC:def 5 ;

h19 . i = f1 . (h . i) by A35, A37;

then h19 . i in rng f by A16, A31, A39, A40, FUNCT_1:def 3;

hence y in the carrier of (TOP-REAL 2) by A38, A41; :: thesis: verum

A42: len h1 >= 1 by A30, A34, XXREAL_0:2;

then A43: h1 . 1 = h1 /. 1 by FINSEQ_4:15;

A44: for i being Nat st 1 <= i & i + 1 <= len h1 holds

|.((h1 /. i) - (h1 /. (i + 1))).| < (min_dist_min (P9,Q9)) / 5

proof

A79:
for i being Nat st i in dom h1 holds
reconsider Pa = P as Subset of (TOP-REAL 2) ;

reconsider W1 = P as Subset of (Euclid 2) by TOPREAL3:8;

let i be Nat; :: thesis: ( 1 <= i & i + 1 <= len h1 implies |.((h1 /. i) - (h1 /. (i + 1))).| < (min_dist_min (P9,Q9)) / 5 )

assume that

A45: 1 <= i and

A46: i + 1 <= len h1 ; :: thesis: |.((h1 /. i) - (h1 /. (i + 1))).| < (min_dist_min (P9,Q9)) / 5

A47: 1 < i + 1 by A45, NAT_1:13;

then A48: h . (i + 1) = h /. (i + 1) by A34, A46, FINSEQ_4:15;

A49: i + 1 in dom h19 by A46, A47, FINSEQ_3:25;

then A50: h19 . (i + 1) = f1 . (h . (i + 1)) by A35;

then A51: h1 /. (i + 1) = f1 . (h . (i + 1)) by A46, A47, FINSEQ_4:15;

A52: i < len h1 by A46, NAT_1:13;

then A53: h . i = h /. i by A34, A45, FINSEQ_4:15;

A54: i in dom h by A34, A45, A52, FINSEQ_3:25;

then A55: h . i in rng h by FUNCT_1:def 3;

A56: i + 1 in dom h by A34, A46, A47, FINSEQ_3:25;

then h . (i + 1) in rng h by FUNCT_1:def 3;

then reconsider R = [.(h /. i),(h /. (i + 1)).] as Subset of I[01] by A31, A55, A53, A48, BORSUK_1:40, XXREAL_2:def 12;

reconsider W = f1 .: R as Subset of (Euclid 2) by TOPREAL3:8;

A57: Pa is compact by A1, JORDAN5A:1;

reconsider Pa = Pa as non empty Subset of (TOP-REAL 2) ;

A58: rng f = [#] ((TOP-REAL 2) | P) by A13, TOPS_2:def 5

.= P by PRE_TOPC:def 5 ;

set r1 = (((E-bound Pa) - (W-bound Pa)) + ((N-bound Pa) - (S-bound Pa))) + 1;

A59: for x, y being Point of (Euclid 2) st x in W1 & y in W1 holds

dist (x,y) <= (((E-bound Pa) - (W-bound Pa)) + ((N-bound Pa) - (S-bound Pa))) + 1

then ( S-bound Pa <= p1 `2 & p1 `2 <= N-bound Pa ) by A57, PSCOMP_1:24;

then S-bound Pa <= N-bound Pa by XXREAL_0:2;

then A68: 0 <= (N-bound Pa) - (S-bound Pa) by XREAL_1:48;

( W-bound Pa <= p1 `1 & p1 `1 <= E-bound Pa ) by A57, A67, PSCOMP_1:24;

then W-bound Pa <= E-bound Pa by XXREAL_0:2;

then 0 <= (E-bound Pa) - (W-bound Pa) by XREAL_1:48;

then A69: W1 is bounded by A68, A59, TBSP_1:def 7;

A70: dom f1 = [#] I[01] by A13, A16, TOPS_2:def 5

.= the carrier of I[01] ;

i + 1 in dom h by A34, A46, A47, FINSEQ_3:25;

then h . (i + 1) in rng h by FUNCT_1:def 3;

then h19 . (i + 1) in rng f by A16, A31, A50, A70, FUNCT_1:def 3;

then A71: f1 . (h . (i + 1)) is Element of (TOP-REAL 2) by A35, A49, A58;

A72: i in dom h19 by A45, A52, FINSEQ_3:25;

then A73: h19 . i = f1 . (h . i) by A35;

then h19 . i in rng f by A16, A31, A55, A70, FUNCT_1:def 3;

then f1 . (h . i) is Element of (TOP-REAL 2) by A35, A72, A58;

then reconsider w1 = f1 . (h . i), w2 = f1 . (h . (i + 1)) as Point of (Euclid 2) by A71, TOPREAL3:8;

i < i + 1 by NAT_1:13;

then A74: h /. i <= h /. (i + 1) by A32, A54, A53, A56, A48, SEQM_3:def 1;

then h . i in R by A53, XXREAL_1:1;

then A75: w1 in f1 .: R by A70, FUNCT_1:def 6;

h . (i + 1) in R by A48, A74, XXREAL_1:1;

then A76: w2 in f1 .: R by A70, FUNCT_1:def 6;

dom f1 = [#] I[01] by A13, A16, TOPS_2:def 5;

then P = f1 .: [.0,1.] by A16, A58, BORSUK_1:40, RELAT_1:113;

then W is bounded by A69, BORSUK_1:40, RELAT_1:123, TBSP_1:14;

then A77: dist (w1,w2) <= diameter W by A75, A76, TBSP_1:def 8;

diameter W < (min_dist_min (P9,Q9)) / 5 by A33, A34, A45, A52;

then A78: dist (w1,w2) < (min_dist_min (P9,Q9)) / 5 by A77, XXREAL_0:2;

h1 /. i = f1 . (h . i) by A45, A52, A73, FINSEQ_4:15;

hence |.((h1 /. i) - (h1 /. (i + 1))).| < (min_dist_min (P9,Q9)) / 5 by A51, A78, Th28; :: thesis: verum

end;reconsider W1 = P as Subset of (Euclid 2) by TOPREAL3:8;

let i be Nat; :: thesis: ( 1 <= i & i + 1 <= len h1 implies |.((h1 /. i) - (h1 /. (i + 1))).| < (min_dist_min (P9,Q9)) / 5 )

assume that

A45: 1 <= i and

A46: i + 1 <= len h1 ; :: thesis: |.((h1 /. i) - (h1 /. (i + 1))).| < (min_dist_min (P9,Q9)) / 5

A47: 1 < i + 1 by A45, NAT_1:13;

then A48: h . (i + 1) = h /. (i + 1) by A34, A46, FINSEQ_4:15;

A49: i + 1 in dom h19 by A46, A47, FINSEQ_3:25;

then A50: h19 . (i + 1) = f1 . (h . (i + 1)) by A35;

then A51: h1 /. (i + 1) = f1 . (h . (i + 1)) by A46, A47, FINSEQ_4:15;

A52: i < len h1 by A46, NAT_1:13;

then A53: h . i = h /. i by A34, A45, FINSEQ_4:15;

A54: i in dom h by A34, A45, A52, FINSEQ_3:25;

then A55: h . i in rng h by FUNCT_1:def 3;

A56: i + 1 in dom h by A34, A46, A47, FINSEQ_3:25;

then h . (i + 1) in rng h by FUNCT_1:def 3;

then reconsider R = [.(h /. i),(h /. (i + 1)).] as Subset of I[01] by A31, A55, A53, A48, BORSUK_1:40, XXREAL_2:def 12;

reconsider W = f1 .: R as Subset of (Euclid 2) by TOPREAL3:8;

A57: Pa is compact by A1, JORDAN5A:1;

reconsider Pa = Pa as non empty Subset of (TOP-REAL 2) ;

A58: rng f = [#] ((TOP-REAL 2) | P) by A13, TOPS_2:def 5

.= P by PRE_TOPC:def 5 ;

set r1 = (((E-bound Pa) - (W-bound Pa)) + ((N-bound Pa) - (S-bound Pa))) + 1;

A59: for x, y being Point of (Euclid 2) st x in W1 & y in W1 holds

dist (x,y) <= (((E-bound Pa) - (W-bound Pa)) + ((N-bound Pa) - (S-bound Pa))) + 1

proof

A67:
p1 in Pa
by A1, TOPREAL1:1;
let x, y be Point of (Euclid 2); :: thesis: ( x in W1 & y in W1 implies dist (x,y) <= (((E-bound Pa) - (W-bound Pa)) + ((N-bound Pa) - (S-bound Pa))) + 1 )

assume that

A60: x in W1 and

A61: y in W1 ; :: thesis: dist (x,y) <= (((E-bound Pa) - (W-bound Pa)) + ((N-bound Pa) - (S-bound Pa))) + 1

reconsider pw1 = x, pw2 = y as Point of (TOP-REAL 2) by A60, A61;

A62: ( S-bound Pa <= pw2 `2 & pw2 `2 <= N-bound Pa ) by A57, A61, PSCOMP_1:24;

( S-bound Pa <= pw1 `2 & pw1 `2 <= N-bound Pa ) by A57, A60, PSCOMP_1:24;

then A63: |.((pw1 `2) - (pw2 `2)).| <= (N-bound Pa) - (S-bound Pa) by A62, Th27;

A64: ( W-bound Pa <= pw2 `1 & pw2 `1 <= E-bound Pa ) by A57, A61, PSCOMP_1:24;

( W-bound Pa <= pw1 `1 & pw1 `1 <= E-bound Pa ) by A57, A60, PSCOMP_1:24;

then |.((pw1 `1) - (pw2 `1)).| <= (E-bound Pa) - (W-bound Pa) by A64, Th27;

then A65: |.((pw1 `1) - (pw2 `1)).| + |.((pw1 `2) - (pw2 `2)).| <= ((E-bound Pa) - (W-bound Pa)) + ((N-bound Pa) - (S-bound Pa)) by A63, XREAL_1:7;

((E-bound Pa) - (W-bound Pa)) + ((N-bound Pa) - (S-bound Pa)) <= (((E-bound Pa) - (W-bound Pa)) + ((N-bound Pa) - (S-bound Pa))) + 1 by XREAL_1:29;

then A66: |.((pw1 `1) - (pw2 `1)).| + |.((pw1 `2) - (pw2 `2)).| <= (((E-bound Pa) - (W-bound Pa)) + ((N-bound Pa) - (S-bound Pa))) + 1 by A65, XXREAL_0:2;

( dist (x,y) = |.(pw1 - pw2).| & |.(pw1 - pw2).| <= |.((pw1 `1) - (pw2 `1)).| + |.((pw1 `2) - (pw2 `2)).| ) by Th28, Th32;

hence dist (x,y) <= (((E-bound Pa) - (W-bound Pa)) + ((N-bound Pa) - (S-bound Pa))) + 1 by A66, XXREAL_0:2; :: thesis: verum

end;assume that

A60: x in W1 and

A61: y in W1 ; :: thesis: dist (x,y) <= (((E-bound Pa) - (W-bound Pa)) + ((N-bound Pa) - (S-bound Pa))) + 1

reconsider pw1 = x, pw2 = y as Point of (TOP-REAL 2) by A60, A61;

A62: ( S-bound Pa <= pw2 `2 & pw2 `2 <= N-bound Pa ) by A57, A61, PSCOMP_1:24;

( S-bound Pa <= pw1 `2 & pw1 `2 <= N-bound Pa ) by A57, A60, PSCOMP_1:24;

then A63: |.((pw1 `2) - (pw2 `2)).| <= (N-bound Pa) - (S-bound Pa) by A62, Th27;

A64: ( W-bound Pa <= pw2 `1 & pw2 `1 <= E-bound Pa ) by A57, A61, PSCOMP_1:24;

( W-bound Pa <= pw1 `1 & pw1 `1 <= E-bound Pa ) by A57, A60, PSCOMP_1:24;

then |.((pw1 `1) - (pw2 `1)).| <= (E-bound Pa) - (W-bound Pa) by A64, Th27;

then A65: |.((pw1 `1) - (pw2 `1)).| + |.((pw1 `2) - (pw2 `2)).| <= ((E-bound Pa) - (W-bound Pa)) + ((N-bound Pa) - (S-bound Pa)) by A63, XREAL_1:7;

((E-bound Pa) - (W-bound Pa)) + ((N-bound Pa) - (S-bound Pa)) <= (((E-bound Pa) - (W-bound Pa)) + ((N-bound Pa) - (S-bound Pa))) + 1 by XREAL_1:29;

then A66: |.((pw1 `1) - (pw2 `1)).| + |.((pw1 `2) - (pw2 `2)).| <= (((E-bound Pa) - (W-bound Pa)) + ((N-bound Pa) - (S-bound Pa))) + 1 by A65, XXREAL_0:2;

( dist (x,y) = |.(pw1 - pw2).| & |.(pw1 - pw2).| <= |.((pw1 `1) - (pw2 `1)).| + |.((pw1 `2) - (pw2 `2)).| ) by Th28, Th32;

hence dist (x,y) <= (((E-bound Pa) - (W-bound Pa)) + ((N-bound Pa) - (S-bound Pa))) + 1 by A66, XXREAL_0:2; :: thesis: verum

then ( S-bound Pa <= p1 `2 & p1 `2 <= N-bound Pa ) by A57, PSCOMP_1:24;

then S-bound Pa <= N-bound Pa by XXREAL_0:2;

then A68: 0 <= (N-bound Pa) - (S-bound Pa) by XREAL_1:48;

( W-bound Pa <= p1 `1 & p1 `1 <= E-bound Pa ) by A57, A67, PSCOMP_1:24;

then W-bound Pa <= E-bound Pa by XXREAL_0:2;

then 0 <= (E-bound Pa) - (W-bound Pa) by XREAL_1:48;

then A69: W1 is bounded by A68, A59, TBSP_1:def 7;

A70: dom f1 = [#] I[01] by A13, A16, TOPS_2:def 5

.= the carrier of I[01] ;

i + 1 in dom h by A34, A46, A47, FINSEQ_3:25;

then h . (i + 1) in rng h by FUNCT_1:def 3;

then h19 . (i + 1) in rng f by A16, A31, A50, A70, FUNCT_1:def 3;

then A71: f1 . (h . (i + 1)) is Element of (TOP-REAL 2) by A35, A49, A58;

A72: i in dom h19 by A45, A52, FINSEQ_3:25;

then A73: h19 . i = f1 . (h . i) by A35;

then h19 . i in rng f by A16, A31, A55, A70, FUNCT_1:def 3;

then f1 . (h . i) is Element of (TOP-REAL 2) by A35, A72, A58;

then reconsider w1 = f1 . (h . i), w2 = f1 . (h . (i + 1)) as Point of (Euclid 2) by A71, TOPREAL3:8;

i < i + 1 by NAT_1:13;

then A74: h /. i <= h /. (i + 1) by A32, A54, A53, A56, A48, SEQM_3:def 1;

then h . i in R by A53, XXREAL_1:1;

then A75: w1 in f1 .: R by A70, FUNCT_1:def 6;

h . (i + 1) in R by A48, A74, XXREAL_1:1;

then A76: w2 in f1 .: R by A70, FUNCT_1:def 6;

dom f1 = [#] I[01] by A13, A16, TOPS_2:def 5;

then P = f1 .: [.0,1.] by A16, A58, BORSUK_1:40, RELAT_1:113;

then W is bounded by A69, BORSUK_1:40, RELAT_1:123, TBSP_1:14;

then A77: dist (w1,w2) <= diameter W by A75, A76, TBSP_1:def 8;

diameter W < (min_dist_min (P9,Q9)) / 5 by A33, A34, A45, A52;

then A78: dist (w1,w2) < (min_dist_min (P9,Q9)) / 5 by A77, XXREAL_0:2;

h1 /. i = f1 . (h . i) by A45, A52, A73, FINSEQ_4:15;

hence |.((h1 /. i) - (h1 /. (i + 1))).| < (min_dist_min (P9,Q9)) / 5 by A51, A78, Th28; :: thesis: verum

( (h1 /. 1) `1 <= (h1 /. i) `1 & (h1 /. i) `1 <= (h1 /. (len h1)) `1 )

proof

for i being Nat st i in dom (X_axis h1) holds
len h in dom h19
by A34, A42, FINSEQ_3:25;

then h1 . (len h1) = f1 . (h . (len h)) by A34, A35;

then A80: h1 /. (len h1) = f1 . (h . (len h)) by A42, FINSEQ_4:15;

let i be Nat; :: thesis: ( i in dom h1 implies ( (h1 /. 1) `1 <= (h1 /. i) `1 & (h1 /. i) `1 <= (h1 /. (len h1)) `1 ) )

assume A81: i in dom h1 ; :: thesis: ( (h1 /. 1) `1 <= (h1 /. i) `1 & (h1 /. i) `1 <= (h1 /. (len h1)) `1 )

then h1 . i = f1 . (h . i) by A35;

then A82: h1 /. i = f1 . (h . i) by A81, PARTFUN1:def 6;

i in Seg (len h) by A34, A81, FINSEQ_1:def 3;

then i in dom h by FINSEQ_1:def 3;

then A83: h . i in rng h by FUNCT_1:def 3;

dom f1 = [#] I[01] by A13, A16, TOPS_2:def 5

.= the carrier of I[01] ;

then A84: h1 /. i in rng f by A16, A31, A82, A83, FUNCT_1:def 3;

1 in dom h19 by A42, FINSEQ_3:25;

then h1 . 1 = f1 . (h . 1) by A35;

then A85: h1 /. 1 = f1 . (h . 1) by A42, FINSEQ_4:15;

rng f = [#] ((TOP-REAL 2) | P) by A13, TOPS_2:def 5

.= P by PRE_TOPC:def 5 ;

hence ( (h1 /. 1) `1 <= (h1 /. i) `1 & (h1 /. i) `1 <= (h1 /. (len h1)) `1 ) by A3, A14, A15, A16, A28, A29, A85, A80, A84; :: thesis: verum

end;then h1 . (len h1) = f1 . (h . (len h)) by A34, A35;

then A80: h1 /. (len h1) = f1 . (h . (len h)) by A42, FINSEQ_4:15;

let i be Nat; :: thesis: ( i in dom h1 implies ( (h1 /. 1) `1 <= (h1 /. i) `1 & (h1 /. i) `1 <= (h1 /. (len h1)) `1 ) )

assume A81: i in dom h1 ; :: thesis: ( (h1 /. 1) `1 <= (h1 /. i) `1 & (h1 /. i) `1 <= (h1 /. (len h1)) `1 )

then h1 . i = f1 . (h . i) by A35;

then A82: h1 /. i = f1 . (h . i) by A81, PARTFUN1:def 6;

i in Seg (len h) by A34, A81, FINSEQ_1:def 3;

then i in dom h by FINSEQ_1:def 3;

then A83: h . i in rng h by FUNCT_1:def 3;

dom f1 = [#] I[01] by A13, A16, TOPS_2:def 5

.= the carrier of I[01] ;

then A84: h1 /. i in rng f by A16, A31, A82, A83, FUNCT_1:def 3;

1 in dom h19 by A42, FINSEQ_3:25;

then h1 . 1 = f1 . (h . 1) by A35;

then A85: h1 /. 1 = f1 . (h . 1) by A42, FINSEQ_4:15;

rng f = [#] ((TOP-REAL 2) | P) by A13, TOPS_2:def 5

.= P by PRE_TOPC:def 5 ;

hence ( (h1 /. 1) `1 <= (h1 /. i) `1 & (h1 /. i) `1 <= (h1 /. (len h1)) `1 ) by A3, A14, A15, A16, A28, A29, A85, A80, A84; :: thesis: verum

( (X_axis h1) . 1 <= (X_axis h1) . i & (X_axis h1) . i <= (X_axis h1) . (len h1) )

proof

then A88:
X_axis h1 lies_between (X_axis h1) . 1,(X_axis h1) . (len h1)
by GOBOARD4:def 2;
let i be Nat; :: thesis: ( i in dom (X_axis h1) implies ( (X_axis h1) . 1 <= (X_axis h1) . i & (X_axis h1) . i <= (X_axis h1) . (len h1) ) )

A86: ( (X_axis h1) . 1 = (h1 /. 1) `1 & (X_axis h1) . (len h1) = (h1 /. (len h1)) `1 ) by A42, Th40;

assume i in dom (X_axis h1) ; :: thesis: ( (X_axis h1) . 1 <= (X_axis h1) . i & (X_axis h1) . i <= (X_axis h1) . (len h1) )

then i in Seg (len (X_axis h1)) by FINSEQ_1:def 3;

then i in Seg (len h1) by A42, Th40;

then A87: i in dom h1 by FINSEQ_1:def 3;

then (X_axis h1) . i = (h1 /. i) `1 by Th42;

hence ( (X_axis h1) . 1 <= (X_axis h1) . i & (X_axis h1) . i <= (X_axis h1) . (len h1) ) by A79, A87, A86; :: thesis: verum

end;A86: ( (X_axis h1) . 1 = (h1 /. 1) `1 & (X_axis h1) . (len h1) = (h1 /. (len h1)) `1 ) by A42, Th40;

assume i in dom (X_axis h1) ; :: thesis: ( (X_axis h1) . 1 <= (X_axis h1) . i & (X_axis h1) . i <= (X_axis h1) . (len h1) )

then i in Seg (len (X_axis h1)) by FINSEQ_1:def 3;

then i in Seg (len h1) by A42, Th40;

then A87: i in dom h1 by FINSEQ_1:def 3;

then (X_axis h1) . i = (h1 /. i) `1 by Th42;

hence ( (X_axis h1) . 1 <= (X_axis h1) . i & (X_axis h1) . i <= (X_axis h1) . (len h1) ) by A79, A87, A86; :: thesis: verum

A89: for i being Nat st i in dom h1 holds

( q1 `2 <= (h1 /. i) `2 & (h1 /. i) `2 <= q2 `2 )

proof

for i being Nat st i in dom (Y_axis h1) holds
let i be Nat; :: thesis: ( i in dom h1 implies ( q1 `2 <= (h1 /. i) `2 & (h1 /. i) `2 <= q2 `2 ) )

A90: rng f = [#] ((TOP-REAL 2) | P) by A13, TOPS_2:def 5

.= P by PRE_TOPC:def 5 ;

assume A91: i in dom h1 ; :: thesis: ( q1 `2 <= (h1 /. i) `2 & (h1 /. i) `2 <= q2 `2 )

then h1 . i = f1 . (h . i) by A35;

then A92: h1 /. i = f1 . (h . i) by A91, PARTFUN1:def 6;

i in Seg (len h1) by A91, FINSEQ_1:def 3;

then i in dom h by A34, FINSEQ_1:def 3;

then A93: h . i in rng h by FUNCT_1:def 3;

dom f1 = [#] I[01] by A13, A16, TOPS_2:def 5

.= the carrier of I[01] ;

then h1 /. i in rng f by A16, A31, A92, A93, FUNCT_1:def 3;

hence ( q1 `2 <= (h1 /. i) `2 & (h1 /. i) `2 <= q2 `2 ) by A5, A90; :: thesis: verum

end;A90: rng f = [#] ((TOP-REAL 2) | P) by A13, TOPS_2:def 5

.= P by PRE_TOPC:def 5 ;

assume A91: i in dom h1 ; :: thesis: ( q1 `2 <= (h1 /. i) `2 & (h1 /. i) `2 <= q2 `2 )

then h1 . i = f1 . (h . i) by A35;

then A92: h1 /. i = f1 . (h . i) by A91, PARTFUN1:def 6;

i in Seg (len h1) by A91, FINSEQ_1:def 3;

then i in dom h by A34, FINSEQ_1:def 3;

then A93: h . i in rng h by FUNCT_1:def 3;

dom f1 = [#] I[01] by A13, A16, TOPS_2:def 5

.= the carrier of I[01] ;

then h1 /. i in rng f by A16, A31, A92, A93, FUNCT_1:def 3;

hence ( q1 `2 <= (h1 /. i) `2 & (h1 /. i) `2 <= q2 `2 ) by A5, A90; :: thesis: verum

( q1 `2 <= (Y_axis h1) . i & (Y_axis h1) . i <= q2 `2 )

proof

then
Y_axis h1 lies_between q1 `2 ,q2 `2
by GOBOARD4:def 2;
let i be Nat; :: thesis: ( i in dom (Y_axis h1) implies ( q1 `2 <= (Y_axis h1) . i & (Y_axis h1) . i <= q2 `2 ) )

assume i in dom (Y_axis h1) ; :: thesis: ( q1 `2 <= (Y_axis h1) . i & (Y_axis h1) . i <= q2 `2 )

then i in Seg (len (Y_axis h1)) by FINSEQ_1:def 3;

then i in Seg (len h1) by A42, Th41;

then A94: i in dom h1 by FINSEQ_1:def 3;

then (Y_axis h1) . i = (h1 /. i) `2 by Th42;

hence ( q1 `2 <= (Y_axis h1) . i & (Y_axis h1) . i <= q2 `2 ) by A89, A94; :: thesis: verum

end;assume i in dom (Y_axis h1) ; :: thesis: ( q1 `2 <= (Y_axis h1) . i & (Y_axis h1) . i <= q2 `2 )

then i in Seg (len (Y_axis h1)) by FINSEQ_1:def 3;

then i in Seg (len h1) by A42, Th41;

then A94: i in dom h1 by FINSEQ_1:def 3;

then (Y_axis h1) . i = (h1 /. i) `2 by Th42;

hence ( q1 `2 <= (Y_axis h1) . i & (Y_axis h1) . i <= q2 `2 ) by A89, A94; :: thesis: verum

then consider f2 being FinSequence of (TOP-REAL 2) such that

A95: f2 is special and

A96: f2 . 1 = h1 . 1 and

A97: f2 . (len f2) = h1 . (len h1) and

A98: len f2 >= len h1 and

A99: ( X_axis f2 lies_between (X_axis h1) . 1,(X_axis h1) . (len h1) & Y_axis f2 lies_between q1 `2 ,q2 `2 ) and

A100: for j being Nat st j in dom f2 holds

ex k being Nat st

( k in dom h1 & |.((f2 /. j) - (h1 /. k)).| < (min_dist_min (P9,Q9)) / 5 ) and

A101: for j being Nat st 1 <= j & j + 1 <= len f2 holds

|.((f2 /. j) - (f2 /. (j + 1))).| < (min_dist_min (P9,Q9)) / 5 by A21, A44, A42, A88, Th38;

A102: len f2 >= 1 by A42, A98, XXREAL_0:2;

then A103: f2 . (len f2) = f2 /. (len f2) by FINSEQ_4:15;

deffunc H

ex h29 being FinSequence st

( len h29 = len hb & ( for i being Nat st i in dom h29 holds

h29 . i = H

then consider h29 being FinSequence such that

A104: len h29 = len hb and

A105: for i being Nat st i in dom h29 holds

h29 . i = g1 . (hb . i) ;

rng h29 c= the carrier of (TOP-REAL 2)

proof

then reconsider h2 = h29 as FinSequence of (TOP-REAL 2) by FINSEQ_1:def 4;
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng h29 or y in the carrier of (TOP-REAL 2) )

assume y in rng h29 ; :: thesis: y in the carrier of (TOP-REAL 2)

then consider x being object such that

A106: x in dom h29 and

A107: y = h29 . x by FUNCT_1:def 3;

reconsider i = x as Element of NAT by A106;

dom h29 = Seg (len h29) by FINSEQ_1:def 3;

then i in dom hb by A104, A106, FINSEQ_1:def 3;

then A108: hb . i in rng hb by FUNCT_1:def 3;

A109: dom g1 = [#] I[01] by A7, A18, TOPS_2:def 5

.= the carrier of I[01] ;

A110: rng g = [#] ((TOP-REAL 2) | Q) by A7, TOPS_2:def 5

.= Q by PRE_TOPC:def 5 ;

h29 . i = g1 . (hb . i) by A105, A106;

then h29 . i in rng g by A18, A25, A108, A109, FUNCT_1:def 3;

hence y in the carrier of (TOP-REAL 2) by A107, A110; :: thesis: verum

end;assume y in rng h29 ; :: thesis: y in the carrier of (TOP-REAL 2)

then consider x being object such that

A106: x in dom h29 and

A107: y = h29 . x by FUNCT_1:def 3;

reconsider i = x as Element of NAT by A106;

dom h29 = Seg (len h29) by FINSEQ_1:def 3;

then i in dom hb by A104, A106, FINSEQ_1:def 3;

then A108: hb . i in rng hb by FUNCT_1:def 3;

A109: dom g1 = [#] I[01] by A7, A18, TOPS_2:def 5

.= the carrier of I[01] ;

A110: rng g = [#] ((TOP-REAL 2) | Q) by A7, TOPS_2:def 5

.= Q by PRE_TOPC:def 5 ;

h29 . i = g1 . (hb . i) by A105, A106;

then h29 . i in rng g by A18, A25, A108, A109, FUNCT_1:def 3;

hence y in the carrier of (TOP-REAL 2) by A107, A110; :: thesis: verum

A111: rng f = [#] ((TOP-REAL 2) | P) by A13, TOPS_2:def 5

.= P by PRE_TOPC:def 5 ;

A112: for i being Nat st 1 <= i & i + 1 <= len h2 holds

|.((h2 /. i) - (h2 /. (i + 1))).| < (min_dist_min (P9,Q9)) / 5

proof

A146:
1 <= len hb
by A24, XXREAL_0:2;
reconsider Qa = Q as Subset of (TOP-REAL 2) ;

reconsider W1 = Q as Subset of (Euclid 2) by TOPREAL3:8;

let i be Nat; :: thesis: ( 1 <= i & i + 1 <= len h2 implies |.((h2 /. i) - (h2 /. (i + 1))).| < (min_dist_min (P9,Q9)) / 5 )

assume that

A113: 1 <= i and

A114: i + 1 <= len h2 ; :: thesis: |.((h2 /. i) - (h2 /. (i + 1))).| < (min_dist_min (P9,Q9)) / 5

A115: Qa is compact by A2, JORDAN5A:1;

reconsider Qa = Qa as non empty Subset of (TOP-REAL 2) ;

A116: rng g = [#] ((TOP-REAL 2) | Q) by A7, TOPS_2:def 5

.= Q by PRE_TOPC:def 5 ;

set r1 = (((E-bound Qa) - (W-bound Qa)) + ((N-bound Qa) - (S-bound Qa))) + 1;

A117: for x, y being Point of (Euclid 2) st x in W1 & y in W1 holds

dist (x,y) <= (((E-bound Qa) - (W-bound Qa)) + ((N-bound Qa) - (S-bound Qa))) + 1

then ( S-bound Qa <= q1 `2 & q1 `2 <= N-bound Qa ) by A115, PSCOMP_1:24;

then S-bound Qa <= N-bound Qa by XXREAL_0:2;

then A126: 0 <= (N-bound Qa) - (S-bound Qa) by XREAL_1:48;

( W-bound Qa <= q1 `1 & q1 `1 <= E-bound Qa ) by A115, A125, PSCOMP_1:24;

then W-bound Qa <= E-bound Qa by XXREAL_0:2;

then 0 <= (E-bound Qa) - (W-bound Qa) by XREAL_1:48;

then A127: W1 is bounded by A126, A117, TBSP_1:def 7;

A128: dom g1 = [#] I[01] by A7, A18, TOPS_2:def 5

.= the carrier of I[01] ;

A129: 1 < i + 1 by A113, NAT_1:13;

then i + 1 in Seg (len hb) by A104, A114, FINSEQ_1:1;

then i + 1 in dom hb by FINSEQ_1:def 3;

then A130: hb . (i + 1) in rng hb by FUNCT_1:def 3;

A131: i < len h2 by A114, NAT_1:13;

then A132: hb . i = hb /. i by A104, A113, FINSEQ_4:15;

A133: i + 1 in dom h29 by A114, A129, FINSEQ_3:25;

then h29 . (i + 1) = g1 . (hb . (i + 1)) by A105;

then h29 . (i + 1) in rng g by A18, A25, A128, A130, FUNCT_1:def 3;

then A134: g1 . (hb . (i + 1)) is Element of (TOP-REAL 2) by A105, A133, A116;

A135: hb . (i + 1) = hb /. (i + 1) by A104, A114, A129, FINSEQ_4:15;

i in dom h29 by A113, A131, FINSEQ_3:25;

then A136: h29 . i = g1 . (hb . i) by A105;

i in Seg (len hb) by A104, A113, A131, FINSEQ_1:1;

then A137: i in dom hb by FINSEQ_1:def 3;

then A138: hb . i in rng hb by FUNCT_1:def 3;

then h29 . i in rng g by A18, A25, A136, A128, FUNCT_1:def 3;

then reconsider w1 = g1 . (hb . i), w2 = g1 . (hb . (i + 1)) as Point of (Euclid 2) by A136, A116, A134, TOPREAL3:8;

i + 1 in Seg (len hb) by A104, A114, A129, FINSEQ_1:1;

then A139: i + 1 in dom hb by FINSEQ_1:def 3;

then hb . (i + 1) in rng hb by FUNCT_1:def 3;

then reconsider R = [.(hb /. i),(hb /. (i + 1)).] as Subset of I[01] by A25, A138, A132, A135, BORSUK_1:40, XXREAL_2:def 12;

i < i + 1 by NAT_1:13;

then A140: hb /. i <= hb /. (i + 1) by A26, A137, A132, A139, A135, SEQM_3:def 1;

then hb . i in R by A132, XXREAL_1:1;

then A141: w1 in g1 .: R by A128, FUNCT_1:def 6;

hb . (i + 1) in R by A135, A140, XXREAL_1:1;

then A142: w2 in g1 .: R by A128, FUNCT_1:def 6;

reconsider W = g1 .: R as Subset of (Euclid 2) by TOPREAL3:8;

dom g1 = [#] I[01] by A7, A18, TOPS_2:def 5;

then Q = g1 .: [.0,1.] by A18, A116, BORSUK_1:40, RELAT_1:113;

then W is bounded by A127, BORSUK_1:40, RELAT_1:123, TBSP_1:14;

then A143: dist (w1,w2) <= diameter W by A141, A142, TBSP_1:def 8;

diameter W < (min_dist_min (P9,Q9)) / 5 by A27, A104, A113, A131;

then A144: dist (w1,w2) < (min_dist_min (P9,Q9)) / 5 by A143, XXREAL_0:2;

h2 . (i + 1) = h2 /. (i + 1) by A114, A129, FINSEQ_4:15;

then A145: h2 /. (i + 1) = g1 . (hb . (i + 1)) by A105, A133;

h2 /. i = g1 . (hb . i) by A113, A131, A136, FINSEQ_4:15;

hence |.((h2 /. i) - (h2 /. (i + 1))).| < (min_dist_min (P9,Q9)) / 5 by A145, A144, Th28; :: thesis: verum

end;reconsider W1 = Q as Subset of (Euclid 2) by TOPREAL3:8;

let i be Nat; :: thesis: ( 1 <= i & i + 1 <= len h2 implies |.((h2 /. i) - (h2 /. (i + 1))).| < (min_dist_min (P9,Q9)) / 5 )

assume that

A113: 1 <= i and

A114: i + 1 <= len h2 ; :: thesis: |.((h2 /. i) - (h2 /. (i + 1))).| < (min_dist_min (P9,Q9)) / 5

A115: Qa is compact by A2, JORDAN5A:1;

reconsider Qa = Qa as non empty Subset of (TOP-REAL 2) ;

A116: rng g = [#] ((TOP-REAL 2) | Q) by A7, TOPS_2:def 5

.= Q by PRE_TOPC:def 5 ;

set r1 = (((E-bound Qa) - (W-bound Qa)) + ((N-bound Qa) - (S-bound Qa))) + 1;

A117: for x, y being Point of (Euclid 2) st x in W1 & y in W1 holds

dist (x,y) <= (((E-bound Qa) - (W-bound Qa)) + ((N-bound Qa) - (S-bound Qa))) + 1

proof

A125:
q1 in Qa
by A2, TOPREAL1:1;
let x, y be Point of (Euclid 2); :: thesis: ( x in W1 & y in W1 implies dist (x,y) <= (((E-bound Qa) - (W-bound Qa)) + ((N-bound Qa) - (S-bound Qa))) + 1 )

assume that

A118: x in W1 and

A119: y in W1 ; :: thesis: dist (x,y) <= (((E-bound Qa) - (W-bound Qa)) + ((N-bound Qa) - (S-bound Qa))) + 1

reconsider pw1 = x, pw2 = y as Point of (TOP-REAL 2) by A118, A119;

A120: ( S-bound Qa <= pw2 `2 & pw2 `2 <= N-bound Qa ) by A115, A119, PSCOMP_1:24;

( S-bound Qa <= pw1 `2 & pw1 `2 <= N-bound Qa ) by A115, A118, PSCOMP_1:24;

then A121: |.((pw1 `2) - (pw2 `2)).| <= (N-bound Qa) - (S-bound Qa) by A120, Th27;

A122: ( W-bound Qa <= pw2 `1 & pw2 `1 <= E-bound Qa ) by A115, A119, PSCOMP_1:24;

( W-bound Qa <= pw1 `1 & pw1 `1 <= E-bound Qa ) by A115, A118, PSCOMP_1:24;

then |.((pw1 `1) - (pw2 `1)).| <= (E-bound Qa) - (W-bound Qa) by A122, Th27;

then A123: |.((pw1 `1) - (pw2 `1)).| + |.((pw1 `2) - (pw2 `2)).| <= ((E-bound Qa) - (W-bound Qa)) + ((N-bound Qa) - (S-bound Qa)) by A121, XREAL_1:7;

((E-bound Qa) - (W-bound Qa)) + ((N-bound Qa) - (S-bound Qa)) <= (((E-bound Qa) - (W-bound Qa)) + ((N-bound Qa) - (S-bound Qa))) + 1 by XREAL_1:29;

then A124: |.((pw1 `1) - (pw2 `1)).| + |.((pw1 `2) - (pw2 `2)).| <= (((E-bound Qa) - (W-bound Qa)) + ((N-bound Qa) - (S-bound Qa))) + 1 by A123, XXREAL_0:2;

( dist (x,y) = |.(pw1 - pw2).| & |.(pw1 - pw2).| <= |.((pw1 `1) - (pw2 `1)).| + |.((pw1 `2) - (pw2 `2)).| ) by Th28, Th32;

hence dist (x,y) <= (((E-bound Qa) - (W-bound Qa)) + ((N-bound Qa) - (S-bound Qa))) + 1 by A124, XXREAL_0:2; :: thesis: verum

end;assume that

A118: x in W1 and

A119: y in W1 ; :: thesis: dist (x,y) <= (((E-bound Qa) - (W-bound Qa)) + ((N-bound Qa) - (S-bound Qa))) + 1

reconsider pw1 = x, pw2 = y as Point of (TOP-REAL 2) by A118, A119;

A120: ( S-bound Qa <= pw2 `2 & pw2 `2 <= N-bound Qa ) by A115, A119, PSCOMP_1:24;

( S-bound Qa <= pw1 `2 & pw1 `2 <= N-bound Qa ) by A115, A118, PSCOMP_1:24;

then A121: |.((pw1 `2) - (pw2 `2)).| <= (N-bound Qa) - (S-bound Qa) by A120, Th27;

A122: ( W-bound Qa <= pw2 `1 & pw2 `1 <= E-bound Qa ) by A115, A119, PSCOMP_1:24;

( W-bound Qa <= pw1 `1 & pw1 `1 <= E-bound Qa ) by A115, A118, PSCOMP_1:24;

then |.((pw1 `1) - (pw2 `1)).| <= (E-bound Qa) - (W-bound Qa) by A122, Th27;

then A123: |.((pw1 `1) - (pw2 `1)).| + |.((pw1 `2) - (pw2 `2)).| <= ((E-bound Qa) - (W-bound Qa)) + ((N-bound Qa) - (S-bound Qa)) by A121, XREAL_1:7;

((E-bound Qa) - (W-bound Qa)) + ((N-bound Qa) - (S-bound Qa)) <= (((E-bound Qa) - (W-bound Qa)) + ((N-bound Qa) - (S-bound Qa))) + 1 by XREAL_1:29;

then A124: |.((pw1 `1) - (pw2 `1)).| + |.((pw1 `2) - (pw2 `2)).| <= (((E-bound Qa) - (W-bound Qa)) + ((N-bound Qa) - (S-bound Qa))) + 1 by A123, XXREAL_0:2;

( dist (x,y) = |.(pw1 - pw2).| & |.(pw1 - pw2).| <= |.((pw1 `1) - (pw2 `1)).| + |.((pw1 `2) - (pw2 `2)).| ) by Th28, Th32;

hence dist (x,y) <= (((E-bound Qa) - (W-bound Qa)) + ((N-bound Qa) - (S-bound Qa))) + 1 by A124, XXREAL_0:2; :: thesis: verum

then ( S-bound Qa <= q1 `2 & q1 `2 <= N-bound Qa ) by A115, PSCOMP_1:24;

then S-bound Qa <= N-bound Qa by XXREAL_0:2;

then A126: 0 <= (N-bound Qa) - (S-bound Qa) by XREAL_1:48;

( W-bound Qa <= q1 `1 & q1 `1 <= E-bound Qa ) by A115, A125, PSCOMP_1:24;

then W-bound Qa <= E-bound Qa by XXREAL_0:2;

then 0 <= (E-bound Qa) - (W-bound Qa) by XREAL_1:48;

then A127: W1 is bounded by A126, A117, TBSP_1:def 7;

A128: dom g1 = [#] I[01] by A7, A18, TOPS_2:def 5

.= the carrier of I[01] ;

A129: 1 < i + 1 by A113, NAT_1:13;

then i + 1 in Seg (len hb) by A104, A114, FINSEQ_1:1;

then i + 1 in dom hb by FINSEQ_1:def 3;

then A130: hb . (i + 1) in rng hb by FUNCT_1:def 3;

A131: i < len h2 by A114, NAT_1:13;

then A132: hb . i = hb /. i by A104, A113, FINSEQ_4:15;

A133: i + 1 in dom h29 by A114, A129, FINSEQ_3:25;

then h29 . (i + 1) = g1 . (hb . (i + 1)) by A105;

then h29 . (i + 1) in rng g by A18, A25, A128, A130, FUNCT_1:def 3;

then A134: g1 . (hb . (i + 1)) is Element of (TOP-REAL 2) by A105, A133, A116;

A135: hb . (i + 1) = hb /. (i + 1) by A104, A114, A129, FINSEQ_4:15;

i in dom h29 by A113, A131, FINSEQ_3:25;

then A136: h29 . i = g1 . (hb . i) by A105;

i in Seg (len hb) by A104, A113, A131, FINSEQ_1:1;

then A137: i in dom hb by FINSEQ_1:def 3;

then A138: hb . i in rng hb by FUNCT_1:def 3;

then h29 . i in rng g by A18, A25, A136, A128, FUNCT_1:def 3;

then reconsider w1 = g1 . (hb . i), w2 = g1 . (hb . (i + 1)) as Point of (Euclid 2) by A136, A116, A134, TOPREAL3:8;

i + 1 in Seg (len hb) by A104, A114, A129, FINSEQ_1:1;

then A139: i + 1 in dom hb by FINSEQ_1:def 3;

then hb . (i + 1) in rng hb by FUNCT_1:def 3;

then reconsider R = [.(hb /. i),(hb /. (i + 1)).] as Subset of I[01] by A25, A138, A132, A135, BORSUK_1:40, XXREAL_2:def 12;

i < i + 1 by NAT_1:13;

then A140: hb /. i <= hb /. (i + 1) by A26, A137, A132, A139, A135, SEQM_3:def 1;

then hb . i in R by A132, XXREAL_1:1;

then A141: w1 in g1 .: R by A128, FUNCT_1:def 6;

hb . (i + 1) in R by A135, A140, XXREAL_1:1;

then A142: w2 in g1 .: R by A128, FUNCT_1:def 6;

reconsider W = g1 .: R as Subset of (Euclid 2) by TOPREAL3:8;

dom g1 = [#] I[01] by A7, A18, TOPS_2:def 5;

then Q = g1 .: [.0,1.] by A18, A116, BORSUK_1:40, RELAT_1:113;

then W is bounded by A127, BORSUK_1:40, RELAT_1:123, TBSP_1:14;

then A143: dist (w1,w2) <= diameter W by A141, A142, TBSP_1:def 8;

diameter W < (min_dist_min (P9,Q9)) / 5 by A27, A104, A113, A131;

then A144: dist (w1,w2) < (min_dist_min (P9,Q9)) / 5 by A143, XXREAL_0:2;

h2 . (i + 1) = h2 /. (i + 1) by A114, A129, FINSEQ_4:15;

then A145: h2 /. (i + 1) = g1 . (hb . (i + 1)) by A105, A133;

h2 /. i = g1 . (hb . i) by A113, A131, A136, FINSEQ_4:15;

hence |.((h2 /. i) - (h2 /. (i + 1))).| < (min_dist_min (P9,Q9)) / 5 by A145, A144, Th28; :: thesis: verum

then A147: len hb in dom hb by FINSEQ_3:25;

A148: 1 <= len hb by A24, XXREAL_0:2;

then A149: h2 . (len h2) = h2 /. (len h2) by A104, FINSEQ_4:15;

A150: dom hb = Seg (len hb) by FINSEQ_1:def 3;

A151: for i being Nat st i in dom hb holds

h2 /. i = g1 . (hb . i)

proof

A154:
f2 . 1 = f2 /. 1
by A102, FINSEQ_4:15;
let i be Nat; :: thesis: ( i in dom hb implies h2 /. i = g1 . (hb . i) )

assume A152: i in dom hb ; :: thesis: h2 /. i = g1 . (hb . i)

then i in dom h29 by A104, FINSEQ_3:29;

then A153: h2 . i = g1 . (hb . i) by A105;

( 1 <= i & i <= len hb ) by A150, A152, FINSEQ_1:1;

hence h2 /. i = g1 . (hb . i) by A104, A153, FINSEQ_4:15; :: thesis: verum

end;assume A152: i in dom hb ; :: thesis: h2 /. i = g1 . (hb . i)

then i in dom h29 by A104, FINSEQ_3:29;

then A153: h2 . i = g1 . (hb . i) by A105;

( 1 <= i & i <= len hb ) by A150, A152, FINSEQ_1:1;

hence h2 /. i = g1 . (hb . i) by A104, A153, FINSEQ_4:15; :: thesis: verum

A155: 1 <= len h by A30, XXREAL_0:2;

then 1 in dom h19 by A34, FINSEQ_3:25;

then A156: h1 /. 1 = f1 . (h . 1) by A35, A43;

len h in dom h19 by A34, A155, FINSEQ_3:25;

then A157: f2 /. 1 <> f2 /. (len f2) by A1, A14, A15, A16, A28, A29, A34, A35, A96, A97, A43, A154, A103, A156, JORDAN6:37;

5 <= len f2 by A30, A34, A98, XXREAL_0:2;

then A158: 2 <= len f2 by XXREAL_0:2;

A159: h1 . (len h1) = h1 /. (len h1) by A42, FINSEQ_4:15;

then A160: (X_axis f2) . (len f2) = (h1 /. (len h1)) `1 by A97, A102, A103, Th40

.= (X_axis h1) . (len h1) by A42, Th40 ;

A161: h2 . 1 = h2 /. 1 by A148, A104, FINSEQ_4:15;

A162: len h2 >= 1 by A24, A104, XXREAL_0:2;

A163: for i being Nat st i in dom h2 holds

( (h2 /. 1) `2 <= (h2 /. i) `2 & (h2 /. i) `2 <= (h2 /. (len h2)) `2 )

proof

for i being Nat st i in dom (Y_axis h2) holds
let i be Nat; :: thesis: ( i in dom h2 implies ( (h2 /. 1) `2 <= (h2 /. i) `2 & (h2 /. i) `2 <= (h2 /. (len h2)) `2 ) )

assume i in dom h2 ; :: thesis: ( (h2 /. 1) `2 <= (h2 /. i) `2 & (h2 /. i) `2 <= (h2 /. (len h2)) `2 )

then i in Seg (len h2) by FINSEQ_1:def 3;

then i in dom hb by A104, FINSEQ_1:def 3;

then A164: ( h2 /. i = g1 . (hb . i) & hb . i in rng hb ) by A151, FUNCT_1:def 3;

dom g1 = [#] I[01] by A7, A18, TOPS_2:def 5

.= the carrier of I[01] ;

then A165: h2 /. i in rng g by A18, A25, A164, FUNCT_1:def 3;

1 in Seg (len hb) by A104, A162, FINSEQ_1:1;

then 1 in dom hb by FINSEQ_1:def 3;

then A166: h2 /. 1 = g1 . (hb . 1) by A151;

len hb in Seg (len hb) by A104, A162, FINSEQ_1:1;

then len hb in dom hb by FINSEQ_1:def 3;

then A167: h2 /. (len h2) = g1 . (hb . (len hb)) by A104, A151;

rng g = [#] ((TOP-REAL 2) | Q) by A7, TOPS_2:def 5

.= Q by PRE_TOPC:def 5 ;

hence ( (h2 /. 1) `2 <= (h2 /. i) `2 & (h2 /. i) `2 <= (h2 /. (len h2)) `2 ) by A6, A8, A9, A18, A22, A23, A166, A167, A165; :: thesis: verum

end;assume i in dom h2 ; :: thesis: ( (h2 /. 1) `2 <= (h2 /. i) `2 & (h2 /. i) `2 <= (h2 /. (len h2)) `2 )

then i in Seg (len h2) by FINSEQ_1:def 3;

then i in dom hb by A104, FINSEQ_1:def 3;

then A164: ( h2 /. i = g1 . (hb . i) & hb . i in rng hb ) by A151, FUNCT_1:def 3;

dom g1 = [#] I[01] by A7, A18, TOPS_2:def 5

.= the carrier of I[01] ;

then A165: h2 /. i in rng g by A18, A25, A164, FUNCT_1:def 3;

1 in Seg (len hb) by A104, A162, FINSEQ_1:1;

then 1 in dom hb by FINSEQ_1:def 3;

then A166: h2 /. 1 = g1 . (hb . 1) by A151;

len hb in Seg (len hb) by A104, A162, FINSEQ_1:1;

then len hb in dom hb by FINSEQ_1:def 3;

then A167: h2 /. (len h2) = g1 . (hb . (len hb)) by A104, A151;

rng g = [#] ((TOP-REAL 2) | Q) by A7, TOPS_2:def 5

.= Q by PRE_TOPC:def 5 ;

hence ( (h2 /. 1) `2 <= (h2 /. i) `2 & (h2 /. i) `2 <= (h2 /. (len h2)) `2 ) by A6, A8, A9, A18, A22, A23, A166, A167, A165; :: thesis: verum

( (Y_axis h2) . 1 <= (Y_axis h2) . i & (Y_axis h2) . i <= (Y_axis h2) . (len h2) )

proof

then A170:
Y_axis h2 lies_between (Y_axis h2) . 1,(Y_axis h2) . (len h2)
by GOBOARD4:def 2;
let i be Nat; :: thesis: ( i in dom (Y_axis h2) implies ( (Y_axis h2) . 1 <= (Y_axis h2) . i & (Y_axis h2) . i <= (Y_axis h2) . (len h2) ) )

A168: ( (Y_axis h2) . 1 = (h2 /. 1) `2 & (Y_axis h2) . (len h2) = (h2 /. (len h2)) `2 ) by A162, Th41;

assume i in dom (Y_axis h2) ; :: thesis: ( (Y_axis h2) . 1 <= (Y_axis h2) . i & (Y_axis h2) . i <= (Y_axis h2) . (len h2) )

then i in Seg (len (Y_axis h2)) by FINSEQ_1:def 3;

then i in Seg (len h2) by A162, Th41;

then A169: i in dom h2 by FINSEQ_1:def 3;

then (Y_axis h2) . i = (h2 /. i) `2 by Th42;

hence ( (Y_axis h2) . 1 <= (Y_axis h2) . i & (Y_axis h2) . i <= (Y_axis h2) . (len h2) ) by A163, A169, A168; :: thesis: verum

end;A168: ( (Y_axis h2) . 1 = (h2 /. 1) `2 & (Y_axis h2) . (len h2) = (h2 /. (len h2)) `2 ) by A162, Th41;

assume i in dom (Y_axis h2) ; :: thesis: ( (Y_axis h2) . 1 <= (Y_axis h2) . i & (Y_axis h2) . i <= (Y_axis h2) . (len h2) )

then i in Seg (len (Y_axis h2)) by FINSEQ_1:def 3;

then i in Seg (len h2) by A162, Th41;

then A169: i in dom h2 by FINSEQ_1:def 3;

then (Y_axis h2) . i = (h2 /. i) `2 by Th42;

hence ( (Y_axis h2) . 1 <= (Y_axis h2) . i & (Y_axis h2) . i <= (Y_axis h2) . (len h2) ) by A163, A169, A168; :: thesis: verum

A171: for i being Nat st i in dom h2 holds

( p1 `1 <= (h2 /. i) `1 & (h2 /. i) `1 <= p2 `1 )

proof

for i being Nat st i in dom (X_axis h2) holds
let i be Nat; :: thesis: ( i in dom h2 implies ( p1 `1 <= (h2 /. i) `1 & (h2 /. i) `1 <= p2 `1 ) )

A172: rng g = [#] ((TOP-REAL 2) | Q) by A7, TOPS_2:def 5

.= Q by PRE_TOPC:def 5 ;

assume i in dom h2 ; :: thesis: ( p1 `1 <= (h2 /. i) `1 & (h2 /. i) `1 <= p2 `1 )

then i in Seg (len h2) by FINSEQ_1:def 3;

then i in dom hb by A104, FINSEQ_1:def 3;

then A173: ( h2 /. i = g1 . (hb . i) & hb . i in rng hb ) by A151, FUNCT_1:def 3;

dom g1 = [#] I[01] by A7, A18, TOPS_2:def 5

.= the carrier of I[01] ;

then h2 /. i in rng g by A18, A25, A173, FUNCT_1:def 3;

hence ( p1 `1 <= (h2 /. i) `1 & (h2 /. i) `1 <= p2 `1 ) by A4, A172; :: thesis: verum

end;A172: rng g = [#] ((TOP-REAL 2) | Q) by A7, TOPS_2:def 5

.= Q by PRE_TOPC:def 5 ;

assume i in dom h2 ; :: thesis: ( p1 `1 <= (h2 /. i) `1 & (h2 /. i) `1 <= p2 `1 )

then i in Seg (len h2) by FINSEQ_1:def 3;

then i in dom hb by A104, FINSEQ_1:def 3;

then A173: ( h2 /. i = g1 . (hb . i) & hb . i in rng hb ) by A151, FUNCT_1:def 3;

dom g1 = [#] I[01] by A7, A18, TOPS_2:def 5

.= the carrier of I[01] ;

then h2 /. i in rng g by A18, A25, A173, FUNCT_1:def 3;

hence ( p1 `1 <= (h2 /. i) `1 & (h2 /. i) `1 <= p2 `1 ) by A4, A172; :: thesis: verum

( p1 `1 <= (X_axis h2) . i & (X_axis h2) . i <= p2 `1 )

proof

then
X_axis h2 lies_between p1 `1 ,p2 `1
by GOBOARD4:def 2;
let i be Nat; :: thesis: ( i in dom (X_axis h2) implies ( p1 `1 <= (X_axis h2) . i & (X_axis h2) . i <= p2 `1 ) )

assume i in dom (X_axis h2) ; :: thesis: ( p1 `1 <= (X_axis h2) . i & (X_axis h2) . i <= p2 `1 )

then i in Seg (len (X_axis h2)) by FINSEQ_1:def 3;

then i in Seg (len h2) by A162, Th40;

then A174: i in dom h2 by FINSEQ_1:def 3;

then (X_axis h2) . i = (h2 /. i) `1 by Th42;

hence ( p1 `1 <= (X_axis h2) . i & (X_axis h2) . i <= p2 `1 ) by A171, A174; :: thesis: verum

end;assume i in dom (X_axis h2) ; :: thesis: ( p1 `1 <= (X_axis h2) . i & (X_axis h2) . i <= p2 `1 )

then i in Seg (len (X_axis h2)) by FINSEQ_1:def 3;

then i in Seg (len h2) by A162, Th40;

then A174: i in dom h2 by FINSEQ_1:def 3;

then (X_axis h2) . i = (h2 /. i) `1 by Th42;

hence ( p1 `1 <= (X_axis h2) . i & (X_axis h2) . i <= p2 `1 ) by A171, A174; :: thesis: verum

then consider g2 being FinSequence of (TOP-REAL 2) such that

A175: g2 is special and

A176: g2 . 1 = h2 . 1 and

A177: g2 . (len g2) = h2 . (len h2) and

A178: len g2 >= len h2 and

A179: ( Y_axis g2 lies_between (Y_axis h2) . 1,(Y_axis h2) . (len h2) & X_axis g2 lies_between p1 `1 ,p2 `1 ) and

A180: for j being Nat st j in dom g2 holds

ex k being Nat st

( k in dom h2 & |.((g2 /. j) - (h2 /. k)).| < (min_dist_min (P9,Q9)) / 5 ) and

A181: for j being Nat st 1 <= j & j + 1 <= len g2 holds

|.((g2 /. j) - (g2 /. (j + 1))).| < (min_dist_min (P9,Q9)) / 5 by A21, A162, A170, A112, Th39;

5 <= len g2 by A24, A104, A178, XXREAL_0:2;

then A182: 2 <= len g2 by XXREAL_0:2;

A183: len g2 >= 1 by A162, A178, XXREAL_0:2;

then g2 . 1 = g2 /. 1 by FINSEQ_4:15;

then A184: (Y_axis g2) . 1 = (h2 /. 1) `2 by A176, A183, A161, Th41

.= (Y_axis h2) . 1 by A162, Th41 ;

1 in dom hb by A146, FINSEQ_3:25;

then h2 /. 1 = g1 . (hb . 1) by A151;

then A185: g2 . 1 <> g2 . (len g2) by A2, A8, A9, A18, A22, A23, A104, A151, A176, A177, A161, A149, A147, JORDAN6:37;

len hb in dom hb by A148, FINSEQ_3:25;

then A186: g2 . (len g2) = q2 by A9, A18, A23, A104, A151, A177, A149;

g2 /. (len g2) = g2 . (len g2) by A183, FINSEQ_4:15;

then A187: (Y_axis g2) . (len g2) = q2 `2 by A183, A186, Th41;

1 in dom hb by A148, FINSEQ_3:25;

then A188: h2 /. 1 = q1 by A8, A18, A22, A151;

A189: rng g = [#] ((TOP-REAL 2) | Q) by A7, TOPS_2:def 5

.= Q by PRE_TOPC:def 5 ;

len h in dom h19 by A34, A42, FINSEQ_3:25;

then h1 /. (len h1) = p2 by A15, A16, A29, A34, A35, A159;

then A190: (X_axis f2) . (len f2) = p2 `1 by A97, A102, A159, A103, Th40;

1 in dom h19 by A42, FINSEQ_3:25;

then h1 . 1 = f1 . (h . 1) by A35;

then A191: (X_axis f2) . 1 = p1 `1 by A14, A16, A28, A96, A102, A154, Th40;

g2 . (len g2) = g2 /. (len g2) by A183, FINSEQ_4:15;

then A192: (Y_axis g2) . (len g2) = (h2 /. (len h2)) `2 by A177, A183, A149, Th41

.= (Y_axis h2) . (len h2) by A162, Th41 ;

g2 /. 1 = g2 . 1 by A183, FINSEQ_4:15;

then A193: (Y_axis g2) . 1 = q1 `2 by A176, A183, A188, A161, Th41;

(X_axis f2) . 1 = (h1 /. 1) `1 by A96, A102, A43, A154, Th40

.= (X_axis h1) . 1 by A42, Th40 ;

then L~ f2 meets L~ g2 by A95, A99, A175, A179, A154, A103, A191, A190, A193, A187, A160, A184, A192, A158, A182, A157, A185, Th26;

then consider s being object such that

A194: s in L~ f2 and

A195: s in L~ g2 by XBOOLE_0:3;

reconsider ps = s as Point of (TOP-REAL 2) by A194;

ps in union { (LSeg (g2,j)) where j is Nat : ( 1 <= j & j + 1 <= len g2 ) } by A195, TOPREAL1:def 4;

then consider y being set such that

A196: ( ps in y & y in { (LSeg (g2,j)) where j is Nat : ( 1 <= j & j + 1 <= len g2 ) } ) by TARSKI:def 4;

ps in union { (LSeg (f2,i)) where i is Nat : ( 1 <= i & i + 1 <= len f2 ) } by A194, TOPREAL1:def 4;

then consider x being set such that

A197: ( ps in x & x in { (LSeg (f2,i)) where i is Nat : ( 1 <= i & i + 1 <= len f2 ) } ) by TARSKI:def 4;

consider i being Nat such that

A198: x = LSeg (f2,i) and

A199: 1 <= i and

A200: i + 1 <= len f2 by A197;

LSeg (f2,i) = LSeg ((f2 /. i),(f2 /. (i + 1))) by A199, A200, TOPREAL1:def 3;

then A201: |.(ps - (f2 /. i)).| <= |.((f2 /. i) - (f2 /. (i + 1))).| by A197, A198, Th35;

i < len f2 by A200, NAT_1:13;

then i in dom f2 by A199, FINSEQ_3:25;

then consider k being Nat such that

A202: k in dom h1 and

A203: |.((f2 /. i) - (h1 /. k)).| < (min_dist_min (P9,Q9)) / 5 by A100;

k in dom h by A34, A202, FINSEQ_3:29;

then A204: h . k in rng h by FUNCT_1:def 3;

reconsider p11 = h1 /. k as Point of (TOP-REAL 2) ;

|.((f2 /. i) - (f2 /. (i + 1))).| < (min_dist_min (P9,Q9)) / 5 by A101, A199, A200;

then |.(ps - (f2 /. i)).| < (min_dist_min (P9,Q9)) / 5 by A201, XXREAL_0:2;

then ( |.(ps - (h1 /. k)).| <= |.(ps - (f2 /. i)).| + |.((f2 /. i) - (h1 /. k)).| & |.(ps - (f2 /. i)).| + |.((f2 /. i) - (h1 /. k)).| < ((min_dist_min (P9,Q9)) / 5) + ((min_dist_min (P9,Q9)) / 5) ) by A203, TOPRNS_1:34, XREAL_1:8;

then |.(ps - (h1 /. k)).| < ((min_dist_min (P9,Q9)) / 5) + ((min_dist_min (P9,Q9)) / 5) by XXREAL_0:2;

then A205: |.(p11 - ps).| < ((min_dist_min (P9,Q9)) / 5) + ((min_dist_min (P9,Q9)) / 5) by TOPRNS_1:27;

k in Seg (len h1) by A202, FINSEQ_1:def 3;

then ( 1 <= k & k <= len h1 ) by FINSEQ_1:1;

then h1 . k = h1 /. k by FINSEQ_4:15;

then A206: h1 /. k = f1 . (h . k) by A35, A202;

consider j being Nat such that

A207: y = LSeg (g2,j) and

A208: 1 <= j and

A209: j + 1 <= len g2 by A196;

LSeg (g2,j) = LSeg ((g2 /. j),(g2 /. (j + 1))) by A208, A209, TOPREAL1:def 3;

then A210: |.(ps - (g2 /. j)).| <= |.((g2 /. j) - (g2 /. (j + 1))).| by A196, A207, Th35;

j < len g2 by A209, NAT_1:13;

then j in Seg (len g2) by A208, FINSEQ_1:1;

then j in dom g2 by FINSEQ_1:def 3;

then consider k9 being Nat such that

A211: k9 in dom h2 and

A212: |.((g2 /. j) - (h2 /. k9)).| < (min_dist_min (P9,Q9)) / 5 by A180;

k9 in Seg (len h2) by A211, FINSEQ_1:def 3;

then A213: k9 in dom hb by A104, FINSEQ_1:def 3;

then A214: hb . k9 in rng hb by FUNCT_1:def 3;

reconsider q11 = h2 /. k9 as Point of (TOP-REAL 2) ;

|.((g2 /. j) - (g2 /. (j + 1))).| < (min_dist_min (P9,Q9)) / 5 by A181, A208, A209;

then |.(ps - (g2 /. j)).| < (min_dist_min (P9,Q9)) / 5 by A210, XXREAL_0:2;

then ( |.(ps - (h2 /. k9)).| <= |.(ps - (g2 /. j)).| + |.((g2 /. j) - (h2 /. k9)).| & |.(ps - (g2 /. j)).| + |.((g2 /. j) - (h2 /. k9)).| < ((min_dist_min (P9,Q9)) / 5) + ((min_dist_min (P9,Q9)) / 5) ) by A212, TOPRNS_1:34, XREAL_1:8;

then |.(ps - (h2 /. k9)).| < ((min_dist_min (P9,Q9)) / 5) + ((min_dist_min (P9,Q9)) / 5) by XXREAL_0:2;

then ( |.(p11 - q11).| <= |.(p11 - ps).| + |.(ps - q11).| & |.(p11 - ps).| + |.(ps - q11).| < (((min_dist_min (P9,Q9)) / 5) + ((min_dist_min (P9,Q9)) / 5)) + (((min_dist_min (P9,Q9)) / 5) + ((min_dist_min (P9,Q9)) / 5)) ) by A205, TOPRNS_1:34, XREAL_1:8;

then A215: |.(p11 - q11).| < ((((min_dist_min (P9,Q9)) / 5) + ((min_dist_min (P9,Q9)) / 5)) + ((min_dist_min (P9,Q9)) / 5)) + ((min_dist_min (P9,Q9)) / 5) by XXREAL_0:2;

h2 /. k9 = g1 . (hb . k9) by A151, A213;

then A216: h2 /. k9 in rng g by A18, A25, A214, A36, FUNCT_1:def 3;

reconsider x1 = p11, x2 = q11 as Point of (Euclid 2) by EUCLID:22;

dom f1 = [#] I[01] by A13, A16, TOPS_2:def 5

.= the carrier of I[01] ;

then h1 /. k in P by A16, A31, A206, A204, A111, FUNCT_1:def 3;

then min_dist_min (P9,Q9) <= dist (x1,x2) by A11, A12, A216, A189, WEIERSTR:34;

then min_dist_min (P9,Q9) <= |.(p11 - q11).| by Th28;

then min_dist_min (P9,Q9) < 4 * ((min_dist_min (P9,Q9)) / 5) by A215, XXREAL_0:2;

then (4 * ((min_dist_min (P9,Q9)) / 5)) - (5 * ((min_dist_min (P9,Q9)) / 5)) > 0 by XREAL_1:50;

then ((4 - 5) * ((min_dist_min (P9,Q9)) / 5)) / ((min_dist_min (P9,Q9)) / 5) > 0 by A21, XREAL_1:139;

then 4 - 5 > 0 by A20;

hence contradiction ; :: thesis: verum