jordan11.miz



    begin

    reserve i,j,k,n for Nat,

C for being_simple_closed_curve Subset of ( TOP-REAL 2);

    

     Lm1: i > 0 & 1 <= j & j <= ( width ( Gauge (C,i))) & k <= j & 1 <= k & k <= ( width ( Gauge (C,i))) & (( LSeg ((( Gauge (C,i)) * (( Center ( Gauge (C,i))),j)),(( Gauge (C,i)) * (( Center ( Gauge (C,i))),k)))) /\ ( Upper_Arc ( L~ ( Cage (C,i))))) = {(( Gauge (C,i)) * (( Center ( Gauge (C,i))),j))} & (( LSeg ((( Gauge (C,i)) * (( Center ( Gauge (C,i))),j)),(( Gauge (C,i)) * (( Center ( Gauge (C,i))),k)))) /\ ( Lower_Arc ( L~ ( Cage (C,i))))) = {(( Gauge (C,i)) * (( Center ( Gauge (C,i))),k))} implies ( LSeg ((( Gauge (C,i)) * (( Center ( Gauge (C,i))),j)),(( Gauge (C,i)) * (( Center ( Gauge (C,i))),k)))) c= ( Cl ( RightComp ( Cage (C,i))))

    proof

      assume that

       A1: i > 0 and

       A2: 1 <= j and

       A3: j <= ( width ( Gauge (C,i))) and

       A4: k <= j and

       A5: 1 <= k and

       A6: k <= ( width ( Gauge (C,i))) and

       A7: (( LSeg ((( Gauge (C,i)) * (( Center ( Gauge (C,i))),j)),(( Gauge (C,i)) * (( Center ( Gauge (C,i))),k)))) /\ ( Upper_Arc ( L~ ( Cage (C,i))))) = {(( Gauge (C,i)) * (( Center ( Gauge (C,i))),j))} and

       A8: (( LSeg ((( Gauge (C,i)) * (( Center ( Gauge (C,i))),j)),(( Gauge (C,i)) * (( Center ( Gauge (C,i))),k)))) /\ ( Lower_Arc ( L~ ( Cage (C,i))))) = {(( Gauge (C,i)) * (( Center ( Gauge (C,i))),k))};

      set p = (( Gauge (C,i)) * (( Center ( Gauge (C,i))),j)), q = (( Gauge (C,i)) * (( Center ( Gauge (C,i))),k)), S = ( RightComp ( Cage (C,i)));

      

       A9: {q} c= ( Lower_Arc ( L~ ( Cage (C,i)))) by A8, XBOOLE_1: 17;

      

       A10: ( X-SpanStart (C,i)) = ( Center ( Gauge (C,i))) by JORDAN1B: 16;

      then

       A11: 1 < ( Center ( Gauge (C,i))) by JORDAN1H: 49, XXREAL_0: 2;

      

       A12: ( Center ( Gauge (C,i))) < ( len ( Gauge (C,i))) by A10, JORDAN1H: 49;

      then

       A13: [( Center ( Gauge (C,i))), j] in ( Indices ( Gauge (C,i))) by A2, A3, A11, MATRIX_0: 30;

      p in {p} by TARSKI:def 1;

      then p in ( Upper_Arc ( L~ ( Cage (C,i)))) by A7, XBOOLE_0:def 4;

      then

       A14: p in ( L~ ( Upper_Seq (C,i))) by A1, JORDAN1G: 55;

      

       A15: [( Center ( Gauge (C,i))), k] in ( Indices ( Gauge (C,i))) by A5, A6, A11, A12, MATRIX_0: 30;

      q in {q} by TARSKI:def 1;

      then q in ( Lower_Arc ( L~ ( Cage (C,i)))) by A8, XBOOLE_0:def 4;

      then q in ( L~ ( Lower_Seq (C,i))) by A1, JORDAN1G: 56;

      then j <> k by A2, A6, A11, A12, A14, JORDAN1J: 57;

      then

       A16: p <> q by A13, A15, JORDAN1H: 26;

      set A = (( LSeg (p,q)) \ {p, q});

      (( LSeg (p,q)) /\ ( L~ ( Cage (C,i)))) = (( LSeg (p,q)) /\ (( Upper_Arc ( L~ ( Cage (C,i)))) \/ ( Lower_Arc ( L~ ( Cage (C,i)))))) by JORDAN6: 50

      .= ((( LSeg (p,q)) /\ ( Upper_Arc ( L~ ( Cage (C,i))))) \/ (( LSeg (p,q)) /\ ( Lower_Arc ( L~ ( Cage (C,i)))))) by XBOOLE_1: 23

      .= {p, q} by A7, A8, ENUMSET1: 1;

      then A misses ( L~ ( Cage (C,i))) by XBOOLE_1: 90;

      then

       A17: A c= (( L~ ( Cage (C,i))) ` ) by SUBSET_1: 23;

      

       A18: C c= S by JORDAN10: 11;

      ( LSeg (q,p)) meets ( Upper_Arc C) by A1, A3, A4, A5, A7, A8, A11, A12, JORDAN1J: 61;

      then

       A19: ( LSeg (q,p)) meets C by JORDAN6: 61, XBOOLE_1: 63;

       {p} c= ( Upper_Arc ( L~ ( Cage (C,i)))) by A7, XBOOLE_1: 17;

      then ( {p} \/ {q}) c= (( Upper_Arc ( L~ ( Cage (C,i)))) \/ ( Lower_Arc ( L~ ( Cage (C,i))))) by A9, XBOOLE_1: 13;

      then ( {p} \/ {q}) c= ( L~ ( Cage (C,i))) by JORDAN6: 50;

      then

       A20: {p, q} c= ( L~ ( Cage (C,i))) by ENUMSET1: 1;

      ( L~ ( Cage (C,i))) misses C by JORDAN10: 5;

      then {p, q} misses C by A20, XBOOLE_1: 63;

      then

       A21: A meets C by A19, XBOOLE_1: 84;

      

       A22: A is convex by JORDAN1: 46;

      S is_a_component_of (( L~ ( Cage (C,i))) ` ) by GOBOARD9:def 2;

      then A c= S by A17, A21, A18, A22, GOBOARD9: 4;

      hence thesis by A16, JORDAN1H: 3;

    end;

    

     Lm2: ex n st n is_sufficiently_large_for C

    proof

      set s = ((( W-bound C) + ( E-bound C)) / 2), e = (( Gauge (C,1)) * (( X-SpanStart (C,1)),( len ( Gauge (C,1))))), f = (( Gauge (C,1)) * (( X-SpanStart (C,1)),1));

      

       A1: ( len ( Gauge (C,1))) = ( width ( Gauge (C,1))) by JORDAN8:def 1;

      

       A2: ( X-SpanStart (C,1)) = ( Center ( Gauge (C,1))) by JORDAN1B: 16;

      then ( X-SpanStart (C,1)) = ((( len ( Gauge (C,1))) div 2) + 1) by JORDAN1A:def 1;

      then

       A3: 1 <= ( X-SpanStart (C,1)) by NAT_1: 11;

      ( len ( Gauge (C,1))) >= 4 by JORDAN8: 10;

      then

       A4: 1 < ( len ( Gauge (C,1))) by XXREAL_0: 2;

      then

       A5: (f `1 ) = s by A2, JORDAN1A: 38;

      then

       A6: f in ( Vertical_Line s) by JORDAN1A: 8;

       0 < ( len ( Gauge (C,1))) by JORDAN8: 10;

      then (( len ( Gauge (C,1))) qua Integer div 2) < ( len ( Gauge (C,1))) by INT_1: 56;

      then ((( len ( Gauge (C,1))) div 2) + 1) <= ( len ( Gauge (C,1))) by NAT_1: 13;

      then ( X-SpanStart (C,1)) <= ( len ( Gauge (C,1))) by A2, JORDAN1A:def 1;

      then

       A7: (f `2 ) < (e `2 ) by A3, A4, A1, GOBOARD5: 4;

      set e1 = ( proj2 . e), f1 = ( proj2 . f);

      

       A8: ( proj2 . e) = (e `2 ) by PSCOMP_1:def 6;

      4 <= ( len ( Gauge (C,1))) by JORDAN8: 10;

      then

       A9: 1 <= ( len ( Gauge (C,1))) by XXREAL_0: 2;

      set AA = (( LSeg (e,f)) /\ ( Upper_Arc C)), BB = (( LSeg (e,f)) /\ ( Lower_Arc C));

      deffunc F( Nat) = ( In (( lower_bound ( proj2 .: (( LSeg (f,e)) /\ ( Upper_Arc ( L~ ( Cage (C,($1 + 1)))))))), REAL ));

      consider Es be Real_Sequence such that

       A10: for i be Element of NAT holds (Es . i) = F(i) from FUNCT_2:sch 4;

      reconsider A = ( proj2 .: AA), B = ( proj2 .: BB) as compact Subset of REAL by JCT_MISC: 15;

      deffunc G( Element of NAT ) = |[s, (Es . $1)]|;

      consider E be sequence of the carrier of ( TOP-REAL 2) such that

       A11: for i be Element of NAT holds (E . i) = G(i) from FUNCT_2:sch 4;

      

       A12: (e `1 ) = s by A2, A4, JORDAN1A: 38;

      then e in ( Vertical_Line s) by JORDAN1A: 8;

      then

       A13: ( LSeg (e,f)) c= ( Vertical_Line s) by A6, JORDAN1A: 13;

      

       A14: A misses B

      proof

        assume A meets B;

        then

        consider z be object such that

         A15: z in A and

         A16: z in B by XBOOLE_0: 3;

        reconsider z as Real by A15;

        consider p be Point of ( TOP-REAL 2) such that

         A17: p in AA and

         A18: z = ( proj2 . p) by A15, FUNCT_2: 65;

        

         A19: p in ( Upper_Arc C) by A17, XBOOLE_0:def 4;

        consider q be Point of ( TOP-REAL 2) such that

         A20: q in BB and

         A21: z = ( proj2 . q) by A16, FUNCT_2: 65;

        

         A22: (p `2 ) = ( proj2 . q) by A18, A21, PSCOMP_1:def 6

        .= (q `2 ) by PSCOMP_1:def 6;

        

         A23: q in ( Lower_Arc C) by A20, XBOOLE_0:def 4;

        

         A24: q in ( LSeg (e,f)) by A20, XBOOLE_0:def 4;

        

         A25: p in ( LSeg (e,f)) by A17, XBOOLE_0:def 4;

        

        then (p `1 ) = s by A13, JORDAN6: 31

        .= (q `1 ) by A13, A24, JORDAN6: 31;

        then p = q by A22, TOPREAL3: 6;

        then p in (( Upper_Arc C) /\ ( Lower_Arc C)) by A19, A23, XBOOLE_0:def 4;

        then

         A26: p in {( W-min C), ( E-max C)} by JORDAN6: 50;

        per cases by A26, TARSKI:def 2;

          suppose

           A27: p = ( W-min C);

          

           A28: (( W-min C) `1 ) = ( W-bound C) by EUCLID: 52;

          (( W-min C) `1 ) = s by A13, A25, A27, JORDAN6: 31;

          hence contradiction by A28, SPRECT_1: 31;

        end;

          suppose

           A29: p = ( E-max C);

          

           A30: (( E-max C) `1 ) = ( E-bound C) by EUCLID: 52;

          (( E-max C) `1 ) = s by A13, A25, A29, JORDAN6: 31;

          hence contradiction by A30, SPRECT_1: 31;

        end;

      end;

      deffunc H( Nat) = ( In (( upper_bound ( proj2 .: (( LSeg (f,(E . $1))) /\ ( Lower_Arc ( L~ ( Cage (C,($1 + 1)))))))), REAL ));

      consider Fs be Real_Sequence such that

       A31: for i be Element of NAT holds (Fs . i) = H(i) from FUNCT_2:sch 4;

      deffunc I( Element of NAT ) = |[s, (Fs . $1)]|;

      consider F be sequence of the carrier of ( TOP-REAL 2) such that

       A32: for i be Element of NAT holds (F . i) = I(i) from FUNCT_2:sch 4;

      deffunc F1( Nat) = ( proj2 .: ( LSeg ((E . $1),(F . $1))));

      consider S be sequence of ( bool REAL ) such that

       A33: for i be Element of NAT holds (S . i) = F1(i) from FUNCT_2:sch 4;

      

       A34: for i holds (E . i) in ( Upper_Arc ( L~ ( Cage (C,(i + 1)))))

      proof

        let i be Nat;

        set p = (E . i);

        

         A35: (i + 1) >= 1 by NAT_1: 11;

        reconsider DD = (( LSeg (f,e)) /\ ( Upper_Arc ( L~ ( Cage (C,(i + 1)))))) as compact Subset of ( TOP-REAL 2);

        reconsider D = ( proj2 .: DD) as compact Subset of REAL by JCT_MISC: 15;

        DD c= the carrier of ( TOP-REAL 2);

        then DD c= ( dom proj2 ) by FUNCT_2:def 1;

        then

         A36: (( dom proj2 ) /\ DD) = DD by XBOOLE_1: 28;

        

         A37: ( X-SpanStart (C,(i + 1))) = ( Center ( Gauge (C,(i + 1)))) by JORDAN1B: 16;

        then ( LSeg ((( Gauge (C,(i + 1))) * (( X-SpanStart (C,(i + 1))),1)),(( Gauge (C,(i + 1))) * (( X-SpanStart (C,(i + 1))),( len ( Gauge (C,(i + 1)))))))) meets ( Upper_Arc ( L~ ( Cage (C,(i + 1))))) by JORDAN1B: 31;

        then ( LSeg (f,e)) meets ( Upper_Arc ( L~ ( Cage (C,(i + 1))))) by A2, A37, A35, JORDAN1A: 44, XBOOLE_1: 63;

        then DD <> {} ;

        then ( dom proj2 ) meets DD by A36;

        then

         A38: D <> {} by RELAT_1: 118;

        

         A39: i in NAT by ORDINAL1:def 12;

        then (Es . i) = F(i) by A10;

        then

        consider dd be Point of ( TOP-REAL 2) such that

         A40: dd in DD and

         A41: (Es . i) = ( proj2 . dd) by A38, FUNCT_2: 65, RCOMP_1: 14;

        

         A42: dd in ( LSeg (e,f)) by A40, XBOOLE_0:def 4;

        

         A43: (E . i) = |[s, (Es . i)]| by A11, A39;

        then (p `2 ) = (Es . i) by EUCLID: 52;

        then

         A44: (dd `2 ) = (p `2 ) by A41, PSCOMP_1:def 6;

        (p `1 ) = s by A43, EUCLID: 52;

        then

         A45: (dd `1 ) = (p `1 ) by A13, A42, JORDAN6: 31;

        dd in ( Upper_Arc ( L~ ( Cage (C,(i + 1))))) by A40, XBOOLE_0:def 4;

        hence thesis by A45, A44, TOPREAL3: 6;

      end;

      

       A46: for i holds (F . i) in ( Lower_Arc ( L~ ( Cage (C,(i + 1)))))

      proof

        let i;

        set p = (F . i);

        

         A47: ( X-SpanStart (C,(i + 1))) = ( Center ( Gauge (C,(i + 1)))) by JORDAN1B: 16;

        reconsider DD = (( LSeg (f,(E . i))) /\ ( Lower_Arc ( L~ ( Cage (C,(i + 1)))))) as compact Subset of ( TOP-REAL 2);

        reconsider D = ( proj2 .: DD) as compact Subset of REAL by JCT_MISC: 15;

        

         A48: (E . i) in ( Upper_Arc ( L~ ( Cage (C,(i + 1))))) by A34;

        

         A49: i in NAT by ORDINAL1:def 12;

        DD c= the carrier of ( TOP-REAL 2);

        then DD c= ( dom proj2 ) by FUNCT_2:def 1;

        then

         A50: (( dom proj2 ) /\ DD) = DD by XBOOLE_1: 28;

        

         A51: (E . i) = |[s, (Es . i)]| by A11, A49;

        then

         A52: ((E . i) `1 ) = s by EUCLID: 52;

        then (E . i) in ( Vertical_Line s) by JORDAN1A: 8;

        then

         A53: ( LSeg ((E . i),f)) c= ( Vertical_Line s) by A6, JORDAN1A: 13;

        ((E . i) `2 ) = (Es . i) by A51, EUCLID: 52

        .= F(i) by A10, A49

        .= ( lower_bound ( proj2 .: (( LSeg (f,e)) /\ ( Upper_Arc ( L~ ( Cage (C,(i + 1))))))));

        then ex j st 1 <= j & j <= ( width ( Gauge (C,(i + 1)))) & (E . i) = (( Gauge (C,(i + 1))) * (( X-SpanStart (C,(i + 1))),j)) by A2, A1, A47, A52, JORDAN1F: 13;

        then ( LSeg (f,(E . i))) meets ( Lower_Arc ( L~ ( Cage (C,(i + 1))))) by A2, A47, A48, JORDAN1J: 62;

        then DD <> {} ;

        then ( dom proj2 ) meets DD by A50;

        then

         A54: D <> {} by RELAT_1: 118;

        

         A55: i in NAT by ORDINAL1:def 12;

        (Fs . i) = H(i) by A31, A55;

        then

        consider dd be Point of ( TOP-REAL 2) such that

         A56: dd in DD and

         A57: (Fs . i) = ( proj2 . dd) by A54, FUNCT_2: 65, RCOMP_1: 14;

        

         A58: dd in ( Lower_Arc ( L~ ( Cage (C,(i + 1))))) by A56, XBOOLE_0:def 4;

        

         A59: (F . i) = |[s, (Fs . i)]| by A32, A55;

        then (p `2 ) = (Fs . i) by EUCLID: 52;

        then

         A60: (dd `2 ) = (p `2 ) by A57, PSCOMP_1:def 6;

        

         A61: dd in ( LSeg ((E . i),f)) by A56, XBOOLE_0:def 4;

        (p `1 ) = s by A59, EUCLID: 52;

        then (dd `1 ) = (p `1 ) by A61, A53, JORDAN6: 31;

        hence thesis by A58, A60, TOPREAL3: 6;

      end;

      

       A62: for i be Nat holds (S . i) qua Subset of REAL is interval & (S . i) meets A & (S . i) meets B

      proof

        let i be Nat;

        reconsider DD = (( LSeg (e,f)) /\ ( Upper_Arc ( L~ ( Cage (C,(i + 1)))))) as compact Subset of ( TOP-REAL 2);

        reconsider D = ( proj2 .: DD) as compact Subset of REAL by JCT_MISC: 15;

        

         A63: ( X-SpanStart (C,(i + 1))) = ( Center ( Gauge (C,(i + 1)))) by JORDAN1B: 16;

        DD c= the carrier of ( TOP-REAL 2);

        then DD c= ( dom proj2 ) by FUNCT_2:def 1;

        then

         A64: (( dom proj2 ) /\ DD) = DD by XBOOLE_1: 28;

        

         A65: 1 <= (i + 1) by NAT_1: 11;

        

         A66: i in NAT by ORDINAL1:def 12;

        ( LSeg ((( Gauge (C,(i + 1))) * (( Center ( Gauge (C,(i + 1)))),1)),(( Gauge (C,(i + 1))) * (( Center ( Gauge (C,(i + 1)))),( len ( Gauge (C,(i + 1)))))))) meets ( Upper_Arc ( L~ ( Cage (C,(i + 1))))) by JORDAN1B: 31;

        then ( LSeg (f,e)) meets ( Upper_Arc ( L~ ( Cage (C,(i + 1))))) by A2, A65, JORDAN1A: 44, XBOOLE_1: 63;

        then DD <> {} ;

        then ( dom proj2 ) meets DD by A64;

        then

         A67: D <> {} by RELAT_1: 118;

        (Es . i) = F(i) by A10, A66;

        then

        consider dd be Point of ( TOP-REAL 2) such that

         A68: dd in DD and

         A69: (Es . i) = ( proj2 . dd) by A67, FUNCT_2: 65, RCOMP_1: 14;

        

         A70: dd in ( LSeg (f,e)) by A68, XBOOLE_0:def 4;

        reconsider DD = (( LSeg (f,(E . i))) /\ ( Lower_Arc ( L~ ( Cage (C,(i + 1)))))) as compact Subset of ( TOP-REAL 2);

        reconsider D = ( proj2 .: DD) as compact Subset of REAL by JCT_MISC: 15;

        DD c= the carrier of ( TOP-REAL 2);

        then DD c= ( dom proj2 ) by FUNCT_2:def 1;

        then

         A71: (( dom proj2 ) /\ DD) = DD by XBOOLE_1: 28;

        

         A72: i in NAT by ORDINAL1:def 12;

        

         A73: (E . i) = |[s, (Es . i)]| by A11, A72;

        then

         A74: ((E . i) `1 ) = s by EUCLID: 52;

        

         A75: (F . i) = |[s, (Fs . i)]| by A32, A72;

        then

         A76: ((F . i) `1 ) = s by EUCLID: 52;

        

         A77: ((F . i) `2 ) = (Fs . i) by A75, EUCLID: 52

        .= H(i) by A31, A72

        .= ( upper_bound ( proj2 .: (( LSeg (f,(E . i))) /\ ( Lower_Arc ( L~ ( Cage (C,(i + 1))))))));

        ((E . i) `2 ) = (Es . i) by A73, EUCLID: 52

        .= F(i) by A10, A72

        .= ( lower_bound ( proj2 .: (( LSeg (f,e)) /\ ( Upper_Arc ( L~ ( Cage (C,(i + 1))))))));

        then

        consider j such that

         A78: 1 <= j and

         A79: j <= ( width ( Gauge (C,(i + 1)))) and

         A80: (E . i) = (( Gauge (C,(i + 1))) * (( X-SpanStart (C,(i + 1))),j)) by A2, A1, A74, A63, JORDAN1F: 13;

        

         A81: (E . i) in ( Upper_Arc ( L~ ( Cage (C,(i + 1))))) by A34;

        then

        consider k such that

         A82: 1 <= k and

         A83: k <= ( width ( Gauge (C,(i + 1)))) and

         A84: (F . i) = (( Gauge (C,(i + 1))) * (( Center ( Gauge (C,(i + 1)))),k)) by A2, A63, A76, A78, A79, A80, A77, JORDAN1I: 28;

        

         A85: i in NAT by ORDINAL1:def 12;

        ((E . i) `2 ) = (Es . i) by A73, EUCLID: 52

        .= F(i) by A10, A85

        .= ( lower_bound ( proj2 .: (( LSeg (f,e)) /\ ( Upper_Arc ( L~ ( Cage (C,(i + 1))))))));

        then ex j st 1 <= j & j <= ( width ( Gauge (C,(i + 1)))) & (E . i) = (( Gauge (C,(i + 1))) * (( X-SpanStart (C,(i + 1))),j)) by A2, A1, A74, A63, JORDAN1F: 13;

        then ( LSeg (f,(E . i))) meets ( Lower_Arc ( L~ ( Cage (C,(i + 1))))) by A2, A63, A81, JORDAN1J: 62;

        then DD <> {} ;

        then ( dom proj2 ) meets DD by A71;

        then

         A86: D <> {} by RELAT_1: 118;

        

         A87: ((E . i) `2 ) = (Es . i) by A73, EUCLID: 52

        .= (dd `2 ) by A69, PSCOMP_1:def 6;

        for p be Real st p in D holds p <= ((E . i) `2 )

        proof

          let p be Real;

          assume p in D;

          then

          consider x be object such that x in ( dom proj2 ) and

           A88: x in DD and

           A89: p = ( proj2 . x) by FUNCT_1:def 6;

          

           A90: (f `2 ) <= ((E . i) `2 ) by A7, A70, A87, TOPREAL1: 4;

          reconsider x as Point of ( TOP-REAL 2) by A88;

          x in ( LSeg (f,(E . i))) by A88, XBOOLE_0:def 4;

          then (x `2 ) <= ((E . i) `2 ) by A90, TOPREAL1: 4;

          hence thesis by A89, PSCOMP_1:def 6;

        end;

        then

         A91: ( upper_bound D) <= ((E . i) `2 ) by A86, SEQ_4: 45;

        (dd `1 ) = ((E . i) `1 ) by A13, A74, A70, JORDAN6: 31;

        then

         A92: (E . i) in ( LSeg (e,f)) by A70, A87, TOPREAL3: 6;

        (Fs . i) = H(i) by A31, A85;

        then

        consider dd be Point of ( TOP-REAL 2) such that

         A93: dd in DD and

         A94: (Fs . i) = ( proj2 . dd) by A86, FUNCT_2: 65, RCOMP_1: 14;

        

         A95: ((F . i) `2 ) = (Fs . i) by A75, EUCLID: 52

        .= (dd `2 ) by A94, PSCOMP_1:def 6;

        

         A96: dd in ( LSeg ((E . i),f)) by A93, XBOOLE_0:def 4;

        (E . i) in ( Vertical_Line s) by A74, JORDAN1A: 8;

        then ( LSeg ((E . i),f)) c= ( Vertical_Line s) by A6, JORDAN1A: 13;

        then (dd `1 ) = ((F . i) `1 ) by A76, A96, JORDAN6: 31;

        then

         A97: (F . i) in ( LSeg ((E . i),f)) by A96, A95, TOPREAL3: 6;

        f in ( LSeg (e,f)) by RLTOPSP1: 68;

        then ( LSeg (f,(E . i))) c= ( LSeg (e,f)) by A92, TOPREAL1: 6;

        then

         A98: ( LSeg ((E . i),(F . i))) c= ( LSeg (e,f)) by A92, A97, TOPREAL1: 6;

        

         A99: for x be set holds x in (( LSeg ((E . i),(F . i))) /\ ( Upper_Arc ( L~ ( Cage (C,(i + 1)))))) implies x = (E . i)

        proof

          let x be set;

          reconsider DD = (( LSeg (f,e)) /\ ( Upper_Arc ( L~ ( Cage (C,(i + 1)))))) as compact Subset of ( TOP-REAL 2);

          reconsider D = ( proj2 .: DD) as compact Subset of REAL by JCT_MISC: 15;

          assume

           A100: x in (( LSeg ((E . i),(F . i))) /\ ( Upper_Arc ( L~ ( Cage (C,(i + 1))))));

          then

          reconsider p = x as Point of ( TOP-REAL 2);

          

           A101: p in ( LSeg ((E . i),(F . i))) by A100, XBOOLE_0:def 4;

          

           A102: i in NAT by ORDINAL1:def 12;

          p in ( Upper_Arc ( L~ ( Cage (C,(i + 1))))) by A100, XBOOLE_0:def 4;

          then p in DD by A98, A101, XBOOLE_0:def 4;

          then ( proj2 . p) in D by FUNCT_2: 35;

          then

           A103: (p `2 ) in D by PSCOMP_1:def 6;

          (E . i) = |[s, (Es . i)]| by A11, A102;

          

          then

           A104: ((E . i) `2 ) = (Es . i) by EUCLID: 52

          .= F(i) by A10, A102

          .= ( lower_bound D);

          D is real-bounded by RCOMP_1: 10;

          then

           A105: ((E . i) `2 ) <= (p `2 ) by A104, A103, SEQ_4:def 2;

          (p `2 ) <= ((E . i) `2 ) by A77, A91, A101, TOPREAL1: 4;

          then

           A106: (p `2 ) = ((E . i) `2 ) by A105, XXREAL_0: 1;

          (p `1 ) = ((E . i) `1 ) by A74, A76, A101, GOBOARD7: 5;

          hence thesis by A106, TOPREAL3: 6;

        end;

        

         A107: (( Gauge (C,(i + 1))) * (( Center ( Gauge (C,(i + 1)))),j)) in ( LSeg ((( Gauge (C,(i + 1))) * (( Center ( Gauge (C,(i + 1)))),k)),(( Gauge (C,(i + 1))) * (( Center ( Gauge (C,(i + 1)))),j)))) by RLTOPSP1: 68;

        

         A108: (( LSeg ((( Gauge (C,(i + 1))) * (( Center ( Gauge (C,(i + 1)))),k)),(( Gauge (C,(i + 1))) * (( Center ( Gauge (C,(i + 1)))),j)))) /\ ( Upper_Arc ( L~ ( Cage (C,(i + 1)))))) = {(( Gauge (C,(i + 1))) * (( Center ( Gauge (C,(i + 1)))),j))}

        proof

          thus (( LSeg ((( Gauge (C,(i + 1))) * (( Center ( Gauge (C,(i + 1)))),k)),(( Gauge (C,(i + 1))) * (( Center ( Gauge (C,(i + 1)))),j)))) /\ ( Upper_Arc ( L~ ( Cage (C,(i + 1)))))) c= {(( Gauge (C,(i + 1))) * (( Center ( Gauge (C,(i + 1)))),j))}

          proof

            let x be object;

            assume x in (( LSeg ((( Gauge (C,(i + 1))) * (( Center ( Gauge (C,(i + 1)))),k)),(( Gauge (C,(i + 1))) * (( Center ( Gauge (C,(i + 1)))),j)))) /\ ( Upper_Arc ( L~ ( Cage (C,(i + 1))))));

            then x = (( Gauge (C,(i + 1))) * (( Center ( Gauge (C,(i + 1)))),j)) by A63, A80, A84, A99;

            hence thesis by TARSKI:def 1;

          end;

          let x be object;

          assume x in {(( Gauge (C,(i + 1))) * (( Center ( Gauge (C,(i + 1)))),j))};

          then x = (( Gauge (C,(i + 1))) * (( Center ( Gauge (C,(i + 1)))),j)) by TARSKI:def 1;

          hence thesis by A63, A81, A80, A107, XBOOLE_0:def 4;

        end;

        (E . i) in ( LSeg ((E . i),f)) by RLTOPSP1: 68;

        then

         A109: ( LSeg ((E . i),(F . i))) c= ( LSeg ((E . i),f)) by A97, TOPREAL1: 6;

        

         A110: for x be set holds x in (( LSeg ((E . i),(F . i))) /\ ( Lower_Arc ( L~ ( Cage (C,(i + 1)))))) implies x = (F . i)

        proof

          let x be set;

          reconsider EE = (( LSeg (f,(E . i))) /\ ( Lower_Arc ( L~ ( Cage (C,(i + 1)))))) as compact Subset of ( TOP-REAL 2);

          reconsider E0 = ( proj2 .: EE) as compact Subset of REAL by JCT_MISC: 15;

          assume

           A111: x in (( LSeg ((E . i),(F . i))) /\ ( Lower_Arc ( L~ ( Cage (C,(i + 1))))));

          then

          reconsider p = x as Point of ( TOP-REAL 2);

          

           A112: p in ( LSeg ((E . i),(F . i))) by A111, XBOOLE_0:def 4;

          

           A113: i in NAT by ORDINAL1:def 12;

          p in ( Lower_Arc ( L~ ( Cage (C,(i + 1))))) by A111, XBOOLE_0:def 4;

          then p in EE by A109, A112, XBOOLE_0:def 4;

          then ( proj2 . p) in E0 by FUNCT_2: 35;

          then

           A114: (p `2 ) in E0 by PSCOMP_1:def 6;

          (F . i) = |[s, (Fs . i)]| by A32, A113;

          

          then

           A115: ((F . i) `2 ) = (Fs . i) by EUCLID: 52

          .= H(i) by A31, A113

          .= ( upper_bound E0);

          E0 is real-bounded by RCOMP_1: 10;

          then

           A116: ((F . i) `2 ) >= (p `2 ) by A115, A114, SEQ_4:def 1;

          (p `2 ) >= ((F . i) `2 ) by A77, A91, A112, TOPREAL1: 4;

          then

           A117: (p `2 ) = ((F . i) `2 ) by A116, XXREAL_0: 1;

          (p `1 ) = ((F . i) `1 ) by A74, A76, A112, GOBOARD7: 5;

          hence thesis by A117, TOPREAL3: 6;

        end;

        

         A118: (F . i) in ( Lower_Arc ( L~ ( Cage (C,(i + 1))))) by A46;

        

         A119: (S . i) = ( proj2 .: ( LSeg ((E . i),(F . i)))) by A33, A85;

        hence (S . i) is interval by JCT_MISC: 6;

        

         A120: ( Center ( Gauge (C,(i + 1)))) <= ( len ( Gauge (C,(i + 1)))) by JORDAN1B: 13;

        

         A121: (( Gauge (C,(i + 1))) * (( Center ( Gauge (C,(i + 1)))),k)) in ( LSeg ((( Gauge (C,(i + 1))) * (( Center ( Gauge (C,(i + 1)))),k)),(( Gauge (C,(i + 1))) * (( Center ( Gauge (C,(i + 1)))),j)))) by RLTOPSP1: 68;

        

         A122: (( LSeg ((( Gauge (C,(i + 1))) * (( Center ( Gauge (C,(i + 1)))),k)),(( Gauge (C,(i + 1))) * (( Center ( Gauge (C,(i + 1)))),j)))) /\ ( Lower_Arc ( L~ ( Cage (C,(i + 1)))))) = {(( Gauge (C,(i + 1))) * (( Center ( Gauge (C,(i + 1)))),k))}

        proof

          thus (( LSeg ((( Gauge (C,(i + 1))) * (( Center ( Gauge (C,(i + 1)))),k)),(( Gauge (C,(i + 1))) * (( Center ( Gauge (C,(i + 1)))),j)))) /\ ( Lower_Arc ( L~ ( Cage (C,(i + 1)))))) c= {(( Gauge (C,(i + 1))) * (( Center ( Gauge (C,(i + 1)))),k))}

          proof

            let x be object;

            assume x in (( LSeg ((( Gauge (C,(i + 1))) * (( Center ( Gauge (C,(i + 1)))),k)),(( Gauge (C,(i + 1))) * (( Center ( Gauge (C,(i + 1)))),j)))) /\ ( Lower_Arc ( L~ ( Cage (C,(i + 1))))));

            then x = (( Gauge (C,(i + 1))) * (( Center ( Gauge (C,(i + 1)))),k)) by A63, A80, A84, A110;

            hence thesis by TARSKI:def 1;

          end;

          let x be object;

          assume x in {(( Gauge (C,(i + 1))) * (( Center ( Gauge (C,(i + 1)))),k))};

          then x = (( Gauge (C,(i + 1))) * (( Center ( Gauge (C,(i + 1)))),k)) by TARSKI:def 1;

          hence thesis by A84, A118, A121, XBOOLE_0:def 4;

        end;

        1 <= ( Center ( Gauge (C,(i + 1)))) by JORDAN1B: 11;

        then

         A123: k <= j by A63, A78, A80, A77, A83, A84, A120, A91, GOBOARD5: 4;

        then ( LSeg ((E . i),(F . i))) meets AA by A63, A98, A79, A80, A82, A84, A108, A122, JORDAN1J: 64, XBOOLE_1: 77;

        hence (S . i) meets A by A119, JORDAN1A: 14;

        ( LSeg ((E . i),(F . i))) meets BB by A63, A98, A79, A80, A82, A84, A123, A108, A122, JORDAN1J: 63, XBOOLE_1: 77;

        hence thesis by A119, JORDAN1A: 14;

      end;

      ( proj2 . f) = (f `2 ) by PSCOMP_1:def 6;

      then

       A124: ( proj2 .: ( LSeg (f,e))) = [.f1, e1.] by A7, A8, SPRECT_1: 53;

      then

       A125: B c= [.f1, e1.] by RELAT_1: 123, XBOOLE_1: 17;

      A c= [.f1, e1.] by A124, RELAT_1: 123, XBOOLE_1: 17;

      then

      consider r be Real such that

       A126: r in [.f1, e1.] and

       A127: not r in (A \/ B) and

       A128: for i be Nat holds ex k be Nat st i <= k & r in (S . k) by A14, A125, A62, JCT_MISC: 12;

      reconsider r as Real;

      set p = |[s, r]|;

      

       A129: (p `1 ) = s by EUCLID: 52;

      for Y be set st Y in ( BDD-Family C) holds p in Y

      proof

        let Y be set;

        

         A130: ( BDD-Family C) = the set of all ( Cl ( BDD ( L~ ( Cage (C,k1))))) where k1 be Nat by JORDAN10:def 2;

        assume Y in ( BDD-Family C);

        then

        consider k1 be Nat such that

         A131: Y = ( Cl ( BDD ( L~ ( Cage (C,k1))))) by A130;

        consider k0 be Nat such that

         A132: k1 <= k0 and

         A133: r in (S . k0) by A128;

        

         A134: ( proj2 . (F . k0)) = ((F . k0) `2 ) by PSCOMP_1:def 6;

        reconsider EE = (( LSeg (f,(E . k0))) /\ ( Lower_Arc ( L~ ( Cage (C,(k0 + 1)))))) as compact Subset of ( TOP-REAL 2);

        reconsider CC = (( LSeg (f,(E . k0))) /\ ( Lower_Arc ( L~ ( Cage (C,(k0 + 1)))))) as compact Subset of ( TOP-REAL 2);

        reconsider W = ( proj2 .: CC) as compact Subset of REAL by JCT_MISC: 15;

        

         A135: ( Center ( Gauge (C,(k0 + 1)))) <= ( len ( Gauge (C,(k0 + 1)))) by JORDAN1B: 13;

        reconsider E0 = ( proj2 .: EE) as compact Subset of REAL by JCT_MISC: 15;

        CC c= the carrier of ( TOP-REAL 2);

        then CC c= ( dom proj2 ) by FUNCT_2:def 1;

        then

         A136: (( dom proj2 ) /\ CC) = CC by XBOOLE_1: 28;

        

         A137: ( RightComp ( Cage (C,(k0 + 1)))) c= ( RightComp ( Cage (C,k0))) by JORDAN1H: 48, NAT_1: 11;

        ( RightComp ( Cage (C,k0))) c= ( RightComp ( Cage (C,k1))) by A132, JORDAN1H: 48;

        then ( RightComp ( Cage (C,(k0 + 1)))) c= ( RightComp ( Cage (C,k1))) by A137;

        then

         A138: ( Cl ( RightComp ( Cage (C,(k0 + 1))))) c= ( Cl ( RightComp ( Cage (C,k1)))) by PRE_TOPC: 19;

        

         A139: (E . k0) in ( Upper_Arc ( L~ ( Cage (C,(k0 + 1))))) by A34;

        

         A140: (1 + 0 ) <= (k0 + 1) by NAT_1: 11;

        

         A141: (E . k0) in ( Upper_Arc ( L~ ( Cage (C,(k0 + 1))))) by A34;

        

         A142: ( X-SpanStart (C,(k0 + 1))) = ( Center ( Gauge (C,(k0 + 1)))) by JORDAN1B: 16;

        reconsider DD = (( LSeg (f,(E . k0))) /\ ( Lower_Arc ( L~ ( Cage (C,(k0 + 1)))))) as compact Subset of ( TOP-REAL 2);

        

         A143: ( proj2 . (E . k0)) = ((E . k0) `2 ) by PSCOMP_1:def 6;

        reconsider D = ( proj2 .: DD) as compact Subset of REAL by JCT_MISC: 15;

        

         A144: k0 in NAT by ORDINAL1:def 12;

        

         A145: (Fs . k0) = H(k0) by A31, A144

        .= ( upper_bound D);

        DD c= the carrier of ( TOP-REAL 2);

        then DD c= ( dom proj2 ) by FUNCT_2:def 1;

        then

         A146: (( dom proj2 ) /\ DD) = DD by XBOOLE_1: 28;

        

         A147: (E . k0) = |[s, (Es . k0)]| by A11, A144;

        then

         A148: ((E . k0) `1 ) = s by EUCLID: 52;

        ((E . k0) `2 ) = (Es . k0) by A147, EUCLID: 52

        .= F(k0) by A10, A144

        .= ( lower_bound ( proj2 .: (( LSeg (f,e)) /\ ( Upper_Arc ( L~ ( Cage (C,(k0 + 1))))))));

        then ex j st 1 <= j & j <= ( width ( Gauge (C,(k0 + 1)))) & (E . k0) = (( Gauge (C,(k0 + 1))) * (( X-SpanStart (C,(k0 + 1))),j)) by A2, A1, A148, A142, JORDAN1F: 13;

        then

         A149: ( LSeg (f,(E . k0))) meets ( Lower_Arc ( L~ ( Cage (C,(k0 + 1))))) by A2, A142, A141, JORDAN1J: 62;

        then DD <> {} ;

        then ( dom proj2 ) meets DD by A146;

        then D <> {} by RELAT_1: 118;

        then

        consider dd be Point of ( TOP-REAL 2) such that

         A150: dd in DD and

         A151: (Fs . k0) = ( proj2 . dd) by A145, FUNCT_2: 65, RCOMP_1: 14;

        

         A152: dd in ( LSeg ((E . k0),f)) by A150, XBOOLE_0:def 4;

        reconsider DD = (( LSeg (f,e)) /\ ( Upper_Arc ( L~ ( Cage (C,(k0 + 1)))))) as compact Subset of ( TOP-REAL 2);

        reconsider D = ( proj2 .: DD) as compact Subset of REAL by JCT_MISC: 15;

        DD c= the carrier of ( TOP-REAL 2);

        then DD c= ( dom proj2 ) by FUNCT_2:def 1;

        then

         A153: (( dom proj2 ) /\ DD) = DD by XBOOLE_1: 28;

        ( LSeg ((( Gauge (C,(k0 + 1))) * (( Center ( Gauge (C,(k0 + 1)))),1)),(( Gauge (C,(k0 + 1))) * (( Center ( Gauge (C,(k0 + 1)))),( len ( Gauge (C,(k0 + 1)))))))) meets ( Upper_Arc ( L~ ( Cage (C,(k0 + 1))))) by JORDAN1B: 31;

        then ( LSeg (f,e)) meets ( Upper_Arc ( L~ ( Cage (C,(k0 + 1))))) by A2, A140, JORDAN1A: 44, XBOOLE_1: 63;

        then DD <> {} ;

        then ( dom proj2 ) meets DD by A153;

        then

         A154: D <> {} by RELAT_1: 118;

        

         A155: (F . k0) = |[s, (Fs . k0)]| by A32, A144;

        then

         A156: ((F . k0) `1 ) = s by EUCLID: 52;

        

         A157: ((F . k0) `2 ) = (Fs . k0) by A155, EUCLID: 52

        .= (dd `2 ) by A151, PSCOMP_1:def 6;

        (E . k0) in ( Vertical_Line s) by A148, JORDAN1A: 8;

        then ( LSeg ((E . k0),f)) c= ( Vertical_Line s) by A6, JORDAN1A: 13;

        then (dd `1 ) = ((F . k0) `1 ) by A156, A152, JORDAN6: 31;

        then

         A158: (F . k0) in ( LSeg ((E . k0),f)) by A152, A157, TOPREAL3: 6;

        (Es . k0) = F(k0) by A10, A144;

        then

        consider dd be Point of ( TOP-REAL 2) such that

         A159: dd in DD and

         A160: (Es . k0) = ( proj2 . dd) by A154, FUNCT_2: 65, RCOMP_1: 14;

        

         A161: dd in ( LSeg (f,e)) by A159, XBOOLE_0:def 4;

        

         A162: ((E . k0) `2 ) = (Es . k0) by A147, EUCLID: 52

        .= (dd `2 ) by A160, PSCOMP_1:def 6;

        then

         A163: (f `2 ) <= ((E . k0) `2 ) by A7, A161, TOPREAL1: 4;

        then

         A164: ((F . k0) `2 ) <= ((E . k0) `2 ) by A152, A157, TOPREAL1: 4;

        r in ( proj2 .: ( LSeg ((E . k0),(F . k0)))) by A33, A133, A144;

        then r in [.( proj2 . (F . k0)), ( proj2 . (E . k0)).] by A143, A134, A164, SPRECT_1: 53;

        then

         A165: p in ( LSeg ((E . k0),(F . k0))) by A148, A156, JORDAN1A: 11;

        

         A166: (F . k0) in ( Lower_Arc ( L~ ( Cage (C,(k0 + 1))))) by A46;

        

         A167: f in ( LSeg (f,e)) by RLTOPSP1: 68;

        

         A168: (E . k0) in ( LSeg (f,(E . k0))) by RLTOPSP1: 68;

        then

         A169: ( LSeg ((E . k0),(F . k0))) c= ( LSeg (f,(E . k0))) by A158, TOPREAL1: 6;

        for x be object holds x in (( LSeg ((E . k0),(F . k0))) /\ ( Lower_Arc ( L~ ( Cage (C,(k0 + 1)))))) iff x = (F . k0)

        proof

          let x be object;

          thus x in (( LSeg ((E . k0),(F . k0))) /\ ( Lower_Arc ( L~ ( Cage (C,(k0 + 1)))))) implies x = (F . k0)

          proof

            (F . k0) = |[s, (Fs . k0)]| by A32, A144;

            

            then

             A170: ((F . k0) `2 ) = (Fs . k0) by EUCLID: 52

            .= H(k0) by A31, A144;

            assume

             A171: x in (( LSeg ((E . k0),(F . k0))) /\ ( Lower_Arc ( L~ ( Cage (C,(k0 + 1))))));

            then

            reconsider p = x as Point of ( TOP-REAL 2);

            

             A172: p in ( LSeg ((E . k0),(F . k0))) by A171, XBOOLE_0:def 4;

            then

             A173: (p `2 ) >= ((F . k0) `2 ) by A164, TOPREAL1: 4;

            p in ( Lower_Arc ( L~ ( Cage (C,(k0 + 1))))) by A171, XBOOLE_0:def 4;

            then p in EE by A169, A172, XBOOLE_0:def 4;

            then ( proj2 . p) in E0 by FUNCT_2: 35;

            then

             A174: (p `2 ) in E0 by PSCOMP_1:def 6;

            E0 is real-bounded by RCOMP_1: 10;

            then ((F . k0) `2 ) >= (p `2 ) by A170, A174, SEQ_4:def 1;

            then

             A175: (p `2 ) = ((F . k0) `2 ) by A173, XXREAL_0: 1;

            (p `1 ) = ((F . k0) `1 ) by A148, A156, A172, GOBOARD7: 5;

            hence thesis by A175, TOPREAL3: 6;

          end;

          assume

           A176: x = (F . k0);

          then x in ( LSeg ((E . k0),(F . k0))) by RLTOPSP1: 68;

          hence thesis by A166, A176, XBOOLE_0:def 4;

        end;

        then

         A177: (( LSeg ((E . k0),(F . k0))) /\ ( Lower_Arc ( L~ ( Cage (C,(k0 + 1)))))) = {(F . k0)} by TARSKI:def 1;

        

         A178: for p be Real st p in W holds p <= ((E . k0) `2 )

        proof

          let p be Real;

          assume p in W;

          then

          consider x be object such that x in ( dom proj2 ) and

           A179: x in CC and

           A180: p = ( proj2 . x) by FUNCT_1:def 6;

          reconsider x as Point of ( TOP-REAL 2) by A179;

          x in ( LSeg (f,(E . k0))) by A179, XBOOLE_0:def 4;

          then (x `2 ) <= ((E . k0) `2 ) by A163, TOPREAL1: 4;

          hence thesis by A180, PSCOMP_1:def 6;

        end;

        CC <> {} by A149;

        then ( dom proj2 ) meets CC by A136;

        then W <> {} by RELAT_1: 118;

        then

         A181: ( upper_bound W) <= ((E . k0) `2 ) by A178, SEQ_4: 45;

        (dd `1 ) = ((E . k0) `1 ) by A13, A148, A161, JORDAN6: 31;

        then (E . k0) in ( LSeg (f,e)) by A161, A162, TOPREAL3: 6;

        then ( LSeg (f,(E . k0))) c= ( LSeg (e,f)) by A167, TOPREAL1: 6;

        then

         A182: ( LSeg ((E . k0),(F . k0))) c= ( LSeg (e,f)) by A158, A168, TOPREAL1: 6;

        for x be object holds x in (( LSeg ((E . k0),(F . k0))) /\ ( Upper_Arc ( L~ ( Cage (C,(k0 + 1)))))) iff x = (E . k0)

        proof

          let x be object;

          thus x in (( LSeg ((E . k0),(F . k0))) /\ ( Upper_Arc ( L~ ( Cage (C,(k0 + 1)))))) implies x = (E . k0)

          proof

            (E . k0) = |[s, (Es . k0)]| by A11, A144;

            

            then

             A183: ((E . k0) `2 ) = (Es . k0) by EUCLID: 52

            .= F(k0) by A10, A144;

            assume

             A184: x in (( LSeg ((E . k0),(F . k0))) /\ ( Upper_Arc ( L~ ( Cage (C,(k0 + 1))))));

            then

            reconsider p = x as Point of ( TOP-REAL 2);

            

             A185: p in ( LSeg ((E . k0),(F . k0))) by A184, XBOOLE_0:def 4;

            then

             A186: (p `2 ) <= ((E . k0) `2 ) by A164, TOPREAL1: 4;

            p in ( Upper_Arc ( L~ ( Cage (C,(k0 + 1))))) by A184, XBOOLE_0:def 4;

            then p in DD by A182, A185, XBOOLE_0:def 4;

            then ( proj2 . p) in D by FUNCT_2: 35;

            then

             A187: (p `2 ) in D by PSCOMP_1:def 6;

            D is real-bounded by RCOMP_1: 10;

            then ((E . k0) `2 ) <= (p `2 ) by A183, A187, SEQ_4:def 2;

            then

             A188: (p `2 ) = ((E . k0) `2 ) by A186, XXREAL_0: 1;

            (p `1 ) = ((E . k0) `1 ) by A148, A156, A185, GOBOARD7: 5;

            hence thesis by A188, TOPREAL3: 6;

          end;

          assume

           A189: x = (E . k0);

          then x in ( LSeg ((E . k0),(F . k0))) by RLTOPSP1: 68;

          hence thesis by A139, A189, XBOOLE_0:def 4;

        end;

        then

         A190: (( LSeg ((E . k0),(F . k0))) /\ ( Upper_Arc ( L~ ( Cage (C,(k0 + 1)))))) = {(E . k0)} by TARSKI:def 1;

        ((E . k0) `2 ) = (Es . k0) by A147, EUCLID: 52

        .= F(k0) by A10, A144

        .= ( lower_bound ( proj2 .: (( LSeg (f,e)) /\ ( Upper_Arc ( L~ ( Cage (C,(k0 + 1))))))));

        then

        consider j such that

         A191: 1 <= j and

         A192: j <= ( width ( Gauge (C,(k0 + 1)))) and

         A193: (E . k0) = (( Gauge (C,(k0 + 1))) * (( X-SpanStart (C,(k0 + 1))),j)) by A2, A1, A148, A142, JORDAN1F: 13;

        

         A194: ((F . k0) `2 ) = (Fs . k0) by A155, EUCLID: 52

        .= H(k0) by A31, A144

        .= ( upper_bound ( proj2 .: (( LSeg (f,(E . k0))) /\ ( Lower_Arc ( L~ ( Cage (C,(k0 + 1))))))));

        then

        consider k such that

         A195: 1 <= k and

         A196: k <= ( width ( Gauge (C,(k0 + 1)))) and

         A197: (F . k0) = (( Gauge (C,(k0 + 1))) * (( X-SpanStart (C,(k0 + 1))),k)) by A2, A156, A142, A191, A192, A193, A139, JORDAN1I: 28;

        1 <= ( Center ( Gauge (C,(k0 + 1)))) by JORDAN1B: 11;

        then k <= j by A142, A191, A193, A194, A196, A197, A135, A181, GOBOARD5: 4;

        then ( LSeg ((E . k0),(F . k0))) c= ( Cl ( RightComp ( Cage (C,(k0 + 1))))) by A142, A191, A192, A193, A195, A196, A197, A190, A177, Lm1;

        then p in ( Cl ( RightComp ( Cage (C,(k0 + 1))))) by A165;

        then p in ( Cl ( RightComp ( Cage (C,k1)))) by A138;

        hence thesis by A131, GOBRD14: 37;

      end;

      then

       A198: p in ( meet ( BDD-Family C)) by SETFAM_1:def 1;

      

       A199: p in ( LSeg (e,f)) by A5, A12, A126, JORDAN1A: 11;

       A200:

      now

        assume p in C;

        then p in (( Lower_Arc C) \/ ( Upper_Arc C)) by JORDAN6: 50;

        then p in ((( Lower_Arc C) \/ ( Upper_Arc C)) /\ ( LSeg (e,f))) by A199, XBOOLE_0:def 4;

        then p in (AA \/ BB) by XBOOLE_1: 23;

        then ( proj2 . p) in ( proj2 .: (AA \/ BB)) by FUNCT_2: 35;

        then r in ( proj2 .: (AA \/ BB)) by PSCOMP_1: 65;

        hence contradiction by A127, RELAT_1: 120;

      end;

      ( meet ( BDD-Family C)) = (C \/ ( BDD C)) by JORDAN10: 21;

      then p in ( BDD C) by A200, A198, XBOOLE_0:def 3;

      then

      consider n, i, j such that

       A201: 1 < i and

       A202: i < ( len ( Gauge (C,n))) and

       A203: 1 < j and

       A204: j < ( width ( Gauge (C,n))) and

       A205: (p `1 ) <> ((( Gauge (C,n)) * (i,j)) `1 ) and

       A206: p in ( cell (( Gauge (C,n)),i,j)) and

       A207: ( cell (( Gauge (C,n)),i,j)) c= ( BDD C) by JORDAN1C: 23;

      take n, j;

      thus j < ( width ( Gauge (C,n))) by A204;

      

       A208: ( X-SpanStart (C,n)) = ( Center ( Gauge (C,n))) by JORDAN1B: 16;

      

       A209: ( len ( Gauge (C,n))) = ( width ( Gauge (C,n))) by JORDAN8:def 1;

      

       A210: ( X-SpanStart (C,n)) <= ( len ( Gauge (C,n))) by JORDAN1H: 49;

      

       A211: 1 <= ( X-SpanStart (C,n)) by JORDAN1H: 49, XXREAL_0: 2;

      n > 0 by A202, A204, A207, JORDAN1B: 41;

      then ((( Gauge (C,n)) * (( X-SpanStart (C,n)),j)) `1 ) = s by A2, A5, A203, A204, A208, A9, A209, JORDAN1A: 36;

      hence thesis by A129, A201, A202, A203, A204, A205, A206, A207, A211, A210, JORDAN1B: 22;

    end;

    definition

      let C;

      :: JORDAN11:def1

      func ApproxIndex C -> Element of NAT means

      : Def1: it is_sufficiently_large_for C & for j st j is_sufficiently_large_for C holds j >= it ;

      existence

      proof

        defpred P[ Nat] means $1 is_sufficiently_large_for C;

        set X = { i where i be Element of NAT : P[i] };

        

         A1: X is Subset of NAT from DOMAIN_1:sch 7;

        consider i such that

         A2: i is_sufficiently_large_for C by Lm2;

        

         A3: i in NAT by ORDINAL1:def 12;

        i in X by A2, A3;

        then

        reconsider X as non empty Subset of NAT by A1;

        take ( min X);

        ( min X) in X by XXREAL_2:def 7;

        then ex i be Element of NAT st i = ( min X) & i is_sufficiently_large_for C;

        hence ( min X) is_sufficiently_large_for C;

        let j;

        

         A4: j in NAT by ORDINAL1:def 12;

        assume j is_sufficiently_large_for C;

        then j in X by A4;

        hence thesis by XXREAL_2:def 7;

      end;

      uniqueness

      proof

        let it1,it2 be Element of NAT such that

         A5: it1 is_sufficiently_large_for C and

         A6: for j st j is_sufficiently_large_for C holds j >= it1 and

         A7: it2 is_sufficiently_large_for C and

         A8: for j st j is_sufficiently_large_for C holds j >= it2;

        

         A9: it2 <= it1 by A5, A8;

        it1 <= it2 by A6, A7;

        hence thesis by A9, XXREAL_0: 1;

      end;

    end

    theorem :: JORDAN11:1

    

     Th1: ( ApproxIndex C) >= 1

    proof

      ( ApproxIndex C) is_sufficiently_large_for C by Def1;

      hence thesis by JORDAN1H: 51;

    end;

    definition

      let C;

      :: JORDAN11:def2

      func Y-InitStart C -> Element of NAT means

      : Def2: it < ( width ( Gauge (C,( ApproxIndex C)))) & ( cell (( Gauge (C,( ApproxIndex C))),(( X-SpanStart (C,( ApproxIndex C))) -' 1),it )) c= ( BDD C) & for j st j < ( width ( Gauge (C,( ApproxIndex C)))) & ( cell (( Gauge (C,( ApproxIndex C))),(( X-SpanStart (C,( ApproxIndex C))) -' 1),j)) c= ( BDD C) holds j >= it ;

      existence

      proof

        set n = ( ApproxIndex C);

        defpred P[ Nat] means $1 < ( width ( Gauge (C,n))) & ( cell (( Gauge (C,n)),(( X-SpanStart (C,n)) -' 1),$1)) c= ( BDD C);

        set X = { i where i be Element of NAT : P[i] };

        

         A1: X is Subset of NAT from DOMAIN_1:sch 7;

        n is_sufficiently_large_for C by Def1;

        then

        consider j such that

         A2: P[j];

        

         A3: j in NAT by ORDINAL1:def 12;

        j in X by A2, A3;

        then

        reconsider X as non empty Subset of NAT by A1;

        take ( min X);

        ( min X) in X by XXREAL_2:def 7;

        then ex i be Element of NAT st i = ( min X) & P[i];

        hence P[( min X)];

        let i;

        

         A4: i in NAT by ORDINAL1:def 12;

        assume P[i];

        then i in X by A4;

        hence thesis by XXREAL_2:def 7;

      end;

      uniqueness

      proof

        let it1,it2 be Element of NAT ;

        assume that

         A5: it1 < ( width ( Gauge (C,( ApproxIndex C)))) and

         A6: ( cell (( Gauge (C,( ApproxIndex C))),(( X-SpanStart (C,( ApproxIndex C))) -' 1),it1)) c= ( BDD C) and

         A7: for j st j < ( width ( Gauge (C,( ApproxIndex C)))) & ( cell (( Gauge (C,( ApproxIndex C))),(( X-SpanStart (C,( ApproxIndex C))) -' 1),j)) c= ( BDD C) holds j >= it1 and

         A8: it2 < ( width ( Gauge (C,( ApproxIndex C)))) and

         A9: ( cell (( Gauge (C,( ApproxIndex C))),(( X-SpanStart (C,( ApproxIndex C))) -' 1),it2)) c= ( BDD C) and

         A10: for j st j < ( width ( Gauge (C,( ApproxIndex C)))) & ( cell (( Gauge (C,( ApproxIndex C))),(( X-SpanStart (C,( ApproxIndex C))) -' 1),j)) c= ( BDD C) holds j >= it2;

        

         A11: it2 <= it1 by A5, A6, A10;

        it1 <= it2 by A7, A8, A9;

        hence thesis by A11, XXREAL_0: 1;

      end;

    end

    theorem :: JORDAN11:2

    

     Th2: ( Y-InitStart C) > 1

    proof

      set m = ( ApproxIndex C);

      

       A1: (( X-SpanStart (C,m)) -' 1) <= ( len ( Gauge (C,m))) by JORDAN1H: 50;

      assume

       A2: ( Y-InitStart C) <= 1;

      per cases by A2, NAT_1: 25;

        suppose

         A3: ( Y-InitStart C) = 0 ;

        

         A4: ( cell (( Gauge (C,m)),(( X-SpanStart (C,m)) -' 1), 0 )) c= ( UBD C) by A1, JORDAN1A: 49;

         0 <= ( width ( Gauge (C,m)));

        then

         A5: ( cell (( Gauge (C,m)),(( X-SpanStart (C,m)) -' 1), 0 )) is non empty by A1, JORDAN1A: 24;

        ( cell (( Gauge (C,m)),(( X-SpanStart (C,m)) -' 1), 0 )) c= ( BDD C) by A3, Def2;

        hence contradiction by A5, A4, JORDAN2C: 24, XBOOLE_1: 68;

      end;

        suppose ( Y-InitStart C) = 1;

        then

         A6: ( cell (( Gauge (C,m)),(( X-SpanStart (C,m)) -' 1),1)) c= ( BDD C) by Def2;

        set i1 = ( X-SpanStart (C,m));

        

         A7: (i1 -' 1) <= i1 by NAT_D: 44;

        i1 < ( len ( Gauge (C,m))) by JORDAN1H: 49;

        then

         A8: (i1 -' 1) < ( len ( Gauge (C,m))) by A7, XXREAL_0: 2;

        ( BDD C) c= (C ` ) by JORDAN2C: 25;

        then

         A9: ( cell (( Gauge (C,m)),(( X-SpanStart (C,m)) -' 1),1)) c= (C ` ) by A6;

        ( UBD C) is_outside_component_of C by JORDAN2C: 68;

        then

         A10: ( UBD C) is_a_component_of (C ` ) by JORDAN2C:def 3;

        

         A11: ( width ( Gauge (C,m))) <> 0 by MATRIX_0:def 10;

        then

         A12: ( 0 + 1) <= ( width ( Gauge (C,m))) by NAT_1: 14;

        then

         A13: ( cell (( Gauge (C,m)),(( X-SpanStart (C,m)) -' 1),1)) is non empty by A1, JORDAN1A: 24;

        1 <= (i1 -' 1) by JORDAN1H: 50;

        then (( cell (( Gauge (C,m)),(i1 -' 1), 0 )) /\ ( cell (( Gauge (C,m)),(i1 -' 1),( 0 + 1)))) = ( LSeg ((( Gauge (C,m)) * ((i1 -' 1),( 0 + 1))),(( Gauge (C,m)) * (((i1 -' 1) + 1),( 0 + 1))))) by A11, A8, GOBOARD5: 26;

        then

         A14: ( cell (( Gauge (C,m)),(i1 -' 1), 0 )) meets ( cell (( Gauge (C,m)),(i1 -' 1),( 0 + 1)));

        ( cell (( Gauge (C,m)),(( X-SpanStart (C,m)) -' 1), 0 )) c= ( UBD C) by A1, JORDAN1A: 49;

        then ( cell (( Gauge (C,m)),(( X-SpanStart (C,m)) -' 1),1)) c= ( UBD C) by A12, A8, A14, A10, A9, GOBOARD9: 4, JORDAN1A: 25;

        hence contradiction by A6, A13, JORDAN2C: 24, XBOOLE_1: 68;

      end;

    end;

    theorem :: JORDAN11:3

    

     Th3: (( Y-InitStart C) + 1) < ( width ( Gauge (C,( ApproxIndex C))))

    proof

      set m = ( ApproxIndex C);

      

       A1: (( X-SpanStart (C,m)) -' 1) <= ( len ( Gauge (C,m))) by JORDAN1H: 50;

      assume (( Y-InitStart C) + 1) >= ( width ( Gauge (C,m)));

      then

       A2: (( Y-InitStart C) + 1) > ( width ( Gauge (C,m))) or (( Y-InitStart C) + 1) = ( width ( Gauge (C,m))) by XXREAL_0: 1;

      

       A3: ( Y-InitStart C) < ( width ( Gauge (C,m))) or ( Y-InitStart C) = ( width ( Gauge (C,m))) by Def2;

      per cases by A2, A3, NAT_1: 13;

        suppose ( Y-InitStart C) = ( width ( Gauge (C,m)));

        hence contradiction by Def2;

      end;

        suppose (( Y-InitStart C) + 1) = ( width ( Gauge (C,m)));

        then ( Y-InitStart C) = (( width ( Gauge (C,m))) -' 1) by NAT_D: 34;

        then

         A4: ( cell (( Gauge (C,m)),(( X-SpanStart (C,m)) -' 1),(( width ( Gauge (C,m))) -' 1))) c= ( BDD C) by Def2;

        ( BDD C) c= (C ` ) by JORDAN2C: 25;

        then

         A5: ( cell (( Gauge (C,m)),(( X-SpanStart (C,m)) -' 1),(( width ( Gauge (C,m))) -' 1))) c= (C ` ) by A4;

        

         A6: ( cell (( Gauge (C,m)),(( X-SpanStart (C,m)) -' 1),( width ( Gauge (C,m))))) c= ( UBD C) by A1, JORDAN1A: 50;

        set i1 = ( X-SpanStart (C,m));

        

         A7: (i1 -' 1) <= i1 by NAT_D: 44;

        i1 < ( len ( Gauge (C,m))) by JORDAN1H: 49;

        then

         A8: (i1 -' 1) < ( len ( Gauge (C,m))) by A7, XXREAL_0: 2;

        ( UBD C) is_outside_component_of C by JORDAN2C: 68;

        then

         A9: ( UBD C) is_a_component_of (C ` ) by JORDAN2C:def 3;

        (( width ( Gauge (C,m))) -' 1) <= ( width ( Gauge (C,m))) by NAT_D: 44;

        then

         A10: ( cell (( Gauge (C,m)),(( X-SpanStart (C,m)) -' 1),(( width ( Gauge (C,m))) -' 1))) is non empty by A1, JORDAN1A: 24;

        

         A11: (( width ( Gauge (C,m))) - 1) < ( width ( Gauge (C,m))) by XREAL_1: 146;

        

         A12: 1 <= (i1 -' 1) by JORDAN1H: 50;

        

         A13: ( width ( Gauge (C,m))) <> 0 by MATRIX_0:def 10;

        then ((( width ( Gauge (C,m))) -' 1) + 1) = ( width ( Gauge (C,m))) by NAT_1: 14, XREAL_1: 235;

        then (( cell (( Gauge (C,m)),(i1 -' 1),( width ( Gauge (C,m))))) /\ ( cell (( Gauge (C,m)),(i1 -' 1),(( width ( Gauge (C,m))) -' 1)))) = ( LSeg ((( Gauge (C,m)) * ((i1 -' 1),( width ( Gauge (C,m))))),(( Gauge (C,m)) * (((i1 -' 1) + 1),( width ( Gauge (C,m))))))) by A8, A11, A12, GOBOARD5: 26;

        then

         A14: ( cell (( Gauge (C,m)),(i1 -' 1),( width ( Gauge (C,m))))) meets ( cell (( Gauge (C,m)),(i1 -' 1),(( width ( Gauge (C,m))) -' 1)));

        (( width ( Gauge (C,m))) -' 1) < ( width ( Gauge (C,m))) by A13, A11, NAT_1: 14, XREAL_1: 233;

        then ( cell (( Gauge (C,m)),(( X-SpanStart (C,m)) -' 1),(( width ( Gauge (C,m))) -' 1))) c= ( UBD C) by A6, A8, A14, A9, A5, GOBOARD9: 4, JORDAN1A: 25;

        hence contradiction by A4, A10, JORDAN2C: 24, XBOOLE_1: 68;

      end;

    end;

    definition

      let C, n;

      assume n is_sufficiently_large_for C;

      then

       A1: n >= ( ApproxIndex C) by Def1;

      set i1 = ( X-SpanStart (C,n));

      :: JORDAN11:def3

      func Y-SpanStart (C,n) -> Element of NAT means

      : Def3: it <= ( width ( Gauge (C,n))) & (for k st it <= k & k <= (((2 |^ (n -' ( ApproxIndex C))) * (( Y-InitStart C) -' 2)) + 2) holds ( cell (( Gauge (C,n)),(( X-SpanStart (C,n)) -' 1),k)) c= ( BDD C)) & for j st j <= ( width ( Gauge (C,n))) & for k st j <= k & k <= (((2 |^ (n -' ( ApproxIndex C))) * (( Y-InitStart C) -' 2)) + 2) holds ( cell (( Gauge (C,n)),(( X-SpanStart (C,n)) -' 1),k)) c= ( BDD C) holds j >= it ;

      existence

      proof

        set m = ( ApproxIndex C);

        defpred P[ Nat] means $1 <= ( width ( Gauge (C,n))) & for k st $1 <= k & k <= (((2 |^ (n -' m)) * (( Y-InitStart C) -' 2)) + 2) holds ( cell (( Gauge (C,n)),(i1 -' 1),k)) c= ( BDD C);

        set X = { i where i be Element of NAT : P[i] };

        set j0 = (((2 |^ (n -' m)) * (( Y-InitStart C) -' 2)) + 2);

        

         A2: X is Subset of NAT from DOMAIN_1:sch 7;

        

         A3: (( Y-InitStart C) + 1) < ( width ( Gauge (C,m))) by Th3;

        then (( Y-InitStart C) + 1) < ((2 |^ m) + (2 + 1)) by JORDAN1A: 28;

        then (( Y-InitStart C) + 1) < (((2 |^ m) + 2) + 1);

        then

         A4: ( Y-InitStart C) < ((2 |^ m) + 2) by XREAL_1: 6;

        

         A5: 1 < ( Y-InitStart C) by Th2;

        then (1 + 1) <= ( Y-InitStart C) by NAT_1: 13;

        then (( Y-InitStart C) -' 2) < (2 |^ m) by A4, NAT_D: 54;

        then ((2 |^ (n -' m)) * (( Y-InitStart C) -' 2)) <= ((2 |^ (n -' m)) * (2 |^ m)) by XREAL_1: 64;

        then ((2 |^ (n -' m)) * (( Y-InitStart C) -' 2)) <= (2 |^ ((n -' m) + m)) by NEWTON: 8;

        then

         A6: ((2 |^ (n -' m)) * (( Y-InitStart C) -' 2)) <= (2 |^ n) by A1, XREAL_1: 235;

         A7:

        now

          (2 |^ (m -' 1)) <= (2 |^ m) by NAT_D: 35, PREPOWER: 93;

          then

           A8: ((2 |^ (m -' 1)) + 2) <= ((2 |^ m) + 2) by XREAL_1: 6;

          ( len ( Gauge (C,m))) = ((2 |^ m) + (2 + 1)) by JORDAN8:def 1

          .= (((2 |^ m) + 2) + 1);

          then

           A9: ( X-SpanStart (C,m)) < ( len ( Gauge (C,m))) by A8, NAT_1: 13;

          

           A10: ( Y-InitStart C) >= (1 + 1) by A5, NAT_1: 13;

          let j;

          assume that

           A11: j0 <= j and

           A12: j <= (((2 |^ (n -' m)) * (( Y-InitStart C) -' 2)) + 2);

          

           A13: m >= 1 by Th1;

          1 <= (2 |^ (m -' 1)) by PREPOWER: 11;

          then

           A14: (2 + 1) <= ( X-SpanStart (C,m)) by XREAL_1: 6;

          

           A15: ( cell (( Gauge (C,m)),(( X-SpanStart (C,m)) -' 1),( Y-InitStart C))) c= ( BDD C) by Def2;

          j = j0 by A11, A12, XXREAL_0: 1;

          then

           A16: j = (((2 |^ (n -' m)) * (( Y-InitStart C) - 2)) + 2) by A10, XREAL_1: 233;

          ((n -' m) + (m -' 1)) = ((n -' m) + (m - 1)) by Th1, XREAL_1: 233

          .= (((n -' m) + m) - 1)

          .= (n - 1) by A1, XREAL_1: 235

          .= (n -' 1) by A1, A13, XREAL_1: 233, XXREAL_0: 2;

          then i1 = (((2 |^ (n -' m)) * (( X-SpanStart (C,m)) - 2)) + 2) by NEWTON: 8;

          then ( cell (( Gauge (C,n)),(i1 -' 1),j)) c= ( cell (( Gauge (C,m)),(( X-SpanStart (C,m)) -' 1),( Y-InitStart C))) by A1, A3, A14, A9, A16, Th2, JORDAN1A: 48;

          hence ( cell (( Gauge (C,n)),(i1 -' 1),j)) c= ( BDD C) by A15;

        end;

        (2 |^ n) <= ((2 |^ n) + 1) by NAT_1: 11;

        then ((2 |^ (n -' m)) * (( Y-InitStart C) -' 2)) <= ((2 |^ n) + 1) by A6, XXREAL_0: 2;

        then j0 <= (((2 |^ n) + 1) + 2) by XREAL_1: 6;

        then j0 <= ((2 |^ n) + (1 + 2));

        then j0 <= ( len ( Gauge (C,n))) by JORDAN8:def 1;

        then j0 <= ( width ( Gauge (C,n))) by JORDAN8:def 1;

        then j0 in X by A7;

        then

        reconsider X as non empty Subset of NAT by A2;

        take ( min X);

        ( min X) in X by XXREAL_2:def 7;

        then ex j be Element of NAT st j = ( min X) & P[j];

        hence P[( min X)];

        let j;

        

         A17: j in NAT by ORDINAL1:def 12;

        assume P[j];

        then j in X by A17;

        hence thesis by XXREAL_2:def 7;

      end;

      uniqueness

      proof

        let it1,it2 be Element of NAT ;

        defpred definiens[ Element of NAT ] means $1 <= ( width ( Gauge (C,n))) & (for i st $1 <= i & i <= (((2 |^ (n -' ( ApproxIndex C))) * (( Y-InitStart C) -' 2)) + 2) holds ( cell (( Gauge (C,n)),(( X-SpanStart (C,n)) -' 1),i)) c= ( BDD C)) & for j st j <= ( width ( Gauge (C,n))) & for i st j <= i & i <= (((2 |^ (n -' ( ApproxIndex C))) * (( Y-InitStart C) -' 2)) + 2) holds ( cell (( Gauge (C,n)),(( X-SpanStart (C,n)) -' 1),i)) c= ( BDD C) holds j >= $1;

        assume that

         A18: definiens[it1] and

         A19: definiens[it2];

        

         A20: it2 <= it1 by A18, A19;

        it1 <= it2 by A18, A19;

        hence thesis by A20, XXREAL_0: 1;

      end;

    end

    theorem :: JORDAN11:4

    

     Th4: n is_sufficiently_large_for C implies ( X-SpanStart (C,n)) = (((2 |^ (n -' ( ApproxIndex C))) * (( X-SpanStart (C,( ApproxIndex C))) - 2)) + 2)

    proof

      set m = ( ApproxIndex C);

      

       A1: m >= 1 by Th1;

      assume n is_sufficiently_large_for C;

      then

       A2: n >= ( ApproxIndex C) by Def1;

      ((n -' m) + (m -' 1)) = ((n -' m) + (m - 1)) by Th1, XREAL_1: 233

      .= (((n -' m) + m) - 1)

      .= (n - 1) by A2, XREAL_1: 235

      .= (n -' 1) by A2, A1, XREAL_1: 233, XXREAL_0: 2;

      hence thesis by NEWTON: 8;

    end;

    theorem :: JORDAN11:5

    

     Th5: n is_sufficiently_large_for C implies ( Y-SpanStart (C,n)) <= (((2 |^ (n -' ( ApproxIndex C))) * (( Y-InitStart C) -' 2)) + 2)

    proof

      set m = ( ApproxIndex C);

      

       A1: ( X-SpanStart (C,m)) > 2 by JORDAN1H: 49;

      set j0 = (((2 |^ (n -' m)) * (( Y-InitStart C) -' 2)) + 2);

      set i1 = ( X-SpanStart (C,n));

      assume

       A2: n is_sufficiently_large_for C;

      then

       A3: n >= ( ApproxIndex C) by Def1;

      

       A4: 1 < ( Y-InitStart C) by Th2;

      then (1 + 1) <= ( Y-InitStart C) by NAT_1: 13;

      then

       A5: (( Y-InitStart C) -' 2) = (( Y-InitStart C) - 2) by XREAL_1: 233;

      

       A6: (( Y-InitStart C) + 1) < ( width ( Gauge (C,m))) by Th3;

       A7:

      now

        (m -' 1) <= m by NAT_D: 44;

        then

         A8: (2 |^ (m -' 1)) <= (2 |^ m) by PREPOWER: 93;

        ( len ( Gauge (C,m))) = ((2 |^ m) + 3) by JORDAN8:def 1;

        then

         A9: ( X-SpanStart (C,m)) < ( len ( Gauge (C,m))) by A8, XREAL_1: 8;

        

         A10: (2 + 1) <= ( X-SpanStart (C,m)) by A1, NAT_1: 13;

        

         A11: i1 = (((2 |^ (n -' m)) * (( X-SpanStart (C,m)) - 2)) + 2) by A2, Th4;

        let j;

        assume that

         A12: j0 <= j and

         A13: j <= (((2 |^ (n -' m)) * (( Y-InitStart C) -' 2)) + 2);

        

         A14: ( cell (( Gauge (C,m)),(( X-SpanStart (C,m)) -' 1),( Y-InitStart C))) c= ( BDD C) by Def2;

        j = j0 by A12, A13, XXREAL_0: 1;

        then ( cell (( Gauge (C,n)),(i1 -' 1),j)) c= ( cell (( Gauge (C,m)),(( X-SpanStart (C,m)) -' 1),( Y-InitStart C))) by A3, A6, A5, A10, A9, A11, Th2, JORDAN1A: 48;

        hence ( cell (( Gauge (C,n)),(i1 -' 1),j)) c= ( BDD C) by A14;

      end;

      ( Y-InitStart C) < (( Y-InitStart C) + 1) by XREAL_1: 29;

      then ( Y-InitStart C) < ( width ( Gauge (C,m))) by Th3, XXREAL_0: 2;

      then j0 <= ( width ( Gauge (C,n))) by A3, A4, A5, JORDAN1A: 32;

      hence thesis by A2, A7, Def3;

    end;

    theorem :: JORDAN11:6

    

     Th6: n is_sufficiently_large_for C implies ( cell (( Gauge (C,n)),(( X-SpanStart (C,n)) -' 1),( Y-SpanStart (C,n)))) c= ( BDD C)

    proof

      assume

       A1: n is_sufficiently_large_for C;

      then ( Y-SpanStart (C,n)) <= (((2 |^ (n -' ( ApproxIndex C))) * (( Y-InitStart C) -' 2)) + 2) by Th5;

      hence thesis by A1, Def3;

    end;

    theorem :: JORDAN11:7

    

     Th7: n is_sufficiently_large_for C implies 1 < ( Y-SpanStart (C,n)) & ( Y-SpanStart (C,n)) <= ( width ( Gauge (C,n)))

    proof

      assume

       A1: n is_sufficiently_large_for C;

      thus 1 < ( Y-SpanStart (C,n))

      proof

        

         A2: (( X-SpanStart (C,n)) -' 1) <= ( len ( Gauge (C,n))) by JORDAN1H: 50;

        assume

         A3: ( Y-SpanStart (C,n)) <= 1;

        per cases by A3, NAT_1: 25;

          suppose

           A4: ( Y-SpanStart (C,n)) = 0 ;

          

           A5: ( cell (( Gauge (C,n)),(( X-SpanStart (C,n)) -' 1), 0 )) c= ( UBD C) by A2, JORDAN1A: 49;

           0 <= ( width ( Gauge (C,n)));

          then

           A6: ( cell (( Gauge (C,n)),(( X-SpanStart (C,n)) -' 1), 0 )) is non empty by A2, JORDAN1A: 24;

          ( cell (( Gauge (C,n)),(( X-SpanStart (C,n)) -' 1), 0 )) c= ( BDD C) by A1, A4, Th6;

          hence contradiction by A6, A5, JORDAN2C: 24, XBOOLE_1: 68;

        end;

          suppose ( Y-SpanStart (C,n)) = 1;

          then

           A7: ( cell (( Gauge (C,n)),(( X-SpanStart (C,n)) -' 1),1)) c= ( BDD C) by A1, Th6;

          set i1 = ( X-SpanStart (C,n));

          

           A8: (i1 -' 1) <= i1 by NAT_D: 44;

          i1 < ( len ( Gauge (C,n))) by JORDAN1H: 49;

          then

           A9: (i1 -' 1) < ( len ( Gauge (C,n))) by A8, XXREAL_0: 2;

          ( BDD C) c= (C ` ) by JORDAN2C: 25;

          then

           A10: ( cell (( Gauge (C,n)),(( X-SpanStart (C,n)) -' 1),1)) c= (C ` ) by A7;

          ( UBD C) is_outside_component_of C by JORDAN2C: 68;

          then

           A11: ( UBD C) is_a_component_of (C ` ) by JORDAN2C:def 3;

          

           A12: ( width ( Gauge (C,n))) <> 0 by MATRIX_0:def 10;

          then

           A13: ( 0 + 1) <= ( width ( Gauge (C,n))) by NAT_1: 14;

          then

           A14: ( cell (( Gauge (C,n)),(( X-SpanStart (C,n)) -' 1),1)) is non empty by A2, JORDAN1A: 24;

          1 <= (i1 -' 1) by JORDAN1H: 50;

          then (( cell (( Gauge (C,n)),(i1 -' 1), 0 )) /\ ( cell (( Gauge (C,n)),(i1 -' 1),( 0 + 1)))) = ( LSeg ((( Gauge (C,n)) * ((i1 -' 1),( 0 + 1))),(( Gauge (C,n)) * (((i1 -' 1) + 1),( 0 + 1))))) by A12, A9, GOBOARD5: 26;

          then

           A15: ( cell (( Gauge (C,n)),(i1 -' 1), 0 )) meets ( cell (( Gauge (C,n)),(i1 -' 1),( 0 + 1)));

          ( cell (( Gauge (C,n)),(( X-SpanStart (C,n)) -' 1), 0 )) c= ( UBD C) by A2, JORDAN1A: 49;

          then ( cell (( Gauge (C,n)),(( X-SpanStart (C,n)) -' 1),1)) c= ( UBD C) by A13, A9, A15, A11, A10, GOBOARD9: 4, JORDAN1A: 25;

          hence contradiction by A7, A14, JORDAN2C: 24, XBOOLE_1: 68;

        end;

      end;

      thus thesis by A1, Def3;

    end;

    theorem :: JORDAN11:8

    n is_sufficiently_large_for C implies [( X-SpanStart (C,n)), ( Y-SpanStart (C,n))] in ( Indices ( Gauge (C,n)))

    proof

      

       A1: ( X-SpanStart (C,n)) < ( len ( Gauge (C,n))) by JORDAN1H: 49;

      (1 + 1) < ( X-SpanStart (C,n)) by JORDAN1H: 49;

      then

       A2: 1 < ( X-SpanStart (C,n)) by NAT_1: 13;

      assume

       A3: n is_sufficiently_large_for C;

      then

       A4: ( Y-SpanStart (C,n)) <= ( width ( Gauge (C,n))) by Th7;

      1 < ( Y-SpanStart (C,n)) by A3, Th7;

      hence thesis by A2, A1, A4, MATRIX_0: 30;

    end;

    theorem :: JORDAN11:9

    n is_sufficiently_large_for C implies [(( X-SpanStart (C,n)) -' 1), ( Y-SpanStart (C,n))] in ( Indices ( Gauge (C,n)))

    proof

      

       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;

      then

       A4: ( Y-SpanStart (C,n)) <= ( width ( Gauge (C,n))) by Th7;

      1 < ( Y-SpanStart (C,n)) by A3, Th7;

      hence thesis by A1, A2, A4, MATRIX_0: 30;

    end;

    theorem :: JORDAN11:10

    n is_sufficiently_large_for C implies ( cell (( Gauge (C,n)),(( X-SpanStart (C,n)) -' 1),(( Y-SpanStart (C,n)) -' 1))) meets C

    proof

      set i1 = ( X-SpanStart (C,n));

      

       A1: (( Y-SpanStart (C,n)) - 1) < ( Y-SpanStart (C,n)) by XREAL_1: 146;

      assume

       A2: n is_sufficiently_large_for C;

      then

       A3: 1 < ( Y-SpanStart (C,n)) by Th7;

      assume

       A4: ( cell (( Gauge (C,n)),(( X-SpanStart (C,n)) -' 1),(( Y-SpanStart (C,n)) -' 1))) misses C;

      

       A5: for k st (( Y-SpanStart (C,n)) -' 1) <= k & k <= (((2 |^ (n -' ( ApproxIndex C))) * (( Y-InitStart C) -' 2)) + 2) holds ( cell (( Gauge (C,n)),(i1 -' 1),k)) c= ( BDD C)

      proof

        let k such that

         A6: (( Y-SpanStart (C,n)) -' 1) <= k and

         A7: k <= (((2 |^ (n -' ( ApproxIndex C))) * (( Y-InitStart C) -' 2)) + 2);

        per cases by A6, XXREAL_0: 1;

          suppose

           A8: (( Y-SpanStart (C,n)) -' 1) = k;

          1 < ( Y-SpanStart (C,n)) by A2, Th7;

          then

           A9: (k + 1) = ( Y-SpanStart (C,n)) by A8, XREAL_1: 235;

          

           A10: ( cell (( Gauge (C,n)),(i1 -' 1),k)) c= (C ` ) by A4, A8, SUBSET_1: 23;

          

           A11: k < (k + 1) by XREAL_1: 29;

          ( Y-SpanStart (C,n)) <= ( width ( Gauge (C,n))) by A2, Th7;

          then

           A12: k < ( width ( Gauge (C,n))) by A9, A11, XXREAL_0: 2;

          set W = { B where B be Subset of ( TOP-REAL 2) : B is_inside_component_of C };

          

           A13: (i1 -' 1) <= i1 by NAT_D: 44;

          i1 < ( len ( Gauge (C,n))) by JORDAN1H: 49;

          then

           A14: (i1 -' 1) < ( len ( Gauge (C,n))) by A13, XXREAL_0: 2;

          

           A15: ( BDD C) = ( union W) by JORDAN2C:def 4;

          (1 + 1) < ( X-SpanStart (C,n)) by JORDAN1H: 49;

          then 1 <= (i1 - 1) by XREAL_1: 19;

          then 1 <= (i1 -' 1) by NAT_D: 39;

          then (( cell (( Gauge (C,n)),(i1 -' 1),k)) /\ ( cell (( Gauge (C,n)),(i1 -' 1),(k + 1)))) = ( LSeg ((( Gauge (C,n)) * ((i1 -' 1),(k + 1))),(( Gauge (C,n)) * (((i1 -' 1) + 1),(k + 1))))) by A14, A12, GOBOARD5: 26;

          then ( cell (( Gauge (C,n)),(i1 -' 1),k)) meets ( cell (( Gauge (C,n)),(i1 -' 1),(k + 1)));

          then ( cell (( Gauge (C,n)),(i1 -' 1),k)) meets ( BDD C) by A2, A9, Th6, XBOOLE_1: 63;

          then

          consider e be set such that

           A16: e in W and

           A17: ( cell (( Gauge (C,n)),(i1 -' 1),k)) meets e by A15, ZFMISC_1: 80;

          consider B be Subset of ( TOP-REAL 2) such that

           A18: e = B and

           A19: B is_inside_component_of C by A16;

          

           A20: B c= ( BDD C) by A15, A16, A18, ZFMISC_1: 74;

          B is_a_component_of (C ` ) by A19, JORDAN2C:def 2;

          then ( cell (( Gauge (C,n)),(i1 -' 1),k)) c= B by A10, A14, A12, A17, A18, GOBOARD9: 4, JORDAN1A: 25;

          hence thesis by A20;

        end;

          suppose (( Y-SpanStart (C,n)) -' 1) < k;

          then ( Y-SpanStart (C,n)) < (k + 1) by NAT_D: 55;

          then ( Y-SpanStart (C,n)) <= k by NAT_1: 13;

          hence thesis by A2, A7, Def3;

        end;

      end;

      ( Y-SpanStart (C,n)) <= ( width ( Gauge (C,n))) by A2, Def3;

      then (( Y-SpanStart (C,n)) -' 1) <= ( width ( Gauge (C,n))) by NAT_D: 44;

      then (( Y-SpanStart (C,n)) -' 1) >= ( Y-SpanStart (C,n)) by A2, A5, Def3;

      hence contradiction by A3, A1, XREAL_1: 233;

    end;

    theorem :: JORDAN11:11

    n is_sufficiently_large_for C implies ( cell (( Gauge (C,n)),(( X-SpanStart (C,n)) -' 1),( Y-SpanStart (C,n)))) misses C

    proof

      assume n is_sufficiently_large_for C;

      then ( cell (( Gauge (C,n)),(( X-SpanStart (C,n)) -' 1),( Y-SpanStart (C,n)))) c= ( BDD C) by Th6;

      hence thesis by JORDAN1A: 7, XBOOLE_1: 63;

    end;

    begin

    reserve p,q for Point of ( TOP-REAL 2),

D for Simple_closed_curve;

    theorem :: JORDAN11:12

    

     Th12: ( UBD C) meets ( UBD D)

    proof

      reconsider A = C as bounded Subset of ( Euclid 2) by JORDAN2C: 11;

      consider r1 be Real, x1 be Point of ( Euclid 2) such that 0 < r1 and

       A1: A c= ( Ball (x1,r1)) by METRIC_6:def 3;

      reconsider B = D as bounded Subset of ( Euclid 2) by JORDAN2C: 11;

      consider r2 be Real, x2 be Point of ( Euclid 2) such that 0 < r2 and

       A2: B c= ( Ball (x2,r2)) by METRIC_6:def 3;

      reconsider C9 = (( Ball (x1,r1)) ` ), D9 = (( Ball (x2,r2)) ` ) as connected Subset of ( TOP-REAL 2) by JORDAN1K: 37;

      consider x3 be Point of ( Euclid 2), r3 be Real such that

       A3: (( Ball (x1,r1)) \/ ( Ball (x2,r2))) c= ( Ball (x3,r3)) by WEIERSTR: 1;

       A4:

      now

        assume D9 is bounded;

        then D9 is bounded Subset of ( Euclid 2) by JORDAN2C: 11;

        hence contradiction by JORDAN1K: 8;

      end;

       A5:

      now

        assume C9 is bounded;

        then C9 is bounded Subset of ( Euclid 2) by JORDAN2C: 11;

        hence contradiction by JORDAN1K: 8;

      end;

      (( Ball (x3,r3)) ` ) c= ((( Ball (x1,r1)) \/ ( Ball (x2,r2))) ` ) by A3, SUBSET_1: 12;

      then

       A6: (( Ball (x3,r3)) ` ) c= ((( Ball (x1,r1)) ` ) /\ (( Ball (x2,r2)) ` )) by XBOOLE_1: 53;

      then

       A7: (( Ball (x3,r3)) ` ) c= (( Ball (x1,r1)) ` ) by XBOOLE_1: 18;

      

       A8: (( Ball (x3,r3)) ` ) c= (( Ball (x2,r2)) ` ) by A6, XBOOLE_1: 18;

      (( Ball (x2,r2)) ` ) c= (B ` ) by A2, SUBSET_1: 12;

      then (( Ball (x2,r2)) ` ) misses B by SUBSET_1: 23;

      then D9 c= ( UBD D) by A4, JORDAN2C: 125;

      then

       A9: (( Ball (x3,r3)) ` ) c= ( UBD D) by A8;

      (( Ball (x1,r1)) ` ) c= (A ` ) by A1, SUBSET_1: 12;

      then (( Ball (x1,r1)) ` ) misses A by SUBSET_1: 23;

      then C9 c= ( UBD C) by A5, JORDAN2C: 125;

      then

       A10: (( Ball (x3,r3)) ` ) c= ( UBD C) by A7;

      (( Ball (x3,r3)) ` ) <> ( {} ( Euclid 2)) by JORDAN1K: 8;

      hence thesis by A10, A9, XBOOLE_1: 68;

    end;

    theorem :: JORDAN11:13

    

     Th13: q in ( UBD C) & p in ( BDD C) implies ( dist (q,C)) < ( dist (q,p))

    proof

      assume that

       A1: q in ( UBD C) and

       A2: p in ( BDD C) and

       A3: ( dist (q,C)) >= ( dist (q,p));

      

       A4: ( UBD C) is_a_component_of (C ` ) by JORDAN2C: 124;

      now

        assume ( LSeg (p,q)) meets C;

        then

        consider x be object such that

         A5: x in ( LSeg (p,q)) and

         A6: x in C by XBOOLE_0: 3;

        reconsider x as Point of ( TOP-REAL 2) by A5;

        

         A7: ( dist (q,C)) <= ( dist (q,x)) by A6, JORDAN1K: 50;

        C misses ( BDD C) by JORDAN1A: 7;

        then x <> p by A2, A6, XBOOLE_0: 3;

        hence contradiction by A3, A5, A7, JORDAN1K: 30, XXREAL_0: 2;

      end;

      then

       A8: ( LSeg (p,q)) c= (C ` ) by SUBSET_1: 23;

      q in ( LSeg (p,q)) by RLTOPSP1: 68;

      then

       A9: ( LSeg (p,q)) meets ( UBD C) by A1, XBOOLE_0: 3;

      

       A10: ( BDD C) = ( union { B where B be Subset of ( TOP-REAL 2) : B is_inside_component_of C }) by JORDAN2C:def 4;

      then

      consider X be set such that

       A11: p in X and

       A12: X in { B where B be Subset of ( TOP-REAL 2) : B is_inside_component_of C } by A2, TARSKI:def 4;

      consider B be Subset of ( TOP-REAL 2) such that

       A13: X = B and

       A14: B is_inside_component_of C by A12;

      B c= ( BDD C) by A10, A12, A13, ZFMISC_1: 74;

      then

       A15: B misses ( UBD C) by JORDAN2C: 24, XBOOLE_1: 63;

      p in ( LSeg (p,q)) by RLTOPSP1: 68;

      then

       A16: ( LSeg (p,q)) meets B by A11, A13, XBOOLE_0: 3;

      B is_a_component_of (C ` ) by A14, JORDAN2C:def 2;

      then ( UBD C) = B by A8, A4, A9, A16, JORDAN9: 1;

      hence contradiction by A15;

    end;

    theorem :: JORDAN11:14

    

     Th14: not p in ( BDD C) implies ( dist (p,C)) <= ( dist (p,( BDD C)))

    proof

      per cases ;

        suppose p in C;

        then ( dist (p,C)) = 0 by JORDAN1K: 45;

        hence thesis by JORDAN1K: 44;

      end;

        suppose

         A1: not p in C;

        assume that

         A2: not p in ( BDD C) and

         A3: ( dist (p,C)) > ( dist (p,( BDD C)));

        

         A4: ex q st q in ( BDD C) & ( dist (p,q)) < ( dist (p,C)) by A3, JORDAN1K: 48;

        p in (C ` ) by A1, SUBSET_1: 29;

        then p in (( BDD C) \/ ( UBD C)) by JORDAN2C: 27;

        then p in ( UBD C) by A2, XBOOLE_0:def 3;

        hence contradiction by A4, Th13;

      end;

    end;

    theorem :: JORDAN11:15

    

     Th15: not (C c= ( BDD D) & D c= ( BDD C))

    proof

      assume that

       A1: C c= ( BDD D) and

       A2: D c= ( BDD C);

      ( UBD C) meets ( UBD D) by Th12;

      then

      consider e be object such that

       A3: e in ( UBD C) and

       A4: e in ( UBD D) by XBOOLE_0: 3;

      reconsider p = e as Point of ( TOP-REAL 2) by A3;

      ( UBD D) misses ( BDD D) by JORDAN2C: 24;

      then

       A5: not p in ( BDD D) by A4, XBOOLE_0: 3;

      ( UBD C) misses ( BDD C) by JORDAN2C: 24;

      then

       A6: not p in ( BDD C) by A3, XBOOLE_0: 3;

      then ( dist (p,C)) <= ( dist (p,( BDD C))) by Th14;

      then ( dist (p,( BDD D))) < ( dist (p,( BDD C))) by A1, A5, JORDAN1K: 51, XXREAL_0: 2;

      then ( dist (p,( BDD D))) < ( dist (p,D)) by A2, A6, JORDAN1K: 51, XXREAL_0: 2;

      hence contradiction by A5, Th14;

    end;

    theorem :: JORDAN11:16

    

     Th16: C c= ( BDD D) implies D c= ( UBD C)

    proof

      assume

       A1: C c= ( BDD D);

      assume

       A2: not D c= ( UBD C);

      C misses D by A1, JORDAN1A: 7, XBOOLE_1: 63;

      then D c= ( BDD C) by A2, JORDAN1K: 19;

      hence contradiction by A1, Th15;

    end;

    theorem :: JORDAN11:17

    ( L~ ( Cage (C,n))) c= ( UBD C)

    proof

      C c= ( BDD ( L~ ( Cage (C,n)))) by JORDAN10: 12;

      hence thesis by Th16;

    end;