:: JGRAPH_8 semantic presentation begin Lm1: I[01] = TopSpaceMetr (Closed-Interval-MSpace (0,1)) by TOPMETR:20, TOPMETR:def_7; Lm2: for x being set for f being FinSequence st 1 <= len f holds ( (f ^ <*x*>) . 1 = f . 1 & (<*x*> ^ f) . ((len f) + 1) = f . (len f) ) proof let x be set ; ::_thesis: for f being FinSequence st 1 <= len f holds ( (f ^ <*x*>) . 1 = f . 1 & (<*x*> ^ f) . ((len f) + 1) = f . (len f) ) let f be FinSequence; ::_thesis: ( 1 <= len f implies ( (f ^ <*x*>) . 1 = f . 1 & (<*x*> ^ f) . ((len f) + 1) = f . (len f) ) ) assume A1: 1 <= len f ; ::_thesis: ( (f ^ <*x*>) . 1 = f . 1 & (<*x*> ^ f) . ((len f) + 1) = f . (len f) ) then A2: len f in dom f by FINSEQ_3:25; A3: (<*x*> ^ f) . ((len f) + 1) = (<*x*> ^ f) . ((len <*x*>) + (len f)) by FINSEQ_1:39 .= f . (len f) by A2, FINSEQ_1:def_7 ; 1 in dom f by A1, FINSEQ_3:25; hence ( (f ^ <*x*>) . 1 = f . 1 & (<*x*> ^ f) . ((len f) + 1) = f . (len f) ) by A3, FINSEQ_1:def_7; ::_thesis: verum end; Lm3: for f being FinSequence of REAL st ( for k being Element of NAT st 1 <= k & k < len f holds f /. k < f /. (k + 1) ) holds f is increasing proof let f be FinSequence of REAL ; ::_thesis: ( ( for k being Element of NAT st 1 <= k & k < len f holds f /. k < f /. (k + 1) ) implies f is increasing ) assume A1: for k being Element of NAT st 1 <= k & k < len f holds f /. k < f /. (k + 1) ; ::_thesis: f is increasing now__::_thesis:_for_i,_j_being_Element_of_NAT_st_i_in_dom_f_&_j_in_dom_f_&_i_<_j_holds_ f_._i_<_f_._j let i, j be Element of NAT ; ::_thesis: ( i in dom f & j in dom f & i < j implies f . i < f . j ) now__::_thesis:_(_i_in_dom_f_&_j_in_dom_f_&_i_<_j_implies_f_._i_<_f_._j_) defpred S1[ Element of NAT ] means ( i + (1 + $1) <= len f implies f /. i < f /. (i + (1 + $1)) ); assume that A2: i in dom f and A3: j in dom f and A4: i < j ; ::_thesis: f . i < f . j A5: 1 <= i by A2, FINSEQ_3:25; A6: for k being Element of NAT st S1[k] holds S1[k + 1] proof let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] ) assume A7: ( i + (1 + k) <= len f implies f /. i < f /. (i + (1 + k)) ) ; ::_thesis: S1[k + 1] now__::_thesis:_(_i_+_(1_+_(k_+_1))_<=_len_f_implies_f_/._i_<_f_/._(i_+_(1_+_(k_+_1)))_) ( 1 <= i + 1 & i + 1 <= (i + 1) + k ) by NAT_1:11; then A8: 1 <= (i + 1) + k by XXREAL_0:2; A9: i + (1 + (k + 1)) = (i + (1 + k)) + 1 ; 1 + k < 1 + (k + 1) by NAT_1:13; then A10: i + (1 + k) < i + (1 + (k + 1)) by XREAL_1:6; assume A11: i + (1 + (k + 1)) <= len f ; ::_thesis: f /. i < f /. (i + (1 + (k + 1))) then i + (1 + k) < len f by A10, XXREAL_0:2; then f /. (i + (1 + k)) < f /. (i + (1 + (k + 1))) by A1, A8, A9; hence f /. i < f /. (i + (1 + (k + 1))) by A7, A11, A10, XXREAL_0:2; ::_thesis: verum end; hence S1[k + 1] ; ::_thesis: verum end; i + 1 <= j by A4, NAT_1:13; then j -' (i + 1) = j - (i + 1) by XREAL_1:233; then A12: i + (1 + (j -' (i + 1))) = j ; A13: f /. i = f . i by A2, PARTFUN1:def_6; A14: j <= len f by A3, FINSEQ_3:25; then i < len f by A4, XXREAL_0:2; then A15: S1[ 0 ] by A1, A5; for k being Element of NAT holds S1[k] from NAT_1:sch_1(A15, A6); then f /. i < f /. j by A14, A12; hence f . i < f . j by A3, A13, PARTFUN1:def_6; ::_thesis: verum end; hence ( i in dom f & j in dom f & i < j implies f . i < f . j ) ; ::_thesis: verum end; hence f is increasing by SEQM_3:def_1; ::_thesis: verum end; registration let a, b, c, d be real number ; cluster closed_inside_of_rectangle (a,b,c,d) -> convex ; coherence closed_inside_of_rectangle (a,b,c,d) is convex proof set P = closed_inside_of_rectangle (a,b,c,d); A1: closed_inside_of_rectangle (a,b,c,d) = { p where p is Point of (TOP-REAL 2) : ( a <= p `1 & p `1 <= b & c <= p `2 & p `2 <= d ) } by JGRAPH_6:def_2; let w1, w2 be Point of (TOP-REAL 2); :: according to JORDAN1:def_1 ::_thesis: ( not w1 in closed_inside_of_rectangle (a,b,c,d) or not w2 in closed_inside_of_rectangle (a,b,c,d) or LSeg (w1,w2) c= closed_inside_of_rectangle (a,b,c,d) ) assume ( w1 in closed_inside_of_rectangle (a,b,c,d) & w2 in closed_inside_of_rectangle (a,b,c,d) ) ; ::_thesis: LSeg (w1,w2) c= closed_inside_of_rectangle (a,b,c,d) then A2: ( ex p3 being Point of (TOP-REAL 2) st ( p3 = w1 & a <= p3 `1 & p3 `1 <= b & c <= p3 `2 & p3 `2 <= d ) & ex p4 being Point of (TOP-REAL 2) st ( p4 = w2 & a <= p4 `1 & p4 `1 <= b & c <= p4 `2 & p4 `2 <= d ) ) by A1; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in LSeg (w1,w2) or x in closed_inside_of_rectangle (a,b,c,d) ) assume x in LSeg (w1,w2) ; ::_thesis: x in closed_inside_of_rectangle (a,b,c,d) then consider l being Real such that A3: x = ((1 - l) * w1) + (l * w2) and A4: ( 0 <= l & l <= 1 ) ; set w = ((1 - l) * w1) + (l * w2); A5: ((1 - l) * w1) + (l * w2) = |[((((1 - l) * w1) `1) + ((l * w2) `1)),((((1 - l) * w1) `2) + ((l * w2) `2))]| by EUCLID:55; A6: l * w2 = |[(l * (w2 `1)),(l * (w2 `2))]| by EUCLID:57; then A7: (l * w2) `2 = l * (w2 `2) by EUCLID:52; A8: (1 - l) * w1 = |[((1 - l) * (w1 `1)),((1 - l) * (w1 `2))]| by EUCLID:57; then ((1 - l) * w1) `2 = (1 - l) * (w1 `2) by EUCLID:52; then (((1 - l) * w1) + (l * w2)) `2 = ((1 - l) * (w1 `2)) + (l * (w2 `2)) by A5, A7, EUCLID:52; then A9: ( c <= (((1 - l) * w1) + (l * w2)) `2 & (((1 - l) * w1) + (l * w2)) `2 <= d ) by A2, A4, XREAL_1:173, XREAL_1:174; A10: (l * w2) `1 = l * (w2 `1) by A6, EUCLID:52; ((1 - l) * w1) `1 = (1 - l) * (w1 `1) by A8, EUCLID:52; then (((1 - l) * w1) + (l * w2)) `1 = ((1 - l) * (w1 `1)) + (l * (w2 `1)) by A5, A10, EUCLID:52; then ( a <= (((1 - l) * w1) + (l * w2)) `1 & (((1 - l) * w1) + (l * w2)) `1 <= b ) by A2, A4, XREAL_1:173, XREAL_1:174; hence x in closed_inside_of_rectangle (a,b,c,d) by A1, A3, A9; ::_thesis: verum end; end; registration let a, b, c, d be real number ; cluster Trectangle (a,b,c,d) -> convex ; coherence Trectangle (a,b,c,d) is convex proof set T = Trectangle (a,b,c,d); thus [#] (Trectangle (a,b,c,d)) is convex Subset of (TOP-REAL 2) by PRE_TOPC:8; :: according to TOPALG_2:def_1 ::_thesis: verum end; end; theorem Th1: :: JGRAPH_8:1 for n being Element of NAT for e being real positive number for g being continuous Function of I[01],(TOP-REAL n) ex h being FinSequence of REAL st ( h . 1 = 0 & h . (len h) = 1 & 5 <= len h & rng h c= the carrier of I[01] & h is increasing & ( for i being Element of NAT for Q being Subset of I[01] for W being Subset of (Euclid n) st 1 <= i & i < len h & Q = [.(h /. i),(h /. (i + 1)).] & W = g .: Q holds diameter W < e ) ) proof let n be Element of NAT ; ::_thesis: for e being real positive number for g being continuous Function of I[01],(TOP-REAL n) ex h being FinSequence of REAL st ( h . 1 = 0 & h . (len h) = 1 & 5 <= len h & rng h c= the carrier of I[01] & h is increasing & ( for i being Element of NAT for Q being Subset of I[01] for W being Subset of (Euclid n) st 1 <= i & i < len h & Q = [.(h /. i),(h /. (i + 1)).] & W = g .: Q holds diameter W < e ) ) 1 in { r where r is Real : ( 0 <= r & r <= 1 ) } ; then A1: 1 in [.0,1.] by RCOMP_1:def_1; {1} c= [.0,1.] proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {1} or x in [.0,1.] ) assume x in {1} ; ::_thesis: x in [.0,1.] hence x in [.0,1.] by A1, TARSKI:def_1; ::_thesis: verum end; then A2: [.0,1.] \/ {1} = [.0,1.] by XBOOLE_1:12; Closed-Interval-TSpace (0,1) = TopSpaceMetr (Closed-Interval-MSpace (0,1)) by TOPMETR:def_7; then A3: the carrier of I[01] = the carrier of (Closed-Interval-MSpace (0,1)) by TOPMETR:12, TOPMETR:20 .= [.0,1.] by TOPMETR:10 ; let e be real positive number ; ::_thesis: for g being continuous Function of I[01],(TOP-REAL n) ex h being FinSequence of REAL st ( h . 1 = 0 & h . (len h) = 1 & 5 <= len h & rng h c= the carrier of I[01] & h is increasing & ( for i being Element of NAT for Q being Subset of I[01] for W being Subset of (Euclid n) st 1 <= i & i < len h & Q = [.(h /. i),(h /. (i + 1)).] & W = g .: Q holds diameter W < e ) ) let g be continuous Function of I[01],(TOP-REAL n); ::_thesis: ex h being FinSequence of REAL st ( h . 1 = 0 & h . (len h) = 1 & 5 <= len h & rng h c= the carrier of I[01] & h is increasing & ( for i being Element of NAT for Q being Subset of I[01] for W being Subset of (Euclid n) st 1 <= i & i < len h & Q = [.(h /. i),(h /. (i + 1)).] & W = g .: Q holds diameter W < e ) ) reconsider e = e as positive Real by XREAL_0:def_1; reconsider f = g as Function of (Closed-Interval-MSpace (0,1)),(Euclid n) by UNIFORM1:10; A4: e / 2 < e by XREAL_1:216; A5: e / 2 > 0 by XREAL_1:215; f is uniformly_continuous by UNIFORM1:8; then consider s1 being Real such that A6: 0 < s1 and A7: for u1, u2 being Element of (Closed-Interval-MSpace (0,1)) st dist (u1,u2) < s1 holds dist ((f /. u1),(f /. u2)) < e / 2 by A5, UNIFORM1:def_1; set s = min (s1,(1 / 2)); defpred S1[ Nat, set ] means $2 = ((min (s1,(1 / 2))) / 2) * ($1 - 1); A8: 0 <= min (s1,(1 / 2)) by A6, XXREAL_0:20; then reconsider j = [/(2 / (min (s1,(1 / 2))))\] as Element of NAT by INT_1:53; A9: 2 / (min (s1,(1 / 2))) <= j by INT_1:def_7; A10: min (s1,(1 / 2)) <= s1 by XXREAL_0:17; A11: for u1, u2 being Element of (Closed-Interval-MSpace (0,1)) st dist (u1,u2) < min (s1,(1 / 2)) holds dist ((f /. u1),(f /. u2)) < e / 2 proof let u1, u2 be Element of (Closed-Interval-MSpace (0,1)); ::_thesis: ( dist (u1,u2) < min (s1,(1 / 2)) implies dist ((f /. u1),(f /. u2)) < e / 2 ) assume dist (u1,u2) < min (s1,(1 / 2)) ; ::_thesis: dist ((f /. u1),(f /. u2)) < e / 2 then dist (u1,u2) < s1 by A10, XXREAL_0:2; hence dist ((f /. u1),(f /. u2)) < e / 2 by A7; ::_thesis: verum end; A12: 2 / (min (s1,(1 / 2))) <= [/(2 / (min (s1,(1 / 2))))\] by INT_1:def_7; then (2 / (min (s1,(1 / 2)))) - j <= 0 by XREAL_1:47; then 1 + ((2 / (min (s1,(1 / 2)))) - j) <= 1 + 0 by XREAL_1:6; then A13: ((min (s1,(1 / 2))) / 2) * (1 + ((2 / (min (s1,(1 / 2)))) - j)) <= ((min (s1,(1 / 2))) / 2) * 1 by A8, XREAL_1:64; A14: for k being Nat st k in Seg j holds ex x being set st S1[k,x] ; consider p being FinSequence such that A15: ( dom p = Seg j & ( for k being Nat st k in Seg j holds S1[k,p . k] ) ) from FINSEQ_1:sch_1(A14); A16: Seg (len p) = Seg j by A15, FINSEQ_1:def_3; rng (p ^ <*1*>) c= REAL proof let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng (p ^ <*1*>) or y in REAL ) A17: len (p ^ <*1*>) = (len p) + 1 by FINSEQ_2:16; assume y in rng (p ^ <*1*>) ; ::_thesis: y in REAL then consider x being set such that A18: x in dom (p ^ <*1*>) and A19: y = (p ^ <*1*>) . x by FUNCT_1:def_3; reconsider nx = x as Element of NAT by A18; A20: dom (p ^ <*1*>) = Seg (len (p ^ <*1*>)) by FINSEQ_1:def_3; then A21: 1 <= nx by A18, FINSEQ_1:1; A22: 1 <= nx by A18, A20, FINSEQ_1:1; A23: nx <= len (p ^ <*1*>) by A18, A20, FINSEQ_1:1; percases ( nx < (len p) + 1 or nx >= (len p) + 1 ) ; suppose nx < (len p) + 1 ; ::_thesis: y in REAL then A24: nx <= len p by NAT_1:13; then nx in Seg j by A16, A22, FINSEQ_1:1; then A25: p . nx = ((min (s1,(1 / 2))) / 2) * (nx - 1) by A15; y = p . nx by A19, A21, A24, FINSEQ_1:64; hence y in REAL by A25; ::_thesis: verum end; suppose nx >= (len p) + 1 ; ::_thesis: y in REAL then nx = (len p) + 1 by A23, A17, XXREAL_0:1; then y = 1 by A19, FINSEQ_1:42; hence y in REAL ; ::_thesis: verum end; end; end; then reconsider h1 = p ^ <*1*> as FinSequence of REAL by FINSEQ_1:def_4; A26: len h1 = (len p) + 1 by FINSEQ_2:16; A27: len p = j by A15, FINSEQ_1:def_3; A28: min (s1,(1 / 2)) <> 0 by A6, XXREAL_0:15; then 2 / (min (s1,(1 / 2))) >= 2 / (1 / 2) by A8, XREAL_1:118, XXREAL_0:17; then 4 <= j by A9, XXREAL_0:2; then A29: 4 + 1 <= (len p) + 1 by A27, XREAL_1:6; A30: (min (s1,(1 / 2))) / 2 > 0 by A8, A28, XREAL_1:215; A31: for i being Element of NAT for r1, r2 being Real st 1 <= i & i < len p & r1 = p . i & r2 = p . (i + 1) holds ( r1 < r2 & r2 - r1 = (min (s1,(1 / 2))) / 2 ) proof let i be Element of NAT ; ::_thesis: for r1, r2 being Real st 1 <= i & i < len p & r1 = p . i & r2 = p . (i + 1) holds ( r1 < r2 & r2 - r1 = (min (s1,(1 / 2))) / 2 ) let r1, r2 be Real; ::_thesis: ( 1 <= i & i < len p & r1 = p . i & r2 = p . (i + 1) implies ( r1 < r2 & r2 - r1 = (min (s1,(1 / 2))) / 2 ) ) assume that A32: ( 1 <= i & i < len p ) and A33: r1 = p . i and A34: r2 = p . (i + 1) ; ::_thesis: ( r1 < r2 & r2 - r1 = (min (s1,(1 / 2))) / 2 ) ( 1 < i + 1 & i + 1 <= len p ) by A32, NAT_1:13; then i + 1 in Seg j by A16, FINSEQ_1:1; then A35: r2 = ((min (s1,(1 / 2))) / 2) * ((i + 1) - 1) by A15, A34; i < i + 1 by NAT_1:13; then A36: i - 1 < (i + 1) - 1 by XREAL_1:9; A37: i in Seg j by A16, A32, FINSEQ_1:1; then r1 = ((min (s1,(1 / 2))) / 2) * (i - 1) by A15, A33; hence r1 < r2 by A30, A35, A36, XREAL_1:68; ::_thesis: r2 - r1 = (min (s1,(1 / 2))) / 2 r2 - r1 = (((min (s1,(1 / 2))) / 2) * i) - (((min (s1,(1 / 2))) / 2) * (i - 1)) by A15, A33, A37, A35; hence r2 - r1 = (min (s1,(1 / 2))) / 2 ; ::_thesis: verum end; 0 < min (s1,(1 / 2)) by A6, A28, XXREAL_0:20; then 0 < j by A12, XREAL_1:139; then A38: 0 + 1 <= j by NAT_1:13; then 1 in Seg j by FINSEQ_1:1; then p . 1 = ((min (s1,(1 / 2))) / 2) * (1 - 1) by A15 .= 0 ; then A39: h1 . 1 = 0 by A38, A27, Lm2; 2 * (min (s1,(1 / 2))) <> 0 by A6, XXREAL_0:15; then A40: ( ((min (s1,(1 / 2))) / 2) * (2 / (min (s1,(1 / 2)))) = (2 * (min (s1,(1 / 2)))) / (2 * (min (s1,(1 / 2)))) & (2 * (min (s1,(1 / 2)))) / (2 * (min (s1,(1 / 2)))) = 1 ) by XCMPLX_1:60, XCMPLX_1:76; then A41: 1 - (((min (s1,(1 / 2))) / 2) * (j - 1)) = ((min (s1,(1 / 2))) / 2) * (1 + ((2 / (min (s1,(1 / 2)))) - [/(2 / (min (s1,(1 / 2))))\])) ; A42: for r1 being Real st r1 = p . (len p) holds 1 - r1 <= (min (s1,(1 / 2))) / 2 proof let r1 be Real; ::_thesis: ( r1 = p . (len p) implies 1 - r1 <= (min (s1,(1 / 2))) / 2 ) assume A43: r1 = p . (len p) ; ::_thesis: 1 - r1 <= (min (s1,(1 / 2))) / 2 len p in Seg j by A38, A27, FINSEQ_1:1; hence 1 - r1 <= (min (s1,(1 / 2))) / 2 by A13, A15, A27, A41, A43; ::_thesis: verum end; A44: for i being Element of NAT st 1 <= i & i < len h1 holds (h1 /. (i + 1)) - (h1 /. i) <= (min (s1,(1 / 2))) / 2 proof let i be Element of NAT ; ::_thesis: ( 1 <= i & i < len h1 implies (h1 /. (i + 1)) - (h1 /. i) <= (min (s1,(1 / 2))) / 2 ) assume that A45: 1 <= i and A46: i < len h1 ; ::_thesis: (h1 /. (i + 1)) - (h1 /. i) <= (min (s1,(1 / 2))) / 2 A47: i + 1 <= len h1 by A46, NAT_1:13; A48: i <= len p by A26, A46, NAT_1:13; A49: 1 < i + 1 by A45, NAT_1:13; percases ( i < len p or i >= len p ) ; supposeA50: i < len p ; ::_thesis: (h1 /. (i + 1)) - (h1 /. i) <= (min (s1,(1 / 2))) / 2 then i + 1 <= len p by NAT_1:13; then A51: h1 . (i + 1) = p . (i + 1) by A49, FINSEQ_1:64; A52: h1 . i = p . i by A45, A50, FINSEQ_1:64; ( h1 . i = h1 /. i & h1 . (i + 1) = h1 /. (i + 1) ) by A45, A46, A47, A49, FINSEQ_4:15; hence (h1 /. (i + 1)) - (h1 /. i) <= (min (s1,(1 / 2))) / 2 by A31, A45, A50, A52, A51; ::_thesis: verum end; suppose i >= len p ; ::_thesis: (h1 /. (i + 1)) - (h1 /. i) <= (min (s1,(1 / 2))) / 2 then A53: i = len p by A48, XXREAL_0:1; A54: h1 /. i = h1 . i by A45, A46, FINSEQ_4:15 .= p . i by A45, A48, FINSEQ_1:64 ; h1 /. (i + 1) = h1 . (i + 1) by A47, A49, FINSEQ_4:15 .= 1 by A53, FINSEQ_1:42 ; hence (h1 /. (i + 1)) - (h1 /. i) <= (min (s1,(1 / 2))) / 2 by A42, A53, A54; ::_thesis: verum end; end; end; [/(2 / (min (s1,(1 / 2))))\] < (2 / (min (s1,(1 / 2)))) + 1 by INT_1:def_7; then [/(2 / (min (s1,(1 / 2))))\] - 1 < ((2 / (min (s1,(1 / 2)))) + 1) - 1 by XREAL_1:9; then A55: ((min (s1,(1 / 2))) / 2) * (j - 1) < ((min (s1,(1 / 2))) / 2) * (2 / (min (s1,(1 / 2)))) by A30, XREAL_1:68; A56: for i being Element of NAT for r1 being Real st 1 <= i & i <= len p & r1 = p . i holds r1 < 1 proof let i be Element of NAT ; ::_thesis: for r1 being Real st 1 <= i & i <= len p & r1 = p . i holds r1 < 1 let r1 be Real; ::_thesis: ( 1 <= i & i <= len p & r1 = p . i implies r1 < 1 ) assume that A57: 1 <= i and A58: i <= len p and A59: r1 = p . i ; ::_thesis: r1 < 1 i - 1 <= j - 1 by A27, A58, XREAL_1:9; then A60: ((min (s1,(1 / 2))) / 2) * (i - 1) <= ((min (s1,(1 / 2))) / 2) * (j - 1) by A8, XREAL_1:64; i in Seg j by A16, A57, A58, FINSEQ_1:1; then r1 = ((min (s1,(1 / 2))) / 2) * (i - 1) by A15, A59; hence r1 < 1 by A55, A40, A60, XXREAL_0:2; ::_thesis: verum end; A61: for i being Element of NAT st 1 <= i & i < len h1 holds h1 /. i < h1 /. (i + 1) proof let i be Element of NAT ; ::_thesis: ( 1 <= i & i < len h1 implies h1 /. i < h1 /. (i + 1) ) assume that A62: 1 <= i and A63: i < len h1 ; ::_thesis: h1 /. i < h1 /. (i + 1) A64: i + 1 <= len h1 by A63, NAT_1:13; A65: 1 < i + 1 by A62, NAT_1:13; A66: i <= len p by A26, A63, NAT_1:13; percases ( i < len p or i >= len p ) ; supposeA67: i < len p ; ::_thesis: h1 /. i < h1 /. (i + 1) then i + 1 <= len p by NAT_1:13; then A68: h1 . (i + 1) = p . (i + 1) by A65, FINSEQ_1:64; A69: h1 . i = p . i by A62, A67, FINSEQ_1:64; ( h1 . i = h1 /. i & h1 . (i + 1) = h1 /. (i + 1) ) by A62, A63, A64, A65, FINSEQ_4:15; hence h1 /. i < h1 /. (i + 1) by A31, A62, A67, A69, A68; ::_thesis: verum end; suppose i >= len p ; ::_thesis: h1 /. i < h1 /. (i + 1) then A70: i = len p by A66, XXREAL_0:1; A71: h1 /. (i + 1) = h1 . (i + 1) by A64, A65, FINSEQ_4:15 .= 1 by A70, FINSEQ_1:42 ; h1 /. i = h1 . i by A62, A63, FINSEQ_4:15 .= p . i by A62, A66, FINSEQ_1:64 ; hence h1 /. i < h1 /. (i + 1) by A56, A62, A66, A71; ::_thesis: verum end; end; end; A72: dom g = the carrier of I[01] by FUNCT_2:def_1; A73: for i being Element of NAT for Q being Subset of I[01] for W being Subset of (Euclid n) st 1 <= i & i < len h1 & Q = [.(h1 /. i),(h1 /. (i + 1)).] & W = g .: Q holds diameter W < e proof let i be Element of NAT ; ::_thesis: for Q being Subset of I[01] for W being Subset of (Euclid n) st 1 <= i & i < len h1 & Q = [.(h1 /. i),(h1 /. (i + 1)).] & W = g .: Q holds diameter W < e let Q be Subset of I[01]; ::_thesis: for W being Subset of (Euclid n) st 1 <= i & i < len h1 & Q = [.(h1 /. i),(h1 /. (i + 1)).] & W = g .: Q holds diameter W < e let W be Subset of (Euclid n); ::_thesis: ( 1 <= i & i < len h1 & Q = [.(h1 /. i),(h1 /. (i + 1)).] & W = g .: Q implies diameter W < e ) assume that A74: ( 1 <= i & i < len h1 ) and A75: Q = [.(h1 /. i),(h1 /. (i + 1)).] and A76: W = g .: Q ; ::_thesis: diameter W < e h1 /. i < h1 /. (i + 1) by A61, A74; then A77: Q <> {} by A75, XXREAL_1:1; A78: for x, y being Point of (Euclid n) st x in W & y in W holds dist (x,y) <= e / 2 proof let x, y be Point of (Euclid n); ::_thesis: ( x in W & y in W implies dist (x,y) <= e / 2 ) assume that A79: x in W and A80: y in W ; ::_thesis: dist (x,y) <= e / 2 consider x3 being set such that A81: x3 in dom g and A82: x3 in Q and A83: x = g . x3 by A76, A79, FUNCT_1:def_6; reconsider x3 = x3 as Element of (Closed-Interval-MSpace (0,1)) by A81, Lm1, TOPMETR:12; reconsider r3 = x3 as Real by A75, A82; A84: (h1 /. (i + 1)) - (h1 /. i) <= (min (s1,(1 / 2))) / 2 by A44, A74; consider y3 being set such that A85: y3 in dom g and A86: y3 in Q and A87: y = g . y3 by A76, A80, FUNCT_1:def_6; reconsider y3 = y3 as Element of (Closed-Interval-MSpace (0,1)) by A85, Lm1, TOPMETR:12; reconsider s3 = y3 as Real by A75, A86; A88: ( f . x3 = f /. x3 & f . y3 = f /. y3 ) ; abs (r3 - s3) <= (h1 /. (i + 1)) - (h1 /. i) by A75, A82, A86, UNIFORM1:12; then abs (r3 - s3) <= (min (s1,(1 / 2))) / 2 by A84, XXREAL_0:2; then A89: dist (x3,y3) <= (min (s1,(1 / 2))) / 2 by HEINE:1; (min (s1,(1 / 2))) / 2 < min (s1,(1 / 2)) by A8, A28, XREAL_1:216; then dist (x3,y3) < min (s1,(1 / 2)) by A89, XXREAL_0:2; hence dist (x,y) <= e / 2 by A11, A83, A87, A88; ::_thesis: verum end; then W is bounded by A5, TBSP_1:def_7; then diameter W <= e / 2 by A72, A76, A77, A78, TBSP_1:def_8; hence diameter W < e by A4, XXREAL_0:2; ::_thesis: verum end; A90: rng p c= [.0,1.] proof let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng p or y in [.0,1.] ) assume y in rng p ; ::_thesis: y in [.0,1.] then consider x being set such that A91: x in dom p and A92: y = p . x by FUNCT_1:def_3; reconsider nx = x as Element of NAT by A91; A93: p . nx = ((min (s1,(1 / 2))) / 2) * (nx - 1) by A15, A91; then reconsider ry = p . nx as Real ; A94: x in Seg (len p) by A91, FINSEQ_1:def_3; then A95: 1 <= nx by FINSEQ_1:1; then A96: nx - 1 >= 1 - 1 by XREAL_1:9; nx <= len p by A94, FINSEQ_1:1; then ry < 1 by A56, A95; then y in { rs where rs is Real : ( 0 <= rs & rs <= 1 ) } by A8, A92, A93, A96; hence y in [.0,1.] by RCOMP_1:def_1; ::_thesis: verum end; rng <*1*> = {1} by FINSEQ_1:38; then rng h1 = (rng p) \/ {1} by FINSEQ_1:31; then A97: rng h1 c= [.0,1.] \/ {1} by A90, XBOOLE_1:13; h1 . (len h1) = 1 by A26, FINSEQ_1:42; hence ex h being FinSequence of REAL st ( h . 1 = 0 & h . (len h) = 1 & 5 <= len h & rng h c= the carrier of I[01] & h is increasing & ( for i being Element of NAT for Q being Subset of I[01] for W being Subset of (Euclid n) st 1 <= i & i < len h & Q = [.(h /. i),(h /. (i + 1)).] & W = g .: Q holds diameter W < e ) ) by A26, A29, A39, A2, A97, A3, A61, A73, Lm3; ::_thesis: verum end; theorem Th2: :: JGRAPH_8:2 for n being Element of NAT for p1, p2 being Point of (TOP-REAL n) for P being Subset of (TOP-REAL n) st P c= LSeg (p1,p2) & p1 in P & p2 in P & P is connected holds P = LSeg (p1,p2) proof let n be Element of NAT ; ::_thesis: for p1, p2 being Point of (TOP-REAL n) for P being Subset of (TOP-REAL n) st P c= LSeg (p1,p2) & p1 in P & p2 in P & P is connected holds P = LSeg (p1,p2) let p1, p2 be Point of (TOP-REAL n); ::_thesis: for P being Subset of (TOP-REAL n) st P c= LSeg (p1,p2) & p1 in P & p2 in P & P is connected holds P = LSeg (p1,p2) let P be Subset of (TOP-REAL n); ::_thesis: ( P c= LSeg (p1,p2) & p1 in P & p2 in P & P is connected implies P = LSeg (p1,p2) ) assume that A1: P c= LSeg (p1,p2) and A2: p1 in P and A3: p2 in P and A4: P is connected ; ::_thesis: P = LSeg (p1,p2) reconsider L = LSeg (p1,p2) as non empty Subset of (TOP-REAL n) by A1, A2; now__::_thesis:_LSeg_(p1,p2)_c=_P A5: the carrier of ((TOP-REAL n) | L) = [#] ((TOP-REAL n) | L) .= L by PRE_TOPC:def_5 ; then reconsider PX = P as Subset of ((TOP-REAL n) | L) by A1; assume not LSeg (p1,p2) c= P ; ::_thesis: contradiction then consider x0 being set such that A6: x0 in LSeg (p1,p2) and A7: not x0 in P by TARSKI:def_3; reconsider p0 = x0 as Point of (TOP-REAL n) by A6; A8: (LSeg (p0,p2)) \ {p0} c= LSeg (p0,p2) by XBOOLE_1:36; A9: p1 in LSeg (p1,p2) by RLTOPSP1:68; then reconsider PX1 = LSeg (p1,p0) as Subset of ((TOP-REAL n) | L) by A6, A5, TOPREAL1:6; A10: (LSeg (p1,p0)) \ {p0} c= LSeg (p1,p0) by XBOOLE_1:36; LSeg (p1,p0) c= L by A6, A9, TOPREAL1:6; then reconsider R1 = (LSeg (p1,p0)) \ {p0} as Subset of ((TOP-REAL n) | L) by A10, A5, XBOOLE_1:1; A11: (TOP-REAL n) | L is T_2 by TOPMETR:2; A12: p2 in LSeg (p1,p2) by RLTOPSP1:68; then LSeg (p0,p2) c= L by A6, TOPREAL1:6; then reconsider R2 = (LSeg (p0,p2)) \ {p0} as Subset of ((TOP-REAL n) | L) by A5, A8, XBOOLE_1:1; reconsider PX2 = LSeg (p0,p2) as Subset of ((TOP-REAL n) | L) by A6, A5, A12, TOPREAL1:6; A13: PX1 /\ PX2 = {p0} by A6, TOPREAL1:8; A14: R1 c= PX1 by XBOOLE_1:36; A15: now__::_thesis:_not_P_c=_R1 assume P c= R1 ; ::_thesis: contradiction then A16: p2 in R1 by A3; p2 in PX2 by RLTOPSP1:68; then p2 in PX1 /\ PX2 by A14, A16, XBOOLE_0:def_4; hence contradiction by A3, A7, A13, TARSKI:def_1; ::_thesis: verum end; A17: {p0} c= LSeg (p1,p0) proof let d be set ; :: according to TARSKI:def_3 ::_thesis: ( not d in {p0} or d in LSeg (p1,p0) ) assume d in {p0} ; ::_thesis: d in LSeg (p1,p0) then d = p0 by TARSKI:def_1; hence d in LSeg (p1,p0) by RLTOPSP1:68; ::_thesis: verum end; A18: {p0} c= LSeg (p0,p2) proof let d be set ; :: according to TARSKI:def_3 ::_thesis: ( not d in {p0} or d in LSeg (p0,p2) ) assume d in {p0} ; ::_thesis: d in LSeg (p0,p2) then d = p0 by TARSKI:def_1; hence d in LSeg (p0,p2) by RLTOPSP1:68; ::_thesis: verum end; PX2 is compact by COMPTS_1:19; then PX2 is closed by A11, COMPTS_1:7; then A19: Cl PX2 = PX2 by PRE_TOPC:22; A20: Cl R2 c= Cl PX2 by PRE_TOPC:19, XBOOLE_1:36; R1 /\ PX2 = (PX1 /\ PX2) \ {p0} by XBOOLE_1:49 .= {} by A13, XBOOLE_1:37 ; then R1 /\ (Cl R2) = {} by A19, A20, XBOOLE_1:3, XBOOLE_1:27; then A21: R1 misses Cl R2 by XBOOLE_0:def_7; A22: PX1 /\ PX2 = {p0} by A6, TOPREAL1:8; A23: R2 c= PX2 by XBOOLE_1:36; A24: now__::_thesis:_not_P_c=_R2 assume P c= R2 ; ::_thesis: contradiction then A25: p1 in R2 by A2; p1 in PX1 by RLTOPSP1:68; then p1 in PX1 /\ PX2 by A23, A25, XBOOLE_0:def_4; hence contradiction by A2, A7, A13, TARSKI:def_1; ::_thesis: verum end; PX1 is compact by COMPTS_1:19; then PX1 is closed by A11, COMPTS_1:7; then A26: Cl PX1 = PX1 by PRE_TOPC:22; A27: L = (LSeg (p1,p0)) \/ (LSeg (p0,p2)) by A6, TOPREAL1:5 .= (((LSeg (p1,p0)) \ {p0}) \/ {p0}) \/ (LSeg (p0,p2)) by A17, XBOOLE_1:45 .= ((LSeg (p1,p0)) \ {p0}) \/ ({p0} \/ (LSeg (p0,p2))) by XBOOLE_1:4 .= R1 \/ PX2 by A18, XBOOLE_1:12 .= R1 \/ ((PX2 \ {p0}) \/ {p0}) by A18, XBOOLE_1:45 .= (R1 \/ {p0}) \/ R2 by XBOOLE_1:4 ; A28: P c= R1 \/ R2 proof let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in P or z in R1 \/ R2 ) assume A29: z in P ; ::_thesis: z in R1 \/ R2 then ( z in R1 \/ {p0} or z in R2 ) by A1, A27, XBOOLE_0:def_3; then ( z in R1 or z in {p0} or z in R2 ) by XBOOLE_0:def_3; hence z in R1 \/ R2 by A7, A29, TARSKI:def_1, XBOOLE_0:def_3; ::_thesis: verum end; A30: Cl R1 c= Cl PX1 by PRE_TOPC:19, XBOOLE_1:36; PX1 /\ R2 = (PX1 /\ PX2) \ {p0} by XBOOLE_1:49 .= {} by A22, XBOOLE_1:37 ; then (Cl R1) /\ R2 = {} by A26, A30, XBOOLE_1:3, XBOOLE_1:27; then Cl R1 misses R2 by XBOOLE_0:def_7; then A31: R1,R2 are_separated by A21, CONNSP_1:def_1; PX is connected by A4, CONNSP_1:46; hence contradiction by A31, A28, A15, A24, CONNSP_1:16; ::_thesis: verum end; hence P = LSeg (p1,p2) by A1, XBOOLE_0:def_10; ::_thesis: verum end; theorem Th3: :: JGRAPH_8:3 for n being Element of NAT for p1, p2 being Point of (TOP-REAL n) for g being Path of p1,p2 st rng g c= LSeg (p1,p2) holds rng g = LSeg (p1,p2) proof let n be Element of NAT ; ::_thesis: for p1, p2 being Point of (TOP-REAL n) for g being Path of p1,p2 st rng g c= LSeg (p1,p2) holds rng g = LSeg (p1,p2) let p1, p2 be Point of (TOP-REAL n); ::_thesis: for g being Path of p1,p2 st rng g c= LSeg (p1,p2) holds rng g = LSeg (p1,p2) let g be Path of p1,p2; ::_thesis: ( rng g c= LSeg (p1,p2) implies rng g = LSeg (p1,p2) ) assume A1: rng g c= LSeg (p1,p2) ; ::_thesis: rng g = LSeg (p1,p2) A2: p2 = g . 1 by BORSUK_2:def_4; A3: p1 = g . 0 by BORSUK_2:def_4; now__::_thesis:_LSeg_(p1,p2)_c=_rng_g A4: g .: ([#] I[01]) c= rng g proof let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in g .: ([#] I[01]) or y in rng g ) assume y in g .: ([#] I[01]) ; ::_thesis: y in rng g then ex x being set st ( x in dom g & x in [#] I[01] & y = g . x ) by FUNCT_1:def_6; hence y in rng g by FUNCT_1:def_3; ::_thesis: verum end; 1 in the carrier of I[01] by BORSUK_1:43; then 1 in dom g by FUNCT_2:def_1; then A5: p2 in g .: ([#] I[01]) by A2, FUNCT_1:def_6; 0 in the carrier of I[01] by BORSUK_1:43; then 0 in dom g by FUNCT_2:def_1; then A6: p1 in g .: ([#] I[01]) by A3, FUNCT_1:def_6; [#] I[01] is connected by CONNSP_1:27; then A7: g .: ([#] I[01]) is connected by TOPS_2:61; assume not LSeg (p1,p2) c= rng g ; ::_thesis: contradiction hence contradiction by A1, A7, A6, A5, A4, Th2, XBOOLE_1:1; ::_thesis: verum end; hence rng g = LSeg (p1,p2) by A1, XBOOLE_0:def_10; ::_thesis: verum end; theorem Th4: :: JGRAPH_8:4 for P, Q being non empty Subset of (TOP-REAL 2) for p1, p2, q1, q2 being Point of (TOP-REAL 2) for f being Path of p1,p2 for g being Path of q1,q2 st rng f = P & rng g = Q & ( 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 proof A1: TopStruct(# the carrier of (TOP-REAL 2), the topology of (TOP-REAL 2) #) = TopSpaceMetr (Euclid 2) by EUCLID:def_8; A2: [#] I[01] is compact by COMPTS_1:1; let P, Q be non empty Subset of (TOP-REAL 2); ::_thesis: for p1, p2, q1, q2 being Point of (TOP-REAL 2) for f being Path of p1,p2 for g being Path of q1,q2 st rng f = P & rng g = Q & ( 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: for f being Path of p1,p2 for g being Path of q1,q2 st rng f = P & rng g = Q & ( 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 f be Path of p1,p2; ::_thesis: for g being Path of q1,q2 st rng f = P & rng g = Q & ( 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 g be Path of q1,q2; ::_thesis: ( rng f = P & rng g = Q & ( 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 A3: rng f = P and A4: rng g = Q and A5: for p being Point of (TOP-REAL 2) st p in P holds ( p1 `1 <= p `1 & p `1 <= p2 `1 ) and A6: for p being Point of (TOP-REAL 2) st p in Q holds ( p1 `1 <= p `1 & p `1 <= p2 `1 ) and A7: for p being Point of (TOP-REAL 2) st p in P holds ( q1 `2 <= p `2 & p `2 <= q2 `2 ) and A8: 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 TopSpaceMetr (Euclid 2) = TopStruct(# the carrier of (TOP-REAL 2), the topology of (TOP-REAL 2) #) by EUCLID:def_8; then reconsider P9 = P, Q9 = Q as Subset of (TopSpaceMetr (Euclid 2)) ; set e = (min_dist_min (P9,Q9)) / 5; f .: the carrier of I[01] = rng f by RELSET_1:22; then P is compact by A3, A2, WEIERSTR:8; then A9: P9 is compact by A1, COMPTS_1:23; g .: ([#] I[01]) = rng g by RELSET_1:22; then Q is compact by A4, A2, WEIERSTR:8; then A10: Q9 is compact by A1, COMPTS_1:23; assume A11: P /\ Q = {} ; :: according to XBOOLE_0:def_7 ::_thesis: contradiction then P misses Q by XBOOLE_0:def_7; then A12: min_dist_min (P9,Q9) > 0 by A10, A9, JGRAPH_1:38; then A13: (min_dist_min (P9,Q9)) / 5 > 0 / 5 by XREAL_1:74; then consider h being FinSequence of REAL such that A14: h . 1 = 0 and A15: h . (len h) = 1 and A16: 5 <= len h and A17: rng h c= the carrier of I[01] and A18: h is increasing and A19: for i being Element of 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 = f .: R holds diameter W < (min_dist_min (P9,Q9)) / 5 by Th1; deffunc H1( Nat) -> set = f . (h . $1); ex h19 being FinSequence st ( len h19 = len h & ( for i being Nat st i in dom h19 holds h19 . i = H1(i) ) ) from FINSEQ_1:sch_2(); then consider h19 being FinSequence such that A20: len h19 = len h and A21: for i being Nat st i in dom h19 holds h19 . i = f . (h . i) ; A22: 1 <= len h by A16, XXREAL_0:2; then A23: len h in dom h19 by A20, FINSEQ_3:25; rng h19 c= the carrier of (TOP-REAL 2) proof let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng h19 or y in the carrier of (TOP-REAL 2) ) A24: dom f = the carrier of I[01] by FUNCT_2:def_1; assume y in rng h19 ; ::_thesis: y in the carrier of (TOP-REAL 2) then consider x being set such that A25: x in dom h19 and A26: y = h19 . x by FUNCT_1:def_3; reconsider i = x as Element of NAT by A25; dom h19 = Seg (len h19) by FINSEQ_1:def_3; then i in dom h by A20, A25, FINSEQ_1:def_3; then A27: h . i in rng h by FUNCT_1:def_3; h19 . i = f . (h . i) by A21, A25; then h19 . i in rng f by A17, A27, A24, FUNCT_1:def_3; hence y in the carrier of (TOP-REAL 2) by A26; ::_thesis: verum end; then reconsider h1 = h19 as FinSequence of (TOP-REAL 2) by FINSEQ_1:def_4; A28: len h1 >= 1 by A16, A20, XXREAL_0:2; then A29: h1 . 1 = h1 /. 1 by FINSEQ_4:15; A30: f . 0 = p1 by BORSUK_2:def_4; A31: for i being Element of NAT st 1 <= i & i + 1 <= len h1 holds |.((h1 /. i) - (h1 /. (i + 1))).| < (min_dist_min (P9,Q9)) / 5 proof reconsider Pa = P as Subset of (TOP-REAL 2) ; A32: dom f = the carrier of I[01] by FUNCT_2:def_1; reconsider W1 = P as Subset of (Euclid 2) by TOPREAL3:8; let i be Element of NAT ; ::_thesis: ( 1 <= i & i + 1 <= len h1 implies |.((h1 /. i) - (h1 /. (i + 1))).| < (min_dist_min (P9,Q9)) / 5 ) assume that A33: 1 <= i and A34: i + 1 <= len h1 ; ::_thesis: |.((h1 /. i) - (h1 /. (i + 1))).| < (min_dist_min (P9,Q9)) / 5 A35: 1 < i + 1 by A33, NAT_1:13; then A36: h . (i + 1) = h /. (i + 1) by A20, A34, FINSEQ_4:15; A37: i + 1 in dom h19 by A34, A35, FINSEQ_3:25; then A38: h19 . (i + 1) = f . (h . (i + 1)) by A21; then A39: h1 /. (i + 1) = f . (h . (i + 1)) by A34, A35, FINSEQ_4:15; set r1 = (((E-bound Pa) - (W-bound Pa)) + ((N-bound Pa) - (S-bound Pa))) + 1; ( [#] I[01] is compact & f .: the carrier of I[01] = rng f ) by COMPTS_1:1, RELSET_1:22; then A40: Pa is compact by A3, WEIERSTR:8; A41: 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 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 A42: x in W1 and A43: 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 A42, A43; A44: ( S-bound Pa <= pw2 `2 & pw2 `2 <= N-bound Pa ) by A40, A43, PSCOMP_1:24; ( S-bound Pa <= pw1 `2 & pw1 `2 <= N-bound Pa ) by A40, A42, PSCOMP_1:24; then A45: abs ((pw1 `2) - (pw2 `2)) <= (N-bound Pa) - (S-bound Pa) by A44, JGRAPH_1:27; A46: ((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; A47: ( W-bound Pa <= pw2 `1 & pw2 `1 <= E-bound Pa ) by A40, A43, PSCOMP_1:24; ( W-bound Pa <= pw1 `1 & pw1 `1 <= E-bound Pa ) by A40, A42, PSCOMP_1:24; then abs ((pw1 `1) - (pw2 `1)) <= (E-bound Pa) - (W-bound Pa) by A47, JGRAPH_1:27; then (abs ((pw1 `1) - (pw2 `1))) + (abs ((pw1 `2) - (pw2 `2))) <= ((E-bound Pa) - (W-bound Pa)) + ((N-bound Pa) - (S-bound Pa)) by A45, XREAL_1:7; then A48: (abs ((pw1 `1) - (pw2 `1))) + (abs ((pw1 `2) - (pw2 `2))) <= (((E-bound Pa) - (W-bound Pa)) + ((N-bound Pa) - (S-bound Pa))) + 1 by A46, XXREAL_0:2; ( dist (x,y) = |.(pw1 - pw2).| & |.(pw1 - pw2).| <= (abs ((pw1 `1) - (pw2 `1))) + (abs ((pw1 `2) - (pw2 `2))) ) by JGRAPH_1:28, JGRAPH_1:32; hence dist (x,y) <= (((E-bound Pa) - (W-bound Pa)) + ((N-bound Pa) - (S-bound Pa))) + 1 by A48, XXREAL_0:2; ::_thesis: verum end; i + 1 in dom h by A20, A34, A35, FINSEQ_3:25; then h . (i + 1) in rng h by FUNCT_1:def_3; then h19 . (i + 1) in rng f by A17, A38, A32, FUNCT_1:def_3; then A49: f . (h . (i + 1)) is Element of (TOP-REAL 2) by A21, A37; A50: i < len h1 by A34, NAT_1:13; then A51: h . i = h /. i by A20, A33, FINSEQ_4:15; A52: i in dom h by A20, A33, A50, FINSEQ_3:25; then A53: h . i in rng h by FUNCT_1:def_3; A54: i + 1 in dom h by A20, A34, A35, 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 A17, A53, A51, A36, BORSUK_1:40, XXREAL_2:def_12; A55: i in dom h19 by A33, A50, FINSEQ_3:25; then A56: h19 . i = f . (h . i) by A21; then h19 . i in rng f by A17, A53, A32, FUNCT_1:def_3; then f . (h . i) is Element of (TOP-REAL 2) by A21, A55; then reconsider w1 = f . (h . i), w2 = f . (h . (i + 1)) as Point of (Euclid 2) by A49, TOPREAL3:8; i < i + 1 by NAT_1:13; then A57: h /. i <= h /. (i + 1) by A18, A52, A51, A54, A36, SEQM_3:def_1; then h . i in R by A51, XXREAL_1:1; then A58: w1 in f .: R by A32, FUNCT_1:def_6; 0 in the carrier of I[01] by BORSUK_1:43; then A59: f . 0 in rng f by A32, FUNCT_1:def_3; then ( S-bound Pa <= p1 `2 & p1 `2 <= N-bound Pa ) by A3, A30, A40, PSCOMP_1:24; then S-bound Pa <= N-bound Pa by XXREAL_0:2; then A60: 0 <= (N-bound Pa) - (S-bound Pa) by XREAL_1:48; ( W-bound Pa <= p1 `1 & p1 `1 <= E-bound Pa ) by A3, A30, A40, A59, 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 A61: W1 is bounded by A60, A41, TBSP_1:def_7; h . (i + 1) in R by A36, A57, XXREAL_1:1; then A62: w2 in f .: R by A32, FUNCT_1:def_6; reconsider W = f .: R as Subset of (Euclid 2) by TOPREAL3:8; dom f = [#] I[01] by FUNCT_2:def_1; then P = f .: [.0,1.] by A3, BORSUK_1:40, RELAT_1:113; then W is bounded by A61, BORSUK_1:40, RELAT_1:123, TBSP_1:14; then A63: dist (w1,w2) <= diameter W by A58, A62, TBSP_1:def_8; diameter W < (min_dist_min (P9,Q9)) / 5 by A19, A20, A33, A50; then A64: dist (w1,w2) < (min_dist_min (P9,Q9)) / 5 by A63, XXREAL_0:2; h1 /. i = f . (h . i) by A33, A50, A56, FINSEQ_4:15; hence |.((h1 /. i) - (h1 /. (i + 1))).| < (min_dist_min (P9,Q9)) / 5 by A39, A64, JGRAPH_1:28; ::_thesis: verum end; A65: for i being Element of NAT st i in dom h1 holds ( q1 `2 <= (h1 /. i) `2 & (h1 /. i) `2 <= q2 `2 ) proof let i be Element of NAT ; ::_thesis: ( i in dom h1 implies ( q1 `2 <= (h1 /. i) `2 & (h1 /. i) `2 <= q2 `2 ) ) assume A66: i in dom h1 ; ::_thesis: ( q1 `2 <= (h1 /. i) `2 & (h1 /. i) `2 <= q2 `2 ) then h1 . i = f . (h . i) by A21; then A67: h1 /. i = f . (h . i) by A66, PARTFUN1:def_6; i in dom h by A20, A66, FINSEQ_3:29; then A68: h . i in rng h by FUNCT_1:def_3; dom f = the carrier of I[01] by FUNCT_2:def_1; then h1 /. i in rng f by A17, A67, A68, FUNCT_1:def_3; hence ( q1 `2 <= (h1 /. i) `2 & (h1 /. i) `2 <= q2 `2 ) by A3, A7; ::_thesis: verum end; for i being Element of NAT st i in dom (Y_axis h1) holds ( q1 `2 <= (Y_axis h1) . i & (Y_axis h1) . i <= q2 `2 ) proof let i be Element of 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 A28, JGRAPH_1:42; then A69: i in dom h1 by FINSEQ_1:def_3; then (Y_axis h1) . i = (h1 /. i) `2 by JGRAPH_1:43; hence ( q1 `2 <= (Y_axis h1) . i & (Y_axis h1) . i <= q2 `2 ) by A65, A69; ::_thesis: verum end; then A70: Y_axis h1 lies_between q1 `2 ,q2 `2 by GOBOARD4:def_2; A71: f . 1 = p2 by BORSUK_2:def_4; A72: for i being Element of NAT st i in dom h1 holds ( (h1 /. 1) `1 <= (h1 /. i) `1 & (h1 /. i) `1 <= (h1 /. (len h1)) `1 ) proof len h in dom h19 by A20, A28, FINSEQ_3:25; then h1 . (len h1) = f . (h . (len h)) by A20, A21; then A73: h1 /. (len h1) = f . (h . (len h)) by A28, FINSEQ_4:15; 1 in dom h19 by A28, FINSEQ_3:25; then h1 . 1 = f . (h . 1) by A21; then A74: h1 /. 1 = f . (h . 1) by A28, FINSEQ_4:15; let i be Element of NAT ; ::_thesis: ( i in dom h1 implies ( (h1 /. 1) `1 <= (h1 /. i) `1 & (h1 /. i) `1 <= (h1 /. (len h1)) `1 ) ) assume A75: i in dom h1 ; ::_thesis: ( (h1 /. 1) `1 <= (h1 /. i) `1 & (h1 /. i) `1 <= (h1 /. (len h1)) `1 ) then h1 . i = f . (h . i) by A21; then A76: h1 /. i = f . (h . i) by A75, PARTFUN1:def_6; i in dom h by A20, A75, FINSEQ_3:29; then A77: h . i in rng h by FUNCT_1:def_3; dom f = the carrier of I[01] by FUNCT_2:def_1; then h1 /. i in rng f by A17, A76, A77, FUNCT_1:def_3; hence ( (h1 /. 1) `1 <= (h1 /. i) `1 & (h1 /. i) `1 <= (h1 /. (len h1)) `1 ) by A3, A5, A30, A71, A14, A15, A74, A73; ::_thesis: verum end; for i being Element of NAT st i in dom (X_axis h1) holds ( (X_axis h1) . 1 <= (X_axis h1) . i & (X_axis h1) . i <= (X_axis h1) . (len h1) ) proof let i be Element of 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) ) ) A78: ( (X_axis h1) . 1 = (h1 /. 1) `1 & (X_axis h1) . (len h1) = (h1 /. (len h1)) `1 ) by A28, JGRAPH_1:41; 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 A28, JGRAPH_1:41; then A79: i in dom h1 by FINSEQ_1:def_3; then (X_axis h1) . i = (h1 /. i) `1 by JGRAPH_1:43; hence ( (X_axis h1) . 1 <= (X_axis h1) . i & (X_axis h1) . i <= (X_axis h1) . (len h1) ) by A72, A79, A78; ::_thesis: verum end; then X_axis h1 lies_between (X_axis h1) . 1,(X_axis h1) . (len h1) by GOBOARD4:def_2; then consider f2 being FinSequence of (TOP-REAL 2) such that A80: f2 is special and A81: f2 . 1 = h1 . 1 and A82: f2 . (len f2) = h1 . (len h1) and A83: len f2 >= len h1 and A84: ( X_axis f2 lies_between (X_axis h1) . 1,(X_axis h1) . (len h1) & Y_axis f2 lies_between q1 `2 ,q2 `2 ) and A85: for j being Element of NAT st j in dom f2 holds ex k being Element of NAT st ( k in dom h1 & |.((f2 /. j) - (h1 /. k)).| < (min_dist_min (P9,Q9)) / 5 ) and A86: for j being Element of NAT st 1 <= j & j + 1 <= len f2 holds |.((f2 /. j) - (f2 /. (j + 1))).| < (min_dist_min (P9,Q9)) / 5 by A13, A31, A28, A70, JGRAPH_1:39; A87: len f2 >= 1 by A28, A83, XXREAL_0:2; then A88: f2 . (len f2) = f2 /. (len f2) by FINSEQ_4:15; consider hb being FinSequence of REAL such that A89: hb . 1 = 0 and A90: hb . (len hb) = 1 and A91: 5 <= len hb and A92: rng hb c= the carrier of I[01] and A93: hb is increasing and A94: for i being Element of 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 = g .: R holds diameter W < (min_dist_min (P9,Q9)) / 5 by A13, Th1; deffunc H2( Nat) -> set = g . (hb . $1); ex h29 being FinSequence st ( len h29 = len hb & ( for i being Nat st i in dom h29 holds h29 . i = H2(i) ) ) from FINSEQ_1:sch_2(); then consider h29 being FinSequence such that A95: len h29 = len hb and A96: for i being Nat st i in dom h29 holds h29 . i = g . (hb . i) ; rng h29 c= the carrier of (TOP-REAL 2) proof let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng h29 or y in the carrier of (TOP-REAL 2) ) A97: dom g = the carrier of I[01] by FUNCT_2:def_1; assume y in rng h29 ; ::_thesis: y in the carrier of (TOP-REAL 2) then consider x being set such that A98: x in dom h29 and A99: y = h29 . x by FUNCT_1:def_3; reconsider i = x as Element of NAT by A98; dom h29 = Seg (len h29) by FINSEQ_1:def_3; then i in dom hb by A95, A98, FINSEQ_1:def_3; then A100: hb . i in rng hb by FUNCT_1:def_3; h29 . i = g . (hb . i) by A96, A98; then h29 . i in rng g by A92, A100, A97, FUNCT_1:def_3; hence y in the carrier of (TOP-REAL 2) by A99; ::_thesis: verum end; then reconsider h2 = h29 as FinSequence of (TOP-REAL 2) by FINSEQ_1:def_4; A101: len h2 >= 1 by A91, A95, XXREAL_0:2; 1 in dom h19 by A20, A22, FINSEQ_3:25; then A102: h1 /. 1 = f . (h . 1) by A21, A29; A103: 0 in the carrier of I[01] by BORSUK_1:43; then 0 in dom f by FUNCT_2:def_1; then A104: p1 in P9 by A3, A30, FUNCT_1:def_3; A105: 1 <= len hb by A91, XXREAL_0:2; then A106: h2 . (len h2) = h2 /. (len h2) by A95, FINSEQ_4:15; A107: g . 0 = q1 by BORSUK_2:def_4; A108: for i being Element of NAT st 1 <= i & i + 1 <= len h2 holds |.((h2 /. i) - (h2 /. (i + 1))).| < (min_dist_min (P9,Q9)) / 5 proof reconsider Qa = Q as Subset of (TOP-REAL 2) ; A109: dom g = the carrier of I[01] by FUNCT_2:def_1; reconsider W1 = Q as Subset of (Euclid 2) by TOPREAL3:8; let i be Element of NAT ; ::_thesis: ( 1 <= i & i + 1 <= len h2 implies |.((h2 /. i) - (h2 /. (i + 1))).| < (min_dist_min (P9,Q9)) / 5 ) assume that A110: 1 <= i and A111: i + 1 <= len h2 ; ::_thesis: |.((h2 /. i) - (h2 /. (i + 1))).| < (min_dist_min (P9,Q9)) / 5 A112: i < len h2 by A111, NAT_1:13; then A113: hb . i = hb /. i by A95, A110, FINSEQ_4:15; A114: 1 < i + 1 by A110, NAT_1:13; then i + 1 in Seg (len hb) by A95, A111, FINSEQ_1:1; then i + 1 in dom hb by FINSEQ_1:def_3; then A115: hb . (i + 1) in rng hb by FUNCT_1:def_3; A116: i + 1 in dom h29 by A111, A114, FINSEQ_3:25; then h29 . (i + 1) = g . (hb . (i + 1)) by A96; then h29 . (i + 1) in rng g by A92, A109, A115, FUNCT_1:def_3; then A117: g . (hb . (i + 1)) is Element of (TOP-REAL 2) by A96, A116; i in dom h29 by A110, A112, FINSEQ_3:25; then A118: h29 . i = g . (hb . i) by A96; ( [#] I[01] is compact & g .: the carrier of I[01] = rng g ) by COMPTS_1:1, RELSET_1:22; then A119: Qa is compact by A4, WEIERSTR:8; reconsider Qa = Qa as non empty Subset of (TOP-REAL 2) ; set r1 = (((E-bound Qa) - (W-bound Qa)) + ((N-bound Qa) - (S-bound Qa))) + 1; A120: hb . (i + 1) = hb /. (i + 1) by A95, A111, A114, FINSEQ_4:15; A121: 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 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 A122: x in W1 and A123: 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 A122, A123; A124: ( S-bound Qa <= pw2 `2 & pw2 `2 <= N-bound Qa ) by A119, A123, PSCOMP_1:24; ( S-bound Qa <= pw1 `2 & pw1 `2 <= N-bound Qa ) by A119, A122, PSCOMP_1:24; then A125: abs ((pw1 `2) - (pw2 `2)) <= (N-bound Qa) - (S-bound Qa) by A124, JGRAPH_1:27; A126: ((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; A127: ( W-bound Qa <= pw2 `1 & pw2 `1 <= E-bound Qa ) by A119, A123, PSCOMP_1:24; ( W-bound Qa <= pw1 `1 & pw1 `1 <= E-bound Qa ) by A119, A122, PSCOMP_1:24; then abs ((pw1 `1) - (pw2 `1)) <= (E-bound Qa) - (W-bound Qa) by A127, JGRAPH_1:27; then (abs ((pw1 `1) - (pw2 `1))) + (abs ((pw1 `2) - (pw2 `2))) <= ((E-bound Qa) - (W-bound Qa)) + ((N-bound Qa) - (S-bound Qa)) by A125, XREAL_1:7; then A128: (abs ((pw1 `1) - (pw2 `1))) + (abs ((pw1 `2) - (pw2 `2))) <= (((E-bound Qa) - (W-bound Qa)) + ((N-bound Qa) - (S-bound Qa))) + 1 by A126, XXREAL_0:2; ( dist (x,y) = |.(pw1 - pw2).| & |.(pw1 - pw2).| <= (abs ((pw1 `1) - (pw2 `1))) + (abs ((pw1 `2) - (pw2 `2))) ) by JGRAPH_1:28, JGRAPH_1:32; hence dist (x,y) <= (((E-bound Qa) - (W-bound Qa)) + ((N-bound Qa) - (S-bound Qa))) + 1 by A128, XXREAL_0:2; ::_thesis: verum end; 0 in the carrier of I[01] by BORSUK_1:43; then A129: g . 0 in rng g by A109, FUNCT_1:def_3; then ( S-bound Qa <= q1 `2 & q1 `2 <= N-bound Qa ) by A4, A107, A119, PSCOMP_1:24; then S-bound Qa <= N-bound Qa by XXREAL_0:2; then A130: 0 <= (N-bound Qa) - (S-bound Qa) by XREAL_1:48; i in Seg (len hb) by A95, A110, A112, FINSEQ_1:1; then A131: i in dom hb by FINSEQ_1:def_3; then A132: hb . i in rng hb by FUNCT_1:def_3; then h29 . i in rng g by A92, A118, A109, FUNCT_1:def_3; then reconsider w1 = g . (hb . i), w2 = g . (hb . (i + 1)) as Point of (Euclid 2) by A118, A117, TOPREAL3:8; i + 1 in Seg (len hb) by A95, A111, A114, FINSEQ_1:1; then A133: 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 A92, A132, A113, A120, BORSUK_1:40, XXREAL_2:def_12; i < i + 1 by NAT_1:13; then A134: hb /. i <= hb /. (i + 1) by A93, A131, A113, A133, A120, SEQM_3:def_1; then hb . i in R by A113, XXREAL_1:1; then A135: w1 in g .: R by A109, FUNCT_1:def_6; ( W-bound Qa <= q1 `1 & q1 `1 <= E-bound Qa ) by A4, A107, A119, A129, 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 A136: W1 is bounded by A130, A121, TBSP_1:def_7; hb . (i + 1) in R by A120, A134, XXREAL_1:1; then A137: w2 in g .: R by A109, FUNCT_1:def_6; reconsider W = g .: R as Subset of (Euclid 2) by TOPREAL3:8; dom g = [#] I[01] by FUNCT_2:def_1; then Q = g .: [.0,1.] by A4, BORSUK_1:40, RELAT_1:113; then W is bounded by A136, BORSUK_1:40, RELAT_1:123, TBSP_1:14; then A138: dist (w1,w2) <= diameter W by A135, A137, TBSP_1:def_8; diameter W < (min_dist_min (P9,Q9)) / 5 by A94, A95, A110, A112; then A139: dist (w1,w2) < (min_dist_min (P9,Q9)) / 5 by A138, XXREAL_0:2; h2 . (i + 1) = h2 /. (i + 1) by A111, A114, FINSEQ_4:15; then A140: h2 /. (i + 1) = g . (hb . (i + 1)) by A96, A116; h2 /. i = g . (hb . i) by A110, A112, A118, FINSEQ_4:15; hence |.((h2 /. i) - (h2 /. (i + 1))).| < (min_dist_min (P9,Q9)) / 5 by A140, A139, JGRAPH_1:28; ::_thesis: verum end; A141: dom hb = Seg (len hb) by FINSEQ_1:def_3; A142: for i being Element of NAT st i in dom hb holds h2 /. i = g . (hb . i) proof let i be Element of NAT ; ::_thesis: ( i in dom hb implies h2 /. i = g . (hb . i) ) assume A143: i in dom hb ; ::_thesis: h2 /. i = g . (hb . i) then i in dom h29 by A95, FINSEQ_3:29; then A144: h2 . i = g . (hb . i) by A96; ( 1 <= i & i <= len hb ) by A141, A143, FINSEQ_1:1; hence h2 /. i = g . (hb . i) by A95, A144, FINSEQ_4:15; ::_thesis: verum end; A145: for i being Element of NAT st i in dom h2 holds ( p1 `1 <= (h2 /. i) `1 & (h2 /. i) `1 <= p2 `1 ) proof let i be Element of NAT ; ::_thesis: ( i in dom h2 implies ( p1 `1 <= (h2 /. i) `1 & (h2 /. i) `1 <= p2 `1 ) ) 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 A95, FINSEQ_1:def_3; then A146: ( h2 /. i = g . (hb . i) & hb . i in rng hb ) by A142, FUNCT_1:def_3; dom g = the carrier of I[01] by FUNCT_2:def_1; then h2 /. i in rng g by A92, A146, FUNCT_1:def_3; hence ( p1 `1 <= (h2 /. i) `1 & (h2 /. i) `1 <= p2 `1 ) by A4, A6; ::_thesis: verum end; for i being Element of NAT st i in dom (X_axis h2) holds ( p1 `1 <= (X_axis h2) . i & (X_axis h2) . i <= p2 `1 ) proof let i be Element of 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 A101, JGRAPH_1:41; then A147: i in dom h2 by FINSEQ_1:def_3; then (X_axis h2) . i = (h2 /. i) `1 by JGRAPH_1:43; hence ( p1 `1 <= (X_axis h2) . i & (X_axis h2) . i <= p2 `1 ) by A145, A147; ::_thesis: verum end; then A148: X_axis h2 lies_between p1 `1 ,p2 `1 by GOBOARD4:def_2; A149: g . 1 = q2 by BORSUK_2:def_4; A150: for i being Element of NAT st i in dom h2 holds ( (h2 /. 1) `2 <= (h2 /. i) `2 & (h2 /. i) `2 <= (h2 /. (len h2)) `2 ) proof let i be Element of 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 A95, FINSEQ_1:def_3; then A151: ( h2 /. i = g . (hb . i) & hb . i in rng hb ) by A142, FUNCT_1:def_3; 1 in Seg (len hb) by A95, A101, FINSEQ_1:1; then 1 in dom hb by FINSEQ_1:def_3; then A152: h2 /. 1 = g . (hb . 1) by A142; len hb in Seg (len hb) by A95, A101, FINSEQ_1:1; then len hb in dom hb by FINSEQ_1:def_3; then A153: h2 /. (len h2) = g . (hb . (len hb)) by A95, A142; dom g = the carrier of I[01] by FUNCT_2:def_1; then h2 /. i in rng g by A92, A151, FUNCT_1:def_3; hence ( (h2 /. 1) `2 <= (h2 /. i) `2 & (h2 /. i) `2 <= (h2 /. (len h2)) `2 ) by A4, A8, A107, A149, A89, A90, A152, A153; ::_thesis: verum end; for i being Element of NAT st i in dom (Y_axis h2) holds ( (Y_axis h2) . 1 <= (Y_axis h2) . i & (Y_axis h2) . i <= (Y_axis h2) . (len h2) ) proof let i be Element of 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) ) ) A154: ( (Y_axis h2) . 1 = (h2 /. 1) `2 & (Y_axis h2) . (len h2) = (h2 /. (len h2)) `2 ) by A101, JGRAPH_1:42; 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 A101, JGRAPH_1:42; then A155: i in dom h2 by FINSEQ_1:def_3; then (Y_axis h2) . i = (h2 /. i) `2 by JGRAPH_1:43; hence ( (Y_axis h2) . 1 <= (Y_axis h2) . i & (Y_axis h2) . i <= (Y_axis h2) . (len h2) ) by A150, A155, A154; ::_thesis: verum end; then Y_axis h2 lies_between (Y_axis h2) . 1,(Y_axis h2) . (len h2) by GOBOARD4:def_2; then consider g2 being FinSequence of (TOP-REAL 2) such that A156: g2 is special and A157: g2 . 1 = h2 . 1 and A158: g2 . (len g2) = h2 . (len h2) and A159: len g2 >= len h2 and A160: ( Y_axis g2 lies_between (Y_axis h2) . 1,(Y_axis h2) . (len h2) & X_axis g2 lies_between p1 `1 ,p2 `1 ) and A161: for j being Element of NAT st j in dom g2 holds ex k being Element of NAT st ( k in dom h2 & |.((g2 /. j) - (h2 /. k)).| < (min_dist_min (P9,Q9)) / 5 ) and A162: for j being Element of NAT st 1 <= j & j + 1 <= len g2 holds |.((g2 /. j) - (g2 /. (j + 1))).| < (min_dist_min (P9,Q9)) / 5 by A13, A101, A148, A108, JGRAPH_1:40; A163: len g2 >= 1 by A101, A159, XXREAL_0:2; then A164: g2 /. (len g2) = g2 . (len g2) by FINSEQ_4:15; 1 in dom hb by A105, FINSEQ_3:25; then A165: h2 /. 1 = q1 by A107, A89, A142; A166: h2 . 1 = h2 /. 1 by A105, A95, FINSEQ_4:15; A167: h1 . (len h1) = h1 /. (len h1) by A28, FINSEQ_4:15; then A168: (X_axis f2) . (len f2) = (h1 /. (len h1)) `1 by A82, A87, A88, JGRAPH_1:41 .= (X_axis h1) . (len h1) by A28, JGRAPH_1:41 ; len h in dom h19 by A20, A28, FINSEQ_3:25; then h1 /. (len h1) = p2 by A71, A15, A20, A21, A167; then A169: (X_axis f2) . (len f2) = p2 `1 by A82, A87, A167, A88, JGRAPH_1:41; 5 <= len f2 by A16, A20, A83, XXREAL_0:2; then A170: 2 <= len f2 by XXREAL_0:2; 0 in dom g by A103, FUNCT_2:def_1; then A171: q1 in Q9 by A4, A107, FUNCT_1:def_3; A172: f2 . 1 = f2 /. 1 by A87, FINSEQ_4:15; g2 . 1 = g2 /. 1 by A163, FINSEQ_4:15; then A173: (Y_axis g2) . 1 = (h2 /. 1) `2 by A157, A163, A166, JGRAPH_1:42 .= (Y_axis h2) . 1 by A101, JGRAPH_1:42 ; g2 /. 1 = g2 . 1 by A163, FINSEQ_4:15; then A174: (Y_axis g2) . 1 = q1 `2 by A157, A163, A165, A166, JGRAPH_1:42; len hb in dom hb by A105, FINSEQ_3:25; then g2 . (len g2) = q2 by A149, A90, A95, A142, A158, A106; then A175: (Y_axis g2) . (len g2) = q2 `2 by A163, A164, JGRAPH_1:42; g2 . (len g2) = g2 /. (len g2) by A163, FINSEQ_4:15; then A176: (Y_axis g2) . (len g2) = (h2 /. (len h2)) `2 by A158, A163, A106, JGRAPH_1:42 .= (Y_axis h2) . (len h2) by A101, JGRAPH_1:42 ; 5 <= len g2 by A91, A95, A159, XXREAL_0:2; then A177: 2 <= len g2 by XXREAL_0:2; 1 in dom h19 by A28, FINSEQ_3:25; then h1 . 1 = f . (h . 1) by A21; then A178: (X_axis f2) . 1 = p1 `1 by A30, A14, A81, A87, A172, JGRAPH_1:41; A179: (X_axis f2) . 1 = (h1 /. 1) `1 by A81, A87, A29, A172, JGRAPH_1:41 .= (X_axis h1) . 1 by A28, JGRAPH_1:41 ; now__::_thesis:_(_(_p1_=_p2_&_contradiction_)_or_(_p1_<>_p2_&_contradiction_)_) percases ( p1 = p2 or p1 <> p2 ) ; caseA180: p1 = p2 ; ::_thesis: contradiction 0 in the carrier of I[01] by BORSUK_1:43; then 0 in dom f by FUNCT_2:def_1; then A181: p1 in P by A3, A30, FUNCT_1:3; 0 in the carrier of I[01] by BORSUK_1:43; then A182: 0 in dom g by FUNCT_2:def_1; then A183: q1 in Q by A4, A107, FUNCT_1:3; A184: for q being Point of (TOP-REAL 2) st q in Q holds q `1 = p1 `1 proof let q be Point of (TOP-REAL 2); ::_thesis: ( q in Q implies q `1 = p1 `1 ) assume q in Q ; ::_thesis: q `1 = p1 `1 then ( p1 `1 <= q `1 & q `1 <= p2 `1 ) by A6; hence q `1 = p1 `1 by A180, XXREAL_0:1; ::_thesis: verum end; A185: now__::_thesis:_not_q1_`2_=_q2_`2 assume A186: q1 `2 = q2 `2 ; ::_thesis: contradiction ( q1 `2 <= p1 `2 & p1 `2 <= q2 `2 ) by A7, A181; then A187: p1 `2 = q1 `2 by A186, XXREAL_0:1; q1 `1 = p1 `1 by A4, A107, A184, A182, FUNCT_1:3; then q1 = p1 by A187, TOPREAL3:6; hence contradiction by A11, A183, A181, XBOOLE_0:def_4; ::_thesis: verum end; A188: p1 in LSeg (q1,q2) proof 1 in the carrier of I[01] by BORSUK_1:43; then 1 in dom g by FUNCT_2:def_1; then g . 1 in rng g by FUNCT_1:3; then ( p1 `1 <= q2 `1 & q2 `1 <= p2 `1 ) by A4, A6, A149; then A189: p1 `1 = q2 `1 by A180, XXREAL_0:1; set ln = ((p1 `2) - (q1 `2)) / ((q2 `2) - (q1 `2)); A190: (((p1 `2) - (q1 `2)) / ((q2 `2) - (q1 `2))) * (q2 `2) = (((p1 `2) - (q1 `2)) * (q2 `2)) / ((q2 `2) - (q1 `2)) by XCMPLX_1:74 .= (((p1 `2) * (q2 `2)) - ((q1 `2) * (q2 `2))) / ((q2 `2) - (q1 `2)) ; A191: (q2 `2) - (q1 `2) <> 0 by A185; then 1 - (((p1 `2) - (q1 `2)) / ((q2 `2) - (q1 `2))) = (((q2 `2) - (q1 `2)) / ((q2 `2) - (q1 `2))) - (((p1 `2) - (q1 `2)) / ((q2 `2) - (q1 `2))) by XCMPLX_1:60 .= (((q2 `2) - (q1 `2)) - ((p1 `2) - (q1 `2))) / ((q2 `2) - (q1 `2)) by XCMPLX_1:120 .= ((q2 `2) - (p1 `2)) / ((q2 `2) - (q1 `2)) ; then A192: (1 - (((p1 `2) - (q1 `2)) / ((q2 `2) - (q1 `2)))) * (q1 `2) = (((q2 `2) - (p1 `2)) * (q1 `2)) / ((q2 `2) - (q1 `2)) by XCMPLX_1:74 .= (((q2 `2) * (q1 `2)) - ((p1 `2) * (q1 `2))) / ((q2 `2) - (q1 `2)) ; 0 in the carrier of I[01] by BORSUK_1:43; then 0 in dom g by FUNCT_2:def_1; then q1 in Q by A4, A107, FUNCT_1:3; then ( p1 `1 <= q1 `1 & q1 `1 <= p2 `1 ) by A6; then A193: p1 `1 = q1 `1 by A180, XXREAL_0:1; 0 in the carrier of I[01] by BORSUK_1:43; then 0 in dom f by FUNCT_2:def_1; then A194: f . 0 in rng f by FUNCT_1:3; then A195: q1 `2 <= p1 `2 by A3, A7, A30; A196: (((1 - (((p1 `2) - (q1 `2)) / ((q2 `2) - (q1 `2)))) * q1) + ((((p1 `2) - (q1 `2)) / ((q2 `2) - (q1 `2))) * q2)) `1 = (((1 - (((p1 `2) - (q1 `2)) / ((q2 `2) - (q1 `2)))) * q1) `1) + (((((p1 `2) - (q1 `2)) / ((q2 `2) - (q1 `2))) * q2) `1) by TOPREAL3:2 .= ((1 - (((p1 `2) - (q1 `2)) / ((q2 `2) - (q1 `2)))) * (q1 `1)) + (((((p1 `2) - (q1 `2)) / ((q2 `2) - (q1 `2))) * q2) `1) by TOPREAL3:4 .= ((1 - (((p1 `2) - (q1 `2)) / ((q2 `2) - (q1 `2)))) * (p1 `1)) + ((((p1 `2) - (q1 `2)) / ((q2 `2) - (q1 `2))) * (p1 `1)) by A193, A189, TOPREAL3:4 .= p1 `1 ; (((1 - (((p1 `2) - (q1 `2)) / ((q2 `2) - (q1 `2)))) * q1) + ((((p1 `2) - (q1 `2)) / ((q2 `2) - (q1 `2))) * q2)) `2 = (((1 - (((p1 `2) - (q1 `2)) / ((q2 `2) - (q1 `2)))) * q1) `2) + (((((p1 `2) - (q1 `2)) / ((q2 `2) - (q1 `2))) * q2) `2) by TOPREAL3:2 .= ((1 - (((p1 `2) - (q1 `2)) / ((q2 `2) - (q1 `2)))) * (q1 `2)) + (((((p1 `2) - (q1 `2)) / ((q2 `2) - (q1 `2))) * q2) `2) by TOPREAL3:4 .= ((1 - (((p1 `2) - (q1 `2)) / ((q2 `2) - (q1 `2)))) * (q1 `2)) + ((((p1 `2) - (q1 `2)) / ((q2 `2) - (q1 `2))) * (q2 `2)) by TOPREAL3:4 .= ((((q2 `2) * (q1 `2)) - ((p1 `2) * (q1 `2))) + (((p1 `2) * (q2 `2)) - ((q1 `2) * (q2 `2)))) / ((q2 `2) - (q1 `2)) by A192, A190, XCMPLX_1:62 .= ((p1 `2) * ((q2 `2) - (q1 `2))) / ((q2 `2) - (q1 `2)) .= (p1 `2) * (((q2 `2) - (q1 `2)) / ((q2 `2) - (q1 `2))) by XCMPLX_1:74 .= (p1 `2) * 1 by A191, XCMPLX_1:60 .= p1 `2 ; then A197: ((1 - (((p1 `2) - (q1 `2)) / ((q2 `2) - (q1 `2)))) * q1) + ((((p1 `2) - (q1 `2)) / ((q2 `2) - (q1 `2))) * q2) = p1 by A196, TOPREAL3:6; A198: p1 `2 <= q2 `2 by A3, A7, A30, A194; then q2 `2 >= q1 `2 by A195, XXREAL_0:2; then q2 `2 > q1 `2 by A185, XXREAL_0:1; then A199: (q2 `2) - (q1 `2) > 0 by XREAL_1:50; (p1 `2) - (q1 `2) <= (q2 `2) - (q1 `2) by A198, XREAL_1:13; then ((p1 `2) - (q1 `2)) / ((q2 `2) - (q1 `2)) <= ((q2 `2) - (q1 `2)) / ((q2 `2) - (q1 `2)) by A199, XREAL_1:72; then A200: ((p1 `2) - (q1 `2)) / ((q2 `2) - (q1 `2)) <= 1 by A199, XCMPLX_1:60; (p1 `2) - (q1 `2) >= 0 by A195, XREAL_1:48; hence p1 in LSeg (q1,q2) by A199, A200, A197; ::_thesis: verum end; 1 in the carrier of I[01] by BORSUK_1:43; then 1 in dom g by FUNCT_2:def_1; then A201: q2 in Q by A4, A149, FUNCT_1:3; Q c= LSeg (q1,q2) proof ( p1 `1 <= q2 `1 & q2 `1 <= p2 `1 ) by A6, A201; then A202: p1 `1 = q2 `1 by A180, XXREAL_0:1; ( p1 `1 <= q1 `1 & q1 `1 <= p2 `1 ) by A6, A183; then A203: p1 `1 = q1 `1 by A180, XXREAL_0:1; let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in Q or z in LSeg (q1,q2) ) assume A204: z in Q ; ::_thesis: z in LSeg (q1,q2) then reconsider qz = z as Point of (TOP-REAL 2) ; A205: qz `2 <= q2 `2 by A8, A204; set ln = ((qz `2) - (q1 `2)) / ((q2 `2) - (q1 `2)); A206: (((qz `2) - (q1 `2)) / ((q2 `2) - (q1 `2))) * (q2 `2) = (((qz `2) - (q1 `2)) * (q2 `2)) / ((q2 `2) - (q1 `2)) by XCMPLX_1:74 .= (((qz `2) * (q2 `2)) - ((q1 `2) * (q2 `2))) / ((q2 `2) - (q1 `2)) ; A207: (q2 `2) - (q1 `2) <> 0 by A185; then 1 - (((qz `2) - (q1 `2)) / ((q2 `2) - (q1 `2))) = (((q2 `2) - (q1 `2)) / ((q2 `2) - (q1 `2))) - (((qz `2) - (q1 `2)) / ((q2 `2) - (q1 `2))) by XCMPLX_1:60 .= (((q2 `2) - (q1 `2)) - ((qz `2) - (q1 `2))) / ((q2 `2) - (q1 `2)) by XCMPLX_1:120 .= ((q2 `2) - (qz `2)) / ((q2 `2) - (q1 `2)) ; then A208: (1 - (((qz `2) - (q1 `2)) / ((q2 `2) - (q1 `2)))) * (q1 `2) = (((q2 `2) - (qz `2)) * (q1 `2)) / ((q2 `2) - (q1 `2)) by XCMPLX_1:74 .= (((q2 `2) * (q1 `2)) - ((qz `2) * (q1 `2))) / ((q2 `2) - (q1 `2)) ; A209: (((1 - (((qz `2) - (q1 `2)) / ((q2 `2) - (q1 `2)))) * q1) + ((((qz `2) - (q1 `2)) / ((q2 `2) - (q1 `2))) * q2)) `2 = (((1 - (((qz `2) - (q1 `2)) / ((q2 `2) - (q1 `2)))) * q1) `2) + (((((qz `2) - (q1 `2)) / ((q2 `2) - (q1 `2))) * q2) `2) by TOPREAL3:2 .= ((1 - (((qz `2) - (q1 `2)) / ((q2 `2) - (q1 `2)))) * (q1 `2)) + (((((qz `2) - (q1 `2)) / ((q2 `2) - (q1 `2))) * q2) `2) by TOPREAL3:4 .= ((1 - (((qz `2) - (q1 `2)) / ((q2 `2) - (q1 `2)))) * (q1 `2)) + ((((qz `2) - (q1 `2)) / ((q2 `2) - (q1 `2))) * (q2 `2)) by TOPREAL3:4 .= ((((q2 `2) * (q1 `2)) - ((qz `2) * (q1 `2))) + (((qz `2) * (q2 `2)) - ((q1 `2) * (q2 `2)))) / ((q2 `2) - (q1 `2)) by A208, A206, XCMPLX_1:62 .= ((qz `2) * ((q2 `2) - (q1 `2))) / ((q2 `2) - (q1 `2)) .= (qz `2) * (((q2 `2) - (q1 `2)) / ((q2 `2) - (q1 `2))) by XCMPLX_1:74 .= (qz `2) * 1 by A207, XCMPLX_1:60 .= qz `2 ; A210: ( p1 `1 <= qz `1 & qz `1 <= p2 `1 ) by A6, A204; (((1 - (((qz `2) - (q1 `2)) / ((q2 `2) - (q1 `2)))) * q1) + ((((qz `2) - (q1 `2)) / ((q2 `2) - (q1 `2))) * q2)) `1 = (((1 - (((qz `2) - (q1 `2)) / ((q2 `2) - (q1 `2)))) * q1) `1) + (((((qz `2) - (q1 `2)) / ((q2 `2) - (q1 `2))) * q2) `1) by TOPREAL3:2 .= ((1 - (((qz `2) - (q1 `2)) / ((q2 `2) - (q1 `2)))) * (q1 `1)) + (((((qz `2) - (q1 `2)) / ((q2 `2) - (q1 `2))) * q2) `1) by TOPREAL3:4 .= ((1 - (((qz `2) - (q1 `2)) / ((q2 `2) - (q1 `2)))) * (p1 `1)) + ((((qz `2) - (q1 `2)) / ((q2 `2) - (q1 `2))) * (p1 `1)) by A203, A202, TOPREAL3:4 .= qz `1 by A180, A210, XXREAL_0:1 ; then A211: ((1 - (((qz `2) - (q1 `2)) / ((q2 `2) - (q1 `2)))) * q1) + ((((qz `2) - (q1 `2)) / ((q2 `2) - (q1 `2))) * q2) = qz by A209, TOPREAL3:6; A212: q1 `2 <= qz `2 by A8, A204; then q2 `2 >= q1 `2 by A205, XXREAL_0:2; then q2 `2 > q1 `2 by A185, XXREAL_0:1; then A213: (q2 `2) - (q1 `2) > 0 by XREAL_1:50; (qz `2) - (q1 `2) <= (q2 `2) - (q1 `2) by A205, XREAL_1:13; then ((qz `2) - (q1 `2)) / ((q2 `2) - (q1 `2)) <= ((q2 `2) - (q1 `2)) / ((q2 `2) - (q1 `2)) by A213, XREAL_1:72; then A214: ((qz `2) - (q1 `2)) / ((q2 `2) - (q1 `2)) <= 1 by A213, XCMPLX_1:60; (qz `2) - (q1 `2) >= 0 by A212, XREAL_1:48; hence z in LSeg (q1,q2) by A213, A214, A211; ::_thesis: verum end; then p1 in Q by A4, A188, Th3; hence contradiction by A104, A11, XBOOLE_0:def_4; ::_thesis: verum end; caseA215: p1 <> p2 ; ::_thesis: contradiction A216: 1 <= len hb by A91, XXREAL_0:2; then 1 in dom hb by FINSEQ_3:25; then A217: h2 /. 1 = g . (hb . 1) by A142; A218: now__::_thesis:_not_q1_=_q2 0 in the carrier of I[01] by BORSUK_1:43; then 0 in dom g by FUNCT_2:def_1; then A219: q1 in Q by A4, A107, FUNCT_1:3; 0 in the carrier of I[01] by BORSUK_1:43; then A220: 0 in dom f by FUNCT_2:def_1; then A221: p1 in P by A3, A30, FUNCT_1:3; assume A222: q1 = q2 ; ::_thesis: contradiction A223: for p being Point of (TOP-REAL 2) st p in P holds p `2 = q1 `2 proof let p be Point of (TOP-REAL 2); ::_thesis: ( p in P implies p `2 = q1 `2 ) assume p in P ; ::_thesis: p `2 = q1 `2 then ( q1 `2 <= p `2 & p `2 <= q2 `2 ) by A7; hence p `2 = q1 `2 by A222, XXREAL_0:1; ::_thesis: verum end; A224: now__::_thesis:_not_p1_`1_=_p2_`1 assume A225: p1 `1 = p2 `1 ; ::_thesis: contradiction ( p1 `1 <= q1 `1 & q1 `1 <= p2 `1 ) by A6, A219; then A226: q1 `1 = p1 `1 by A225, XXREAL_0:1; p1 `2 = q1 `2 by A3, A30, A223, A220, FUNCT_1:3; then p1 = q1 by A226, TOPREAL3:6; hence contradiction by A11, A221, A219, XBOOLE_0:def_4; ::_thesis: verum end; A227: q1 in LSeg (p1,p2) proof 1 in the carrier of I[01] by BORSUK_1:43; then 1 in dom f by FUNCT_2:def_1; then f . 1 in rng f by FUNCT_1:3; then ( q1 `2 <= p2 `2 & p2 `2 <= q2 `2 ) by A3, A7, A71; then A228: q1 `2 = p2 `2 by A222, XXREAL_0:1; set ln = ((q1 `1) - (p1 `1)) / ((p2 `1) - (p1 `1)); A229: (((q1 `1) - (p1 `1)) / ((p2 `1) - (p1 `1))) * (p2 `1) = (((q1 `1) - (p1 `1)) * (p2 `1)) / ((p2 `1) - (p1 `1)) by XCMPLX_1:74 .= (((q1 `1) * (p2 `1)) - ((p1 `1) * (p2 `1))) / ((p2 `1) - (p1 `1)) ; A230: (p2 `1) - (p1 `1) <> 0 by A224; then 1 - (((q1 `1) - (p1 `1)) / ((p2 `1) - (p1 `1))) = (((p2 `1) - (p1 `1)) / ((p2 `1) - (p1 `1))) - (((q1 `1) - (p1 `1)) / ((p2 `1) - (p1 `1))) by XCMPLX_1:60 .= (((p2 `1) - (p1 `1)) - ((q1 `1) - (p1 `1))) / ((p2 `1) - (p1 `1)) by XCMPLX_1:120 .= ((p2 `1) - (q1 `1)) / ((p2 `1) - (p1 `1)) ; then A231: (1 - (((q1 `1) - (p1 `1)) / ((p2 `1) - (p1 `1)))) * (p1 `1) = (((p2 `1) - (q1 `1)) * (p1 `1)) / ((p2 `1) - (p1 `1)) by XCMPLX_1:74 .= (((p2 `1) * (p1 `1)) - ((q1 `1) * (p1 `1))) / ((p2 `1) - (p1 `1)) ; 0 in the carrier of I[01] by BORSUK_1:43; then 0 in dom f by FUNCT_2:def_1; then f . 0 in rng f by FUNCT_1:3; then ( q1 `2 <= p1 `2 & p1 `2 <= q2 `2 ) by A3, A7, A30; then A232: q1 `2 = p1 `2 by A222, XXREAL_0:1; 0 in the carrier of I[01] by BORSUK_1:43; then 0 in dom g by FUNCT_2:def_1; then A233: g . 0 in rng g by FUNCT_1:3; then A234: p1 `1 <= q1 `1 by A4, A6, A107; A235: (((1 - (((q1 `1) - (p1 `1)) / ((p2 `1) - (p1 `1)))) * p1) + ((((q1 `1) - (p1 `1)) / ((p2 `1) - (p1 `1))) * p2)) `2 = (((1 - (((q1 `1) - (p1 `1)) / ((p2 `1) - (p1 `1)))) * p1) `2) + (((((q1 `1) - (p1 `1)) / ((p2 `1) - (p1 `1))) * p2) `2) by TOPREAL3:2 .= ((1 - (((q1 `1) - (p1 `1)) / ((p2 `1) - (p1 `1)))) * (p1 `2)) + (((((q1 `1) - (p1 `1)) / ((p2 `1) - (p1 `1))) * p2) `2) by TOPREAL3:4 .= ((1 - (((q1 `1) - (p1 `1)) / ((p2 `1) - (p1 `1)))) * (q1 `2)) + ((((q1 `1) - (p1 `1)) / ((p2 `1) - (p1 `1))) * (q1 `2)) by A232, A228, TOPREAL3:4 ; (((1 - (((q1 `1) - (p1 `1)) / ((p2 `1) - (p1 `1)))) * p1) + ((((q1 `1) - (p1 `1)) / ((p2 `1) - (p1 `1))) * p2)) `1 = (((1 - (((q1 `1) - (p1 `1)) / ((p2 `1) - (p1 `1)))) * p1) `1) + (((((q1 `1) - (p1 `1)) / ((p2 `1) - (p1 `1))) * p2) `1) by TOPREAL3:2 .= ((1 - (((q1 `1) - (p1 `1)) / ((p2 `1) - (p1 `1)))) * (p1 `1)) + (((((q1 `1) - (p1 `1)) / ((p2 `1) - (p1 `1))) * p2) `1) by TOPREAL3:4 .= ((1 - (((q1 `1) - (p1 `1)) / ((p2 `1) - (p1 `1)))) * (p1 `1)) + ((((q1 `1) - (p1 `1)) / ((p2 `1) - (p1 `1))) * (p2 `1)) by TOPREAL3:4 .= ((((p2 `1) * (p1 `1)) - ((q1 `1) * (p1 `1))) + (((q1 `1) * (p2 `1)) - ((p1 `1) * (p2 `1)))) / ((p2 `1) - (p1 `1)) by A231, A229, XCMPLX_1:62 .= ((q1 `1) * ((p2 `1) - (p1 `1))) / ((p2 `1) - (p1 `1)) .= (q1 `1) * (((p2 `1) - (p1 `1)) / ((p2 `1) - (p1 `1))) by XCMPLX_1:74 .= (q1 `1) * 1 by A230, XCMPLX_1:60 ; then A236: ((1 - (((q1 `1) - (p1 `1)) / ((p2 `1) - (p1 `1)))) * p1) + ((((q1 `1) - (p1 `1)) / ((p2 `1) - (p1 `1))) * p2) = q1 by A235, TOPREAL3:6; A237: q1 `1 <= p2 `1 by A4, A6, A107, A233; then p2 `1 >= p1 `1 by A234, XXREAL_0:2; then p2 `1 > p1 `1 by A224, XXREAL_0:1; then A238: (p2 `1) - (p1 `1) > 0 by XREAL_1:50; (q1 `1) - (p1 `1) <= (p2 `1) - (p1 `1) by A237, XREAL_1:13; then ((q1 `1) - (p1 `1)) / ((p2 `1) - (p1 `1)) <= ((p2 `1) - (p1 `1)) / ((p2 `1) - (p1 `1)) by A238, XREAL_1:72; then A239: ((q1 `1) - (p1 `1)) / ((p2 `1) - (p1 `1)) <= 1 by A238, XCMPLX_1:60; (q1 `1) - (p1 `1) >= 0 by A234, XREAL_1:48; hence q1 in LSeg (p1,p2) by A238, A239, A236; ::_thesis: verum end; 1 in the carrier of I[01] by BORSUK_1:43; then 1 in dom f by FUNCT_2:def_1; then A240: p2 in P by A3, A71, FUNCT_1:3; P c= LSeg (p1,p2) proof ( q1 `2 <= p2 `2 & p2 `2 <= q2 `2 ) by A7, A240; then A241: q1 `2 = p2 `2 by A222, XXREAL_0:1; ( q1 `2 <= p1 `2 & p1 `2 <= q2 `2 ) by A7, A221; then A242: q1 `2 = p1 `2 by A222, XXREAL_0:1; let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in P or z in LSeg (p1,p2) ) assume A243: z in P ; ::_thesis: z in LSeg (p1,p2) then reconsider pz = z as Point of (TOP-REAL 2) ; A244: pz `1 <= p2 `1 by A5, A243; set ln = ((pz `1) - (p1 `1)) / ((p2 `1) - (p1 `1)); A245: (((pz `1) - (p1 `1)) / ((p2 `1) - (p1 `1))) * (p2 `1) = (((pz `1) - (p1 `1)) * (p2 `1)) / ((p2 `1) - (p1 `1)) by XCMPLX_1:74 .= (((pz `1) * (p2 `1)) - ((p1 `1) * (p2 `1))) / ((p2 `1) - (p1 `1)) ; A246: (p2 `1) - (p1 `1) <> 0 by A224; then 1 - (((pz `1) - (p1 `1)) / ((p2 `1) - (p1 `1))) = (((p2 `1) - (p1 `1)) / ((p2 `1) - (p1 `1))) - (((pz `1) - (p1 `1)) / ((p2 `1) - (p1 `1))) by XCMPLX_1:60 .= (((p2 `1) - (p1 `1)) - ((pz `1) - (p1 `1))) / ((p2 `1) - (p1 `1)) by XCMPLX_1:120 .= ((p2 `1) - (pz `1)) / ((p2 `1) - (p1 `1)) ; then A247: (1 - (((pz `1) - (p1 `1)) / ((p2 `1) - (p1 `1)))) * (p1 `1) = (((p2 `1) - (pz `1)) * (p1 `1)) / ((p2 `1) - (p1 `1)) by XCMPLX_1:74 .= (((p2 `1) * (p1 `1)) - ((pz `1) * (p1 `1))) / ((p2 `1) - (p1 `1)) ; A248: (((1 - (((pz `1) - (p1 `1)) / ((p2 `1) - (p1 `1)))) * p1) + ((((pz `1) - (p1 `1)) / ((p2 `1) - (p1 `1))) * p2)) `1 = (((1 - (((pz `1) - (p1 `1)) / ((p2 `1) - (p1 `1)))) * p1) `1) + (((((pz `1) - (p1 `1)) / ((p2 `1) - (p1 `1))) * p2) `1) by TOPREAL3:2 .= ((1 - (((pz `1) - (p1 `1)) / ((p2 `1) - (p1 `1)))) * (p1 `1)) + (((((pz `1) - (p1 `1)) / ((p2 `1) - (p1 `1))) * p2) `1) by TOPREAL3:4 .= ((1 - (((pz `1) - (p1 `1)) / ((p2 `1) - (p1 `1)))) * (p1 `1)) + ((((pz `1) - (p1 `1)) / ((p2 `1) - (p1 `1))) * (p2 `1)) by TOPREAL3:4 .= ((((p2 `1) * (p1 `1)) - ((pz `1) * (p1 `1))) + (((pz `1) * (p2 `1)) - ((p1 `1) * (p2 `1)))) / ((p2 `1) - (p1 `1)) by A247, A245, XCMPLX_1:62 .= ((pz `1) * ((p2 `1) - (p1 `1))) / ((p2 `1) - (p1 `1)) .= (pz `1) * (((p2 `1) - (p1 `1)) / ((p2 `1) - (p1 `1))) by XCMPLX_1:74 .= (pz `1) * 1 by A246, XCMPLX_1:60 .= pz `1 ; A249: ( q1 `2 <= pz `2 & pz `2 <= q2 `2 ) by A7, A243; (((1 - (((pz `1) - (p1 `1)) / ((p2 `1) - (p1 `1)))) * p1) + ((((pz `1) - (p1 `1)) / ((p2 `1) - (p1 `1))) * p2)) `2 = (((1 - (((pz `1) - (p1 `1)) / ((p2 `1) - (p1 `1)))) * p1) `2) + (((((pz `1) - (p1 `1)) / ((p2 `1) - (p1 `1))) * p2) `2) by TOPREAL3:2 .= ((1 - (((pz `1) - (p1 `1)) / ((p2 `1) - (p1 `1)))) * (p1 `2)) + (((((pz `1) - (p1 `1)) / ((p2 `1) - (p1 `1))) * p2) `2) by TOPREAL3:4 .= ((1 - (((pz `1) - (p1 `1)) / ((p2 `1) - (p1 `1)))) * (q1 `2)) + ((((pz `1) - (p1 `1)) / ((p2 `1) - (p1 `1))) * (q1 `2)) by A242, A241, TOPREAL3:4 .= pz `2 by A222, A249, XXREAL_0:1 ; then A250: ((1 - (((pz `1) - (p1 `1)) / ((p2 `1) - (p1 `1)))) * p1) + ((((pz `1) - (p1 `1)) / ((p2 `1) - (p1 `1))) * p2) = pz by A248, TOPREAL3:6; A251: p1 `1 <= pz `1 by A5, A243; then p2 `1 >= p1 `1 by A244, XXREAL_0:2; then p2 `1 > p1 `1 by A224, XXREAL_0:1; then A252: (p2 `1) - (p1 `1) > 0 by XREAL_1:50; (pz `1) - (p1 `1) <= (p2 `1) - (p1 `1) by A244, XREAL_1:13; then ((pz `1) - (p1 `1)) / ((p2 `1) - (p1 `1)) <= ((p2 `1) - (p1 `1)) / ((p2 `1) - (p1 `1)) by A252, XREAL_1:72; then A253: ((pz `1) - (p1 `1)) / ((p2 `1) - (p1 `1)) <= 1 by A252, XCMPLX_1:60; (pz `1) - (p1 `1) >= 0 by A251, XREAL_1:48; hence z in LSeg (p1,p2) by A252, A253, A250; ::_thesis: verum end; then q1 in P by A3, A227, Th3; hence contradiction by A171, A11, XBOOLE_0:def_4; ::_thesis: verum end; len hb in dom hb by A216, FINSEQ_3:25; then A254: g2 . 1 <> g2 . (len g2) by A107, A149, A89, A90, A95, A142, A157, A158, A166, A106, A218, A217; f2 /. 1 <> f2 /. (len f2) by A30, A71, A14, A15, A20, A21, A81, A82, A29, A172, A88, A102, A23, A215; then L~ f2 meets L~ g2 by A80, A84, A156, A160, A172, A88, A178, A169, A174, A175, A179, A168, A173, A176, A170, A177, A254, JGRAPH_1:26; then consider s being set such that A255: s in L~ f2 and A256: s in L~ g2 by XBOOLE_0:3; reconsider ps = s as Point of (TOP-REAL 2) by A255; ps in union { (LSeg (f2,i)) where i is Element of NAT : ( 1 <= i & i + 1 <= len f2 ) } by A255, TOPREAL1:def_4; then consider x being set such that A257: ( ps in x & x in { (LSeg (f2,i)) where i is Element of NAT : ( 1 <= i & i + 1 <= len f2 ) } ) by TARSKI:def_4; ps in union { (LSeg (g2,j)) where j is Element of NAT : ( 1 <= j & j + 1 <= len g2 ) } by A256, TOPREAL1:def_4; then consider y being set such that A258: ( ps in y & y in { (LSeg (g2,j)) where j is Element of NAT : ( 1 <= j & j + 1 <= len g2 ) } ) by TARSKI:def_4; consider i being Element of NAT such that A259: x = LSeg (f2,i) and A260: 1 <= i and A261: i + 1 <= len f2 by A257; LSeg (f2,i) = LSeg ((f2 /. i),(f2 /. (i + 1))) by A260, A261, TOPREAL1:def_3; then A262: |.(ps - (f2 /. i)).| <= |.((f2 /. i) - (f2 /. (i + 1))).| by A257, A259, JGRAPH_1:36; i < len f2 by A261, NAT_1:13; then i in dom f2 by A260, FINSEQ_3:25; then consider k being Element of NAT such that A263: k in dom h1 and A264: |.((f2 /. i) - (h1 /. k)).| < (min_dist_min (P9,Q9)) / 5 by A85; consider j being Element of NAT such that A265: y = LSeg (g2,j) and A266: 1 <= j and A267: j + 1 <= len g2 by A258; LSeg (g2,j) = LSeg ((g2 /. j),(g2 /. (j + 1))) by A266, A267, TOPREAL1:def_3; then A268: |.(ps - (g2 /. j)).| <= |.((g2 /. j) - (g2 /. (j + 1))).| by A258, A265, JGRAPH_1:36; reconsider p11 = h1 /. k as Point of (TOP-REAL 2) ; |.((f2 /. i) - (f2 /. (i + 1))).| < (min_dist_min (P9,Q9)) / 5 by A86, A260, A261; then |.(ps - (f2 /. i)).| < (min_dist_min (P9,Q9)) / 5 by A262, 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 A264, 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 A269: |.(p11 - ps).| < ((min_dist_min (P9,Q9)) / 5) + ((min_dist_min (P9,Q9)) / 5) by TOPRNS_1:27; A270: k in Seg (len h1) by A263, FINSEQ_1:def_3; then ( 1 <= k & k <= len h1 ) by FINSEQ_1:1; then h1 . k = h1 /. k by FINSEQ_4:15; then A271: h1 /. k = f . (h . k) by A21, A263; j < len g2 by A267, NAT_1:13; then j in dom g2 by A266, FINSEQ_3:25; then consider k9 being Element of NAT such that A272: k9 in dom h2 and A273: |.((g2 /. j) - (h2 /. k9)).| < (min_dist_min (P9,Q9)) / 5 by A161; k9 in Seg (len h2) by A272, FINSEQ_1:def_3; then k9 in dom hb by A95, FINSEQ_1:def_3; then A274: ( hb . k9 in rng hb & h2 /. k9 = g . (hb . k9) ) by A142, FUNCT_1:def_3; reconsider q11 = h2 /. k9 as Point of (TOP-REAL 2) ; reconsider x1 = p11, x2 = q11 as Point of (Euclid 2) by EUCLID:22; dom g = the carrier of I[01] by FUNCT_2:def_1; then A275: h2 /. k9 in rng g by A92, A274, FUNCT_1:def_3; k in dom h by A20, A270, FINSEQ_1:def_3; then A276: h . k in rng h by FUNCT_1:def_3; dom f = the carrier of I[01] by FUNCT_2:def_1; then h1 /. k in P by A3, A17, A271, A276, FUNCT_1:def_3; then min_dist_min (P9,Q9) <= dist (x1,x2) by A4, A10, A9, A275, WEIERSTR:34; then A277: min_dist_min (P9,Q9) <= |.(p11 - q11).| by JGRAPH_1:28; |.((g2 /. j) - (g2 /. (j + 1))).| < (min_dist_min (P9,Q9)) / 5 by A162, A266, A267; then |.(ps - (g2 /. j)).| < (min_dist_min (P9,Q9)) / 5 by A268, 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 A273, 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 A269, TOPRNS_1:34, XREAL_1:8; then |.(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; then min_dist_min (P9,Q9) < 4 * ((min_dist_min (P9,Q9)) / 5) by A277, 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 A13, XREAL_1:139; then 4 - 5 > 0 by A12; hence contradiction ; ::_thesis: verum end; end; end; hence contradiction ; ::_thesis: verum end; theorem Th5: :: JGRAPH_8:5 for a, b, c, d being real number for f, g being continuous Function of I[01],(TOP-REAL 2) for O, I being Point of I[01] st O = 0 & I = 1 & (f . O) `1 = a & (f . I) `1 = b & (g . O) `2 = c & (g . I) `2 = d & ( for r being Point of I[01] holds ( a <= (f . r) `1 & (f . r) `1 <= b & a <= (g . r) `1 & (g . r) `1 <= b & c <= (f . r) `2 & (f . r) `2 <= d & c <= (g . r) `2 & (g . r) `2 <= d ) ) holds rng f meets rng g proof let a, b, c, d be real number ; ::_thesis: for f, g being continuous Function of I[01],(TOP-REAL 2) for O, I being Point of I[01] st O = 0 & I = 1 & (f . O) `1 = a & (f . I) `1 = b & (g . O) `2 = c & (g . I) `2 = d & ( for r being Point of I[01] holds ( a <= (f . r) `1 & (f . r) `1 <= b & a <= (g . r) `1 & (g . r) `1 <= b & c <= (f . r) `2 & (f . r) `2 <= d & c <= (g . r) `2 & (g . r) `2 <= d ) ) holds rng f meets rng g let f, g be continuous Function of I[01],(TOP-REAL 2); ::_thesis: for O, I being Point of I[01] st O = 0 & I = 1 & (f . O) `1 = a & (f . I) `1 = b & (g . O) `2 = c & (g . I) `2 = d & ( for r being Point of I[01] holds ( a <= (f . r) `1 & (f . r) `1 <= b & a <= (g . r) `1 & (g . r) `1 <= b & c <= (f . r) `2 & (f . r) `2 <= d & c <= (g . r) `2 & (g . r) `2 <= d ) ) holds rng f meets rng g let O, I be Point of I[01]; ::_thesis: ( O = 0 & I = 1 & (f . O) `1 = a & (f . I) `1 = b & (g . O) `2 = c & (g . I) `2 = d & ( for r being Point of I[01] holds ( a <= (f . r) `1 & (f . r) `1 <= b & a <= (g . r) `1 & (g . r) `1 <= b & c <= (f . r) `2 & (f . r) `2 <= d & c <= (g . r) `2 & (g . r) `2 <= d ) ) implies rng f meets rng g ) assume that A1: ( O = 0 & I = 1 ) and A2: (f . O) `1 = a and A3: (f . I) `1 = b and A4: (g . O) `2 = c and A5: (g . I) `2 = d and A6: for r being Point of I[01] holds ( a <= (f . r) `1 & (f . r) `1 <= b & a <= (g . r) `1 & (g . r) `1 <= b & c <= (f . r) `2 & (f . r) `2 <= d & c <= (g . r) `2 & (g . r) `2 <= d ) ; ::_thesis: rng f meets rng g reconsider Q = rng g as non empty Subset of (TOP-REAL 2) ; A7: the carrier of ((TOP-REAL 2) | Q) = [#] ((TOP-REAL 2) | Q) .= rng g by PRE_TOPC:def_5 ; dom g = the carrier of I[01] by FUNCT_2:def_1; then reconsider g1 = g as Function of I[01],((TOP-REAL 2) | Q) by A7, FUNCT_2:1; reconsider q2 = g1 . I as Point of (TOP-REAL 2) by A5; reconsider q1 = g1 . O as Point of (TOP-REAL 2) by A4; reconsider P = rng f as non empty Subset of (TOP-REAL 2) ; A8: the carrier of ((TOP-REAL 2) | P) = [#] ((TOP-REAL 2) | P) .= rng f by PRE_TOPC:def_5 ; dom f = the carrier of I[01] by FUNCT_2:def_1; then reconsider f1 = f as Function of I[01],((TOP-REAL 2) | P) by A8, FUNCT_2:1; reconsider p2 = f1 . I as Point of (TOP-REAL 2) by A3; reconsider p1 = f1 . O as Point of (TOP-REAL 2) by A2; A9: for p being Point of (TOP-REAL 2) st p in P holds ( p1 `1 <= p `1 & p `1 <= p2 `1 ) proof let p be Point of (TOP-REAL 2); ::_thesis: ( p in P implies ( p1 `1 <= p `1 & p `1 <= p2 `1 ) ) assume p in P ; ::_thesis: ( p1 `1 <= p `1 & p `1 <= p2 `1 ) then ex x being set st ( x in dom f1 & p = f1 . x ) by FUNCT_1:def_3; hence ( p1 `1 <= p `1 & p `1 <= p2 `1 ) by A2, A3, A6; ::_thesis: verum end; A10: for p being Point of (TOP-REAL 2) st p in P holds ( q1 `2 <= p `2 & p `2 <= q2 `2 ) proof let p be Point of (TOP-REAL 2); ::_thesis: ( p in P implies ( q1 `2 <= p `2 & p `2 <= q2 `2 ) ) assume p in P ; ::_thesis: ( q1 `2 <= p `2 & p `2 <= q2 `2 ) then ex x being set st ( x in dom f1 & p = f1 . x ) by FUNCT_1:def_3; hence ( q1 `2 <= p `2 & p `2 <= q2 `2 ) by A4, A5, A6; ::_thesis: verum end; A11: for p being Point of (TOP-REAL 2) st p in Q holds ( q1 `2 <= p `2 & p `2 <= q2 `2 ) proof let p be Point of (TOP-REAL 2); ::_thesis: ( p in Q implies ( q1 `2 <= p `2 & p `2 <= q2 `2 ) ) assume p in Q ; ::_thesis: ( q1 `2 <= p `2 & p `2 <= q2 `2 ) then ex x being set st ( x in dom g1 & p = g1 . x ) by FUNCT_1:def_3; hence ( q1 `2 <= p `2 & p `2 <= q2 `2 ) by A4, A5, A6; ::_thesis: verum end; A12: for p being Point of (TOP-REAL 2) st p in Q holds ( p1 `1 <= p `1 & p `1 <= p2 `1 ) proof let p be Point of (TOP-REAL 2); ::_thesis: ( p in Q implies ( p1 `1 <= p `1 & p `1 <= p2 `1 ) ) assume p in Q ; ::_thesis: ( p1 `1 <= p `1 & p `1 <= p2 `1 ) then ex x being set st ( x in dom g1 & p = g1 . x ) by FUNCT_1:def_3; hence ( p1 `1 <= p `1 & p `1 <= p2 `1 ) by A2, A3, A6; ::_thesis: verum end; ( f is Path of p1,p2 & g is Path of q1,q2 ) by A1, BORSUK_2:def_4; hence rng f meets rng g by A9, A12, A10, A11, Th4; ::_thesis: verum end; theorem :: JGRAPH_8:6 for a, b, c, d being real number for ar, br, cr, dr being Point of (Trectangle (a,b,c,d)) for h being Path of ar,br for v being Path of dr,cr for Ar, Br, Cr, Dr being Point of (TOP-REAL 2) st Ar `1 = a & Br `1 = b & Cr `2 = c & Dr `2 = d & ar = Ar & br = Br & cr = Cr & dr = Dr holds ex s, t being Point of I[01] st h . s = v . t proof let a, b, c, d be real number ; ::_thesis: for ar, br, cr, dr being Point of (Trectangle (a,b,c,d)) for h being Path of ar,br for v being Path of dr,cr for Ar, Br, Cr, Dr being Point of (TOP-REAL 2) st Ar `1 = a & Br `1 = b & Cr `2 = c & Dr `2 = d & ar = Ar & br = Br & cr = Cr & dr = Dr holds ex s, t being Point of I[01] st h . s = v . t let ar, br, cr, dr be Point of (Trectangle (a,b,c,d)); ::_thesis: for h being Path of ar,br for v being Path of dr,cr for Ar, Br, Cr, Dr being Point of (TOP-REAL 2) st Ar `1 = a & Br `1 = b & Cr `2 = c & Dr `2 = d & ar = Ar & br = Br & cr = Cr & dr = Dr holds ex s, t being Point of I[01] st h . s = v . t let h be Path of ar,br; ::_thesis: for v being Path of dr,cr for Ar, Br, Cr, Dr being Point of (TOP-REAL 2) st Ar `1 = a & Br `1 = b & Cr `2 = c & Dr `2 = d & ar = Ar & br = Br & cr = Cr & dr = Dr holds ex s, t being Point of I[01] st h . s = v . t let v be Path of dr,cr; ::_thesis: for Ar, Br, Cr, Dr being Point of (TOP-REAL 2) st Ar `1 = a & Br `1 = b & Cr `2 = c & Dr `2 = d & ar = Ar & br = Br & cr = Cr & dr = Dr holds ex s, t being Point of I[01] st h . s = v . t let Ar, Br, Cr, Dr be Point of (TOP-REAL 2); ::_thesis: ( Ar `1 = a & Br `1 = b & Cr `2 = c & Dr `2 = d & ar = Ar & br = Br & cr = Cr & dr = Dr implies ex s, t being Point of I[01] st h . s = v . t ) assume A1: ( Ar `1 = a & Br `1 = b & Cr `2 = c & Dr `2 = d & ar = Ar & br = Br & cr = Cr & dr = Dr ) ; ::_thesis: ex s, t being Point of I[01] st h . s = v . t set TR = Trectangle (a,b,c,d); percases ( Trectangle (a,b,c,d) is empty or not Trectangle (a,b,c,d) is empty ) ; supposeA2: Trectangle (a,b,c,d) is empty ; ::_thesis: ex s, t being Point of I[01] st h . s = v . t take 1[01] ; ::_thesis: ex t being Point of I[01] st h . 1[01] = v . t take 1[01] ; ::_thesis: h . 1[01] = v . 1[01] thus h . 1[01] = v . 1[01] by A2; ::_thesis: verum end; suppose not Trectangle (a,b,c,d) is empty ; ::_thesis: ex s, t being Point of I[01] st h . s = v . t then reconsider TR = Trectangle (a,b,c,d) as non empty convex SubSpace of TOP-REAL 2 ; reconsider ar = ar, br = br, cr = cr, dr = dr as Point of TR ; reconsider h = h as Path of ar,br ; reconsider v = v as Path of dr,cr ; A3: ( h . 0 = ar & h . 1 = br ) by BORSUK_2:def_4; the carrier of TR is Subset of (TOP-REAL 2) by TSEP_1:1; then reconsider f = h, g = - v as Function of I[01],(TOP-REAL 2) by FUNCT_2:7; A4: ( (- v) . 0 = cr & (- v) . 1 = dr ) by BORSUK_2:def_4; A5: for r being Point of I[01] holds ( a <= (f . r) `1 & (f . r) `1 <= b & a <= (g . r) `1 & (g . r) `1 <= b & c <= (f . r) `2 & (f . r) `2 <= d & c <= (g . r) `2 & (g . r) `2 <= d ) proof let r be Point of I[01]; ::_thesis: ( a <= (f . r) `1 & (f . r) `1 <= b & a <= (g . r) `1 & (g . r) `1 <= b & c <= (f . r) `2 & (f . r) `2 <= d & c <= (g . r) `2 & (g . r) `2 <= d ) A6: the carrier of TR = closed_inside_of_rectangle (a,b,c,d) by PRE_TOPC:8 .= { p where p is Point of (TOP-REAL 2) : ( a <= p `1 & p `1 <= b & c <= p `2 & p `2 <= d ) } by JGRAPH_6:def_2 ; (- v) . r in the carrier of TR ; then A7: ex p being Point of (TOP-REAL 2) st ( (- v) . r = p & a <= p `1 & p `1 <= b & c <= p `2 & p `2 <= d ) by A6; h . r in the carrier of TR ; then ex p being Point of (TOP-REAL 2) st ( h . r = p & a <= p `1 & p `1 <= b & c <= p `2 & p `2 <= d ) by A6; hence ( a <= (f . r) `1 & (f . r) `1 <= b & a <= (g . r) `1 & (g . r) `1 <= b & c <= (f . r) `2 & (f . r) `2 <= d & c <= (g . r) `2 & (g . r) `2 <= d ) by A7; ::_thesis: verum end; ( f is continuous & g is continuous ) by PRE_TOPC:26; then rng f meets rng g by A1, A3, A4, A5, Th5, BORSUK_1:def_14, BORSUK_1:def_15; then consider y being set such that A8: y in rng f and A9: y in rng g by XBOOLE_0:3; consider t being set such that A10: t in dom g and A11: g . t = y by A9, FUNCT_1:def_3; consider s being set such that A12: s in dom f and A13: f . s = y by A8, FUNCT_1:def_3; reconsider s = s, t = t as Point of I[01] by A12, A10; reconsider t1 = 1 - t as Point of I[01] by JORDAN5B:4; take s ; ::_thesis: ex t being Point of I[01] st h . s = v . t take t1 ; ::_thesis: h . s = v . t1 dr,cr are_connected by BORSUK_2:def_3; hence h . s = v . t1 by A13, A11, BORSUK_2:def_6; ::_thesis: verum end; end; end;