:: JORDAN14 semantic presentation begin theorem Th1: :: JORDAN14:1 for f being non constant standard special_circular_sequence holds ( BDD (L~ f) = RightComp f or BDD (L~ f) = LeftComp f ) proof let f be non constant standard special_circular_sequence; ::_thesis: ( BDD (L~ f) = RightComp f or BDD (L~ f) = LeftComp f ) BDD (L~ f) is_inside_component_of L~ f by JORDAN2C:108; then BDD (L~ f) is_a_component_of (L~ f) ` by JORDAN2C:def_2; hence ( BDD (L~ f) = RightComp f or BDD (L~ f) = LeftComp f ) by JORDAN1H:24; ::_thesis: verum end; theorem :: JORDAN14:2 for f being non constant standard special_circular_sequence holds ( UBD (L~ f) = RightComp f or UBD (L~ f) = LeftComp f ) proof let f be non constant standard special_circular_sequence; ::_thesis: ( UBD (L~ f) = RightComp f or UBD (L~ f) = LeftComp f ) UBD (L~ f) is_outside_component_of L~ f by JORDAN2C:68; then UBD (L~ f) is_a_component_of (L~ f) ` by JORDAN2C:def_3; hence ( UBD (L~ f) = RightComp f or UBD (L~ f) = LeftComp f ) by JORDAN1H:24; ::_thesis: verum end; theorem :: JORDAN14:3 for G being Go-board for f being FinSequence of (TOP-REAL 2) for k being Element of NAT st 1 <= k & k + 1 <= len f & f is_sequence_on G holds left_cell (f,k,G) is closed proof let G be Go-board; ::_thesis: for f being FinSequence of (TOP-REAL 2) for k being Element of NAT st 1 <= k & k + 1 <= len f & f is_sequence_on G holds left_cell (f,k,G) is closed let f be FinSequence of (TOP-REAL 2); ::_thesis: for k being Element of NAT st 1 <= k & k + 1 <= len f & f is_sequence_on G holds left_cell (f,k,G) is closed let k be Element of NAT ; ::_thesis: ( 1 <= k & k + 1 <= len f & f is_sequence_on G implies left_cell (f,k,G) is closed ) assume that A1: 1 <= k and A2: k + 1 <= len f and A3: f is_sequence_on G ; ::_thesis: left_cell (f,k,G) is closed consider i1, j1, i2, j2 being Element of NAT such that A4: [i1,j1] in Indices G and A5: f /. k = G * (i1,j1) and A6: [i2,j2] in Indices G and A7: f /. (k + 1) = G * (i2,j2) and A8: ( ( i1 = i2 & j1 + 1 = j2 ) or ( i1 + 1 = i2 & j1 = j2 ) or ( i1 = i2 + 1 & j1 = j2 ) or ( i1 = i2 & j1 = j2 + 1 ) ) by A1, A2, A3, JORDAN8:3; ( ( i1 = i2 & j1 + 1 = j2 & left_cell (f,k,G) = cell (G,(i1 -' 1),j1) ) or ( i1 + 1 = i2 & j1 = j2 & left_cell (f,k,G) = cell (G,i1,j1) ) or ( i1 = i2 + 1 & j1 = j2 & left_cell (f,k,G) = cell (G,i2,(j2 -' 1)) ) or ( i1 = i2 & j1 = j2 + 1 & left_cell (f,k,G) = cell (G,i1,j2) ) ) by A1, A2, A3, A4, A5, A6, A7, A8, GOBRD13:def_3; hence left_cell (f,k,G) is closed by GOBRD11:33; ::_thesis: verum end; theorem Th4: :: JORDAN14:4 for G being Go-board for p being Point of (TOP-REAL 2) for i, j being Element of NAT st 1 <= i & i + 1 <= len G & 1 <= j & j + 1 <= width G holds ( p in Int (cell (G,i,j)) iff ( (G * (i,j)) `1 < p `1 & p `1 < (G * ((i + 1),j)) `1 & (G * (i,j)) `2 < p `2 & p `2 < (G * (i,(j + 1))) `2 ) ) proof let G be Go-board; ::_thesis: for p being Point of (TOP-REAL 2) for i, j being Element of NAT st 1 <= i & i + 1 <= len G & 1 <= j & j + 1 <= width G holds ( p in Int (cell (G,i,j)) iff ( (G * (i,j)) `1 < p `1 & p `1 < (G * ((i + 1),j)) `1 & (G * (i,j)) `2 < p `2 & p `2 < (G * (i,(j + 1))) `2 ) ) let p be Point of (TOP-REAL 2); ::_thesis: for i, j being Element of NAT st 1 <= i & i + 1 <= len G & 1 <= j & j + 1 <= width G holds ( p in Int (cell (G,i,j)) iff ( (G * (i,j)) `1 < p `1 & p `1 < (G * ((i + 1),j)) `1 & (G * (i,j)) `2 < p `2 & p `2 < (G * (i,(j + 1))) `2 ) ) let i, j be Element of NAT ; ::_thesis: ( 1 <= i & i + 1 <= len G & 1 <= j & j + 1 <= width G implies ( p in Int (cell (G,i,j)) iff ( (G * (i,j)) `1 < p `1 & p `1 < (G * ((i + 1),j)) `1 & (G * (i,j)) `2 < p `2 & p `2 < (G * (i,(j + 1))) `2 ) ) ) assume that A1: 1 <= i and A2: i + 1 <= len G and A3: 1 <= j and A4: j + 1 <= width G ; ::_thesis: ( p in Int (cell (G,i,j)) iff ( (G * (i,j)) `1 < p `1 & p `1 < (G * ((i + 1),j)) `1 & (G * (i,j)) `2 < p `2 & p `2 < (G * (i,(j + 1))) `2 ) ) set Z = { |[r,s]| where r, s is Real : ( (G * (i,1)) `1 < r & r < (G * ((i + 1),1)) `1 & (G * (1,j)) `2 < s & s < (G * (1,(j + 1))) `2 ) } ; A5: j < width G by A4, NAT_1:13; i + 1 >= 1 by NAT_1:11; then A6: (G * ((i + 1),1)) `1 = (G * ((i + 1),j)) `1 by A2, A3, A5, GOBOARD5:2; A7: i < len G by A2, NAT_1:13; then A8: (G * (1,j)) `2 = (G * (i,j)) `2 by A1, A3, A5, GOBOARD5:1; j + 1 >= 1 by NAT_1:11; then A9: (G * (1,(j + 1))) `2 = (G * (i,(j + 1))) `2 by A1, A4, A7, GOBOARD5:1; A10: (G * (i,1)) `1 = (G * (i,j)) `1 by A1, A3, A7, A5, GOBOARD5:2; thus ( p in Int (cell (G,i,j)) implies ( (G * (i,j)) `1 < p `1 & p `1 < (G * ((i + 1),j)) `1 & (G * (i,j)) `2 < p `2 & p `2 < (G * (i,(j + 1))) `2 ) ) ::_thesis: ( (G * (i,j)) `1 < p `1 & p `1 < (G * ((i + 1),j)) `1 & (G * (i,j)) `2 < p `2 & p `2 < (G * (i,(j + 1))) `2 implies p in Int (cell (G,i,j)) ) proof assume p in Int (cell (G,i,j)) ; ::_thesis: ( (G * (i,j)) `1 < p `1 & p `1 < (G * ((i + 1),j)) `1 & (G * (i,j)) `2 < p `2 & p `2 < (G * (i,(j + 1))) `2 ) then p in { |[r,s]| where r, s is Real : ( (G * (i,1)) `1 < r & r < (G * ((i + 1),1)) `1 & (G * (1,j)) `2 < s & s < (G * (1,(j + 1))) `2 ) } by A1, A3, A7, A5, GOBOARD6:26; then ex r, s being Real st ( p = |[r,s]| & (G * (i,1)) `1 < r & r < (G * ((i + 1),1)) `1 & (G * (1,j)) `2 < s & s < (G * (1,(j + 1))) `2 ) ; hence ( (G * (i,j)) `1 < p `1 & p `1 < (G * ((i + 1),j)) `1 & (G * (i,j)) `2 < p `2 & p `2 < (G * (i,(j + 1))) `2 ) by A10, A6, A8, A9, EUCLID:52; ::_thesis: verum end; assume that A11: (G * (i,j)) `1 < p `1 and A12: p `1 < (G * ((i + 1),j)) `1 and A13: (G * (i,j)) `2 < p `2 and A14: p `2 < (G * (i,(j + 1))) `2 ; ::_thesis: p in Int (cell (G,i,j)) p = |[(p `1),(p `2)]| by EUCLID:53; then p in { |[r,s]| where r, s is Real : ( (G * (i,1)) `1 < r & r < (G * ((i + 1),1)) `1 & (G * (1,j)) `2 < s & s < (G * (1,(j + 1))) `2 ) } by A10, A6, A8, A9, A11, A12, A13, A14; hence p in Int (cell (G,i,j)) by A1, A3, A7, A5, GOBOARD6:26; ::_thesis: verum end; theorem Th5: :: JORDAN14:5 for f being non constant standard special_circular_sequence holds BDD (L~ f) is connected proof let f be non constant standard special_circular_sequence; ::_thesis: BDD (L~ f) is connected ( BDD (L~ f) = RightComp f or BDD (L~ f) = LeftComp f ) by Th1; hence BDD (L~ f) is connected ; ::_thesis: verum end; registration let f be non constant standard special_circular_sequence; cluster BDD (L~ f) -> connected ; coherence BDD (L~ f) is connected by Th5; end; definition let C be Simple_closed_curve; let n be Element of NAT ; func SpanStart (C,n) -> Point of (TOP-REAL 2) equals :: JORDAN14:def 1 (Gauge (C,n)) * ((X-SpanStart (C,n)),(Y-SpanStart (C,n))); coherence (Gauge (C,n)) * ((X-SpanStart (C,n)),(Y-SpanStart (C,n))) is Point of (TOP-REAL 2) ; end; :: deftheorem defines SpanStart JORDAN14:def_1_:_ for C being Simple_closed_curve for n being Element of NAT holds SpanStart (C,n) = (Gauge (C,n)) * ((X-SpanStart (C,n)),(Y-SpanStart (C,n))); theorem Th6: :: JORDAN14:6 for C being Simple_closed_curve for n being Element of NAT st n is_sufficiently_large_for C holds SpanStart (C,n) in BDD C proof let C be Simple_closed_curve; ::_thesis: for n being Element of NAT st n is_sufficiently_large_for C holds SpanStart (C,n) in BDD C let n be Element of NAT ; ::_thesis: ( n is_sufficiently_large_for C implies SpanStart (C,n) in BDD C ) A1: 1 <= (X-SpanStart (C,n)) -' 1 by JORDAN1H:50; A2: (X-SpanStart (C,n)) -' 1 < len (Gauge (C,n)) by JORDAN1H:50; assume A3: n is_sufficiently_large_for C ; ::_thesis: SpanStart (C,n) in BDD C then A4: cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),(Y-SpanStart (C,n))) c= BDD C by JORDAN11:6; A5: Y-SpanStart (C,n) <= width (Gauge (C,n)) by A3, JORDAN11:7; 1 < Y-SpanStart (C,n) by A3, JORDAN11:7; then LSeg (((Gauge (C,n)) * (((X-SpanStart (C,n)) -' 1),(Y-SpanStart (C,n)))),((Gauge (C,n)) * ((((X-SpanStart (C,n)) -' 1) + 1),(Y-SpanStart (C,n))))) c= cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),(Y-SpanStart (C,n))) by A1, A2, A5, GOBOARD5:22; then A6: LSeg (((Gauge (C,n)) * (((X-SpanStart (C,n)) -' 1),(Y-SpanStart (C,n)))),((Gauge (C,n)) * ((((X-SpanStart (C,n)) -' 1) + 1),(Y-SpanStart (C,n))))) c= BDD C by A4, XBOOLE_1:1; A7: 2 < X-SpanStart (C,n) by JORDAN1H:49; (Gauge (C,n)) * ((((X-SpanStart (C,n)) -' 1) + 1),(Y-SpanStart (C,n))) in LSeg (((Gauge (C,n)) * (((X-SpanStart (C,n)) -' 1),(Y-SpanStart (C,n)))),((Gauge (C,n)) * ((((X-SpanStart (C,n)) -' 1) + 1),(Y-SpanStart (C,n))))) by RLTOPSP1:68; then (Gauge (C,n)) * ((((X-SpanStart (C,n)) -' 1) + 1),(Y-SpanStart (C,n))) in BDD C by A6; hence SpanStart (C,n) in BDD C by A7, XREAL_1:235, XXREAL_0:2; ::_thesis: verum end; theorem Th7: :: JORDAN14:7 for C being Simple_closed_curve for n, k being Element of NAT st n is_sufficiently_large_for C & 1 <= k & k + 1 <= len (Span (C,n)) holds ( right_cell ((Span (C,n)),k,(Gauge (C,n))) misses C & left_cell ((Span (C,n)),k,(Gauge (C,n))) meets C ) proof let C be Simple_closed_curve; ::_thesis: for n, k being Element of NAT st n is_sufficiently_large_for C & 1 <= k & k + 1 <= len (Span (C,n)) holds ( right_cell ((Span (C,n)),k,(Gauge (C,n))) misses C & left_cell ((Span (C,n)),k,(Gauge (C,n))) meets C ) let n, k be Element of NAT ; ::_thesis: ( n is_sufficiently_large_for C & 1 <= k & k + 1 <= len (Span (C,n)) implies ( right_cell ((Span (C,n)),k,(Gauge (C,n))) misses C & left_cell ((Span (C,n)),k,(Gauge (C,n))) meets C ) ) set G = Gauge (C,n); set f = Span (C,n); defpred S1[ Element of NAT ] means for m being Element of NAT st 1 <= m & m + 1 <= len ((Span (C,n)) | $1) holds ( right_cell (((Span (C,n)) | $1),m,(Gauge (C,n))) misses C & left_cell (((Span (C,n)) | $1),m,(Gauge (C,n))) meets C ); A1: (Span (C,n)) | (len (Span (C,n))) = Span (C,n) by FINSEQ_1:58; assume A2: n is_sufficiently_large_for C ; ::_thesis: ( not 1 <= k or not k + 1 <= len (Span (C,n)) or ( right_cell ((Span (C,n)),k,(Gauge (C,n))) misses C & left_cell ((Span (C,n)),k,(Gauge (C,n))) meets C ) ) then A3: Span (C,n) is_sequence_on Gauge (C,n) by JORDAN13:def_1; A4: (Span (C,n)) /. 2 = (Gauge (C,n)) * (((X-SpanStart (C,n)) -' 1),(Y-SpanStart (C,n))) by A2, JORDAN13:def_1; A5: (Span (C,n)) /. 1 = (Gauge (C,n)) * ((X-SpanStart (C,n)),(Y-SpanStart (C,n))) by A2, JORDAN13:def_1; 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: for m being Element of NAT st 1 <= m & m + 1 <= len ((Span (C,n)) | k) holds ( right_cell (((Span (C,n)) | k),m,(Gauge (C,n))) misses C & left_cell (((Span (C,n)) | k),m,(Gauge (C,n))) meets C ) ; ::_thesis: S1[k + 1] A8: (Span (C,n)) | (k + 1) is_sequence_on Gauge (C,n) by A3, GOBOARD1:22; A9: (Span (C,n)) | k is_sequence_on Gauge (C,n) by A3, GOBOARD1:22; percases ( k >= len (Span (C,n)) or k < len (Span (C,n)) ) ; supposeA10: k >= len (Span (C,n)) ; ::_thesis: S1[k + 1] then A11: (Span (C,n)) | (k + 1) = Span (C,n) by FINSEQ_1:58, NAT_1:12; (Span (C,n)) | k = Span (C,n) by A10, FINSEQ_1:58; hence S1[k + 1] by A7, A11; ::_thesis: verum end; supposeA12: k < len (Span (C,n)) ; ::_thesis: S1[k + 1] let m be Element of NAT ; ::_thesis: ( 1 <= m & m + 1 <= len ((Span (C,n)) | (k + 1)) implies ( right_cell (((Span (C,n)) | (k + 1)),m,(Gauge (C,n))) misses C & left_cell (((Span (C,n)) | (k + 1)),m,(Gauge (C,n))) meets C ) ) assume that A13: 1 <= m and A14: m + 1 <= len ((Span (C,n)) | (k + 1)) ; ::_thesis: ( right_cell (((Span (C,n)) | (k + 1)),m,(Gauge (C,n))) misses C & left_cell (((Span (C,n)) | (k + 1)),m,(Gauge (C,n))) meets C ) A15: k + 1 <= len (Span (C,n)) by A12, NAT_1:13; then A16: len ((Span (C,n)) | (k + 1)) = k + 1 by FINSEQ_1:59; A17: len ((Span (C,n)) | k) = k by A12, FINSEQ_1:59; now__::_thesis:_(_right_cell_(((Span_(C,n))_|_(k_+_1)),m,(Gauge_(C,n)))_misses_C_&_left_cell_(((Span_(C,n))_|_(k_+_1)),m,(Gauge_(C,n)))_meets_C_) percases ( k = 0 or k = 1 or k > 1 ) by NAT_1:25; supposeA18: k = 0 ; ::_thesis: ( right_cell (((Span (C,n)) | (k + 1)),m,(Gauge (C,n))) misses C & left_cell (((Span (C,n)) | (k + 1)),m,(Gauge (C,n))) meets C ) 1 <= m + 1 by NAT_1:12; then m + 1 = 0 + 1 by A16, A14, A18, XXREAL_0:1; hence ( right_cell (((Span (C,n)) | (k + 1)),m,(Gauge (C,n))) misses C & left_cell (((Span (C,n)) | (k + 1)),m,(Gauge (C,n))) meets C ) by A13; ::_thesis: verum end; supposeA19: k = 1 ; ::_thesis: ( right_cell (((Span (C,n)) | (k + 1)),m,(Gauge (C,n))) misses C & left_cell (((Span (C,n)) | (k + 1)),m,(Gauge (C,n))) meets C ) set j = Y-SpanStart (C,n); set i = X-SpanStart (C,n); A20: (Span (C,n)) | (k + 1) = <*((Gauge (C,n)) * ((X-SpanStart (C,n)),(Y-SpanStart (C,n)))),((Gauge (C,n)) * (((X-SpanStart (C,n)) -' 1),(Y-SpanStart (C,n))))*> by A5, A4, A15, A19, FINSEQ_5:81; then A21: ((Span (C,n)) | (k + 1)) /. 1 = (Gauge (C,n)) * ((X-SpanStart (C,n)),(Y-SpanStart (C,n))) by FINSEQ_4:17; 1 + 1 <= m + 1 by A13, XREAL_1:6; then A22: m + 1 = 1 + 1 by A16, A14, A19, XXREAL_0:1; A23: [((X-SpanStart (C,n)) -' 1),(Y-SpanStart (C,n))] in Indices (Gauge (C,n)) by A2, JORDAN11:9; A24: [(X-SpanStart (C,n)),(Y-SpanStart (C,n))] in Indices (Gauge (C,n)) by A2, JORDAN11:8; (X-SpanStart (C,n)) -' 1 <= X-SpanStart (C,n) by NAT_D:35; then A25: (X-SpanStart (C,n)) + 1 <> (X-SpanStart (C,n)) -' 1 by NAT_1:13; A26: Y-SpanStart (C,n) <> (Y-SpanStart (C,n)) + 1 ; A27: ((Span (C,n)) | (k + 1)) /. 2 = (Gauge (C,n)) * (((X-SpanStart (C,n)) -' 1),(Y-SpanStart (C,n))) by A20, FINSEQ_4:17; then right_cell (((Span (C,n)) | (k + 1)),m,(Gauge (C,n))) = cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),(Y-SpanStart (C,n))) by A8, A14, A21, A24, A23, A22, A26, A25, GOBRD13:def_2; hence right_cell (((Span (C,n)) | (k + 1)),m,(Gauge (C,n))) misses C by A2, JORDAN11:11; ::_thesis: left_cell (((Span (C,n)) | (k + 1)),m,(Gauge (C,n))) meets C left_cell (((Span (C,n)) | (k + 1)),m,(Gauge (C,n))) = cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),((Y-SpanStart (C,n)) -' 1)) by A8, A14, A21, A27, A24, A23, A22, A26, A25, GOBRD13:def_3; hence left_cell (((Span (C,n)) | (k + 1)),m,(Gauge (C,n))) meets C by A2, JORDAN11:10; ::_thesis: verum end; supposeA28: k > 1 ; ::_thesis: ( right_cell (((Span (C,n)) | (k + 1)),m,(Gauge (C,n))) misses C & left_cell (((Span (C,n)) | (k + 1)),m,(Gauge (C,n))) meets C ) A29: len ((Span (C,n)) | k) <= len (Span (C,n)) by FINSEQ_5:16; A30: 1 <= (len ((Span (C,n)) | k)) -' 1 by A17, A28, NAT_D:49; A31: ((len ((Span (C,n)) | k)) -' 1) + 1 = len ((Span (C,n)) | k) by A17, A28, XREAL_1:235; then A32: ((len ((Span (C,n)) | k)) -' 1) + (1 + 1) = (len ((Span (C,n)) | k)) + 1 ; now__::_thesis:_(_right_cell_(((Span_(C,n))_|_(k_+_1)),m,(Gauge_(C,n)))_misses_C_&_left_cell_(((Span_(C,n))_|_(k_+_1)),m,(Gauge_(C,n)))_meets_C_) percases ( m + 1 = len ((Span (C,n)) | (k + 1)) or m + 1 <> len ((Span (C,n)) | (k + 1)) ) ; supposeA33: m + 1 = len ((Span (C,n)) | (k + 1)) ; ::_thesis: ( right_cell (((Span (C,n)) | (k + 1)),m,(Gauge (C,n))) misses C & left_cell (((Span (C,n)) | (k + 1)),m,(Gauge (C,n))) meets C ) left_cell (((Span (C,n)) | k),((len ((Span (C,n)) | k)) -' 1),(Gauge (C,n))) meets C by A7, A30, A31; then A34: left_cell ((Span (C,n)),((len ((Span (C,n)) | k)) -' 1),(Gauge (C,n))) meets C by A3, A17, A30, A31, A29, GOBRD13:31; consider i1, j1, i2, j2 being Element of NAT such that A35: [i1,j1] in Indices (Gauge (C,n)) and A36: (Span (C,n)) /. ((len ((Span (C,n)) | k)) -' 1) = (Gauge (C,n)) * (i1,j1) and A37: [i2,j2] in Indices (Gauge (C,n)) and A38: (Span (C,n)) /. (len ((Span (C,n)) | k)) = (Gauge (C,n)) * (i2,j2) and ( ( i1 = i2 & j1 + 1 = j2 ) or ( i1 + 1 = i2 & j1 = j2 ) or ( i1 = i2 + 1 & j1 = j2 ) or ( i1 = i2 & j1 = j2 + 1 ) ) by A3, A12, A17, A30, A31, JORDAN8:3; 1 <= i2 by A37, MATRIX_1:38; then A39: (i2 -' 1) + 1 = i2 by XREAL_1:235; A40: 1 <= j2 by A37, MATRIX_1:38; then A41: (j2 -' 1) + 1 = j2 by XREAL_1:235; right_cell (((Span (C,n)) | k),((len ((Span (C,n)) | k)) -' 1),(Gauge (C,n))) misses C by A7, A30, A31; then A42: right_cell ((Span (C,n)),((len ((Span (C,n)) | k)) -' 1),(Gauge (C,n))) misses C by A3, A17, A30, A31, A29, GOBRD13:31; now__::_thesis:_(_right_cell_(((Span_(C,n))_|_(k_+_1)),m,(Gauge_(C,n)))_misses_C_&_left_cell_(((Span_(C,n))_|_(k_+_1)),m,(Gauge_(C,n)))_meets_C_) percases ( ( front_right_cell ((Span (C,n)),((len ((Span (C,n)) | k)) -' 1),(Gauge (C,n))) misses C & front_left_cell ((Span (C,n)),((len ((Span (C,n)) | k)) -' 1),(Gauge (C,n))) misses C ) or ( front_right_cell ((Span (C,n)),((len ((Span (C,n)) | k)) -' 1),(Gauge (C,n))) misses C & front_left_cell ((Span (C,n)),((len ((Span (C,n)) | k)) -' 1),(Gauge (C,n))) meets C ) or front_right_cell ((Span (C,n)),((len ((Span (C,n)) | k)) -' 1),(Gauge (C,n))) meets C ) ; supposeA43: ( front_right_cell ((Span (C,n)),((len ((Span (C,n)) | k)) -' 1),(Gauge (C,n))) misses C & front_left_cell ((Span (C,n)),((len ((Span (C,n)) | k)) -' 1),(Gauge (C,n))) misses C ) ; ::_thesis: ( right_cell (((Span (C,n)) | (k + 1)),m,(Gauge (C,n))) misses C & left_cell (((Span (C,n)) | (k + 1)),m,(Gauge (C,n))) meets C ) then A44: Span (C,n) turns_left (len ((Span (C,n)) | k)) -' 1, Gauge (C,n) by A2, A15, A17, A30, A32, JORDAN13:def_1; now__::_thesis:_(_right_cell_(((Span_(C,n))_|_(k_+_1)),m,(Gauge_(C,n)))_misses_C_&_left_cell_(((Span_(C,n))_|_(k_+_1)),m,(Gauge_(C,n)))_meets_C_) percases ( ( i1 = i2 & j1 + 1 = j2 & [(i2 -' 1),j2] in Indices (Gauge (C,n)) & (Span (C,n)) /. (((len ((Span (C,n)) | k)) -' 1) + 2) = (Gauge (C,n)) * ((i2 -' 1),j2) ) or ( i1 + 1 = i2 & j1 = j2 & [i2,(j2 + 1)] in Indices (Gauge (C,n)) & (Span (C,n)) /. (((len ((Span (C,n)) | k)) -' 1) + 2) = (Gauge (C,n)) * (i2,(j2 + 1)) ) or ( i1 = i2 + 1 & j1 = j2 & [i2,(j2 -' 1)] in Indices (Gauge (C,n)) & (Span (C,n)) /. (((len ((Span (C,n)) | k)) -' 1) + 2) = (Gauge (C,n)) * (i2,(j2 -' 1)) ) or ( i1 = i2 & j1 = j2 + 1 & [(i2 + 1),j2] in Indices (Gauge (C,n)) & (Span (C,n)) /. (((len ((Span (C,n)) | k)) -' 1) + 2) = (Gauge (C,n)) * ((i2 + 1),j2) ) ) by A31, A35, A36, A37, A38, A44, GOBRD13:def_7; supposethat A45: ( i1 = i2 & j1 + 1 = j2 ) and A46: [(i2 -' 1),j2] in Indices (Gauge (C,n)) and A47: (Span (C,n)) /. (((len ((Span (C,n)) | k)) -' 1) + 2) = (Gauge (C,n)) * ((i2 -' 1),j2) ; ::_thesis: ( right_cell (((Span (C,n)) | (k + 1)),m,(Gauge (C,n))) misses C & left_cell (((Span (C,n)) | (k + 1)),m,(Gauge (C,n))) meets C ) cell ((Gauge (C,n)),(i1 -' 1),(j1 + 1)) misses C by A3, A30, A31, A29, A35, A36, A37, A38, A43, A45, GOBRD13:34; then right_cell ((Span (C,n)),m,(Gauge (C,n))) misses C by A3, A15, A16, A17, A28, A31, A33, A37, A38, A39, A45, A46, A47, GOBRD13:26; hence right_cell (((Span (C,n)) | (k + 1)),m,(Gauge (C,n))) misses C by A3, A15, A16, A13, A33, GOBRD13:31; ::_thesis: left_cell (((Span (C,n)) | (k + 1)),m,(Gauge (C,n))) meets C A48: (j1 + 1) -' 1 = j1 by NAT_D:34; cell ((Gauge (C,n)),(i1 -' 1),j1) meets C by A3, A12, A17, A30, A31, A35, A36, A37, A38, A34, A45, GOBRD13:21; then left_cell ((Span (C,n)),m,(Gauge (C,n))) meets C by A3, A15, A16, A17, A28, A31, A33, A37, A38, A39, A45, A46, A47, A48, GOBRD13:25; hence left_cell (((Span (C,n)) | (k + 1)),m,(Gauge (C,n))) meets C by A3, A15, A16, A13, A33, GOBRD13:31; ::_thesis: verum end; supposethat A49: ( i1 + 1 = i2 & j1 = j2 ) and A50: [i2,(j2 + 1)] in Indices (Gauge (C,n)) and A51: (Span (C,n)) /. (((len ((Span (C,n)) | k)) -' 1) + 2) = (Gauge (C,n)) * (i2,(j2 + 1)) ; ::_thesis: ( right_cell (((Span (C,n)) | (k + 1)),m,(Gauge (C,n))) misses C & left_cell (((Span (C,n)) | (k + 1)),m,(Gauge (C,n))) meets C ) cell ((Gauge (C,n)),i2,j2) misses C by A3, A30, A31, A29, A35, A36, A37, A38, A43, A49, GOBRD13:36; then right_cell ((Span (C,n)),m,(Gauge (C,n))) misses C by A3, A15, A16, A17, A28, A31, A33, A37, A38, A50, A51, GOBRD13:22; hence right_cell (((Span (C,n)) | (k + 1)),m,(Gauge (C,n))) misses C by A3, A15, A16, A13, A33, GOBRD13:31; ::_thesis: left_cell (((Span (C,n)) | (k + 1)),m,(Gauge (C,n))) meets C A52: (i1 + 1) -' 1 = i1 by NAT_D:34; cell ((Gauge (C,n)),i1,j2) meets C by A3, A12, A17, A30, A31, A35, A36, A37, A38, A34, A49, GOBRD13:23; then left_cell ((Span (C,n)),m,(Gauge (C,n))) meets C by A3, A15, A16, A17, A28, A31, A33, A37, A38, A49, A50, A51, A52, GOBRD13:21; hence left_cell (((Span (C,n)) | (k + 1)),m,(Gauge (C,n))) meets C by A3, A15, A16, A13, A33, GOBRD13:31; ::_thesis: verum end; supposethat A53: ( i1 = i2 + 1 & j1 = j2 ) and A54: [i2,(j2 -' 1)] in Indices (Gauge (C,n)) and A55: (Span (C,n)) /. (((len ((Span (C,n)) | k)) -' 1) + 2) = (Gauge (C,n)) * (i2,(j2 -' 1)) ; ::_thesis: ( right_cell (((Span (C,n)) | (k + 1)),m,(Gauge (C,n))) misses C & left_cell (((Span (C,n)) | (k + 1)),m,(Gauge (C,n))) meets C ) cell ((Gauge (C,n)),(i2 -' 1),(j2 -' 1)) misses C by A3, A30, A31, A29, A35, A36, A37, A38, A43, A53, GOBRD13:38; then right_cell ((Span (C,n)),m,(Gauge (C,n))) misses C by A3, A15, A16, A17, A28, A31, A33, A37, A38, A41, A54, A55, GOBRD13:28; hence right_cell (((Span (C,n)) | (k + 1)),m,(Gauge (C,n))) misses C by A3, A15, A16, A13, A33, GOBRD13:31; ::_thesis: left_cell (((Span (C,n)) | (k + 1)),m,(Gauge (C,n))) meets C cell ((Gauge (C,n)),i2,(j2 -' 1)) meets C by A3, A12, A17, A30, A31, A35, A36, A37, A38, A34, A53, GOBRD13:25; then left_cell ((Span (C,n)),m,(Gauge (C,n))) meets C by A3, A15, A16, A17, A28, A31, A33, A37, A38, A41, A54, A55, GOBRD13:27; hence left_cell (((Span (C,n)) | (k + 1)),m,(Gauge (C,n))) meets C by A3, A15, A16, A13, A33, GOBRD13:31; ::_thesis: verum end; supposethat A56: ( i1 = i2 & j1 = j2 + 1 ) and A57: [(i2 + 1),j2] in Indices (Gauge (C,n)) and A58: (Span (C,n)) /. (((len ((Span (C,n)) | k)) -' 1) + 2) = (Gauge (C,n)) * ((i2 + 1),j2) ; ::_thesis: ( right_cell (((Span (C,n)) | (k + 1)),m,(Gauge (C,n))) misses C & left_cell (((Span (C,n)) | (k + 1)),m,(Gauge (C,n))) meets C ) cell ((Gauge (C,n)),i1,(j2 -' 1)) misses C by A3, A30, A31, A29, A35, A36, A37, A38, A43, A56, GOBRD13:40; then right_cell ((Span (C,n)),m,(Gauge (C,n))) misses C by A3, A15, A16, A17, A28, A31, A33, A37, A38, A56, A57, A58, GOBRD13:24; hence right_cell (((Span (C,n)) | (k + 1)),m,(Gauge (C,n))) misses C by A3, A15, A16, A13, A33, GOBRD13:31; ::_thesis: left_cell (((Span (C,n)) | (k + 1)),m,(Gauge (C,n))) meets C cell ((Gauge (C,n)),i1,j2) meets C by A3, A12, A17, A30, A31, A35, A36, A37, A38, A34, A56, GOBRD13:27; then left_cell ((Span (C,n)),m,(Gauge (C,n))) meets C by A3, A15, A16, A17, A28, A31, A33, A37, A38, A56, A57, A58, GOBRD13:23; hence left_cell (((Span (C,n)) | (k + 1)),m,(Gauge (C,n))) meets C by A3, A15, A16, A13, A33, GOBRD13:31; ::_thesis: verum end; end; end; hence ( right_cell (((Span (C,n)) | (k + 1)),m,(Gauge (C,n))) misses C & left_cell (((Span (C,n)) | (k + 1)),m,(Gauge (C,n))) meets C ) ; ::_thesis: verum end; supposeA59: ( front_right_cell ((Span (C,n)),((len ((Span (C,n)) | k)) -' 1),(Gauge (C,n))) misses C & front_left_cell ((Span (C,n)),((len ((Span (C,n)) | k)) -' 1),(Gauge (C,n))) meets C ) ; ::_thesis: ( right_cell (((Span (C,n)) | (k + 1)),m,(Gauge (C,n))) misses C & left_cell (((Span (C,n)) | (k + 1)),m,(Gauge (C,n))) meets C ) then A60: Span (C,n) goes_straight (len ((Span (C,n)) | k)) -' 1, Gauge (C,n) by A2, A15, A17, A30, A32, JORDAN13:def_1; now__::_thesis:_(_right_cell_(((Span_(C,n))_|_(k_+_1)),m,(Gauge_(C,n)))_misses_C_&_left_cell_(((Span_(C,n))_|_(k_+_1)),m,(Gauge_(C,n)))_meets_C_) percases ( ( i1 = i2 & j1 + 1 = j2 & [i2,(j2 + 1)] in Indices (Gauge (C,n)) & (Span (C,n)) /. (((len ((Span (C,n)) | k)) -' 1) + 2) = (Gauge (C,n)) * (i2,(j2 + 1)) ) or ( i1 + 1 = i2 & j1 = j2 & [(i2 + 1),j2] in Indices (Gauge (C,n)) & (Span (C,n)) /. (((len ((Span (C,n)) | k)) -' 1) + 2) = (Gauge (C,n)) * ((i2 + 1),j2) ) or ( i1 = i2 + 1 & j1 = j2 & [(i2 -' 1),j2] in Indices (Gauge (C,n)) & (Span (C,n)) /. (((len ((Span (C,n)) | k)) -' 1) + 2) = (Gauge (C,n)) * ((i2 -' 1),j2) ) or ( i1 = i2 & j1 = j2 + 1 & [i2,(j2 -' 1)] in Indices (Gauge (C,n)) & (Span (C,n)) /. (((len ((Span (C,n)) | k)) -' 1) + 2) = (Gauge (C,n)) * (i2,(j2 -' 1)) ) ) by A31, A35, A36, A37, A38, A60, GOBRD13:def_8; supposethat A61: ( i1 = i2 & j1 + 1 = j2 ) and A62: [i2,(j2 + 1)] in Indices (Gauge (C,n)) and A63: (Span (C,n)) /. (((len ((Span (C,n)) | k)) -' 1) + 2) = (Gauge (C,n)) * (i2,(j2 + 1)) ; ::_thesis: ( right_cell (((Span (C,n)) | (k + 1)),m,(Gauge (C,n))) misses C & left_cell (((Span (C,n)) | (k + 1)),m,(Gauge (C,n))) meets C ) cell ((Gauge (C,n)),i1,(j1 + 1)) misses C by A3, A30, A31, A29, A35, A36, A37, A38, A59, A61, GOBRD13:35; then right_cell ((Span (C,n)),m,(Gauge (C,n))) misses C by A3, A15, A16, A17, A28, A31, A33, A37, A38, A61, A62, A63, GOBRD13:22; hence right_cell (((Span (C,n)) | (k + 1)),m,(Gauge (C,n))) misses C by A3, A15, A16, A13, A33, GOBRD13:31; ::_thesis: left_cell (((Span (C,n)) | (k + 1)),m,(Gauge (C,n))) meets C cell ((Gauge (C,n)),(i2 -' 1),j2) meets C by A3, A12, A17, A30, A31, A35, A36, A37, A38, A59, A61, GOBRD13:34; then left_cell ((Span (C,n)),m,(Gauge (C,n))) meets C by A3, A15, A16, A17, A28, A31, A33, A37, A38, A62, A63, GOBRD13:21; hence left_cell (((Span (C,n)) | (k + 1)),m,(Gauge (C,n))) meets C by A3, A15, A16, A13, A33, GOBRD13:31; ::_thesis: verum end; supposethat A64: ( i1 + 1 = i2 & j1 = j2 ) and A65: [(i2 + 1),j2] in Indices (Gauge (C,n)) and A66: (Span (C,n)) /. (((len ((Span (C,n)) | k)) -' 1) + 2) = (Gauge (C,n)) * ((i2 + 1),j2) ; ::_thesis: ( right_cell (((Span (C,n)) | (k + 1)),m,(Gauge (C,n))) misses C & left_cell (((Span (C,n)) | (k + 1)),m,(Gauge (C,n))) meets C ) cell ((Gauge (C,n)),(i1 + 1),(j1 -' 1)) misses C by A3, A30, A31, A29, A35, A36, A37, A38, A59, A64, GOBRD13:37; then right_cell ((Span (C,n)),m,(Gauge (C,n))) misses C by A3, A15, A16, A17, A28, A31, A33, A37, A38, A64, A65, A66, GOBRD13:24; hence right_cell (((Span (C,n)) | (k + 1)),m,(Gauge (C,n))) misses C by A3, A15, A16, A13, A33, GOBRD13:31; ::_thesis: left_cell (((Span (C,n)) | (k + 1)),m,(Gauge (C,n))) meets C cell ((Gauge (C,n)),(i1 + 1),j1) meets C by A3, A12, A17, A30, A31, A35, A36, A37, A38, A59, A64, GOBRD13:36; then left_cell ((Span (C,n)),m,(Gauge (C,n))) meets C by A3, A15, A16, A17, A28, A31, A33, A37, A38, A64, A65, A66, GOBRD13:23; hence left_cell (((Span (C,n)) | (k + 1)),m,(Gauge (C,n))) meets C by A3, A15, A16, A13, A33, GOBRD13:31; ::_thesis: verum end; supposethat A67: ( i1 = i2 + 1 & j1 = j2 ) and A68: [(i2 -' 1),j2] in Indices (Gauge (C,n)) and A69: (Span (C,n)) /. (((len ((Span (C,n)) | k)) -' 1) + 2) = (Gauge (C,n)) * ((i2 -' 1),j2) ; ::_thesis: ( right_cell (((Span (C,n)) | (k + 1)),m,(Gauge (C,n))) misses C & left_cell (((Span (C,n)) | (k + 1)),m,(Gauge (C,n))) meets C ) cell ((Gauge (C,n)),(i2 -' 1),j2) misses C by A3, A30, A31, A29, A35, A36, A37, A38, A59, A67, GOBRD13:39; then right_cell ((Span (C,n)),m,(Gauge (C,n))) misses C by A3, A15, A16, A17, A28, A31, A33, A37, A38, A39, A68, A69, GOBRD13:26; hence right_cell (((Span (C,n)) | (k + 1)),m,(Gauge (C,n))) misses C by A3, A15, A16, A13, A33, GOBRD13:31; ::_thesis: left_cell (((Span (C,n)) | (k + 1)),m,(Gauge (C,n))) meets C cell ((Gauge (C,n)),(i2 -' 1),(j2 -' 1)) meets C by A3, A12, A17, A30, A31, A35, A36, A37, A38, A59, A67, GOBRD13:38; then left_cell ((Span (C,n)),m,(Gauge (C,n))) meets C by A3, A15, A16, A17, A28, A31, A33, A37, A38, A39, A68, A69, GOBRD13:25; hence left_cell (((Span (C,n)) | (k + 1)),m,(Gauge (C,n))) meets C by A3, A15, A16, A13, A33, GOBRD13:31; ::_thesis: verum end; supposethat A70: ( i1 = i2 & j1 = j2 + 1 ) and A71: [i2,(j2 -' 1)] in Indices (Gauge (C,n)) and A72: (Span (C,n)) /. (((len ((Span (C,n)) | k)) -' 1) + 2) = (Gauge (C,n)) * (i2,(j2 -' 1)) ; ::_thesis: ( right_cell (((Span (C,n)) | (k + 1)),m,(Gauge (C,n))) misses C & left_cell (((Span (C,n)) | (k + 1)),m,(Gauge (C,n))) meets C ) A73: (j2 -' 1) + 1 = j2 by A40, XREAL_1:235; cell ((Gauge (C,n)),(i2 -' 1),(j2 -' 1)) misses C by A3, A30, A31, A29, A35, A36, A37, A38, A59, A70, GOBRD13:41; then right_cell ((Span (C,n)),m,(Gauge (C,n))) misses C by A3, A15, A16, A17, A28, A31, A33, A37, A38, A71, A72, A73, GOBRD13:28; hence right_cell (((Span (C,n)) | (k + 1)),m,(Gauge (C,n))) misses C by A3, A15, A16, A13, A33, GOBRD13:31; ::_thesis: left_cell (((Span (C,n)) | (k + 1)),m,(Gauge (C,n))) meets C cell ((Gauge (C,n)),i2,(j2 -' 1)) meets C by A3, A12, A17, A30, A31, A35, A36, A37, A38, A59, A70, GOBRD13:40; then left_cell ((Span (C,n)),m,(Gauge (C,n))) meets C by A3, A15, A16, A17, A28, A31, A33, A37, A38, A41, A71, A72, GOBRD13:27; hence left_cell (((Span (C,n)) | (k + 1)),m,(Gauge (C,n))) meets C by A3, A15, A16, A13, A33, GOBRD13:31; ::_thesis: verum end; end; end; hence ( right_cell (((Span (C,n)) | (k + 1)),m,(Gauge (C,n))) misses C & left_cell (((Span (C,n)) | (k + 1)),m,(Gauge (C,n))) meets C ) ; ::_thesis: verum end; supposeA74: front_right_cell ((Span (C,n)),((len ((Span (C,n)) | k)) -' 1),(Gauge (C,n))) meets C ; ::_thesis: ( right_cell (((Span (C,n)) | (k + 1)),m,(Gauge (C,n))) misses C & left_cell (((Span (C,n)) | (k + 1)),m,(Gauge (C,n))) meets C ) then A75: Span (C,n) turns_right (len ((Span (C,n)) | k)) -' 1, Gauge (C,n) by A2, A15, A17, A30, A32, JORDAN13:def_1; now__::_thesis:_(_right_cell_(((Span_(C,n))_|_(k_+_1)),m,(Gauge_(C,n)))_misses_C_&_left_cell_(((Span_(C,n))_|_(k_+_1)),m,(Gauge_(C,n)))_meets_C_) percases ( ( i1 = i2 & j1 + 1 = j2 & [(i2 + 1),j2] in Indices (Gauge (C,n)) & (Span (C,n)) /. (((len ((Span (C,n)) | k)) -' 1) + 2) = (Gauge (C,n)) * ((i2 + 1),j2) ) or ( i1 + 1 = i2 & j1 = j2 & [i2,(j2 -' 1)] in Indices (Gauge (C,n)) & (Span (C,n)) /. (((len ((Span (C,n)) | k)) -' 1) + 2) = (Gauge (C,n)) * (i2,(j2 -' 1)) ) or ( i1 = i2 + 1 & j1 = j2 & [i2,(j2 + 1)] in Indices (Gauge (C,n)) & (Span (C,n)) /. (((len ((Span (C,n)) | k)) -' 1) + 2) = (Gauge (C,n)) * (i2,(j2 + 1)) ) or ( i1 = i2 & j1 = j2 + 1 & [(i2 -' 1),j2] in Indices (Gauge (C,n)) & (Span (C,n)) /. (((len ((Span (C,n)) | k)) -' 1) + 2) = (Gauge (C,n)) * ((i2 -' 1),j2) ) ) by A31, A35, A36, A37, A38, A75, GOBRD13:def_6; supposethat A76: ( i1 = i2 & j1 + 1 = j2 ) and A77: [(i2 + 1),j2] in Indices (Gauge (C,n)) and A78: (Span (C,n)) /. (((len ((Span (C,n)) | k)) -' 1) + 2) = (Gauge (C,n)) * ((i2 + 1),j2) ; ::_thesis: ( right_cell (((Span (C,n)) | (k + 1)),m,(Gauge (C,n))) misses C & left_cell (((Span (C,n)) | (k + 1)),m,(Gauge (C,n))) meets C ) A79: (j1 + 1) -' 1 = j1 by NAT_D:34; cell ((Gauge (C,n)),i1,j1) misses C by A3, A30, A31, A29, A35, A36, A37, A38, A42, A76, GOBRD13:22; then right_cell ((Span (C,n)),m,(Gauge (C,n))) misses C by A3, A15, A16, A17, A28, A31, A33, A37, A38, A76, A77, A78, A79, GOBRD13:24; hence right_cell (((Span (C,n)) | (k + 1)),m,(Gauge (C,n))) misses C by A3, A15, A16, A13, A33, GOBRD13:31; ::_thesis: left_cell (((Span (C,n)) | (k + 1)),m,(Gauge (C,n))) meets C cell ((Gauge (C,n)),i2,j2) meets C by A3, A12, A17, A30, A31, A35, A36, A37, A38, A74, A76, GOBRD13:35; then left_cell ((Span (C,n)),m,(Gauge (C,n))) meets C by A3, A15, A16, A17, A28, A31, A33, A37, A38, A77, A78, GOBRD13:23; hence left_cell (((Span (C,n)) | (k + 1)),m,(Gauge (C,n))) meets C by A3, A15, A16, A13, A33, GOBRD13:31; ::_thesis: verum end; supposethat A80: ( i1 + 1 = i2 & j1 = j2 ) and A81: [i2,(j2 -' 1)] in Indices (Gauge (C,n)) and A82: (Span (C,n)) /. (((len ((Span (C,n)) | k)) -' 1) + 2) = (Gauge (C,n)) * (i2,(j2 -' 1)) ; ::_thesis: ( right_cell (((Span (C,n)) | (k + 1)),m,(Gauge (C,n))) misses C & left_cell (((Span (C,n)) | (k + 1)),m,(Gauge (C,n))) meets C ) A83: (i1 + 1) -' 1 = i1 by NAT_D:34; cell ((Gauge (C,n)),i1,(j1 -' 1)) misses C by A3, A30, A31, A29, A35, A36, A37, A38, A42, A80, GOBRD13:24; then right_cell ((Span (C,n)),m,(Gauge (C,n))) misses C by A3, A15, A16, A17, A28, A31, A33, A37, A38, A41, A80, A81, A82, A83, GOBRD13:28; hence right_cell (((Span (C,n)) | (k + 1)),m,(Gauge (C,n))) misses C by A3, A15, A16, A13, A33, GOBRD13:31; ::_thesis: left_cell (((Span (C,n)) | (k + 1)),m,(Gauge (C,n))) meets C cell ((Gauge (C,n)),i2,(j2 -' 1)) meets C by A3, A12, A17, A30, A31, A35, A36, A37, A38, A74, A80, GOBRD13:37; then left_cell ((Span (C,n)),m,(Gauge (C,n))) meets C by A3, A15, A16, A17, A28, A31, A33, A37, A38, A41, A81, A82, GOBRD13:27; hence left_cell (((Span (C,n)) | (k + 1)),m,(Gauge (C,n))) meets C by A3, A15, A16, A13, A33, GOBRD13:31; ::_thesis: verum end; supposethat A84: ( i1 = i2 + 1 & j1 = j2 ) and A85: [i2,(j2 + 1)] in Indices (Gauge (C,n)) and A86: (Span (C,n)) /. (((len ((Span (C,n)) | k)) -' 1) + 2) = (Gauge (C,n)) * (i2,(j2 + 1)) ; ::_thesis: ( right_cell (((Span (C,n)) | (k + 1)),m,(Gauge (C,n))) misses C & left_cell (((Span (C,n)) | (k + 1)),m,(Gauge (C,n))) meets C ) cell ((Gauge (C,n)),i2,j2) misses C by A3, A30, A31, A29, A35, A36, A37, A38, A42, A84, GOBRD13:26; then right_cell ((Span (C,n)),m,(Gauge (C,n))) misses C by A3, A15, A16, A17, A28, A31, A33, A37, A38, A85, A86, GOBRD13:22; hence right_cell (((Span (C,n)) | (k + 1)),m,(Gauge (C,n))) misses C by A3, A15, A16, A13, A33, GOBRD13:31; ::_thesis: left_cell (((Span (C,n)) | (k + 1)),m,(Gauge (C,n))) meets C cell ((Gauge (C,n)),(i2 -' 1),j2) meets C by A3, A12, A17, A30, A31, A35, A36, A37, A38, A74, A84, GOBRD13:39; then left_cell ((Span (C,n)),m,(Gauge (C,n))) meets C by A3, A15, A16, A17, A28, A31, A33, A37, A38, A85, A86, GOBRD13:21; hence left_cell (((Span (C,n)) | (k + 1)),m,(Gauge (C,n))) meets C by A3, A15, A16, A13, A33, GOBRD13:31; ::_thesis: verum end; supposethat A87: ( i1 = i2 & j1 = j2 + 1 ) and A88: [(i2 -' 1),j2] in Indices (Gauge (C,n)) and A89: (Span (C,n)) /. (((len ((Span (C,n)) | k)) -' 1) + 2) = (Gauge (C,n)) * ((i2 -' 1),j2) ; ::_thesis: ( right_cell (((Span (C,n)) | (k + 1)),m,(Gauge (C,n))) misses C & left_cell (((Span (C,n)) | (k + 1)),m,(Gauge (C,n))) meets C ) cell ((Gauge (C,n)),(i2 -' 1),j2) misses C by A3, A30, A31, A29, A35, A36, A37, A38, A42, A87, GOBRD13:28; then right_cell ((Span (C,n)),m,(Gauge (C,n))) misses C by A3, A15, A16, A17, A28, A31, A33, A37, A38, A39, A88, A89, GOBRD13:26; hence right_cell (((Span (C,n)) | (k + 1)),m,(Gauge (C,n))) misses C by A3, A15, A16, A13, A33, GOBRD13:31; ::_thesis: left_cell (((Span (C,n)) | (k + 1)),m,(Gauge (C,n))) meets C cell ((Gauge (C,n)),(i2 -' 1),(j2 -' 1)) meets C by A3, A12, A17, A30, A31, A35, A36, A37, A38, A74, A87, GOBRD13:41; then left_cell ((Span (C,n)),m,(Gauge (C,n))) meets C by A3, A15, A16, A17, A28, A31, A33, A37, A38, A39, A88, A89, GOBRD13:25; hence left_cell (((Span (C,n)) | (k + 1)),m,(Gauge (C,n))) meets C by A3, A15, A16, A13, A33, GOBRD13:31; ::_thesis: verum end; end; end; hence ( right_cell (((Span (C,n)) | (k + 1)),m,(Gauge (C,n))) misses C & left_cell (((Span (C,n)) | (k + 1)),m,(Gauge (C,n))) meets C ) ; ::_thesis: verum end; end; end; hence ( right_cell (((Span (C,n)) | (k + 1)),m,(Gauge (C,n))) misses C & left_cell (((Span (C,n)) | (k + 1)),m,(Gauge (C,n))) meets C ) ; ::_thesis: verum end; suppose m + 1 <> len ((Span (C,n)) | (k + 1)) ; ::_thesis: ( right_cell (((Span (C,n)) | (k + 1)),m,(Gauge (C,n))) misses C & left_cell (((Span (C,n)) | (k + 1)),m,(Gauge (C,n))) meets C ) then m + 1 < len ((Span (C,n)) | (k + 1)) by A14, XXREAL_0:1; then A90: m + 1 <= len ((Span (C,n)) | k) by A16, A17, NAT_1:13; then consider i1, j1, i2, j2 being Element of NAT such that A91: [i1,j1] in Indices (Gauge (C,n)) and A92: ((Span (C,n)) | k) /. m = (Gauge (C,n)) * (i1,j1) and A93: [i2,j2] in Indices (Gauge (C,n)) and A94: ((Span (C,n)) | k) /. (m + 1) = (Gauge (C,n)) * (i2,j2) and A95: ( ( i1 = i2 & j1 + 1 = j2 ) or ( i1 + 1 = i2 & j1 = j2 ) or ( i1 = i2 + 1 & j1 = j2 ) or ( i1 = i2 & j1 = j2 + 1 ) ) by A9, A13, JORDAN8:3; A96: right_cell (((Span (C,n)) | k),m,(Gauge (C,n))) misses C by A7, A13, A90; A97: (Span (C,n)) | (k + 1) = ((Span (C,n)) | k) ^ <*((Span (C,n)) /. (k + 1))*> by A15, FINSEQ_5:82; 1 <= m + 1 by NAT_1:12; then m + 1 in dom ((Span (C,n)) | k) by A90, FINSEQ_3:25; then A98: ((Span (C,n)) | (k + 1)) /. (m + 1) = (Gauge (C,n)) * (i2,j2) by A94, A97, FINSEQ_4:68; A99: left_cell (((Span (C,n)) | k),m,(Gauge (C,n))) meets C by A7, A13, A90; m <= len ((Span (C,n)) | k) by A90, NAT_1:13; then m in dom ((Span (C,n)) | k) by A13, FINSEQ_3:25; then A100: ((Span (C,n)) | (k + 1)) /. m = (Gauge (C,n)) * (i1,j1) by A92, A97, FINSEQ_4:68; now__::_thesis:_(_right_cell_(((Span_(C,n))_|_(k_+_1)),m,(Gauge_(C,n)))_misses_C_&_left_cell_(((Span_(C,n))_|_(k_+_1)),m,(Gauge_(C,n)))_meets_C_) percases ( ( i1 = i2 & j1 + 1 = j2 ) or ( i1 + 1 = i2 & j1 = j2 ) or ( i1 = i2 + 1 & j1 = j2 ) or ( i1 = i2 & j1 = j2 + 1 ) ) by A95; supposeA101: ( i1 = i2 & j1 + 1 = j2 ) ; ::_thesis: ( right_cell (((Span (C,n)) | (k + 1)),m,(Gauge (C,n))) misses C & left_cell (((Span (C,n)) | (k + 1)),m,(Gauge (C,n))) meets C ) then A102: left_cell (((Span (C,n)) | k),m,(Gauge (C,n))) = cell ((Gauge (C,n)),(i1 -' 1),j1) by A9, A13, A90, A91, A92, A93, A94, GOBRD13:21; right_cell (((Span (C,n)) | k),m,(Gauge (C,n))) = cell ((Gauge (C,n)),i1,j1) by A9, A13, A90, A91, A92, A93, A94, A101, GOBRD13:22; hence ( right_cell (((Span (C,n)) | (k + 1)),m,(Gauge (C,n))) misses C & left_cell (((Span (C,n)) | (k + 1)),m,(Gauge (C,n))) meets C ) by A8, A13, A14, A91, A93, A96, A99, A100, A98, A101, A102, GOBRD13:21, GOBRD13:22; ::_thesis: verum end; supposeA103: ( i1 + 1 = i2 & j1 = j2 ) ; ::_thesis: ( right_cell (((Span (C,n)) | (k + 1)),m,(Gauge (C,n))) misses C & left_cell (((Span (C,n)) | (k + 1)),m,(Gauge (C,n))) meets C ) then A104: left_cell (((Span (C,n)) | k),m,(Gauge (C,n))) = cell ((Gauge (C,n)),i1,j1) by A9, A13, A90, A91, A92, A93, A94, GOBRD13:23; right_cell (((Span (C,n)) | k),m,(Gauge (C,n))) = cell ((Gauge (C,n)),i1,(j1 -' 1)) by A9, A13, A90, A91, A92, A93, A94, A103, GOBRD13:24; hence ( right_cell (((Span (C,n)) | (k + 1)),m,(Gauge (C,n))) misses C & left_cell (((Span (C,n)) | (k + 1)),m,(Gauge (C,n))) meets C ) by A8, A13, A14, A91, A93, A96, A99, A100, A98, A103, A104, GOBRD13:23, GOBRD13:24; ::_thesis: verum end; supposeA105: ( i1 = i2 + 1 & j1 = j2 ) ; ::_thesis: ( right_cell (((Span (C,n)) | (k + 1)),m,(Gauge (C,n))) misses C & left_cell (((Span (C,n)) | (k + 1)),m,(Gauge (C,n))) meets C ) then A106: left_cell (((Span (C,n)) | k),m,(Gauge (C,n))) = cell ((Gauge (C,n)),i2,(j2 -' 1)) by A9, A13, A90, A91, A92, A93, A94, GOBRD13:25; right_cell (((Span (C,n)) | k),m,(Gauge (C,n))) = cell ((Gauge (C,n)),i2,j2) by A9, A13, A90, A91, A92, A93, A94, A105, GOBRD13:26; hence ( right_cell (((Span (C,n)) | (k + 1)),m,(Gauge (C,n))) misses C & left_cell (((Span (C,n)) | (k + 1)),m,(Gauge (C,n))) meets C ) by A8, A13, A14, A91, A93, A96, A99, A100, A98, A105, A106, GOBRD13:25, GOBRD13:26; ::_thesis: verum end; supposeA107: ( i1 = i2 & j1 = j2 + 1 ) ; ::_thesis: ( right_cell (((Span (C,n)) | (k + 1)),m,(Gauge (C,n))) misses C & left_cell (((Span (C,n)) | (k + 1)),m,(Gauge (C,n))) meets C ) then A108: left_cell (((Span (C,n)) | k),m,(Gauge (C,n))) = cell ((Gauge (C,n)),i1,j2) by A9, A13, A90, A91, A92, A93, A94, GOBRD13:27; right_cell (((Span (C,n)) | k),m,(Gauge (C,n))) = cell ((Gauge (C,n)),(i2 -' 1),j2) by A9, A13, A90, A91, A92, A93, A94, A107, GOBRD13:28; hence ( right_cell (((Span (C,n)) | (k + 1)),m,(Gauge (C,n))) misses C & left_cell (((Span (C,n)) | (k + 1)),m,(Gauge (C,n))) meets C ) by A8, A13, A14, A91, A93, A96, A99, A100, A98, A107, A108, GOBRD13:27, GOBRD13:28; ::_thesis: verum end; end; end; hence ( right_cell (((Span (C,n)) | (k + 1)),m,(Gauge (C,n))) misses C & left_cell (((Span (C,n)) | (k + 1)),m,(Gauge (C,n))) meets C ) ; ::_thesis: verum end; end; end; hence ( right_cell (((Span (C,n)) | (k + 1)),m,(Gauge (C,n))) misses C & left_cell (((Span (C,n)) | (k + 1)),m,(Gauge (C,n))) meets C ) ; ::_thesis: verum end; end; end; hence ( right_cell (((Span (C,n)) | (k + 1)),m,(Gauge (C,n))) misses C & left_cell (((Span (C,n)) | (k + 1)),m,(Gauge (C,n))) meets C ) ; ::_thesis: verum end; end; end; A109: S1[ 0 ] proof let m be Element of NAT ; ::_thesis: ( 1 <= m & m + 1 <= len ((Span (C,n)) | 0) implies ( right_cell (((Span (C,n)) | 0),m,(Gauge (C,n))) misses C & left_cell (((Span (C,n)) | 0),m,(Gauge (C,n))) meets C ) ) assume that 1 <= m and A110: m + 1 <= len ((Span (C,n)) | 0) ; ::_thesis: ( right_cell (((Span (C,n)) | 0),m,(Gauge (C,n))) misses C & left_cell (((Span (C,n)) | 0),m,(Gauge (C,n))) meets C ) 1 <= m + 1 by NAT_1:12; hence ( right_cell (((Span (C,n)) | 0),m,(Gauge (C,n))) misses C & left_cell (((Span (C,n)) | 0),m,(Gauge (C,n))) meets C ) by A110, CARD_1:27, XXREAL_0:2; ::_thesis: verum end; for k being Element of NAT holds S1[k] from NAT_1:sch_1(A109, A6); hence ( not 1 <= k or not k + 1 <= len (Span (C,n)) or ( right_cell ((Span (C,n)),k,(Gauge (C,n))) misses C & left_cell ((Span (C,n)),k,(Gauge (C,n))) meets C ) ) by A1; ::_thesis: verum end; theorem Th8: :: JORDAN14:8 for C being Simple_closed_curve for n being Element of NAT st n is_sufficiently_large_for C holds C misses L~ (Span (C,n)) proof let C be Simple_closed_curve; ::_thesis: for n being Element of NAT st n is_sufficiently_large_for C holds C misses L~ (Span (C,n)) let n be Element of NAT ; ::_thesis: ( n is_sufficiently_large_for C implies C misses L~ (Span (C,n)) ) assume A1: n is_sufficiently_large_for C ; ::_thesis: C misses L~ (Span (C,n)) set G = Gauge (C,n); set f = Span (C,n); assume not C misses L~ (Span (C,n)) ; ::_thesis: contradiction then consider c being set such that A2: c in C and A3: c in L~ (Span (C,n)) by XBOOLE_0:3; L~ (Span (C,n)) = union { (LSeg ((Span (C,n)),i)) where i is Element of NAT : ( 1 <= i & i + 1 <= len (Span (C,n)) ) } by TOPREAL1:def_4; then consider Z being set such that A4: c in Z and A5: Z in { (LSeg ((Span (C,n)),i)) where i is Element of NAT : ( 1 <= i & i + 1 <= len (Span (C,n)) ) } by A3, TARSKI:def_4; consider i being Element of NAT such that A6: Z = LSeg ((Span (C,n)),i) and A7: 1 <= i and A8: i + 1 <= len (Span (C,n)) by A5; Span (C,n) is_sequence_on Gauge (C,n) by A1, JORDAN13:def_1; then LSeg ((Span (C,n)),i) = (left_cell ((Span (C,n)),i,(Gauge (C,n)))) /\ (right_cell ((Span (C,n)),i,(Gauge (C,n)))) by A7, A8, GOBRD13:29; then A9: c in right_cell ((Span (C,n)),i,(Gauge (C,n))) by A4, A6, XBOOLE_0:def_4; right_cell ((Span (C,n)),i,(Gauge (C,n))) misses C by A1, A7, A8, Th7; hence contradiction by A2, A9, XBOOLE_0:3; ::_thesis: verum end; registration let C be Simple_closed_curve; let n be Element of NAT ; cluster Cl (RightComp (Span (C,n))) -> compact ; coherence Cl (RightComp (Span (C,n))) is compact by GOBRD14:32; end; theorem Th9: :: JORDAN14:9 for C being Simple_closed_curve for n being Element of NAT st n is_sufficiently_large_for C holds C meets LeftComp (Span (C,n)) proof let C be Simple_closed_curve; ::_thesis: for n being Element of NAT st n is_sufficiently_large_for C holds C meets LeftComp (Span (C,n)) let n be Element of NAT ; ::_thesis: ( n is_sufficiently_large_for C implies C meets LeftComp (Span (C,n)) ) assume A1: n is_sufficiently_large_for C ; ::_thesis: C meets LeftComp (Span (C,n)) then A2: Span (C,n) is_sequence_on Gauge (C,n) by JORDAN13:def_1; A3: 1 + 1 <= len (Span (C,n)) by GOBOARD7:34, XXREAL_0:2; then left_cell ((Span (C,n)),1,(Gauge (C,n))) meets C by A1, Th7; then (left_cell ((Span (C,n)),1,(Gauge (C,n)))) \ (L~ (Span (C,n))) meets C by A1, Th8, XBOOLE_1:84; hence C meets LeftComp (Span (C,n)) by A3, A2, JORDAN9:27, XBOOLE_1:63; ::_thesis: verum end; theorem Th10: :: JORDAN14:10 for C being Simple_closed_curve for n being Element of NAT st n is_sufficiently_large_for C holds C misses RightComp (Span (C,n)) proof let C be Simple_closed_curve; ::_thesis: for n being Element of NAT st n is_sufficiently_large_for C holds C misses RightComp (Span (C,n)) let n be Element of NAT ; ::_thesis: ( n is_sufficiently_large_for C implies C misses RightComp (Span (C,n)) ) set f = Span (C,n); RightComp (Span (C,n)) is_a_component_of (L~ (Span (C,n))) ` by GOBOARD9:def_2; then A1: ex L being Subset of ((TOP-REAL 2) | ((L~ (Span (C,n))) `)) st ( L = RightComp (Span (C,n)) & L is a_component ) by CONNSP_1:def_6; LeftComp (Span (C,n)) is_a_component_of (L~ (Span (C,n))) ` by GOBOARD9:def_1; then A2: ex R being Subset of ((TOP-REAL 2) | ((L~ (Span (C,n))) `)) st ( R = LeftComp (Span (C,n)) & R is a_component ) by CONNSP_1:def_6; assume A3: n is_sufficiently_large_for C ; ::_thesis: C misses RightComp (Span (C,n)) then A4: C misses L~ (Span (C,n)) by Th8; C c= the carrier of ((TOP-REAL 2) | ((L~ (Span (C,n))) `)) proof let c be set ; :: according to TARSKI:def_3 ::_thesis: ( not c in C or c in the carrier of ((TOP-REAL 2) | ((L~ (Span (C,n))) `)) ) assume A5: c in C ; ::_thesis: c in the carrier of ((TOP-REAL 2) | ((L~ (Span (C,n))) `)) then not c in L~ (Span (C,n)) by A4, XBOOLE_0:3; then c in (L~ (Span (C,n))) ` by A5, SUBSET_1:29; hence c in the carrier of ((TOP-REAL 2) | ((L~ (Span (C,n))) `)) by PRE_TOPC:8; ::_thesis: verum end; then reconsider C1 = C as Subset of ((TOP-REAL 2) | ((L~ (Span (C,n))) `)) ; assume A6: C meets RightComp (Span (C,n)) ; ::_thesis: contradiction A7: C1 is connected by CONNSP_1:23; C meets LeftComp (Span (C,n)) by A3, Th9; hence contradiction by A6, A1, A2, A7, JORDAN2C:92, SPRECT_4:6; ::_thesis: verum end; theorem Th11: :: JORDAN14:11 for C being Simple_closed_curve for n being Element of NAT st n is_sufficiently_large_for C holds C c= LeftComp (Span (C,n)) proof let C be Simple_closed_curve; ::_thesis: for n being Element of NAT st n is_sufficiently_large_for C holds C c= LeftComp (Span (C,n)) let n be Element of NAT ; ::_thesis: ( n is_sufficiently_large_for C implies C c= LeftComp (Span (C,n)) ) assume A1: n is_sufficiently_large_for C ; ::_thesis: C c= LeftComp (Span (C,n)) let c be set ; :: according to TARSKI:def_3 ::_thesis: ( not c in C or c in LeftComp (Span (C,n)) ) set f = Span (C,n); assume A2: c in C ; ::_thesis: c in LeftComp (Span (C,n)) C misses L~ (Span (C,n)) by A1, Th8; then A3: not c in L~ (Span (C,n)) by A2, XBOOLE_0:3; C misses RightComp (Span (C,n)) by A1, Th10; then not c in RightComp (Span (C,n)) by A2, XBOOLE_0:3; hence c in LeftComp (Span (C,n)) by A2, A3, GOBRD14:18; ::_thesis: verum end; theorem Th12: :: JORDAN14:12 for C being Simple_closed_curve for n being Element of NAT st n is_sufficiently_large_for C holds C c= UBD (L~ (Span (C,n))) proof let C be Simple_closed_curve; ::_thesis: for n being Element of NAT st n is_sufficiently_large_for C holds C c= UBD (L~ (Span (C,n))) let n be Element of NAT ; ::_thesis: ( n is_sufficiently_large_for C implies C c= UBD (L~ (Span (C,n))) ) assume n is_sufficiently_large_for C ; ::_thesis: C c= UBD (L~ (Span (C,n))) then A1: C c= LeftComp (Span (C,n)) by Th11; LeftComp (Span (C,n)) c= UBD (L~ (Span (C,n))) by GOBRD14:34, JORDAN2C:23; hence C c= UBD (L~ (Span (C,n))) by A1, XBOOLE_1:1; ::_thesis: verum end; theorem Th13: :: JORDAN14:13 for C being Simple_closed_curve for n being Element of NAT st n is_sufficiently_large_for C holds BDD (L~ (Span (C,n))) c= BDD C proof let C be Simple_closed_curve; ::_thesis: for n being Element of NAT st n is_sufficiently_large_for C holds BDD (L~ (Span (C,n))) c= BDD C let n be Element of NAT ; ::_thesis: ( n is_sufficiently_large_for C implies BDD (L~ (Span (C,n))) c= BDD C ) assume that A1: n is_sufficiently_large_for C and A2: not BDD (L~ (Span (C,n))) c= BDD C ; ::_thesis: contradiction set f = Span (C,n); A3: Cl (BDD (L~ (Span (C,n)))) = Cl (RightComp (Span (C,n))) by GOBRD14:37 .= (RightComp (Span (C,n))) \/ (L~ (Span (C,n))) by GOBRD14:21 ; len (Span (C,n)) >= 1 by GOBOARD7:34, XXREAL_0:2; then A4: 1 in dom (Span (C,n)) by FINSEQ_3:25; len (Span (C,n)) > 4 by GOBOARD7:34; then (Span (C,n)) /. 1 in L~ (Span (C,n)) by A4, GOBOARD1:1, XXREAL_0:2; then SpanStart (C,n) in L~ (Span (C,n)) by A1, JORDAN13:def_1; then A5: SpanStart (C,n) in Cl (BDD (L~ (Span (C,n)))) by A3, XBOOLE_0:def_3; SpanStart (C,n) in BDD C by A1, Th6; then A6: BDD (L~ (Span (C,n))) meets BDD C by A5, PRE_TOPC:def_7; BDD C misses UBD C by JORDAN2C:24; then A7: BDD C, UBD C are_separated by TSEP_1:37; BDD (L~ (Span (C,n))) misses UBD (L~ (Span (C,n))) by JORDAN2C:24; then C misses BDD (L~ (Span (C,n))) by A1, Th12, XBOOLE_1:63; then A8: BDD (L~ (Span (C,n))) c= C ` by SUBSET_1:23; (BDD C) \/ (UBD C) = C ` by JORDAN2C:27; then BDD (L~ (Span (C,n))) c= UBD C by A2, A8, A7, CONNSP_1:16; then BDD C meets UBD C by A6, XBOOLE_1:63; hence contradiction by JORDAN2C:24; ::_thesis: verum end; theorem Th14: :: JORDAN14:14 for C being Simple_closed_curve for n being Element of NAT st n is_sufficiently_large_for C holds UBD C c= UBD (L~ (Span (C,n))) proof let C be Simple_closed_curve; ::_thesis: for n being Element of NAT st n is_sufficiently_large_for C holds UBD C c= UBD (L~ (Span (C,n))) let n be Element of NAT ; ::_thesis: ( n is_sufficiently_large_for C implies UBD C c= UBD (L~ (Span (C,n))) ) assume A1: n is_sufficiently_large_for C ; ::_thesis: UBD C c= UBD (L~ (Span (C,n))) let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in UBD C or x in UBD (L~ (Span (C,n))) ) A2: BDD C misses UBD C by JORDAN2C:24; assume A3: x in UBD C ; ::_thesis: x in UBD (L~ (Span (C,n))) then reconsider p = x as Point of (TOP-REAL 2) ; A4: Cl (BDD (L~ (Span (C,n)))) c= Cl (BDD C) by A1, Th13, PRE_TOPC:19; A5: now__::_thesis:_not_x_in_L~_(Span_(C,n)) assume x in L~ (Span (C,n)) ; ::_thesis: contradiction then p in (RightComp (Span (C,n))) \/ (L~ (Span (C,n))) by XBOOLE_0:def_3; then p in Cl (RightComp (Span (C,n))) by GOBRD14:21; then p in Cl (BDD (L~ (Span (C,n)))) by GOBRD14:37; hence contradiction by A4, A2, A3, PRE_TOPC:def_7; ::_thesis: verum end; BDD (L~ (Span (C,n))) c= BDD C by A1, Th13; then not x in BDD (L~ (Span (C,n))) by A2, A3, XBOOLE_0:3; then not x in RightComp (Span (C,n)) by GOBRD14:37; then p in LeftComp (Span (C,n)) by A5, GOBRD14:17; hence x in UBD (L~ (Span (C,n))) by GOBRD14:36; ::_thesis: verum end; theorem :: JORDAN14:15 for C being Simple_closed_curve for n being Element of NAT st n is_sufficiently_large_for C holds RightComp (Span (C,n)) c= BDD C proof let C be Simple_closed_curve; ::_thesis: for n being Element of NAT st n is_sufficiently_large_for C holds RightComp (Span (C,n)) c= BDD C let n be Element of NAT ; ::_thesis: ( n is_sufficiently_large_for C implies RightComp (Span (C,n)) c= BDD C ) assume n is_sufficiently_large_for C ; ::_thesis: RightComp (Span (C,n)) c= BDD C then BDD (L~ (Span (C,n))) c= BDD C by Th13; hence RightComp (Span (C,n)) c= BDD C by GOBRD14:37; ::_thesis: verum end; theorem Th16: :: JORDAN14:16 for C being Simple_closed_curve for n being Element of NAT st n is_sufficiently_large_for C holds UBD C c= LeftComp (Span (C,n)) proof let C be Simple_closed_curve; ::_thesis: for n being Element of NAT st n is_sufficiently_large_for C holds UBD C c= LeftComp (Span (C,n)) let n be Element of NAT ; ::_thesis: ( n is_sufficiently_large_for C implies UBD C c= LeftComp (Span (C,n)) ) assume n is_sufficiently_large_for C ; ::_thesis: UBD C c= LeftComp (Span (C,n)) then UBD C c= UBD (L~ (Span (C,n))) by Th14; hence UBD C c= LeftComp (Span (C,n)) by GOBRD14:36; ::_thesis: verum end; theorem Th17: :: JORDAN14:17 for C being Simple_closed_curve for n being Element of NAT st n is_sufficiently_large_for C holds UBD C misses BDD (L~ (Span (C,n))) proof let C be Simple_closed_curve; ::_thesis: for n being Element of NAT st n is_sufficiently_large_for C holds UBD C misses BDD (L~ (Span (C,n))) let n be Element of NAT ; ::_thesis: ( n is_sufficiently_large_for C implies UBD C misses BDD (L~ (Span (C,n))) ) assume that A1: n is_sufficiently_large_for C and A2: UBD C meets BDD (L~ (Span (C,n))) ; ::_thesis: contradiction UBD (L~ (Span (C,n))) meets BDD (L~ (Span (C,n))) by A1, A2, Th14, XBOOLE_1:63; hence contradiction by JORDAN2C:24; ::_thesis: verum end; theorem :: JORDAN14:18 for C being Simple_closed_curve for n being Element of NAT st n is_sufficiently_large_for C holds UBD C misses RightComp (Span (C,n)) proof let C be Simple_closed_curve; ::_thesis: for n being Element of NAT st n is_sufficiently_large_for C holds UBD C misses RightComp (Span (C,n)) let n be Element of NAT ; ::_thesis: ( n is_sufficiently_large_for C implies UBD C misses RightComp (Span (C,n)) ) assume n is_sufficiently_large_for C ; ::_thesis: UBD C misses RightComp (Span (C,n)) then UBD C misses BDD (L~ (Span (C,n))) by Th17; hence UBD C misses RightComp (Span (C,n)) by GOBRD14:37; ::_thesis: verum end; theorem Th19: :: JORDAN14:19 for C being Simple_closed_curve for P being Subset of (TOP-REAL 2) for n being Element of NAT st n is_sufficiently_large_for C & P is_outside_component_of C holds P misses L~ (Span (C,n)) proof let C be Simple_closed_curve; ::_thesis: for P being Subset of (TOP-REAL 2) for n being Element of NAT st n is_sufficiently_large_for C & P is_outside_component_of C holds P misses L~ (Span (C,n)) let P be Subset of (TOP-REAL 2); ::_thesis: for n being Element of NAT st n is_sufficiently_large_for C & P is_outside_component_of C holds P misses L~ (Span (C,n)) let n be Element of NAT ; ::_thesis: ( n is_sufficiently_large_for C & P is_outside_component_of C implies P misses L~ (Span (C,n)) ) assume that A1: n is_sufficiently_large_for C and A2: P is_outside_component_of C and A3: P meets L~ (Span (C,n)) ; ::_thesis: contradiction A4: UBD C c= LeftComp (Span (C,n)) by A1, Th16; consider x being set such that A5: x in P and A6: x in L~ (Span (C,n)) by A3, XBOOLE_0:3; P c= UBD C by A2, JORDAN2C:23; then x in UBD C by A5; hence contradiction by A6, A4, GOBRD14:17; ::_thesis: verum end; theorem Th20: :: JORDAN14:20 for C being Simple_closed_curve for n being Element of NAT st n is_sufficiently_large_for C holds UBD C misses L~ (Span (C,n)) proof let C be Simple_closed_curve; ::_thesis: for n being Element of NAT st n is_sufficiently_large_for C holds UBD C misses L~ (Span (C,n)) let n be Element of NAT ; ::_thesis: ( n is_sufficiently_large_for C implies UBD C misses L~ (Span (C,n)) ) assume A1: n is_sufficiently_large_for C ; ::_thesis: UBD C misses L~ (Span (C,n)) assume UBD C meets L~ (Span (C,n)) ; ::_thesis: contradiction then consider x being set such that A2: x in UBD C and A3: x in L~ (Span (C,n)) by XBOOLE_0:3; UBD C = union { B where B is Subset of (TOP-REAL 2) : B is_outside_component_of C } by JORDAN2C:def_5; then consider Z being set such that A4: x in Z and A5: Z in { B where B is Subset of (TOP-REAL 2) : B is_outside_component_of C } by A2, TARSKI:def_4; consider B being Subset of (TOP-REAL 2) such that A6: Z = B and A7: B is_outside_component_of C by A5; B misses L~ (Span (C,n)) by A1, A7, Th19; hence contradiction by A3, A4, A6, XBOOLE_0:3; ::_thesis: verum end; theorem Th21: :: JORDAN14:21 for C being Simple_closed_curve for n being Element of NAT st n is_sufficiently_large_for C holds L~ (Span (C,n)) c= BDD C proof let C be Simple_closed_curve; ::_thesis: for n being Element of NAT st n is_sufficiently_large_for C holds L~ (Span (C,n)) c= BDD C let n be Element of NAT ; ::_thesis: ( n is_sufficiently_large_for C implies L~ (Span (C,n)) c= BDD C ) assume A1: n is_sufficiently_large_for C ; ::_thesis: L~ (Span (C,n)) c= BDD C then C misses L~ (Span (C,n)) by Th8; then L~ (Span (C,n)) c= C ` by SUBSET_1:23; then A2: L~ (Span (C,n)) c= (BDD C) \/ (UBD C) by JORDAN2C:27; UBD C misses L~ (Span (C,n)) by A1, Th20; hence L~ (Span (C,n)) c= BDD C by A2, XBOOLE_1:73; ::_thesis: verum end; theorem Th22: :: JORDAN14:22 for C being Simple_closed_curve for i, j, k, n being Element of NAT st n is_sufficiently_large_for C & 1 <= k & k <= len (Span (C,n)) & [i,j] in Indices (Gauge (C,n)) & (Span (C,n)) /. k = (Gauge (C,n)) * (i,j) holds i > 1 proof let C be Simple_closed_curve; ::_thesis: for i, j, k, n being Element of NAT st n is_sufficiently_large_for C & 1 <= k & k <= len (Span (C,n)) & [i,j] in Indices (Gauge (C,n)) & (Span (C,n)) /. k = (Gauge (C,n)) * (i,j) holds i > 1 let i, j, k, n be Element of NAT ; ::_thesis: ( n is_sufficiently_large_for C & 1 <= k & k <= len (Span (C,n)) & [i,j] in Indices (Gauge (C,n)) & (Span (C,n)) /. k = (Gauge (C,n)) * (i,j) implies i > 1 ) assume that A1: n is_sufficiently_large_for C and A2: 1 <= k and A3: k <= len (Span (C,n)) and A4: [i,j] in Indices (Gauge (C,n)) and A5: (Span (C,n)) /. k = (Gauge (C,n)) * (i,j) ; ::_thesis: i > 1 A6: len (Span (C,n)) > 4 by GOBOARD7:34; SpanStart (C,n) in BDD C by A1, Th6; then A7: W-bound C <= W-bound (BDD C) by JORDAN1C:6; A8: j <= width (Gauge (C,n)) by A4, MATRIX_1:38; k in dom (Span (C,n)) by A2, A3, FINSEQ_3:25; then (Span (C,n)) /. k in L~ (Span (C,n)) by A6, GOBOARD1:1, XXREAL_0:2; then A9: W-bound (L~ (Span (C,n))) <= ((Gauge (C,n)) * (i,j)) `1 by A5, PSCOMP_1:24; A10: BDD C c= Cl (BDD C) by PRE_TOPC:18; A11: BDD C is bounded by JORDAN2C:106; then A12: Cl (BDD C) is compact by TOPREAL6:79; SpanStart (C,n) in BDD C by A1, Th6; then A13: W-bound (BDD C) = W-bound (Cl (BDD C)) by A11, TOPREAL6:85; L~ (Span (C,n)) c= BDD C by A1, Th21; then W-bound (L~ (Span (C,n))) >= W-bound (Cl (BDD C)) by A12, A10, PSCOMP_1:69, XBOOLE_1:1; then A14: W-bound (BDD C) <= ((Gauge (C,n)) * (i,j)) `1 by A13, A9, XXREAL_0:2; len (Gauge (C,n)) >= 4 by JORDAN8:10; then A15: len (Gauge (C,n)) >= 2 by XXREAL_0:2; A16: 1 <= i by A4, MATRIX_1:38; A17: 1 <= j by A4, MATRIX_1:38; len (Gauge (C,n)) = width (Gauge (C,n)) by JORDAN8:def_1; then ((Gauge (C,n)) * (2,j)) `1 = W-bound C by A17, A8, JORDAN8:11; then ((Gauge (C,n)) * (2,j)) `1 <= ((Gauge (C,n)) * (i,j)) `1 by A7, A14, XXREAL_0:2; then i >= 1 + 1 by A16, A17, A8, A15, GOBOARD5:3; hence i > 1 by NAT_1:13; ::_thesis: verum end; theorem Th23: :: JORDAN14:23 for C being Simple_closed_curve for i, j, k, n being Element of NAT st n is_sufficiently_large_for C & 1 <= k & k <= len (Span (C,n)) & [i,j] in Indices (Gauge (C,n)) & (Span (C,n)) /. k = (Gauge (C,n)) * (i,j) holds i < len (Gauge (C,n)) proof let C be Simple_closed_curve; ::_thesis: for i, j, k, n being Element of NAT st n is_sufficiently_large_for C & 1 <= k & k <= len (Span (C,n)) & [i,j] in Indices (Gauge (C,n)) & (Span (C,n)) /. k = (Gauge (C,n)) * (i,j) holds i < len (Gauge (C,n)) let i, j, k, n be Element of NAT ; ::_thesis: ( n is_sufficiently_large_for C & 1 <= k & k <= len (Span (C,n)) & [i,j] in Indices (Gauge (C,n)) & (Span (C,n)) /. k = (Gauge (C,n)) * (i,j) implies i < len (Gauge (C,n)) ) assume that A1: n is_sufficiently_large_for C and A2: 1 <= k and A3: k <= len (Span (C,n)) and A4: [i,j] in Indices (Gauge (C,n)) and A5: (Span (C,n)) /. k = (Gauge (C,n)) * (i,j) ; ::_thesis: i < len (Gauge (C,n)) A6: len (Span (C,n)) > 4 by GOBOARD7:34; SpanStart (C,n) in BDD C by A1, Th6; then A7: E-bound C >= E-bound (BDD C) by JORDAN1C:7; A8: 1 <= j by A4, MATRIX_1:38; k in dom (Span (C,n)) by A2, A3, FINSEQ_3:25; then (Span (C,n)) /. k in L~ (Span (C,n)) by A6, GOBOARD1:1, XXREAL_0:2; then A9: E-bound (L~ (Span (C,n))) >= ((Gauge (C,n)) * (i,j)) `1 by A5, PSCOMP_1:24; A10: BDD C c= Cl (BDD C) by PRE_TOPC:18; A11: BDD C is bounded by JORDAN2C:106; then A12: Cl (BDD C) is compact by TOPREAL6:79; SpanStart (C,n) in BDD C by A1, Th6; then A13: E-bound (BDD C) = E-bound (Cl (BDD C)) by A11, TOPREAL6:86; L~ (Span (C,n)) c= BDD C by A1, Th21; then E-bound (L~ (Span (C,n))) <= E-bound (Cl (BDD C)) by A12, A10, PSCOMP_1:67, XBOOLE_1:1; then A14: E-bound (BDD C) >= ((Gauge (C,n)) * (i,j)) `1 by A13, A9, XXREAL_0:2; A15: len (Gauge (C,n)) >= 4 by JORDAN8:10; then len (Gauge (C,n)) >= 1 + 1 by XXREAL_0:2; then A16: (len (Gauge (C,n))) - 1 >= 1 by XREAL_1:19; len (Gauge (C,n)) >= 0 + 1 by A15, XXREAL_0:2; then (len (Gauge (C,n))) - 1 >= 0 by XREAL_1:19; then A17: (len (Gauge (C,n))) -' 1 >= 1 by A16, XREAL_0:def_2; A18: j <= width (Gauge (C,n)) by A4, MATRIX_1:38; len (Gauge (C,n)) = width (Gauge (C,n)) by JORDAN8:def_1; then ((Gauge (C,n)) * (((len (Gauge (C,n))) -' 1),j)) `1 = E-bound C by A8, A18, JORDAN8:12; then A19: ((Gauge (C,n)) * (((len (Gauge (C,n))) -' 1),j)) `1 >= ((Gauge (C,n)) * (i,j)) `1 by A7, A14, XXREAL_0:2; i <= len (Gauge (C,n)) by A4, MATRIX_1:38; then i <= (len (Gauge (C,n))) -' 1 by A8, A18, A17, A19, GOBOARD5:3; then i < ((len (Gauge (C,n))) -' 1) + 1 by NAT_1:13; hence i < len (Gauge (C,n)) by A15, XREAL_1:235, XXREAL_0:2; ::_thesis: verum end; theorem Th24: :: JORDAN14:24 for C being Simple_closed_curve for i, j, k, n being Element of NAT st n is_sufficiently_large_for C & 1 <= k & k <= len (Span (C,n)) & [i,j] in Indices (Gauge (C,n)) & (Span (C,n)) /. k = (Gauge (C,n)) * (i,j) holds j > 1 proof let C be Simple_closed_curve; ::_thesis: for i, j, k, n being Element of NAT st n is_sufficiently_large_for C & 1 <= k & k <= len (Span (C,n)) & [i,j] in Indices (Gauge (C,n)) & (Span (C,n)) /. k = (Gauge (C,n)) * (i,j) holds j > 1 let i, j, k, n be Element of NAT ; ::_thesis: ( n is_sufficiently_large_for C & 1 <= k & k <= len (Span (C,n)) & [i,j] in Indices (Gauge (C,n)) & (Span (C,n)) /. k = (Gauge (C,n)) * (i,j) implies j > 1 ) assume that A1: n is_sufficiently_large_for C and A2: 1 <= k and A3: k <= len (Span (C,n)) and A4: [i,j] in Indices (Gauge (C,n)) and A5: (Span (C,n)) /. k = (Gauge (C,n)) * (i,j) ; ::_thesis: j > 1 A6: len (Span (C,n)) > 4 by GOBOARD7:34; SpanStart (C,n) in BDD C by A1, Th6; then A7: S-bound C <= S-bound (BDD C) by JORDAN1C:8; A8: i <= len (Gauge (C,n)) by A4, MATRIX_1:38; k in dom (Span (C,n)) by A2, A3, FINSEQ_3:25; then (Span (C,n)) /. k in L~ (Span (C,n)) by A6, GOBOARD1:1, XXREAL_0:2; then A9: S-bound (L~ (Span (C,n))) <= ((Gauge (C,n)) * (i,j)) `2 by A5, PSCOMP_1:24; A10: BDD C c= Cl (BDD C) by PRE_TOPC:18; A11: BDD C is bounded by JORDAN2C:106; then A12: Cl (BDD C) is compact by TOPREAL6:79; SpanStart (C,n) in BDD C by A1, Th6; then A13: S-bound (BDD C) = S-bound (Cl (BDD C)) by A11, TOPREAL6:88; L~ (Span (C,n)) c= BDD C by A1, Th21; then S-bound (L~ (Span (C,n))) >= S-bound (Cl (BDD C)) by A12, A10, PSCOMP_1:68, XBOOLE_1:1; then A14: S-bound (BDD C) <= ((Gauge (C,n)) * (i,j)) `2 by A13, A9, XXREAL_0:2; len (Gauge (C,n)) >= 4 by JORDAN8:10; then A15: len (Gauge (C,n)) >= 2 by XXREAL_0:2; A16: len (Gauge (C,n)) = width (Gauge (C,n)) by JORDAN8:def_1; A17: 1 <= i by A4, MATRIX_1:38; then ((Gauge (C,n)) * (i,2)) `2 = S-bound C by A8, JORDAN8:13; then A18: ((Gauge (C,n)) * (i,2)) `2 <= ((Gauge (C,n)) * (i,j)) `2 by A7, A14, XXREAL_0:2; 1 <= j by A4, MATRIX_1:38; then j >= 1 + 1 by A17, A8, A16, A15, A18, GOBOARD5:4; hence j > 1 by NAT_1:13; ::_thesis: verum end; theorem Th25: :: JORDAN14:25 for C being Simple_closed_curve for i, j, k, n being Element of NAT st n is_sufficiently_large_for C & 1 <= k & k <= len (Span (C,n)) & [i,j] in Indices (Gauge (C,n)) & (Span (C,n)) /. k = (Gauge (C,n)) * (i,j) holds j < width (Gauge (C,n)) proof let C be Simple_closed_curve; ::_thesis: for i, j, k, n being Element of NAT st n is_sufficiently_large_for C & 1 <= k & k <= len (Span (C,n)) & [i,j] in Indices (Gauge (C,n)) & (Span (C,n)) /. k = (Gauge (C,n)) * (i,j) holds j < width (Gauge (C,n)) let i, j, k, n be Element of NAT ; ::_thesis: ( n is_sufficiently_large_for C & 1 <= k & k <= len (Span (C,n)) & [i,j] in Indices (Gauge (C,n)) & (Span (C,n)) /. k = (Gauge (C,n)) * (i,j) implies j < width (Gauge (C,n)) ) assume that A1: n is_sufficiently_large_for C and A2: 1 <= k and A3: k <= len (Span (C,n)) and A4: [i,j] in Indices (Gauge (C,n)) and A5: (Span (C,n)) /. k = (Gauge (C,n)) * (i,j) ; ::_thesis: j < width (Gauge (C,n)) A6: len (Span (C,n)) > 4 by GOBOARD7:34; k in dom (Span (C,n)) by A2, A3, FINSEQ_3:25; then (Span (C,n)) /. k in L~ (Span (C,n)) by A6, GOBOARD1:1, XXREAL_0:2; then A7: N-bound (L~ (Span (C,n))) >= ((Gauge (C,n)) * (i,j)) `2 by A5, PSCOMP_1:24; A8: BDD C c= Cl (BDD C) by PRE_TOPC:18; A9: BDD C is bounded by JORDAN2C:106; then A10: Cl (BDD C) is compact by TOPREAL6:79; SpanStart (C,n) in BDD C by A1, Th6; then A11: N-bound (BDD C) = N-bound (Cl (BDD C)) by A9, TOPREAL6:87; L~ (Span (C,n)) c= BDD C by A1, Th21; then N-bound (L~ (Span (C,n))) <= N-bound (Cl (BDD C)) by A10, A8, PSCOMP_1:66, XBOOLE_1:1; then A12: N-bound (BDD C) >= ((Gauge (C,n)) * (i,j)) `2 by A11, A7, XXREAL_0:2; A13: len (Gauge (C,n)) = width (Gauge (C,n)) by JORDAN8:def_1; A14: len (Gauge (C,n)) >= 4 by JORDAN8:10; then len (Gauge (C,n)) >= 1 + 1 by XXREAL_0:2; then A15: (len (Gauge (C,n))) - 1 >= 1 by XREAL_1:19; SpanStart (C,n) in BDD C by A1, Th6; then A16: N-bound C >= N-bound (BDD C) by JORDAN1C:9; A17: i <= len (Gauge (C,n)) by A4, MATRIX_1:38; A18: 1 <= i by A4, MATRIX_1:38; then ((Gauge (C,n)) * (i,((len (Gauge (C,n))) -' 1))) `2 = N-bound C by A17, JORDAN8:14; then A19: ((Gauge (C,n)) * (i,((len (Gauge (C,n))) -' 1))) `2 >= ((Gauge (C,n)) * (i,j)) `2 by A16, A12, XXREAL_0:2; len (Gauge (C,n)) >= 0 + 1 by A14, XXREAL_0:2; then (len (Gauge (C,n))) - 1 >= 0 by XREAL_1:19; then A20: (len (Gauge (C,n))) -' 1 >= 1 by A15, XREAL_0:def_2; j <= width (Gauge (C,n)) by A4, MATRIX_1:38; then j <= (len (Gauge (C,n))) -' 1 by A18, A17, A20, A19, GOBOARD5:4; then j < ((len (Gauge (C,n))) -' 1) + 1 by NAT_1:13; hence j < width (Gauge (C,n)) by A13, A14, XREAL_1:235, XXREAL_0:2; ::_thesis: verum end; theorem :: JORDAN14:26 for C being Simple_closed_curve for n being Element of NAT st n is_sufficiently_large_for C holds Y-SpanStart (C,n) < width (Gauge (C,n)) proof let C be Simple_closed_curve; ::_thesis: for n being Element of NAT st n is_sufficiently_large_for C holds Y-SpanStart (C,n) < width (Gauge (C,n)) let n be Element of NAT ; ::_thesis: ( n is_sufficiently_large_for C implies Y-SpanStart (C,n) < width (Gauge (C,n)) ) A1: len (Span (C,n)) > 1 by GOBOARD7:34, XXREAL_0:2; assume A2: n is_sufficiently_large_for C ; ::_thesis: Y-SpanStart (C,n) < width (Gauge (C,n)) then A3: (Span (C,n)) /. 1 = (Gauge (C,n)) * ((X-SpanStart (C,n)),(Y-SpanStart (C,n))) by JORDAN13:def_1; [(X-SpanStart (C,n)),(Y-SpanStart (C,n))] in Indices (Gauge (C,n)) by A2, JORDAN11:8; hence Y-SpanStart (C,n) < width (Gauge (C,n)) by A2, A1, A3, Th25; ::_thesis: verum end; theorem Th27: :: JORDAN14:27 for C being compact non horizontal non vertical Subset of (TOP-REAL 2) for n, m being Element of NAT st m >= n & n >= 1 holds X-SpanStart (C,m) = ((2 |^ (m -' n)) * ((X-SpanStart (C,n)) - 2)) + 2 proof let C be compact non horizontal non vertical Subset of (TOP-REAL 2); ::_thesis: for n, m being Element of NAT st m >= n & n >= 1 holds X-SpanStart (C,m) = ((2 |^ (m -' n)) * ((X-SpanStart (C,n)) - 2)) + 2 let n, m be Element of NAT ; ::_thesis: ( m >= n & n >= 1 implies X-SpanStart (C,m) = ((2 |^ (m -' n)) * ((X-SpanStart (C,n)) - 2)) + 2 ) A1: X-SpanStart (C,n) = (2 |^ (n -' 1)) + 2 by JORDAN1H:def_2; assume A2: m >= n ; ::_thesis: ( not n >= 1 or X-SpanStart (C,m) = ((2 |^ (m -' n)) * ((X-SpanStart (C,n)) - 2)) + 2 ) assume A3: n >= 1 ; ::_thesis: X-SpanStart (C,m) = ((2 |^ (m -' n)) * ((X-SpanStart (C,n)) - 2)) + 2 then (m -' n) + (n -' 1) = (m -' n) + (n - 1) by XREAL_1:233 .= ((m -' n) + n) - 1 .= m - 1 by A2, XREAL_1:235 .= m -' 1 by A2, A3, XREAL_1:233, XXREAL_0:2 ; then 2 |^ (m -' 1) = (2 |^ (m -' n)) * ((X-SpanStart (C,n)) - 2) by A1, NEWTON:8; hence X-SpanStart (C,m) = ((2 |^ (m -' n)) * ((X-SpanStart (C,n)) - 2)) + 2 by JORDAN1H:def_2; ::_thesis: verum end; theorem Th28: :: JORDAN14:28 for C being compact non horizontal non vertical Subset of (TOP-REAL 2) for n, m being Element of NAT st n <= m & n is_sufficiently_large_for C holds m is_sufficiently_large_for C proof let C be compact non horizontal non vertical Subset of (TOP-REAL 2); ::_thesis: for n, m being Element of NAT st n <= m & n is_sufficiently_large_for C holds m is_sufficiently_large_for C let n, m be Element of NAT ; ::_thesis: ( n <= m & n is_sufficiently_large_for C implies m is_sufficiently_large_for C ) assume that A1: n <= m and A2: n is_sufficiently_large_for C ; ::_thesis: m is_sufficiently_large_for C consider j being Element of NAT such that A3: j < width (Gauge (C,n)) and A4: cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),j) c= BDD C by A2, JORDAN1H:def_3; set iin = X-SpanStart (C,n); set iim = X-SpanStart (C,m); n >= 1 by A2, JORDAN1H:51; then A5: X-SpanStart (C,m) = ((2 |^ (m -' n)) * ((X-SpanStart (C,n)) - 2)) + 2 by A1, Th27; A6: j > 1 proof A7: (X-SpanStart (C,n)) -' 1 <= len (Gauge (C,n)) by JORDAN1H:50; assume A8: j <= 1 ; ::_thesis: contradiction percases ( j = 0 or j = 1 ) by A8, NAT_1:25; supposeA9: j = 0 ; ::_thesis: contradiction width (Gauge (C,n)) >= 0 by NAT_1:2; then A10: not cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),0) is empty by A7, JORDAN1A:24; cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),0) c= UBD C by A7, JORDAN1A:49; hence contradiction by A4, A9, A10, JORDAN2C:24, XBOOLE_1:68; ::_thesis: verum end; supposeA11: j = 1 ; ::_thesis: contradiction set i1 = X-SpanStart (C,n); A12: (X-SpanStart (C,n)) -' 1 <= X-SpanStart (C,n) by NAT_D:44; X-SpanStart (C,n) < len (Gauge (C,n)) by JORDAN1H:49; then A13: (X-SpanStart (C,n)) -' 1 < len (Gauge (C,n)) by A12, XXREAL_0:2; BDD C c= C ` by JORDAN2C:25; then A14: cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),1) c= C ` by A4, A11, XBOOLE_1:1; UBD C is_outside_component_of C by JORDAN2C:68; then A15: UBD C is_a_component_of C ` by JORDAN2C:def_3; width (Gauge (C,n)) <> 0 by GOBOARD1:def_3; then A16: 0 + 1 <= width (Gauge (C,n)) by NAT_1:14; then A17: not cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),1) is empty by A7, JORDAN1A:24; A18: 1 <= (X-SpanStart (C,n)) -' 1 by JORDAN1H:50; 0 < width (Gauge (C,n)) by A16, NAT_1:13; then (cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),0)) /\ (cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),(0 + 1))) = LSeg (((Gauge (C,n)) * (((X-SpanStart (C,n)) -' 1),(0 + 1))),((Gauge (C,n)) * ((((X-SpanStart (C,n)) -' 1) + 1),(0 + 1)))) by A13, A18, GOBOARD5:26; then A19: cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),0) meets cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),(0 + 1)) by XBOOLE_0:def_7; cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),0) c= UBD C by A7, JORDAN1A:49; then cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),1) c= UBD C by A16, A13, A19, A15, A14, GOBOARD9:4, JORDAN1A:25; hence contradiction by A4, A11, A17, JORDAN2C:24, XBOOLE_1:68; ::_thesis: verum end; end; end; then ((2 |^ (m -' n)) * (j - 2)) + 2 > 1 by A1, A3, JORDAN1A:32; then reconsider j1 = ((2 |^ (m -' n)) * (j - 2)) + 2 as Element of NAT by INT_1:3, XXREAL_0:2; X-SpanStart (C,n) > 2 by JORDAN1H:49; then A20: X-SpanStart (C,n) >= 2 + 1 by NAT_1:13; A21: j + 1 < width (Gauge (C,n)) proof assume j + 1 >= width (Gauge (C,n)) ; ::_thesis: contradiction then A22: ( j + 1 > width (Gauge (C,n)) or j + 1 = width (Gauge (C,n)) ) by XXREAL_0:1; A23: (X-SpanStart (C,n)) -' 1 <= len (Gauge (C,n)) by JORDAN1H:50; percases ( j = width (Gauge (C,n)) or j + 1 = width (Gauge (C,n)) ) by A3, A22, NAT_1:13; supposeA24: j = width (Gauge (C,n)) ; ::_thesis: contradiction A25: cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),(width (Gauge (C,n)))) c= UBD C by A23, JORDAN1A:50; not cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),j) is empty by A23, A24, JORDAN1A:24; hence contradiction by A4, A24, A25, JORDAN2C:24, XBOOLE_1:68; ::_thesis: verum end; suppose j + 1 = width (Gauge (C,n)) ; ::_thesis: contradiction then A26: cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),((width (Gauge (C,n))) -' 1)) c= BDD C by A4, NAT_D:34; BDD C c= C ` by JORDAN2C:25; then A27: cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),((width (Gauge (C,n))) -' 1)) c= C ` by A26, XBOOLE_1:1; A28: cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),(width (Gauge (C,n)))) c= UBD C by A23, JORDAN1A:50; set i1 = X-SpanStart (C,n); A29: (X-SpanStart (C,n)) -' 1 <= X-SpanStart (C,n) by NAT_D:44; X-SpanStart (C,n) < len (Gauge (C,n)) by JORDAN1H:49; then A30: (X-SpanStart (C,n)) -' 1 < len (Gauge (C,n)) by A29, XXREAL_0:2; UBD C is_outside_component_of C by JORDAN2C:68; then A31: UBD C is_a_component_of C ` by JORDAN2C:def_3; (width (Gauge (C,n))) -' 1 <= width (Gauge (C,n)) by NAT_D:44; then A32: not cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),((width (Gauge (C,n))) -' 1)) is empty by A23, JORDAN1A:24; A33: (width (Gauge (C,n))) - 1 < width (Gauge (C,n)) by XREAL_1:146; A34: 1 <= (X-SpanStart (C,n)) -' 1 by JORDAN1H:50; A35: width (Gauge (C,n)) <> 0 by GOBOARD1:def_3; then ((width (Gauge (C,n))) -' 1) + 1 = width (Gauge (C,n)) by NAT_1:14, XREAL_1:235; then (cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),(width (Gauge (C,n))))) /\ (cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),((width (Gauge (C,n))) -' 1))) = LSeg (((Gauge (C,n)) * (((X-SpanStart (C,n)) -' 1),(width (Gauge (C,n))))),((Gauge (C,n)) * ((((X-SpanStart (C,n)) -' 1) + 1),(width (Gauge (C,n)))))) by A30, A33, A34, GOBOARD5:26; then A36: cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),(width (Gauge (C,n)))) meets cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),((width (Gauge (C,n))) -' 1)) by XBOOLE_0:def_7; (width (Gauge (C,n))) -' 1 < width (Gauge (C,n)) by A35, A33, NAT_1:14, XREAL_1:233; then cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),((width (Gauge (C,n))) -' 1)) c= UBD C by A28, A30, A36, A31, A27, GOBOARD9:4, JORDAN1A:25; hence contradiction by A26, A32, JORDAN2C:24, XBOOLE_1:68; ::_thesis: verum end; end; end; X-SpanStart (C,n) < len (Gauge (C,n)) by JORDAN1H:49; then cell ((Gauge (C,m)),((X-SpanStart (C,m)) -' 1),j1) c= cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),j) by A1, A5, A20, A6, A21, JORDAN1A:48; then A37: cell ((Gauge (C,m)),((X-SpanStart (C,m)) -' 1),j1) c= BDD C by A4, XBOOLE_1:1; j1 < width (Gauge (C,m)) by A1, A3, A6, JORDAN1A:32; hence m is_sufficiently_large_for C by A37, JORDAN1H:def_3; ::_thesis: verum end; theorem Th29: :: JORDAN14:29 for G being Go-board for f being FinSequence of (TOP-REAL 2) for i, j being Element of NAT st f is_sequence_on G & f is special & i <= len G & j <= width G holds (cell (G,i,j)) \ (L~ f) is connected proof let G be Go-board; ::_thesis: for f being FinSequence of (TOP-REAL 2) for i, j being Element of NAT st f is_sequence_on G & f is special & i <= len G & j <= width G holds (cell (G,i,j)) \ (L~ f) is connected let f be FinSequence of (TOP-REAL 2); ::_thesis: for i, j being Element of NAT st f is_sequence_on G & f is special & i <= len G & j <= width G holds (cell (G,i,j)) \ (L~ f) is connected let i, j be Element of NAT ; ::_thesis: ( f is_sequence_on G & f is special & i <= len G & j <= width G implies (cell (G,i,j)) \ (L~ f) is connected ) assume that A1: f is_sequence_on G and A2: f is special and A3: i <= len G and A4: j <= width G ; ::_thesis: (cell (G,i,j)) \ (L~ f) is connected Int (cell (G,i,j)) misses L~ f by A1, A2, A3, A4, JORDAN9:14; then A5: Int (cell (G,i,j)) c= (L~ f) ` by SUBSET_1:23; (cell (G,i,j)) \ (L~ f) c= cell (G,i,j) by XBOOLE_1:36; then A6: (cell (G,i,j)) \ (L~ f) c= Cl (Int (cell (G,i,j))) by A3, A4, GOBRD11:35; A7: Int (cell (G,i,j)) c= cell (G,i,j) by TOPS_1:16; A8: Int (cell (G,i,j)) is convex by A3, A4, GOBOARD9:17; (cell (G,i,j)) \ (L~ f) = (cell (G,i,j)) /\ ((L~ f) `) by SUBSET_1:13; then Int (cell (G,i,j)) c= (cell (G,i,j)) \ (L~ f) by A5, A7, XBOOLE_1:19; hence (cell (G,i,j)) \ (L~ f) is connected by A6, A8, CONNSP_1:18; ::_thesis: verum end; theorem Th30: :: JORDAN14:30 for C being Simple_closed_curve for n, k being Element of NAT st n is_sufficiently_large_for C & Y-SpanStart (C,n) <= k & k <= ((2 |^ (n -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2 holds (cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),k)) \ (L~ (Span (C,n))) c= BDD (L~ (Span (C,n))) proof let C be Simple_closed_curve; ::_thesis: for n, k being Element of NAT st n is_sufficiently_large_for C & Y-SpanStart (C,n) <= k & k <= ((2 |^ (n -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2 holds (cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),k)) \ (L~ (Span (C,n))) c= BDD (L~ (Span (C,n))) let n, k be Element of NAT ; ::_thesis: ( n is_sufficiently_large_for C & Y-SpanStart (C,n) <= k & k <= ((2 |^ (n -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2 implies (cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),k)) \ (L~ (Span (C,n))) c= BDD (L~ (Span (C,n))) ) set G = Gauge (C,n); set f = Span (C,n); set AI = ApproxIndex C; set YI = Y-InitStart C; set XS = X-SpanStart (C,n); set YS = Y-SpanStart (C,n); assume that A1: n is_sufficiently_large_for C and A2: Y-SpanStart (C,n) <= k and A3: k <= ((2 |^ (n -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2 ; ::_thesis: (cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),k)) \ (L~ (Span (C,n))) c= BDD (L~ (Span (C,n))) A4: Span (C,n) is_sequence_on Gauge (C,n) by A1, JORDAN13:def_1; reconsider ro = k - (Y-SpanStart (C,n)) as Element of NAT by A2, INT_1:5; A5: ro <= (((2 |^ (n -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2) - (Y-SpanStart (C,n)) by A3, XREAL_1:9; A6: k = (Y-SpanStart (C,n)) + ro ; defpred S1[ Element of NAT ] means ( $1 <= (((2 |^ (n -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2) - (Y-SpanStart (C,n)) implies (cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),((Y-SpanStart (C,n)) + $1))) \ (L~ (Span (C,n))) c= BDD (L~ (Span (C,n))) ); A7: 1 <= (X-SpanStart (C,n)) -' 1 by JORDAN1H:50; X-SpanStart (C,n) > 2 by JORDAN1H:49; then A8: ((X-SpanStart (C,n)) -' 1) + 1 = X-SpanStart (C,n) by XREAL_1:235, XXREAL_0:2; A9: (X-SpanStart (C,n)) -' 1 < len (Gauge (C,n)) by JORDAN1H:50; A10: for t being Element of NAT st S1[t] holds S1[t + 1] proof let t be Element of NAT ; ::_thesis: ( S1[t] implies S1[t + 1] ) assume A11: ( t <= (((2 |^ (n -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2) - (Y-SpanStart (C,n)) implies (cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),((Y-SpanStart (C,n)) + t))) \ (L~ (Span (C,n))) c= BDD (L~ (Span (C,n))) ) ; ::_thesis: S1[t + 1] set Ls = LSeg (((Gauge (C,n)) * (((X-SpanStart (C,n)) -' 1),((Y-SpanStart (C,n)) + (t + 1)))),((Gauge (C,n)) * ((X-SpanStart (C,n)),((Y-SpanStart (C,n)) + (t + 1))))); A12: t < t + 1 by NAT_1:13; set p = (1 / 2) * (((Gauge (C,n)) * (((X-SpanStart (C,n)) -' 1),((Y-SpanStart (C,n)) + (t + 1)))) + ((Gauge (C,n)) * ((X-SpanStart (C,n)),((Y-SpanStart (C,n)) + (t + 1))))); A13: (cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),((Y-SpanStart (C,n)) + (t + 1)))) \ (L~ (Span (C,n))) c= (L~ (Span (C,n))) ` proof let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in (cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),((Y-SpanStart (C,n)) + (t + 1)))) \ (L~ (Span (C,n))) or y in (L~ (Span (C,n))) ` ) assume A14: y in (cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),((Y-SpanStart (C,n)) + (t + 1)))) \ (L~ (Span (C,n))) ; ::_thesis: y in (L~ (Span (C,n))) ` then not y in L~ (Span (C,n)) by XBOOLE_0:def_5; hence y in (L~ (Span (C,n))) ` by A14, SUBSET_1:29; ::_thesis: verum end; A15: (1 / 2) * (((Gauge (C,n)) * (((X-SpanStart (C,n)) -' 1),((Y-SpanStart (C,n)) + (t + 1)))) + ((Gauge (C,n)) * ((X-SpanStart (C,n)),((Y-SpanStart (C,n)) + (t + 1))))) in LSeg (((Gauge (C,n)) * (((X-SpanStart (C,n)) -' 1),((Y-SpanStart (C,n)) + (t + 1)))),((Gauge (C,n)) * ((X-SpanStart (C,n)),((Y-SpanStart (C,n)) + (t + 1))))) by RLTOPSP1:69; A16: ((Y-SpanStart (C,n)) + t) + 1 = (Y-SpanStart (C,n)) + (t + 1) ; then A17: 1 <= (Y-SpanStart (C,n)) + (t + 1) by NAT_1:11; A18: Y-InitStart C > 1 by JORDAN11:2; then Y-InitStart C >= (1 + 1) + 0 by NAT_1:13; then (Y-InitStart C) - 2 >= 0 by XREAL_1:19; then A19: (Y-InitStart C) -' 2 = (Y-InitStart C) - 2 by XREAL_0:def_2; assume A20: t + 1 <= (((2 |^ (n -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2) - (Y-SpanStart (C,n)) ; ::_thesis: (cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),((Y-SpanStart (C,n)) + (t + 1)))) \ (L~ (Span (C,n))) c= BDD (L~ (Span (C,n))) then A21: (t + 1) + (Y-SpanStart (C,n)) <= ((2 |^ (n -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2 by XREAL_1:19; assume not (cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),((Y-SpanStart (C,n)) + (t + 1)))) \ (L~ (Span (C,n))) c= BDD (L~ (Span (C,n))) ; ::_thesis: contradiction then consider x being set such that A22: x in (cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),((Y-SpanStart (C,n)) + (t + 1)))) \ (L~ (Span (C,n))) and A23: not x in BDD (L~ (Span (C,n))) by TARSKI:def_3; not x in L~ (Span (C,n)) by A22, XBOOLE_0:def_5; then x in (L~ (Span (C,n))) ` by A22, SUBSET_1:29; then x in (BDD (L~ (Span (C,n)))) \/ (UBD (L~ (Span (C,n)))) by JORDAN2C:27; then x in UBD (L~ (Span (C,n))) by A23, XBOOLE_0:def_3; then A24: (cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),((Y-SpanStart (C,n)) + (t + 1)))) \ (L~ (Span (C,n))) meets UBD (L~ (Span (C,n))) by A22, XBOOLE_0:3; A25: Y-InitStart C < width (Gauge (C,(ApproxIndex C))) by JORDAN11:def_2; ApproxIndex C <= n by A1, JORDAN11:def_1; then ((2 |^ (n -' (ApproxIndex C))) * ((Y-InitStart C) - 2)) + 2 < width (Gauge (C,n)) by A18, A25, JORDAN1A:32; then A26: ((Y-SpanStart (C,n)) + t) + 1 <= width (Gauge (C,n)) by A19, A21, XXREAL_0:2; A27: ((Y-SpanStart (C,n)) + t) + 1 <= ((2 |^ (n -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2 by A21; A28: now__::_thesis:_not_(1_/_2)_*_(((Gauge_(C,n))_*_(((X-SpanStart_(C,n))_-'_1),((Y-SpanStart_(C,n))_+_(t_+_1))))_+_((Gauge_(C,n))_*_((X-SpanStart_(C,n)),((Y-SpanStart_(C,n))_+_(t_+_1)))))_in_L~_(Span_(C,n)) A29: Y-SpanStart (C,n) <= (Y-SpanStart (C,n)) + (t + 1) by NAT_1:11; A30: X-SpanStart (C,n) < len (Gauge (C,n)) by JORDAN1H:49; assume (1 / 2) * (((Gauge (C,n)) * (((X-SpanStart (C,n)) -' 1),((Y-SpanStart (C,n)) + (t + 1)))) + ((Gauge (C,n)) * ((X-SpanStart (C,n)),((Y-SpanStart (C,n)) + (t + 1))))) in L~ (Span (C,n)) ; ::_thesis: contradiction then consider i being Element of NAT such that A31: 1 <= i and A32: i + 1 <= len (Span (C,n)) and A33: (1 / 2) * (((Gauge (C,n)) * (((X-SpanStart (C,n)) -' 1),((Y-SpanStart (C,n)) + (t + 1)))) + ((Gauge (C,n)) * ((X-SpanStart (C,n)),((Y-SpanStart (C,n)) + (t + 1))))) in LSeg ((Span (C,n)),i) by SPPOL_2:13; A34: LSeg ((Span (C,n)),i) = LSeg (((Span (C,n)) /. i),((Span (C,n)) /. (i + 1))) by A31, A32, TOPREAL1:def_3; consider i1, j1, i2, j2 being Element of NAT such that A35: [i1,j1] in Indices (Gauge (C,n)) and A36: (Span (C,n)) /. i = (Gauge (C,n)) * (i1,j1) and A37: [i2,j2] in Indices (Gauge (C,n)) and A38: (Span (C,n)) /. (i + 1) = (Gauge (C,n)) * (i2,j2) and A39: ( ( i1 = i2 & j1 + 1 = j2 ) or ( i1 + 1 = i2 & j1 = j2 ) or ( i1 = i2 + 1 & j1 = j2 ) or ( i1 = i2 & j1 = j2 + 1 ) ) by A4, A31, A32, JORDAN8:3; A40: 1 <= i1 by A35, MATRIX_1:38; A41: i2 <= len (Gauge (C,n)) by A37, MATRIX_1:38; A42: 1 <= i2 by A37, MATRIX_1:38; A43: j1 <= width (Gauge (C,n)) by A35, MATRIX_1:38; A44: 1 <= j2 by A37, MATRIX_1:38; A45: i1 <= len (Gauge (C,n)) by A35, MATRIX_1:38; A46: j2 <= width (Gauge (C,n)) by A37, MATRIX_1:38; A47: 1 <= j1 by A35, MATRIX_1:38; percases ( ( i1 = i2 & j1 + 1 = j2 ) or ( i1 + 1 = i2 & j1 = j2 ) or ( i1 = i2 + 1 & j1 = j2 ) or ( i1 = i2 & j1 = j2 + 1 ) ) by A39; suppose ( i1 = i2 & j1 + 1 = j2 ) ; ::_thesis: contradiction hence contradiction by A7, A8, A26, A17, A33, A34, A36, A38, A40, A45, A47, A46, A30, GOBOARD7:27; ::_thesis: verum end; supposeA48: ( i1 + 1 = i2 & j1 = j2 ) ; ::_thesis: contradiction then A49: (Y-SpanStart (C,n)) + (t + 1) = j1 by A7, A8, A26, A17, A33, A34, A36, A38, A40, A47, A43, A41, A30, GOBOARD7:26; A50: cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),((Y-SpanStart (C,n)) + (t + 1))) c= BDD C by A1, A21, A29, JORDAN11:def_3; A51: left_cell ((Span (C,n)),i,(Gauge (C,n))) = cell ((Gauge (C,n)),i1,j1) by A4, A31, A32, A35, A36, A37, A38, A48, GOBRD13:23; (X-SpanStart (C,n)) -' 1 = i1 by A7, A8, A26, A17, A33, A34, A36, A38, A40, A47, A43, A41, A30, A48, GOBOARD7:26; then cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),((Y-SpanStart (C,n)) + (t + 1))) meets C by A1, A31, A32, A49, A51, Th7; hence contradiction by A50, JORDAN1A:7, XBOOLE_1:63; ::_thesis: verum end; supposeA52: ( i1 = i2 + 1 & j1 = j2 ) ; ::_thesis: contradiction then A53: left_cell ((Span (C,n)),i,(Gauge (C,n))) = cell ((Gauge (C,n)),i2,(j2 -' 1)) by A4, A31, A32, A35, A36, A37, A38, GOBRD13:25; A54: (Y-SpanStart (C,n)) + (t + 1) = j2 by A7, A8, A26, A17, A33, A34, A36, A38, A45, A47, A43, A42, A30, A52, GOBOARD7:26; (X-SpanStart (C,n)) -' 1 = i2 by A7, A8, A26, A17, A33, A34, A36, A38, A45, A47, A43, A42, A30, A52, GOBOARD7:26; then cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),(((Y-SpanStart (C,n)) + (t + 1)) -' 1)) meets C by A1, A31, A32, A54, A53, Th7; then A55: cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),((Y-SpanStart (C,n)) + t)) meets C by A16, NAT_D:34; A56: Y-SpanStart (C,n) <= (Y-SpanStart (C,n)) + t by NAT_1:11; (Y-SpanStart (C,n)) + t <= ((2 |^ (n -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2 by A27, NAT_1:13; then cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),((Y-SpanStart (C,n)) + t)) c= BDD C by A1, A56, JORDAN11:def_3; hence contradiction by A55, JORDAN1A:7, XBOOLE_1:63; ::_thesis: verum end; suppose ( i1 = i2 & j1 = j2 + 1 ) ; ::_thesis: contradiction hence contradiction by A7, A8, A26, A17, A33, A34, A36, A38, A40, A45, A43, A44, A30, GOBOARD7:27; ::_thesis: verum end; end; end; (Y-SpanStart (C,n)) + t < width (Gauge (C,n)) by A26, NAT_1:13; then LSeg (((Gauge (C,n)) * (((X-SpanStart (C,n)) -' 1),((Y-SpanStart (C,n)) + (t + 1)))),((Gauge (C,n)) * ((X-SpanStart (C,n)),((Y-SpanStart (C,n)) + (t + 1))))) c= cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),((Y-SpanStart (C,n)) + t)) by A7, A9, A8, A16, GOBOARD5:21; then A57: (1 / 2) * (((Gauge (C,n)) * (((X-SpanStart (C,n)) -' 1),((Y-SpanStart (C,n)) + (t + 1)))) + ((Gauge (C,n)) * ((X-SpanStart (C,n)),((Y-SpanStart (C,n)) + (t + 1))))) in (cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),((Y-SpanStart (C,n)) + t))) \ (L~ (Span (C,n))) by A28, A15, XBOOLE_0:def_5; LSeg (((Gauge (C,n)) * (((X-SpanStart (C,n)) -' 1),((Y-SpanStart (C,n)) + (t + 1)))),((Gauge (C,n)) * ((X-SpanStart (C,n)),((Y-SpanStart (C,n)) + (t + 1))))) c= cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),((Y-SpanStart (C,n)) + (t + 1))) by A7, A9, A8, A26, A17, GOBOARD5:22; then A58: (1 / 2) * (((Gauge (C,n)) * (((X-SpanStart (C,n)) -' 1),((Y-SpanStart (C,n)) + (t + 1)))) + ((Gauge (C,n)) * ((X-SpanStart (C,n)),((Y-SpanStart (C,n)) + (t + 1))))) in (cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),((Y-SpanStart (C,n)) + (t + 1)))) \ (L~ (Span (C,n))) by A28, A15, XBOOLE_0:def_5; LeftComp (Span (C,n)) is_a_component_of (L~ (Span (C,n))) ` by GOBOARD9:def_1; then UBD (L~ (Span (C,n))) is_a_component_of (L~ (Span (C,n))) ` by GOBRD14:36; then (cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),((Y-SpanStart (C,n)) + (t + 1)))) \ (L~ (Span (C,n))) c= UBD (L~ (Span (C,n))) by A4, A9, A26, A24, A13, Th29, GOBOARD9:4; then BDD (L~ (Span (C,n))) meets UBD (L~ (Span (C,n))) by A11, A20, A12, A57, A58, XBOOLE_0:3, XXREAL_0:2; hence contradiction by JORDAN2C:24; ::_thesis: verum end; A59: S1[ 0 ] proof assume 0 <= (((2 |^ (n -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2) - (Y-SpanStart (C,n)) ; ::_thesis: (cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),((Y-SpanStart (C,n)) + 0))) \ (L~ (Span (C,n))) c= BDD (L~ (Span (C,n))) A60: (Span (C,n)) /. (1 + 1) = (Gauge (C,n)) * (((X-SpanStart (C,n)) -' 1),(Y-SpanStart (C,n))) by A1, JORDAN13:def_1; A61: [(X-SpanStart (C,n)),(Y-SpanStart (C,n))] in Indices (Gauge (C,n)) by A1, JORDAN11:8; A62: [((X-SpanStart (C,n)) -' 1),(Y-SpanStart (C,n))] in Indices (Gauge (C,n)) by A1, JORDAN11:9; A63: len (Span (C,n)) >= 1 + 1 by GOBOARD7:34, XXREAL_0:2; then A64: (right_cell ((Span (C,n)),1,(Gauge (C,n)))) \ (L~ (Span (C,n))) c= RightComp (Span (C,n)) by A4, JORDAN9:27; (Span (C,n)) /. 1 = (Gauge (C,n)) * ((X-SpanStart (C,n)),(Y-SpanStart (C,n))) by A1, JORDAN13:def_1; then right_cell ((Span (C,n)),1,(Gauge (C,n))) = cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),(Y-SpanStart (C,n))) by A4, A8, A63, A60, A61, A62, GOBRD13:26; hence (cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),((Y-SpanStart (C,n)) + 0))) \ (L~ (Span (C,n))) c= BDD (L~ (Span (C,n))) by A64, GOBRD14:37; ::_thesis: verum end; for t being Element of NAT holds S1[t] from NAT_1:sch_1(A59, A10); hence (cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),k)) \ (L~ (Span (C,n))) c= BDD (L~ (Span (C,n))) by A6, A5; ::_thesis: verum end; theorem Th31: :: JORDAN14:31 for C being Subset of (TOP-REAL 2) for n, m, i being Element of NAT st m <= n & 1 < i & i + 1 < len (Gauge (C,m)) holds (((2 |^ (n -' m)) * (i - 2)) + 2) + 1 < len (Gauge (C,n)) proof let C be Subset of (TOP-REAL 2); ::_thesis: for n, m, i being Element of NAT st m <= n & 1 < i & i + 1 < len (Gauge (C,m)) holds (((2 |^ (n -' m)) * (i - 2)) + 2) + 1 < len (Gauge (C,n)) let n, m, i be Element of NAT ; ::_thesis: ( m <= n & 1 < i & i + 1 < len (Gauge (C,m)) implies (((2 |^ (n -' m)) * (i - 2)) + 2) + 1 < len (Gauge (C,n)) ) assume that A1: m <= n and A2: 1 < i and A3: i + 1 < len (Gauge (C,m)) ; ::_thesis: (((2 |^ (n -' m)) * (i - 2)) + 2) + 1 < len (Gauge (C,n)) 1 + 1 <= i by A2, NAT_1:13; then reconsider i2 = i - 2 as Element of NAT by INT_1:5; A4: 2 |^ (n -' m) > 0 by NEWTON:83; len (Gauge (C,m)) = (2 |^ m) + (2 + 1) by JORDAN8:def_1 .= ((2 |^ m) + 2) + 1 ; then i < (2 |^ m) + 2 by A3, XREAL_1:7; then i2 < 2 |^ m by XREAL_1:19; then (2 |^ (n -' m)) * i2 < (2 |^ (n -' m)) * (2 |^ m) by A4, XREAL_1:68; then (2 |^ (n -' m)) * i2 < 2 |^ ((n -' m) + m) by NEWTON:8; then (2 |^ (n -' m)) * i2 < 2 |^ n by A1, XREAL_1:235; then ((2 |^ (n -' m)) * i2) + 2 < (2 |^ n) + 2 by XREAL_1:8; then (((2 |^ (n -' m)) * (i - 2)) + 2) + 1 < ((2 |^ n) + 2) + 1 by XREAL_1:8; then (((2 |^ (n -' m)) * (i - 2)) + 2) + 1 < (2 |^ n) + (1 + 2) ; hence (((2 |^ (n -' m)) * (i - 2)) + 2) + 1 < len (Gauge (C,n)) by JORDAN8:def_1; ::_thesis: verum end; theorem Th32: :: JORDAN14:32 for C being Simple_closed_curve for n, m being Element of NAT st n is_sufficiently_large_for C & n <= m holds RightComp (Span (C,n)) meets RightComp (Span (C,m)) proof let C be Simple_closed_curve; ::_thesis: for n, m being Element of NAT st n is_sufficiently_large_for C & n <= m holds RightComp (Span (C,n)) meets RightComp (Span (C,m)) let n, m be Element of NAT ; ::_thesis: ( n is_sufficiently_large_for C & n <= m implies RightComp (Span (C,n)) meets RightComp (Span (C,m)) ) assume that A1: n is_sufficiently_large_for C and A2: n <= m ; ::_thesis: RightComp (Span (C,n)) meets RightComp (Span (C,m)) set i1 = X-SpanStart (C,m); set G1 = Gauge (C,m); set YI = Y-InitStart C; set AI = ApproxIndex C; A3: m is_sufficiently_large_for C by A1, A2, Th28; then A4: ApproxIndex C <= m by JORDAN11:def_1; set i = X-SpanStart (C,n); set G = Gauge (C,n); A5: 1 <= (X-SpanStart (C,m)) -' 1 by JORDAN1H:50; set j1 = Y-SpanStart (C,m); set f1 = Span (C,m); Y-SpanStart (C,m) <= ((2 |^ (m -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2 by A3, JORDAN11:5; then A6: (cell ((Gauge (C,m)),((X-SpanStart (C,m)) -' 1),(((2 |^ (m -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2))) \ (L~ (Span (C,m))) c= BDD (L~ (Span (C,m))) by A1, A2, Th28, Th30; A7: X-SpanStart (C,n) < len (Gauge (C,n)) by JORDAN1H:49; then (X-SpanStart (C,n)) + 1 <= len (Gauge (C,n)) by NAT_1:13; then A8: X-SpanStart (C,n) <= (len (Gauge (C,n))) - 1 by XREAL_1:19; set XSAI = X-SpanStart (C,(ApproxIndex C)); set p2 = (Gauge (C,(ApproxIndex C))) * ((X-SpanStart (C,(ApproxIndex C))),(Y-InitStart C)); A9: 1 < X-SpanStart (C,(ApproxIndex C)) by JORDAN1H:49, XXREAL_0:2; A10: (Y-InitStart C) + 1 < width (Gauge (C,(ApproxIndex C))) by JORDAN11:3; then A11: Y-InitStart C < width (Gauge (C,(ApproxIndex C))) by NAT_1:13; set j4 = ((2 |^ (n -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2; A12: X-SpanStart (C,m) < len (Gauge (C,m)) by JORDAN1H:49; set j = Y-SpanStart (C,n); set f = Span (C,n); Y-SpanStart (C,n) <= ((2 |^ (n -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2 by A1, JORDAN11:5; then A13: (cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),(((2 |^ (n -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2))) \ (L~ (Span (C,n))) c= BDD (L~ (Span (C,n))) by A1, Th30; A14: Int (cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),(((2 |^ (n -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2))) c= cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),(((2 |^ (n -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2)) by TOPS_1:16; A15: 2 < X-SpanStart (C,n) by JORDAN1H:49; then A16: ((X-SpanStart (C,n)) -' 1) + 1 = X-SpanStart (C,n) by XREAL_1:235, XXREAL_0:2; then A17: (X-SpanStart (C,n)) -' 1 >= 1 + 1 by A15, NAT_1:13; set j3 = ((2 |^ (m -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2; A18: X-SpanStart (C,n) < len (Gauge (C,n)) by JORDAN1H:49; A19: Y-InitStart C > 1 by JORDAN11:2; then Y-InitStart C >= (1 + 1) + 0 by NAT_1:13; then A20: (Y-InitStart C) - 2 >= 0 by XREAL_1:19; then A21: ((2 |^ (n -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2 = ((2 |^ (n -' (ApproxIndex C))) * ((Y-InitStart C) - 2)) + 2 by XREAL_0:def_2; A22: ((2 |^ (m -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2 = ((2 |^ (m -' (ApproxIndex C))) * ((Y-InitStart C) - 2)) + 2 by A20, XREAL_0:def_2; then A23: 1 < ((2 |^ (m -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2 by A4, A11, A19, JORDAN1A:32; set p3 = (1 / 2) * (((Gauge (C,m)) * (((X-SpanStart (C,m)) -' 1),(((2 |^ (m -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2))) + ((Gauge (C,m)) * ((X-SpanStart (C,m)),((((2 |^ (m -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2) + 1)))); A24: (X-SpanStart (C,m)) -' 1 < len (Gauge (C,m)) by JORDAN1H:50; A25: ((2 |^ (m -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2 < width (Gauge (C,m)) by A4, A11, A19, A22, JORDAN1A:32; then A26: (((2 |^ (m -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2) + 1 <= width (Gauge (C,m)) by NAT_1:13; 2 < X-SpanStart (C,m) by JORDAN1H:49; then A27: ((X-SpanStart (C,m)) -' 1) + 1 = X-SpanStart (C,m) by XREAL_1:235, XXREAL_0:2; then A28: (1 / 2) * (((Gauge (C,m)) * (((X-SpanStart (C,m)) -' 1),(((2 |^ (m -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2))) + ((Gauge (C,m)) * ((X-SpanStart (C,m)),((((2 |^ (m -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2) + 1)))) in Int (cell ((Gauge (C,m)),((X-SpanStart (C,m)) -' 1),(((2 |^ (m -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2))) by A12, A23, A5, A26, GOBOARD6:31; then A29: ((Gauge (C,m)) * (((X-SpanStart (C,m)) -' 1),(((2 |^ (m -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2))) `2 < ((1 / 2) * (((Gauge (C,m)) * (((X-SpanStart (C,m)) -' 1),(((2 |^ (m -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2))) + ((Gauge (C,m)) * ((X-SpanStart (C,m)),((((2 |^ (m -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2) + 1))))) `2 by A12, A23, A27, A5, A26, Th4; A30: ((1 / 2) * (((Gauge (C,m)) * (((X-SpanStart (C,m)) -' 1),(((2 |^ (m -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2))) + ((Gauge (C,m)) * ((X-SpanStart (C,m)),((((2 |^ (m -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2) + 1))))) `2 < ((Gauge (C,m)) * (((X-SpanStart (C,m)) -' 1),((((2 |^ (m -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2) + 1))) `2 by A12, A23, A27, A5, A26, A28, Th4; A31: ((Gauge (C,m)) * (((X-SpanStart (C,m)) -' 1),(((2 |^ (m -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2))) `1 < ((1 / 2) * (((Gauge (C,m)) * (((X-SpanStart (C,m)) -' 1),(((2 |^ (m -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2))) + ((Gauge (C,m)) * ((X-SpanStart (C,m)),((((2 |^ (m -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2) + 1))))) `1 by A12, A23, A27, A5, A26, A28, Th4; A32: 1 < X-SpanStart (C,m) by JORDAN1H:49, XXREAL_0:2; then A33: ((Gauge (C,m)) * ((X-SpanStart (C,m)),(((2 |^ (m -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2))) `2 = ((Gauge (C,m)) * (1,(((2 |^ (m -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2))) `2 by A12, A23, A25, GOBOARD5:1 .= ((Gauge (C,m)) * (((X-SpanStart (C,m)) -' 1),(((2 |^ (m -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2))) `2 by A23, A25, A5, A24, GOBOARD5:1 ; A34: (((2 |^ (m -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2) + 1 >= 1 by NAT_1:11; then A35: ((Gauge (C,m)) * ((X-SpanStart (C,m)),((((2 |^ (m -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2) + 1))) `2 = ((Gauge (C,m)) * (1,((((2 |^ (m -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2) + 1))) `2 by A12, A32, A26, GOBOARD5:1 .= ((Gauge (C,m)) * (((X-SpanStart (C,m)) -' 1),((((2 |^ (m -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2) + 1))) `2 by A5, A24, A26, A34, GOBOARD5:1 ; A36: 1 <= (X-SpanStart (C,n)) -' 1 by JORDAN1H:50; A37: ApproxIndex C <= n by A1, JORDAN11:def_1; then A38: 1 < ((2 |^ (n -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2 by A11, A19, A21, JORDAN1A:32; (Y-InitStart C) + 1 < len (Gauge (C,(ApproxIndex C))) by A10, JORDAN8:def_1; then (((2 |^ (n -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2) + 1 < len (Gauge (C,n)) by A37, A21, Th31, JORDAN11:2; then ((((2 |^ (n -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2) + 1) + 1 <= len (Gauge (C,n)) by NAT_1:13; then A39: (((2 |^ (n -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2) + 1 <= (len (Gauge (C,n))) - 1 by XREAL_1:19; A40: (X-SpanStart (C,n)) -' 1 < len (Gauge (C,n)) by JORDAN1H:50; then ((X-SpanStart (C,n)) -' 1) + 1 <= len (Gauge (C,n)) by NAT_1:13; then A41: (X-SpanStart (C,n)) -' 1 <= (len (Gauge (C,n))) - 1 by XREAL_1:19; A42: ((2 |^ (n -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2 < width (Gauge (C,n)) by A37, A11, A19, A21, JORDAN1A:32; then A43: (((2 |^ (n -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2) + 1 <= width (Gauge (C,n)) by NAT_1:13; ((2 |^ (n -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2 < len (Gauge (C,n)) by A42, JORDAN8:def_1; then (((2 |^ (n -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2) + 1 <= len (Gauge (C,n)) by NAT_1:13; then A44: ((2 |^ (n -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2 <= (len (Gauge (C,n))) - 1 by XREAL_1:19; A45: X-SpanStart (C,(ApproxIndex C)) < len (Gauge (C,(ApproxIndex C))) by JORDAN1H:49; X-SpanStart (C,m) = ((2 |^ (m -' (ApproxIndex C))) * ((X-SpanStart (C,(ApproxIndex C))) - 2)) + 2 by A1, A2, Th28, JORDAN11:4; then A46: (Gauge (C,(ApproxIndex C))) * ((X-SpanStart (C,(ApproxIndex C))),(Y-InitStart C)) = (Gauge (C,m)) * ((X-SpanStart (C,m)),(((2 |^ (m -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2)) by A4, A9, A45, A11, A19, A22, JORDAN1A:33; A47: X-SpanStart (C,n) = ((2 |^ (n -' (ApproxIndex C))) * ((X-SpanStart (C,(ApproxIndex C))) - 2)) + 2 by A1, JORDAN11:4; then A48: (Gauge (C,(ApproxIndex C))) * ((X-SpanStart (C,(ApproxIndex C))),(Y-InitStart C)) = (Gauge (C,n)) * ((X-SpanStart (C,n)),(((2 |^ (n -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2)) by A37, A9, A45, A11, A19, A21, JORDAN1A:33; A49: 1 < X-SpanStart (C,n) by JORDAN1H:49, XXREAL_0:2; then ((Gauge (C,n)) * ((X-SpanStart (C,n)),(((2 |^ (n -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2))) `2 = ((Gauge (C,n)) * (1,(((2 |^ (n -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2))) `2 by A18, A38, A42, GOBOARD5:1 .= ((Gauge (C,n)) * (((X-SpanStart (C,n)) -' 1),(((2 |^ (n -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2))) `2 by A38, A42, A36, A40, GOBOARD5:1 ; then A50: ((Gauge (C,n)) * (((X-SpanStart (C,n)) -' 1),(((2 |^ (n -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2))) `2 < ((1 / 2) * (((Gauge (C,m)) * (((X-SpanStart (C,m)) -' 1),(((2 |^ (m -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2))) + ((Gauge (C,m)) * ((X-SpanStart (C,m)),((((2 |^ (m -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2) + 1))))) `2 by A47, A37, A9, A45, A11, A19, A21, A46, A29, A33, JORDAN1A:33; ((1 / 2) * (((Gauge (C,m)) * (((X-SpanStart (C,m)) -' 1),(((2 |^ (m -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2))) + ((Gauge (C,m)) * ((X-SpanStart (C,m)),((((2 |^ (m -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2) + 1))))) `1 < ((Gauge (C,m)) * ((X-SpanStart (C,m)),(((2 |^ (m -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2))) `1 by A12, A23, A27, A5, A26, A28, Th4; then A51: ((1 / 2) * (((Gauge (C,m)) * (((X-SpanStart (C,m)) -' 1),(((2 |^ (m -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2))) + ((Gauge (C,m)) * ((X-SpanStart (C,m)),((((2 |^ (m -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2) + 1))))) `1 < ((Gauge (C,n)) * ((X-SpanStart (C,n)),(((2 |^ (n -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2))) `1 by A47, A37, A9, A45, A11, A19, A21, A46, JORDAN1A:33; ((2 |^ (n -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2 >= 1 + 1 by A38, NAT_1:13; then ex c, d being Element of NAT st ( 2 <= c & c <= (len (Gauge (C,m))) - 1 & 2 <= d & d <= (len (Gauge (C,m))) - 1 & [c,d] in Indices (Gauge (C,m)) & (Gauge (C,n)) * (((X-SpanStart (C,n)) -' 1),(((2 |^ (n -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2)) = (Gauge (C,m)) * (c,d) & c = 2 + ((2 |^ (m -' n)) * (((X-SpanStart (C,n)) -' 1) -' 2)) & d = 2 + ((2 |^ (m -' n)) * ((((2 |^ (n -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2) -' 2)) ) by A2, A17, A41, A44, GOBRD14:8; then (Gauge (C,n)) * (((X-SpanStart (C,n)) -' 1),(((2 |^ (n -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2)) in { ((Gauge (C,m)) * (ii,jj)) where ii, jj is Element of NAT : [ii,jj] in Indices (Gauge (C,m)) } ; then (Gauge (C,n)) * (((X-SpanStart (C,n)) -' 1),(((2 |^ (n -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2)) in Values (Gauge (C,m)) by MATRIX_1:45; then ((Gauge (C,n)) * (((X-SpanStart (C,n)) -' 1),(((2 |^ (n -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2))) `1 <= ((Gauge (C,m)) * (((X-SpanStart (C,m)) -' 1),(((2 |^ (m -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2))) `1 by A48, A46, A49, A18, A38, A42, A12, A32, A23, A25, GOBRD13:14; then A52: ((Gauge (C,n)) * (((X-SpanStart (C,n)) -' 1),(((2 |^ (n -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2))) `1 < ((1 / 2) * (((Gauge (C,m)) * (((X-SpanStart (C,m)) -' 1),(((2 |^ (m -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2))) + ((Gauge (C,m)) * ((X-SpanStart (C,m)),((((2 |^ (m -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2) + 1))))) `1 by A31, XXREAL_0:2; (((2 |^ (n -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2) + 1 > 1 + 1 by A38, XREAL_1:6; then ex c, d being Element of NAT st ( 2 <= c & c <= (len (Gauge (C,m))) - 1 & 2 <= d & d <= (len (Gauge (C,m))) - 1 & [c,d] in Indices (Gauge (C,m)) & (Gauge (C,n)) * ((X-SpanStart (C,n)),((((2 |^ (n -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2) + 1)) = (Gauge (C,m)) * (c,d) & c = 2 + ((2 |^ (m -' n)) * ((X-SpanStart (C,n)) -' 2)) & d = 2 + ((2 |^ (m -' n)) * (((((2 |^ (n -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2) + 1) -' 2)) ) by A2, A15, A8, A39, GOBRD14:8; then (Gauge (C,n)) * ((X-SpanStart (C,n)),((((2 |^ (n -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2) + 1)) in { ((Gauge (C,m)) * (ii,jj)) where ii, jj is Element of NAT : [ii,jj] in Indices (Gauge (C,m)) } ; then (Gauge (C,n)) * ((X-SpanStart (C,n)),((((2 |^ (n -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2) + 1)) in Values (Gauge (C,m)) by MATRIX_1:45; then A53: ((Gauge (C,m)) * ((X-SpanStart (C,m)),((((2 |^ (m -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2) + 1))) `2 <= ((Gauge (C,n)) * ((X-SpanStart (C,n)),((((2 |^ (n -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2) + 1))) `2 by A48, A46, A49, A18, A38, A42, A12, A32, A23, A25, GOBRD13:15; A54: (((2 |^ (n -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2) + 1 >= 1 by NAT_1:11; then ((Gauge (C,n)) * ((X-SpanStart (C,n)),((((2 |^ (n -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2) + 1))) `2 = ((Gauge (C,n)) * (1,((((2 |^ (n -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2) + 1))) `2 by A49, A18, A43, GOBOARD5:1 .= ((Gauge (C,n)) * (((X-SpanStart (C,n)) -' 1),((((2 |^ (n -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2) + 1))) `2 by A36, A40, A43, A54, GOBOARD5:1 ; then ((1 / 2) * (((Gauge (C,m)) * (((X-SpanStart (C,m)) -' 1),(((2 |^ (m -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2))) + ((Gauge (C,m)) * ((X-SpanStart (C,m)),((((2 |^ (m -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2) + 1))))) `2 < ((Gauge (C,n)) * (((X-SpanStart (C,n)) -' 1),((((2 |^ (n -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2) + 1))) `2 by A30, A35, A53, XXREAL_0:2; then A55: (1 / 2) * (((Gauge (C,m)) * (((X-SpanStart (C,m)) -' 1),(((2 |^ (m -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2))) + ((Gauge (C,m)) * ((X-SpanStart (C,m)),((((2 |^ (m -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2) + 1)))) in Int (cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),(((2 |^ (n -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2))) by A7, A38, A16, A36, A52, A51, A43, A50, Th4; Span (C,n) is_sequence_on Gauge (C,n) by A1, JORDAN13:def_1; then Int (cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),(((2 |^ (n -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2))) misses L~ (Span (C,n)) by A42, A40, JORDAN9:14; then not (1 / 2) * (((Gauge (C,m)) * (((X-SpanStart (C,m)) -' 1),(((2 |^ (m -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2))) + ((Gauge (C,m)) * ((X-SpanStart (C,m)),((((2 |^ (m -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2) + 1)))) in L~ (Span (C,n)) by A55, XBOOLE_0:3; then (1 / 2) * (((Gauge (C,m)) * (((X-SpanStart (C,m)) -' 1),(((2 |^ (m -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2))) + ((Gauge (C,m)) * ((X-SpanStart (C,m)),((((2 |^ (m -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2) + 1)))) in (cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),(((2 |^ (n -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2))) \ (L~ (Span (C,n))) by A55, A14, XBOOLE_0:def_5; then (1 / 2) * (((Gauge (C,m)) * (((X-SpanStart (C,m)) -' 1),(((2 |^ (m -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2))) + ((Gauge (C,m)) * ((X-SpanStart (C,m)),((((2 |^ (m -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2) + 1)))) in BDD (L~ (Span (C,n))) by A13; then A56: (1 / 2) * (((Gauge (C,m)) * (((X-SpanStart (C,m)) -' 1),(((2 |^ (m -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2))) + ((Gauge (C,m)) * ((X-SpanStart (C,m)),((((2 |^ (m -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2) + 1)))) in RightComp (Span (C,n)) by GOBRD14:37; Span (C,m) is_sequence_on Gauge (C,m) by A3, JORDAN13:def_1; then Int (cell ((Gauge (C,m)),((X-SpanStart (C,m)) -' 1),(((2 |^ (m -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2))) misses L~ (Span (C,m)) by A25, A24, JORDAN9:14; then A57: not (1 / 2) * (((Gauge (C,m)) * (((X-SpanStart (C,m)) -' 1),(((2 |^ (m -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2))) + ((Gauge (C,m)) * ((X-SpanStart (C,m)),((((2 |^ (m -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2) + 1)))) in L~ (Span (C,m)) by A28, XBOOLE_0:3; Int (cell ((Gauge (C,m)),((X-SpanStart (C,m)) -' 1),(((2 |^ (m -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2))) c= cell ((Gauge (C,m)),((X-SpanStart (C,m)) -' 1),(((2 |^ (m -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2)) by TOPS_1:16; then (1 / 2) * (((Gauge (C,m)) * (((X-SpanStart (C,m)) -' 1),(((2 |^ (m -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2))) + ((Gauge (C,m)) * ((X-SpanStart (C,m)),((((2 |^ (m -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2) + 1)))) in (cell ((Gauge (C,m)),((X-SpanStart (C,m)) -' 1),(((2 |^ (m -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2))) \ (L~ (Span (C,m))) by A28, A57, XBOOLE_0:def_5; then (1 / 2) * (((Gauge (C,m)) * (((X-SpanStart (C,m)) -' 1),(((2 |^ (m -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2))) + ((Gauge (C,m)) * ((X-SpanStart (C,m)),((((2 |^ (m -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2) + 1)))) in BDD (L~ (Span (C,m))) by A6; then (1 / 2) * (((Gauge (C,m)) * (((X-SpanStart (C,m)) -' 1),(((2 |^ (m -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2))) + ((Gauge (C,m)) * ((X-SpanStart (C,m)),((((2 |^ (m -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2) + 1)))) in RightComp (Span (C,m)) by GOBRD14:37; hence RightComp (Span (C,n)) meets RightComp (Span (C,m)) by A56, XBOOLE_0:3; ::_thesis: verum end; theorem Th33: :: JORDAN14:33 for G being Go-board for f being FinSequence of (TOP-REAL 2) st f is_sequence_on G & f is special holds for i, j being Element of NAT st i <= len G & j <= width G holds Int (cell (G,i,j)) c= (L~ f) ` proof let G be Go-board; ::_thesis: for f being FinSequence of (TOP-REAL 2) st f is_sequence_on G & f is special holds for i, j being Element of NAT st i <= len G & j <= width G holds Int (cell (G,i,j)) c= (L~ f) ` let f be FinSequence of (TOP-REAL 2); ::_thesis: ( f is_sequence_on G & f is special implies for i, j being Element of NAT st i <= len G & j <= width G holds Int (cell (G,i,j)) c= (L~ f) ` ) assume that A1: f is_sequence_on G and A2: f is special ; ::_thesis: for i, j being Element of NAT st i <= len G & j <= width G holds Int (cell (G,i,j)) c= (L~ f) ` let i, j be Element of NAT ; ::_thesis: ( i <= len G & j <= width G implies Int (cell (G,i,j)) c= (L~ f) ` ) assume that A3: i <= len G and A4: j <= width G ; ::_thesis: Int (cell (G,i,j)) c= (L~ f) ` Int (cell (G,i,j)) misses L~ f by A1, A2, A3, A4, JORDAN9:14; hence Int (cell (G,i,j)) c= (L~ f) ` by SUBSET_1:23; ::_thesis: verum end; theorem Th34: :: JORDAN14:34 for C being Simple_closed_curve for n, m being Element of NAT st n is_sufficiently_large_for C & n <= m holds L~ (Span (C,m)) c= Cl (LeftComp (Span (C,n))) proof let C be Simple_closed_curve; ::_thesis: for n, m being Element of NAT st n is_sufficiently_large_for C & n <= m holds L~ (Span (C,m)) c= Cl (LeftComp (Span (C,n))) let i, j be Element of NAT ; ::_thesis: ( i is_sufficiently_large_for C & i <= j implies L~ (Span (C,j)) c= Cl (LeftComp (Span (C,i))) ) assume that A1: i is_sufficiently_large_for C and A2: i <= j and A3: not L~ (Span (C,j)) c= Cl (LeftComp (Span (C,i))) ; ::_thesis: contradiction A4: j is_sufficiently_large_for C by A1, A2, Th28; then A5: Span (C,j) is_sequence_on Gauge (C,j) by JORDAN13:def_1; set G = Gauge (C,j); set f = Span (C,j); consider p being Point of (TOP-REAL 2) such that A6: p in L~ (Span (C,j)) and A7: not p in Cl (LeftComp (Span (C,i))) by A3, SUBSET_1:2; consider i1 being Element of NAT such that A8: 1 <= i1 and A9: i1 + 1 <= len (Span (C,j)) and A10: p in LSeg ((Span (C,j)),i1) by A6, SPPOL_2:13; A11: i1 < len (Span (C,j)) by A9, NAT_1:13; A12: Span (C,i) is_sequence_on Gauge (C,i) by A1, JORDAN13:def_1; now__::_thesis:_left_cell_((Span_(C,j)),i1,(Gauge_(C,j)))_c=_Cl_(RightComp_(Span_(C,i))) ex i2, j2 being Element of NAT st ( 1 <= i2 & i2 + 1 <= len (Gauge (C,i)) & 1 <= j2 & j2 + 1 <= width (Gauge (C,i)) & left_cell ((Span (C,j)),i1,(Gauge (C,j))) c= cell ((Gauge (C,i)),i2,j2) ) proof A13: 1 <= i1 + 1 by NAT_1:11; then A14: i1 + 1 in dom (Span (C,j)) by A9, FINSEQ_3:25; then consider i5, j5 being Element of NAT such that A15: [i5,j5] in Indices (Gauge (C,j)) and A16: (Span (C,j)) /. (i1 + 1) = (Gauge (C,j)) * (i5,j5) by A5, GOBOARD1:def_9; A17: 1 <= i5 by A15, MATRIX_1:38; A18: j5 <= width (Gauge (C,j)) by A15, MATRIX_1:38; A19: i5 <= len (Gauge (C,j)) by A15, MATRIX_1:38; A20: 1 <= j5 by A15, MATRIX_1:38; A21: i1 in dom (Span (C,j)) by A8, A11, FINSEQ_3:25; then consider i4, j4 being Element of NAT such that A22: [i4,j4] in Indices (Gauge (C,j)) and A23: (Span (C,j)) /. i1 = (Gauge (C,j)) * (i4,j4) by A5, GOBOARD1:def_9; A24: 1 <= i4 by A22, MATRIX_1:38; (abs (i4 - i5)) + (abs (j4 - j5)) = 1 by A5, A21, A22, A23, A14, A15, A16, GOBOARD1:def_9; then A25: ( ( abs (i4 - i5) = 1 & j4 = j5 ) or ( abs (j4 - j5) = 1 & i4 = i5 ) ) by SEQM_3:42; A26: 1 <= j4 by A22, MATRIX_1:38; left_cell ((Span (C,j)),i1,(Gauge (C,j))) = left_cell ((Span (C,j)),i1,(Gauge (C,j))) ; then A27: ( ( i4 = i5 & j4 + 1 = j5 & left_cell ((Span (C,j)),i1,(Gauge (C,j))) = cell ((Gauge (C,j)),(i4 -' 1),j4) ) or ( i4 + 1 = i5 & j4 = j5 & left_cell ((Span (C,j)),i1,(Gauge (C,j))) = cell ((Gauge (C,j)),i4,j4) ) or ( i4 = i5 + 1 & j4 = j5 & left_cell ((Span (C,j)),i1,(Gauge (C,j))) = cell ((Gauge (C,j)),i5,(j5 -' 1)) ) or ( i4 = i5 & j4 = j5 + 1 & left_cell ((Span (C,j)),i1,(Gauge (C,j))) = cell ((Gauge (C,j)),i4,j5) ) ) by A5, A8, A9, A22, A23, A15, A16, GOBRD13:def_3; A28: j4 <= width (Gauge (C,j)) by A22, MATRIX_1:38; A29: i4 <= len (Gauge (C,j)) by A22, MATRIX_1:38; percases ( ( i4 = i5 & j4 + 1 = j5 ) or ( i4 + 1 = i5 & j4 = j5 ) or ( i4 = i5 + 1 & j4 = j5 ) or ( i4 = i5 & j4 = j5 + 1 ) ) by A25, SEQM_3:41; supposeA30: ( i4 = i5 & j4 + 1 = j5 ) ; ::_thesis: ex i2, j2 being Element of NAT st ( 1 <= i2 & i2 + 1 <= len (Gauge (C,i)) & 1 <= j2 & j2 + 1 <= width (Gauge (C,i)) & left_cell ((Span (C,j)),i1,(Gauge (C,j))) c= cell ((Gauge (C,i)),i2,j2) ) 1 < i4 by A1, A2, A8, A11, A22, A23, Th22, Th28; then 1 + 1 <= i4 by NAT_1:13; then A31: 1 <= i4 -' 1 by JORDAN5B:2; (i4 -' 1) + 1 = i4 by A24, XREAL_1:235; hence ex i2, j2 being Element of NAT st ( 1 <= i2 & i2 + 1 <= len (Gauge (C,i)) & 1 <= j2 & j2 + 1 <= width (Gauge (C,i)) & left_cell ((Span (C,j)),i1,(Gauge (C,j))) c= cell ((Gauge (C,i)),i2,j2) ) by A2, A29, A26, A18, A27, A30, A31, JORDAN1H:38; ::_thesis: verum end; supposeA32: ( i4 + 1 = i5 & j4 = j5 ) ; ::_thesis: ex i2, j2 being Element of NAT st ( 1 <= i2 & i2 + 1 <= len (Gauge (C,i)) & 1 <= j2 & j2 + 1 <= width (Gauge (C,i)) & left_cell ((Span (C,j)),i1,(Gauge (C,j))) c= cell ((Gauge (C,i)),i2,j2) ) j4 < width (Gauge (C,j)) by A1, A2, A8, A11, A22, A23, Th25, Th28; then j4 + 1 <= width (Gauge (C,j)) by NAT_1:13; hence ex i2, j2 being Element of NAT st ( 1 <= i2 & i2 + 1 <= len (Gauge (C,i)) & 1 <= j2 & j2 + 1 <= width (Gauge (C,i)) & left_cell ((Span (C,j)),i1,(Gauge (C,j))) c= cell ((Gauge (C,i)),i2,j2) ) by A2, A24, A26, A19, A27, A32, JORDAN1H:38; ::_thesis: verum end; supposeA33: ( i4 = i5 + 1 & j4 = j5 ) ; ::_thesis: ex i2, j2 being Element of NAT st ( 1 <= i2 & i2 + 1 <= len (Gauge (C,i)) & 1 <= j2 & j2 + 1 <= width (Gauge (C,i)) & left_cell ((Span (C,j)),i1,(Gauge (C,j))) c= cell ((Gauge (C,i)),i2,j2) ) 1 < j5 by A1, A2, A9, A13, A15, A16, Th24, Th28; then 1 + 1 <= j5 by NAT_1:13; then A34: 1 <= j5 -' 1 by JORDAN5B:2; (j5 -' 1) + 1 = j5 by A20, XREAL_1:235; hence ex i2, j2 being Element of NAT st ( 1 <= i2 & i2 + 1 <= len (Gauge (C,i)) & 1 <= j2 & j2 + 1 <= width (Gauge (C,i)) & left_cell ((Span (C,j)),i1,(Gauge (C,j))) c= cell ((Gauge (C,i)),i2,j2) ) by A2, A29, A17, A18, A27, A33, A34, JORDAN1H:38; ::_thesis: verum end; supposeA35: ( i4 = i5 & j4 = j5 + 1 ) ; ::_thesis: ex i2, j2 being Element of NAT st ( 1 <= i2 & i2 + 1 <= len (Gauge (C,i)) & 1 <= j2 & j2 + 1 <= width (Gauge (C,i)) & left_cell ((Span (C,j)),i1,(Gauge (C,j))) c= cell ((Gauge (C,i)),i2,j2) ) i4 < len (Gauge (C,j)) by A1, A2, A8, A11, A22, A23, Th23, Th28; then i4 + 1 <= len (Gauge (C,j)) by NAT_1:13; hence ex i2, j2 being Element of NAT st ( 1 <= i2 & i2 + 1 <= len (Gauge (C,i)) & 1 <= j2 & j2 + 1 <= width (Gauge (C,i)) & left_cell ((Span (C,j)),i1,(Gauge (C,j))) c= cell ((Gauge (C,i)),i2,j2) ) by A2, A24, A28, A20, A27, A35, JORDAN1H:38; ::_thesis: verum end; end; end; then consider i2, j2 being Element of NAT such that 1 <= i2 and A36: i2 + 1 <= len (Gauge (C,i)) and 1 <= j2 and A37: j2 + 1 <= width (Gauge (C,i)) and A38: left_cell ((Span (C,j)),i1,(Gauge (C,j))) c= cell ((Gauge (C,i)),i2,j2) ; A39: j2 < width (Gauge (C,i)) by A37, NAT_1:13; A40: LeftComp (Span (C,i)) is_a_component_of (L~ (Span (C,i))) ` by GOBOARD9:def_1; A41: (Cl (RightComp (Span (C,i)))) \/ (LeftComp (Span (C,i))) = ((L~ (Span (C,i))) \/ (RightComp (Span (C,i)))) \/ (LeftComp (Span (C,i))) by GOBRD14:21 .= the carrier of (TOP-REAL 2) by GOBRD14:15 ; assume not left_cell ((Span (C,j)),i1,(Gauge (C,j))) c= Cl (RightComp (Span (C,i))) ; ::_thesis: contradiction then not cell ((Gauge (C,i)),i2,j2) c= Cl (RightComp (Span (C,i))) by A38, XBOOLE_1:1; then A42: cell ((Gauge (C,i)),i2,j2) meets LeftComp (Span (C,i)) by A41, XBOOLE_1:73; A43: i2 < len (Gauge (C,i)) by A36, NAT_1:13; then cell ((Gauge (C,i)),i2,j2) = Cl (Int (cell ((Gauge (C,i)),i2,j2))) by A39, GOBRD11:35; then A44: Int (cell ((Gauge (C,i)),i2,j2)) meets LeftComp (Span (C,i)) by A42, TSEP_1:36; A45: Int (left_cell ((Span (C,j)),i1,(Gauge (C,j)))) c= Int (cell ((Gauge (C,i)),i2,j2)) by A38, TOPS_1:19; A46: Int (cell ((Gauge (C,i)),i2,j2)) is convex by A43, A39, GOBOARD9:17; Int (cell ((Gauge (C,i)),i2,j2)) c= (L~ (Span (C,i))) ` by A12, A43, A39, Th33; then Int (cell ((Gauge (C,i)),i2,j2)) c= LeftComp (Span (C,i)) by A44, A40, A46, GOBOARD9:4; then Int (left_cell ((Span (C,j)),i1,(Gauge (C,j)))) c= LeftComp (Span (C,i)) by A45, XBOOLE_1:1; then Cl (Int (left_cell ((Span (C,j)),i1,(Gauge (C,j))))) c= Cl (LeftComp (Span (C,i))) by PRE_TOPC:19; then A47: left_cell ((Span (C,j)),i1,(Gauge (C,j))) c= Cl (LeftComp (Span (C,i))) by A5, A8, A9, JORDAN9:11; LSeg ((Span (C,j)),i1) c= left_cell ((Span (C,j)),i1,(Gauge (C,j))) by A5, A8, A9, JORDAN1H:20; then LSeg ((Span (C,j)),i1) c= Cl (LeftComp (Span (C,i))) by A47, XBOOLE_1:1; hence contradiction by A7, A10; ::_thesis: verum end; then A48: C meets Cl (RightComp (Span (C,i))) by A4, A8, A9, Th7, XBOOLE_1:63; A49: Cl (RightComp (Span (C,i))) = (RightComp (Span (C,i))) \/ (L~ (Span (C,i))) by GOBRD14:21; C misses L~ (Span (C,i)) by A1, Th8; then A50: C meets RightComp (Span (C,i)) by A48, A49, XBOOLE_1:70; C meets C ; then A51: C meets LeftComp (Span (C,i)) by A1, Th11, XBOOLE_1:63; reconsider D = (L~ (Span (C,i))) ` as Subset of (TOP-REAL 2) ; D = (RightComp (Span (C,i))) \/ (LeftComp (Span (C,i))) by GOBRD12:10; then A52: LeftComp (Span (C,i)) c= D by XBOOLE_1:7; C c= LeftComp (Span (C,i)) by A1, Th11; then A53: C c= D by A52, XBOOLE_1:1; A54: LeftComp (Span (C,i)) is_a_component_of D by GOBOARD9:def_1; RightComp (Span (C,i)) is_a_component_of D by GOBOARD9:def_2; hence contradiction by A50, A53, A54, A51, JORDAN9:1, SPRECT_4:6; ::_thesis: verum end; theorem Th35: :: JORDAN14:35 for C being Simple_closed_curve for n, m being Element of NAT st n is_sufficiently_large_for C & n <= m holds RightComp (Span (C,n)) c= RightComp (Span (C,m)) proof let C be Simple_closed_curve; ::_thesis: for n, m being Element of NAT st n is_sufficiently_large_for C & n <= m holds RightComp (Span (C,n)) c= RightComp (Span (C,m)) let n, m be Element of NAT ; ::_thesis: ( n is_sufficiently_large_for C & n <= m implies RightComp (Span (C,n)) c= RightComp (Span (C,m)) ) assume that A1: n is_sufficiently_large_for C and A2: n <= m ; ::_thesis: RightComp (Span (C,n)) c= RightComp (Span (C,m)) A3: L~ (Span (C,n)) misses RightComp (Span (C,n)) by SPRECT_3:25; A4: RightComp (Span (C,n)) misses LeftComp (Span (C,n)) by GOBRD14:14; Cl (LeftComp (Span (C,n))) = (LeftComp (Span (C,n))) \/ (L~ (Span (C,n))) by GOBRD14:22; then Cl (LeftComp (Span (C,n))) misses RightComp (Span (C,n)) by A3, A4, XBOOLE_1:70; then L~ (Span (C,m)) misses RightComp (Span (C,n)) by A1, A2, Th34, XBOOLE_1:63; then A5: RightComp (Span (C,n)) c= (L~ (Span (C,m))) ` by SUBSET_1:23; A6: RightComp (Span (C,m)) is_a_component_of (L~ (Span (C,m))) ` by GOBOARD9:def_2; RightComp (Span (C,n)) meets RightComp (Span (C,m)) by A1, A2, Th32; hence RightComp (Span (C,n)) c= RightComp (Span (C,m)) by A6, A5, GOBOARD9:4; ::_thesis: verum end; theorem :: JORDAN14:36 for C being Simple_closed_curve for n, m being Element of NAT st n is_sufficiently_large_for C & n <= m holds LeftComp (Span (C,m)) c= LeftComp (Span (C,n)) proof let C be Simple_closed_curve; ::_thesis: for n, m being Element of NAT st n is_sufficiently_large_for C & n <= m holds LeftComp (Span (C,m)) c= LeftComp (Span (C,n)) let n, m be Element of NAT ; ::_thesis: ( n is_sufficiently_large_for C & n <= m implies LeftComp (Span (C,m)) c= LeftComp (Span (C,n)) ) assume that A1: n is_sufficiently_large_for C and A2: n <= m ; ::_thesis: LeftComp (Span (C,m)) c= LeftComp (Span (C,n)) A3: (Cl (RightComp (Span (C,n)))) ` = LeftComp (Span (C,n)) by JORDAN1H:43; A4: (Cl (RightComp (Span (C,m)))) ` = LeftComp (Span (C,m)) by JORDAN1H:43; Cl (RightComp (Span (C,n))) c= Cl (RightComp (Span (C,m))) by A1, A2, Th35, PRE_TOPC:19; hence LeftComp (Span (C,m)) c= LeftComp (Span (C,n)) by A3, A4, SUBSET_1:12; ::_thesis: verum end;