jordan1c.miz



    begin

    reserve C for Simple_closed_curve,

i,j,n for Nat,

p for Point of ( TOP-REAL 2);

     Lm1:

    now

      let r be Real, j;

      

      thus ( [\(r + j)/] - j) = (( [\r/] + j) - j) by INT_1: 28

      .= [\r/];

    end;

    

     Lm2: for a,b,c be Real st a <> 0 & b <> 0 holds ((a / b) * ((c / a) * b)) = c

    proof

      let a,b,c be Real;

      assume that

       A1: a <> 0 and

       A2: b <> 0 ;

      ((a / b) * ((c / a) * b)) = (((a / b) * b) * (c / a))

      .= (a * (c / a)) by A2, XCMPLX_1: 87

      .= c by A1, XCMPLX_1: 87;

      hence thesis;

    end;

    

     Lm3: for p be Point of ( TOP-REAL 2) holds p is Point of ( Euclid 2)

    proof

      let p be Point of ( TOP-REAL 2);

      ( TopSpaceMetr ( Euclid 2)) = the TopStruct of ( TOP-REAL 2) by EUCLID:def 8;

      then the TopStruct of ( TOP-REAL 2) = TopStruct (# the carrier of ( Euclid 2), ( Family_open_set ( Euclid 2)) #) by PCOMPS_1:def 5;

      hence thesis;

    end;

    

     Lm4: for r be Real st r > 0 holds (2 * (r / 4)) < r

    proof

      let r be Real;

      

       A1: (2 * (r / 4)) = (r / 2);

      assume r > 0 ;

      hence thesis by A1, XREAL_1: 216;

    end;

    theorem :: JORDAN1C:1

    

     Th1: [i, j] in ( Indices ( Gauge (C,n))) & [(i + 1), j] in ( Indices ( Gauge (C,n))) implies ( dist ((( Gauge (C,n)) * (1,1)),(( Gauge (C,n)) * (2,1)))) = (((( Gauge (C,n)) * ((i + 1),j)) `1 ) - ((( Gauge (C,n)) * (i,j)) `1 ))

    proof

      set G = ( Gauge (C,n));

      assume that

       A1: [i, j] in ( Indices G) and

       A2: [(i + 1), j] in ( Indices G);

      

       A3: j <= ( width G) by A1, MATRIX_0: 32;

      1 <= j by A1, MATRIX_0: 32;

      then

       A4: 1 <= ( width G) by A3, XXREAL_0: 2;

      

       A5: ( len G) >= 4 by JORDAN8: 10;

      then 2 <= ( len G) by XXREAL_0: 2;

      then

       A6: [2, 1] in ( Indices G) by A4, MATRIX_0: 30;

      

       A7: ( dist ((G * (i,j)),(G * ((i + 1),j)))) = ((( E-bound C) - ( W-bound C)) / (2 |^ n)) by A1, A2, GOBRD14: 10;

      1 <= ( len G) by A5, XXREAL_0: 2;

      then [1, 1] in ( Indices G) by A4, MATRIX_0: 30;

      

      then ( dist ((G * (1,1)),(G * ((1 + 1),1)))) = ( dist ((G * (i,j)),(G * ((i + 1),j)))) by A6, A7, GOBRD14: 10

      .= (((G * ((i + 1),j)) `1 ) - ((G * (i,j)) `1 )) by A1, A2, GOBRD14: 5;

      hence thesis;

    end;

    theorem :: JORDAN1C:2

    

     Th2: [i, j] in ( Indices ( Gauge (C,n))) & [i, (j + 1)] in ( Indices ( Gauge (C,n))) implies ( dist ((( Gauge (C,n)) * (1,1)),(( Gauge (C,n)) * (1,2)))) = (((( Gauge (C,n)) * (i,(j + 1))) `2 ) - ((( Gauge (C,n)) * (i,j)) `2 ))

    proof

      set G = ( Gauge (C,n));

      assume that

       A1: [i, j] in ( Indices G) and

       A2: [i, (j + 1)] in ( Indices G);

      

       A3: 1 <= (j + 1) by A2, MATRIX_0: 32;

      ( len G) >= 4 by JORDAN8: 10;

      then

       A4: 1 <= ( len G) by XXREAL_0: 2;

      ((2 |^ n) + 3) >= 3 by NAT_1: 11;

      then ( width G) >= 3 by JORDAN1A: 28;

      then 2 <= ( width G) by XXREAL_0: 2;

      then

       A5: [1, 2] in ( Indices G) by A4, MATRIX_0: 30;

      (j + 1) <= ( width G) by A2, MATRIX_0: 32;

      then 1 <= ( width G) by A3, XXREAL_0: 2;

      then

       A6: [1, 1] in ( Indices G) by A4, MATRIX_0: 30;

      ( dist ((G * (i,j)),(G * (i,(j + 1))))) = ((( N-bound C) - ( S-bound C)) / (2 |^ n)) by A1, A2, GOBRD14: 9;

      

      then ( dist ((G * (1,1)),(G * (1,(1 + 1))))) = ( dist ((G * (i,j)),(G * (i,(j + 1))))) by A6, A5, GOBRD14: 9

      .= (((G * (i,(j + 1))) `2 ) - ((G * (i,j)) `2 )) by A1, A2, GOBRD14: 6;

      hence thesis;

    end;

    ( TopSpaceMetr ( Euclid 2)) = the TopStruct of ( TOP-REAL 2) by EUCLID:def 8;

    then

     Lm5: the TopStruct of ( TOP-REAL 2) = TopStruct (# the carrier of ( Euclid 2), ( Family_open_set ( Euclid 2)) #) by PCOMPS_1:def 5;

    

     Lm6: for r be Real, q be Point of ( Euclid 2) st 1 <= i & (i + 1) <= ( len ( Gauge (C,n))) & 1 <= j & (j + 1) <= ( width ( Gauge (C,n))) & r > 0 & p = q & ( dist ((( Gauge (C,n)) * (1,1)),(( Gauge (C,n)) * (1,2)))) < (r / 4) & ( dist ((( Gauge (C,n)) * (1,1)),(( Gauge (C,n)) * (2,1)))) < (r / 4) & p in ( cell (( Gauge (C,n)),i,j)) holds ( cell (( Gauge (C,n)),i,j)) c= ( Ball (q,r))

    proof

      let r be Real, q be Point of ( Euclid 2);

      assume that

       A1: 1 <= i and

       A2: (i + 1) <= ( len ( Gauge (C,n))) and

       A3: 1 <= j and

       A4: (j + 1) <= ( width ( Gauge (C,n))) and

       A5: r > 0 and

       A6: p = q and

       A7: ( dist ((( Gauge (C,n)) * (1,1)),(( Gauge (C,n)) * (1,2)))) < (r / 4) and

       A8: ( dist ((( Gauge (C,n)) * (1,1)),(( Gauge (C,n)) * (2,1)))) < (r / 4) and

       A9: p in ( cell (( Gauge (C,n)),i,j));

      set G = ( Gauge (C,n));

      set I = i, J = j, l = (r / 4);

      let x be object;

      assume

       A10: x in ( cell (( Gauge (C,n)),i,j));

      then

      reconsider Q = q, X = x as Point of ( TOP-REAL 2) by Lm5;

      

       A11: (Q `1 ) <= ((G * ((I + 1),J)) `1 ) by A1, A2, A3, A4, A6, A9, JORDAN9: 17;

      

       A12: ((G * (I,J)) `2 ) <= (Q `2 ) by A1, A2, A3, A4, A6, A9, JORDAN9: 17;

      

       A13: ((G * (I,J)) `1 ) <= (X `1 ) by A1, A2, A3, A4, A10, JORDAN9: 17;

      j < (j + 1) by XREAL_1: 29;

      then

       A14: j <= ( width G) by A4, XXREAL_0: 2;

      i < (i + 1) by XREAL_1: 29;

      then

       A15: i <= ( len G) by A2, XXREAL_0: 2;

      then

       A16: [i, j] in ( Indices G) by A1, A3, A14, MATRIX_0: 30;

      

       A17: (X `2 ) <= ((G * (I,(J + 1))) `2 ) by A1, A2, A3, A4, A10, JORDAN9: 17;

      

       A18: ((G * (I,J)) `2 ) <= (X `2 ) by A1, A2, A3, A4, A10, JORDAN9: 17;

      

       A19: (Q `2 ) <= ((G * (I,(J + 1))) `2 ) by A1, A2, A3, A4, A6, A9, JORDAN9: 17;

      

       A20: (X `1 ) <= ((G * ((I + 1),J)) `1 ) by A1, A2, A3, A4, A10, JORDAN9: 17;

      1 <= (j + 1) by A3, XREAL_1: 29;

      then [i, (j + 1)] in ( Indices G) by A1, A4, A15, MATRIX_0: 30;

      then

       A21: (((G * (I,(J + 1))) `2 ) - ((G * (I,J)) `2 )) < l by A7, A16, Th2;

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

      then [(i + 1), j] in ( Indices G) by A2, A3, A14, MATRIX_0: 30;

      then (((G * ((I + 1),J)) `1 ) - ((G * (I,J)) `1 )) < l by A8, A16, Th1;

      then

       A22: ((((G * ((I + 1),J)) `1 ) - ((G * (I,J)) `1 )) + (((G * (I,(J + 1))) `2 ) - ((G * (I,J)) `2 ))) <= (l + l) by A21, XREAL_1: 7;

      ((G * (I,J)) `1 ) <= (Q `1 ) by A1, A2, A3, A4, A6, A9, JORDAN9: 17;

      then ( dist (Q,X)) <= ((((G * ((I + 1),J)) `1 ) - ((G * (I,J)) `1 )) + (((G * (I,(J + 1))) `2 ) - ((G * (I,J)) `2 ))) by A11, A12, A19, A13, A20, A18, A17, TOPREAL6: 95;

      then

       A23: ( dist (p,X)) <= (l + l) by A6, A22, XXREAL_0: 2;

      reconsider x9 = x as Point of ( Euclid 2) by A10, Lm3;

      (2 * (r / 4)) < r by A5, Lm4;

      then ( dist (X,p)) < r by A23, XXREAL_0: 2;

      then ( dist (x9,q)) < r by A6, TOPREAL6:def 1;

      hence thesis by METRIC_1: 11;

    end;

    theorem :: JORDAN1C:3

    

     Th3: for S be Subset of ( TOP-REAL 2) st S is bounded holds ( proj1 .: S) is real-bounded

    proof

      let S be Subset of ( TOP-REAL 2);

      assume S is bounded;

      then

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

      consider r be Real, x be Point of ( Euclid 2) such that

       A1: 0 < r and

       A2: C c= ( Ball (x,r)) by METRIC_6:def 3;

      reconsider P = ( Ball (x,r)) as Subset of ( TOP-REAL 2) by TOPREAL3: 8;

      reconsider p = x as Point of ( TOP-REAL 2) by TOPREAL3: 8;

      set t = ( max ( |.((p `1 ) - r).|, |.((p `1 ) + r).|));

      now

        assume that

         A3: |.((p `1 ) - r).| <= 0 and

         A4: |.((p `1 ) + r).| <= 0 ;

         |.((p `1 ) - r).| = 0 by A3, COMPLEX1: 46;

        then |.(r - (p `1 )).| = 0 by UNIFORM1: 11;

        then

         A5: (r - (p `1 )) = 0 by ABSVALUE: 2;

         |.((p `1 ) + r).| = 0 by A4, COMPLEX1: 46;

        hence contradiction by A1, A5, ABSVALUE: 2;

      end;

      then

       A6: t > 0 by XXREAL_0: 30;

      

       A7: ( proj1 .: P) = ].((p `1 ) - r), ((p `1 ) + r).[ by TOPREAL6: 43;

      for s be Real st s in ( proj1 .: S) holds |.s.| < t

      proof

        let s be Real;

        ( proj1 .: S) c= ( proj1 .: P) by A2, RELAT_1: 123;

        hence thesis by A7, JCT_MISC: 3;

      end;

      hence thesis by A6, SEQ_4: 4;

    end;

    theorem :: JORDAN1C:4

    for C1 be non empty compact Subset of ( TOP-REAL 2), C2,S be non empty Subset of ( TOP-REAL 2) holds S = (C1 \/ C2) & ( proj1 .: C2) is non empty bounded_below implies ( W-bound S) = ( min (( W-bound C1),( W-bound C2)))

    proof

      let C1 be non empty compact Subset of ( TOP-REAL 2), C2,S be non empty Subset of ( TOP-REAL 2);

      assume that

       A1: S = (C1 \/ C2) and

       A2: ( proj1 .: C2) is non empty bounded_below;

      set P1 = ( proj1 .: C1), P2 = ( proj1 .: C2), PS = ( proj1 .: S);

      

       A3: ( W-bound C1) = ( lower_bound P1) by SPRECT_1: 43;

      

       A4: ( W-bound C2) = ( lower_bound P2) by SPRECT_1: 43;

      

      thus ( W-bound S) = ( lower_bound PS) by SPRECT_1: 43

      .= ( lower_bound (P1 \/ P2)) by A1, RELAT_1: 120

      .= ( min (( W-bound C1),( W-bound C2))) by A2, A3, A4, SEQ_4: 142;

    end;

    

     Lm7: for X be Subset of ( TOP-REAL 2) holds p in X & X is bounded implies ( lower_bound ( proj1 | X)) <= (p `1 ) & (p `1 ) <= ( upper_bound ( proj1 | X))

    proof

      set T = ( TOP-REAL 2);

      let X be Subset of ( TOP-REAL 2);

      assume that

       A1: p in X and

       A2: X is bounded;

      reconsider X as non empty Subset of ( TOP-REAL 2) by A1;

      

       A3: the carrier of (T | X) = X by PRE_TOPC: 8;

      

       A4: (( proj1 | X) .: X) = ( proj1 .: X) by RELAT_1: 129;

      

       A5: ( proj1 .: X) is real-bounded by A2, Th3;

      then (( proj1 | X) .: X) is bounded_below by A4, XXREAL_2:def 11;

      then

       A6: ( proj1 | X) is bounded_below by A3, MEASURE6:def 10;

      (( proj1 | X) .: X) is bounded_above by A4, A5, XXREAL_2:def 11;

      then ( proj1 | X) is bounded_above by A3, MEASURE6:def 11;

      then

      reconsider f = ( proj1 | X) as bounded RealMap of (T | X) by A6;

      reconsider p9 = p as Point of (T | X) by A1, PRE_TOPC: 8;

      

       A7: (( proj1 | X) . p9) = (p `1 ) by A1, PSCOMP_1: 22;

      then ( lower_bound f) <= (p `1 ) by PSCOMP_1: 1;

      hence thesis by A7, PSCOMP_1: 4;

    end;

    

     Lm8: for X be Subset of ( TOP-REAL 2) holds p in X & X is bounded implies ( lower_bound ( proj2 | X)) <= (p `2 ) & (p `2 ) <= ( upper_bound ( proj2 | X))

    proof

      set T = ( TOP-REAL 2);

      let X be Subset of ( TOP-REAL 2);

      assume that

       A1: p in X and

       A2: X is bounded;

      reconsider X as non empty Subset of ( TOP-REAL 2) by A1;

      

       A3: the carrier of (T | X) = X by PRE_TOPC: 8;

      

       A4: (( proj2 | X) .: X) = ( proj2 .: X) by RELAT_1: 129;

      

       A5: ( proj2 .: X) is real-bounded by A2, JCT_MISC: 14;

      then (( proj2 | X) .: X) is bounded_below by A4, XXREAL_2:def 11;

      then

       A6: ( proj2 | X) is bounded_below by A3, MEASURE6:def 10;

      (( proj2 | X) .: X) is bounded_above by A4, A5, XXREAL_2:def 11;

      then ( proj2 | X) is bounded_above by A3, MEASURE6:def 11;

      then

      reconsider f = ( proj2 | X) as bounded RealMap of (T | X) by A6;

      reconsider p9 = p as Point of (T | X) by A1, PRE_TOPC: 8;

      

       A7: (( proj2 | X) . p9) = (p `2 ) by A1, PSCOMP_1: 23;

      then ( lower_bound f) <= (p `2 ) by PSCOMP_1: 1;

      hence thesis by A7, PSCOMP_1: 4;

    end;

    theorem :: JORDAN1C:5

    

     Th5: for X be Subset of ( TOP-REAL 2) holds p in X & X is bounded implies ( W-bound X) <= (p `1 ) & (p `1 ) <= ( E-bound X) & ( S-bound X) <= (p `2 ) & (p `2 ) <= ( N-bound X)

    proof

      let X be Subset of ( TOP-REAL 2);

      assume that

       A1: p in X and

       A2: X is bounded;

      ( W-bound X) = ( lower_bound ( proj1 | X)) by PSCOMP_1:def 7;

      hence ( W-bound X) <= (p `1 ) by A1, A2, Lm7;

      ( E-bound X) = ( upper_bound ( proj1 | X)) by PSCOMP_1:def 9;

      hence ( E-bound X) >= (p `1 ) by A1, A2, Lm7;

      ( S-bound X) = ( lower_bound ( proj2 | X)) by PSCOMP_1:def 10;

      hence ( S-bound X) <= (p `2 ) by A1, A2, Lm8;

      ( N-bound X) = ( upper_bound ( proj2 | X)) by PSCOMP_1:def 8;

      hence thesis by A1, A2, Lm8;

    end;

    

     Lm9: for C be Subset of ( TOP-REAL 2) st C is bounded holds for h be Real st ( BDD C) <> {} & h > ( W-bound ( BDD C)) & (for p st p in ( BDD C) holds (p `1 ) >= h) holds contradiction

    proof

      let C be Subset of ( TOP-REAL 2) such that

       A1: C is bounded;

      set X = ( proj1 | ( BDD C));

      let h be Real;

      assume that

       A2: ( BDD C) <> {} and

       A3: h > ( W-bound ( BDD C)) and

       A4: for p st p in ( BDD C) holds (p `1 ) >= h;

      reconsider T = (( TOP-REAL 2) | ( BDD C)) as non empty TopSpace by A2;

      the carrier of T = ( BDD C) by PRE_TOPC: 8;

      then (X .: the carrier of T) = ( proj1 .: ( BDD C)) by RELAT_1: 129;

      then (X .: the carrier of T) is real-bounded by A1, Th3, JORDAN2C: 106;

      then (X .: the carrier of T) is bounded_below by XXREAL_2:def 11;

      then

      reconsider X as bounded_below RealMap of T by MEASURE6:def 10;

      

       A5: for p be Point of T holds (X . p) >= h

      proof

        let p be Point of T;

        

         A6: the carrier of T = ( BDD C) by PRE_TOPC: 8;

        then p in ( BDD C);

        then

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

        (X . p) = ( proj1 . p9) by A6, FUNCT_1: 49;

        then (X . p) = (p9 `1 ) by PSCOMP_1:def 5;

        hence thesis by A4, A6;

      end;

      ( lower_bound X) = ( W-bound ( BDD C)) by PSCOMP_1:def 7;

      hence thesis by A3, A5, PSCOMP_1: 2;

    end;

    

     Lm10: for C be Subset of ( TOP-REAL 2) st C is bounded holds for h be Real st ( BDD C) <> {} & h < ( E-bound ( BDD C)) & (for p st p in ( BDD C) holds (p `1 ) <= h) holds contradiction

    proof

      let C be Subset of ( TOP-REAL 2) such that

       A1: C is bounded;

      set X = ( proj1 | ( BDD C));

      let h be Real;

      assume that

       A2: ( BDD C) <> {} and

       A3: h < ( E-bound ( BDD C)) and

       A4: for p st p in ( BDD C) holds (p `1 ) <= h;

      reconsider T = (( TOP-REAL 2) | ( BDD C)) as non empty TopSpace by A2;

      the carrier of T = ( BDD C) by PRE_TOPC: 8;

      then (X .: the carrier of T) = ( proj1 .: ( BDD C)) by RELAT_1: 129;

      then (X .: the carrier of T) is real-bounded by A1, Th3, JORDAN2C: 106;

      then (X .: the carrier of T) is bounded_above by XXREAL_2:def 11;

      then

      reconsider X as bounded_above RealMap of T by MEASURE6:def 11;

      

       A5: for p be Point of T holds (X . p) <= h

      proof

        let p be Point of T;

        

         A6: the carrier of T = ( BDD C) by PRE_TOPC: 8;

        then p in ( BDD C);

        then

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

        (X . p) = ( proj1 . p9) by A6, FUNCT_1: 49;

        then (X . p) = (p9 `1 ) by PSCOMP_1:def 5;

        hence thesis by A4, A6;

      end;

      ( upper_bound X) = ( E-bound ( BDD C)) by PSCOMP_1:def 9;

      hence thesis by A3, A5, PSCOMP_1: 5;

    end;

    

     Lm11: for C be Subset of ( TOP-REAL 2) st C is bounded holds for h be Real st ( BDD C) <> {} & h < ( N-bound ( BDD C)) & (for p st p in ( BDD C) holds (p `2 ) <= h) holds contradiction

    proof

      let C be Subset of ( TOP-REAL 2) such that

       A1: C is bounded;

      set X = ( proj2 | ( BDD C));

      let h be Real;

      assume that

       A2: ( BDD C) <> {} and

       A3: h < ( N-bound ( BDD C)) and

       A4: for p st p in ( BDD C) holds (p `2 ) <= h;

      reconsider T = (( TOP-REAL 2) | ( BDD C)) as non empty TopSpace by A2;

      the carrier of T = ( BDD C) by PRE_TOPC: 8;

      then (X .: the carrier of T) = ( proj2 .: ( BDD C)) by RELAT_1: 129;

      then (X .: the carrier of T) is real-bounded by A1, JCT_MISC: 14, JORDAN2C: 106;

      then (X .: the carrier of T) is bounded_above by XXREAL_2:def 11;

      then

      reconsider X as bounded_above RealMap of T by MEASURE6:def 11;

      

       A5: for p be Point of T holds (X . p) <= h

      proof

        let p be Point of T;

        

         A6: the carrier of T = ( BDD C) by PRE_TOPC: 8;

        then p in ( BDD C);

        then

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

        (X . p) = ( proj2 . p9) by A6, FUNCT_1: 49;

        then (X . p) = (p9 `2 ) by PSCOMP_1:def 6;

        hence thesis by A4, A6;

      end;

      ( upper_bound X) = ( N-bound ( BDD C)) by PSCOMP_1:def 8;

      hence thesis by A3, A5, PSCOMP_1: 5;

    end;

    

     Lm12: for C be Subset of ( TOP-REAL 2) st C is bounded holds for h be Real st ( BDD C) <> {} & h > ( S-bound ( BDD C)) & (for p st p in ( BDD C) holds (p `2 ) >= h) holds contradiction

    proof

      let C be Subset of ( TOP-REAL 2) such that

       A1: C is bounded;

      set X = ( proj2 | ( BDD C));

      let h be Real;

      assume that

       A2: ( BDD C) <> {} and

       A3: h > ( S-bound ( BDD C)) and

       A4: for p st p in ( BDD C) holds (p `2 ) >= h;

      reconsider T = (( TOP-REAL 2) | ( BDD C)) as non empty TopSpace by A2;

      the carrier of T = ( BDD C) by PRE_TOPC: 8;

      then (X .: the carrier of T) = ( proj2 .: ( BDD C)) by RELAT_1: 129;

      then (X .: the carrier of T) is real-bounded by A1, JCT_MISC: 14, JORDAN2C: 106;

      then (X .: the carrier of T) is bounded_below by XXREAL_2:def 11;

      then

      reconsider X as bounded_below RealMap of T by MEASURE6:def 10;

      

       A5: for p be Point of T holds (X . p) >= h

      proof

        let p be Point of T;

        

         A6: the carrier of T = ( BDD C) by PRE_TOPC: 8;

        then p in ( BDD C);

        then

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

        (X . p) = ( proj2 . p9) by A6, FUNCT_1: 49;

        then (X . p) = (p9 `2 ) by PSCOMP_1:def 6;

        hence thesis by A4, A6;

      end;

      ( lower_bound X) = ( S-bound ( BDD C)) by PSCOMP_1:def 10;

      hence thesis by A3, A5, PSCOMP_1: 2;

    end;

     Lm13:

    now

      let C be Subset of ( TOP-REAL 2);

      assume C is bounded;

      then ( UBD C) is_outside_component_of C by JORDAN2C: 68;

      hence ( UBD C) is non empty by JORDAN2C:def 3;

    end;

    theorem :: JORDAN1C:6

    

     Th6: for C be compact Subset of ( TOP-REAL 2) holds ( BDD C) <> {} implies ( W-bound C) <= ( W-bound ( BDD C))

    proof

      let C be compact Subset of ( TOP-REAL 2);

      set WC = ( W-bound C), WB = ( W-bound ( BDD C));

      set hal = ((WB + WC) / 2);

      assume that

       A1: ( BDD C) <> {} and

       A2: WC > WB;

      

       A3: hal < WC by A2, XREAL_1: 226;

      now

        per cases ;

          suppose for q1 be Point of ( TOP-REAL 2) st q1 in ( BDD C) holds (q1 `1 ) >= hal;

          hence contradiction by A1, A2, Lm9, XREAL_1: 226;

        end;

          suppose ex q1 be Point of ( TOP-REAL 2) st q1 in ( BDD C) & (q1 `1 ) < hal;

          then

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

           A4: q1 in ( BDD C) and

           A5: (q1 `1 ) < hal;

          set Q = |[((WC + (q1 `1 )) / 2), (q1 `2 )]|;

          set WH = ( west_halfline Q);

          

           A6: (Q `1 ) = ((WC + (q1 `1 )) / 2) by EUCLID: 52;

          

           A7: (q1 `1 ) < WC by A3, A5, XXREAL_0: 2;

          WH misses C

          proof

            

             A8: (Q `1 ) < WC by A7, A6, XREAL_1: 226;

            assume WH meets C;

            then

            consider y be object such that

             A9: y in (WH /\ C) by XBOOLE_0: 4;

            

             A10: y in C by A9, XBOOLE_0:def 4;

            

             A11: y in WH by A9, XBOOLE_0:def 4;

            reconsider y as Point of ( TOP-REAL 2) by A9;

            (y `1 ) <= (Q `1 ) by A11, TOPREAL1:def 13;

            then (y `1 ) < WC by A8, XXREAL_0: 2;

            hence thesis by A10, PSCOMP_1: 24;

          end;

          then

           A12: WH c= ( UBD C) by JORDAN2C: 126;

          

           A13: (q1 `2 ) = (Q `2 ) by EUCLID: 52;

          (q1 `1 ) < (Q `1 ) by A7, A6, XREAL_1: 226;

          then q1 in WH by A13, TOPREAL1:def 13;

          then q1 in (( BDD C) /\ ( UBD C)) by A4, A12, XBOOLE_0:def 4;

          then ( BDD C) meets ( UBD C);

          hence contradiction by JORDAN2C: 24;

        end;

      end;

      hence thesis;

    end;

    theorem :: JORDAN1C:7

    

     Th7: for C be compact Subset of ( TOP-REAL 2) holds ( BDD C) <> {} implies ( E-bound C) >= ( E-bound ( BDD C))

    proof

      let C be compact Subset of ( TOP-REAL 2);

      set WC = ( E-bound ( BDD C)), WB = ( E-bound C);

      set hal = ((WB + WC) / 2);

      assume that

       A1: ( BDD C) <> {} and

       A2: WC > WB;

      

       A3: hal > WB by A2, XREAL_1: 226;

      now

        per cases ;

          suppose for q1 be Point of ( TOP-REAL 2) st q1 in ( BDD C) holds (q1 `1 ) <= hal;

          hence contradiction by A1, A2, Lm10, XREAL_1: 226;

        end;

          suppose ex q1 be Point of ( TOP-REAL 2) st q1 in ( BDD C) & (q1 `1 ) > hal;

          then

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

           A4: q1 in ( BDD C) and

           A5: (q1 `1 ) > hal;

          set Q = |[((WB + (q1 `1 )) / 2), (q1 `2 )]|;

          set WH = ( east_halfline Q);

          

           A6: (Q `1 ) = ((WB + (q1 `1 )) / 2) by EUCLID: 52;

          

           A7: (q1 `1 ) > WB by A3, A5, XXREAL_0: 2;

          WH misses C

          proof

            

             A8: (Q `1 ) > WB by A7, A6, XREAL_1: 226;

            assume (WH /\ C) <> {} ;

            then

            consider y be object such that

             A9: y in (WH /\ C) by XBOOLE_0:def 1;

            

             A10: y in C by A9, XBOOLE_0:def 4;

            

             A11: y in WH by A9, XBOOLE_0:def 4;

            reconsider y as Point of ( TOP-REAL 2) by A9;

            (y `1 ) >= (Q `1 ) by A11, TOPREAL1:def 11;

            then (y `1 ) > WB by A8, XXREAL_0: 2;

            hence thesis by A10, PSCOMP_1: 24;

          end;

          then

           A12: WH c= ( UBD C) by JORDAN2C: 127;

          

           A13: (q1 `2 ) = (Q `2 ) by EUCLID: 52;

          (q1 `1 ) > (Q `1 ) by A7, A6, XREAL_1: 226;

          then q1 in WH by A13, TOPREAL1:def 11;

          then q1 in (( BDD C) /\ ( UBD C)) by A4, A12, XBOOLE_0:def 4;

          then ( BDD C) meets ( UBD C);

          hence contradiction by JORDAN2C: 24;

        end;

      end;

      hence thesis;

    end;

    theorem :: JORDAN1C:8

    

     Th8: for C be compact Subset of ( TOP-REAL 2) holds ( BDD C) <> {} implies ( S-bound C) <= ( S-bound ( BDD C))

    proof

      let C be compact Subset of ( TOP-REAL 2);

      set WC = ( S-bound C), WB = ( S-bound ( BDD C));

      set hal = ((WB + WC) / 2);

      assume that

       A1: ( BDD C) <> {} and

       A2: WC > WB;

      

       A3: hal < WC by A2, XREAL_1: 226;

      now

        per cases ;

          suppose for q1 be Point of ( TOP-REAL 2) st q1 in ( BDD C) holds (q1 `2 ) >= hal;

          hence contradiction by A1, A2, Lm12, XREAL_1: 226;

        end;

          suppose ex q1 be Point of ( TOP-REAL 2) st q1 in ( BDD C) & (q1 `2 ) < hal;

          then

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

           A4: q1 in ( BDD C) and

           A5: (q1 `2 ) < hal;

          set Q = |[(q1 `1 ), ((WC + (q1 `2 )) / 2)]|;

          set WH = ( south_halfline Q);

          

           A6: (Q `2 ) = ((WC + (q1 `2 )) / 2) by EUCLID: 52;

          

           A7: (q1 `2 ) < WC by A3, A5, XXREAL_0: 2;

          WH misses C

          proof

            

             A8: (Q `2 ) < WC by A7, A6, XREAL_1: 226;

            assume (WH /\ C) <> {} ;

            then

            consider y be object such that

             A9: y in (WH /\ C) by XBOOLE_0:def 1;

            

             A10: y in C by A9, XBOOLE_0:def 4;

            

             A11: y in WH by A9, XBOOLE_0:def 4;

            reconsider y as Point of ( TOP-REAL 2) by A9;

            (y `2 ) <= (Q `2 ) by A11, TOPREAL1:def 12;

            then (y `2 ) < WC by A8, XXREAL_0: 2;

            hence thesis by A10, PSCOMP_1: 24;

          end;

          then

           A12: WH c= ( UBD C) by JORDAN2C: 128;

          

           A13: (q1 `1 ) = (Q `1 ) by EUCLID: 52;

          (q1 `2 ) < (Q `2 ) by A7, A6, XREAL_1: 226;

          then q1 in WH by A13, TOPREAL1:def 12;

          then q1 in (( BDD C) /\ ( UBD C)) by A4, A12, XBOOLE_0:def 4;

          then ( BDD C) meets ( UBD C);

          hence contradiction by JORDAN2C: 24;

        end;

      end;

      hence thesis;

    end;

    theorem :: JORDAN1C:9

    

     Th9: for C be compact Subset of ( TOP-REAL 2) holds ( BDD C) <> {} implies ( N-bound C) >= ( N-bound ( BDD C))

    proof

      let C be compact Subset of ( TOP-REAL 2);

      set WC = ( N-bound ( BDD C)), WB = ( N-bound C);

      set hal = ((WB + WC) / 2);

      assume that

       A1: ( BDD C) <> {} and

       A2: WC > WB;

      

       A3: hal > WB by A2, XREAL_1: 226;

      now

        per cases ;

          suppose for q1 be Point of ( TOP-REAL 2) st q1 in ( BDD C) holds (q1 `2 ) <= hal;

          hence contradiction by A1, A2, Lm11, XREAL_1: 226;

        end;

          suppose ex q1 be Point of ( TOP-REAL 2) st q1 in ( BDD C) & (q1 `2 ) > hal;

          then

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

           A4: q1 in ( BDD C) and

           A5: (q1 `2 ) > hal;

          set Q = |[(q1 `1 ), ((WB + (q1 `2 )) / 2)]|;

          set WH = ( north_halfline Q);

          

           A6: (Q `2 ) = ((WB + (q1 `2 )) / 2) by EUCLID: 52;

          

           A7: (q1 `2 ) > WB by A3, A5, XXREAL_0: 2;

          WH misses C

          proof

            

             A8: (Q `2 ) > WB by A7, A6, XREAL_1: 226;

            assume (WH /\ C) <> {} ;

            then

            consider y be object such that

             A9: y in (WH /\ C) by XBOOLE_0:def 1;

            

             A10: y in C by A9, XBOOLE_0:def 4;

            

             A11: y in WH by A9, XBOOLE_0:def 4;

            reconsider y as Point of ( TOP-REAL 2) by A9;

            (y `2 ) >= (Q `2 ) by A11, TOPREAL1:def 10;

            then (y `2 ) > WB by A8, XXREAL_0: 2;

            hence thesis by A10, PSCOMP_1: 24;

          end;

          then

           A12: WH c= ( UBD C) by JORDAN2C: 129;

          

           A13: (q1 `1 ) = (Q `1 ) by EUCLID: 52;

          (q1 `2 ) > (Q `2 ) by A7, A6, XREAL_1: 226;

          then q1 in WH by A13, TOPREAL1:def 10;

          then q1 in (( BDD C) /\ ( UBD C)) by A4, A12, XBOOLE_0:def 4;

          then ( BDD C) meets ( UBD C);

          hence contradiction by JORDAN2C: 24;

        end;

      end;

      hence thesis;

    end;

    theorem :: JORDAN1C:10

    

     Th10: for C be compact non vertical Subset of ( TOP-REAL 2) holds for I be Integer st p in ( BDD C) & I = [\(((((p `1 ) - ( W-bound C)) / (( E-bound C) - ( W-bound C))) * (2 |^ n)) + 2)/] holds 1 < I

    proof

      let C be compact non vertical Subset of ( TOP-REAL 2);

      set W = ( W-bound C), E = ( E-bound C);

      set pW = ((p `1 ) - W), EW = (E - W);

      let I be Integer;

      assume that

       A1: p in ( BDD C) and

       A2: I = [\(((pW / EW) * (2 |^ n)) + 2)/];

      

       A3: W <= ( W-bound ( BDD C)) by A1, Th6;

      ( BDD C) is bounded by JORDAN2C: 106;

      then (p `1 ) >= ( W-bound ( BDD C)) by A1, Th5;

      then (p `1 ) >= W by A3, XXREAL_0: 2;

      then

       A4: pW >= 0 by XREAL_1: 48;

      set K = [\((pW / EW) * (2 |^ n))/];

      (((pW / EW) * (2 |^ n)) - 1) < K by INT_1:def 6;

      then

       A5: ((((pW / EW) * (2 |^ n)) - 1) + 2) < (K + 2) by XREAL_1: 6;

      EW > 0 by SPRECT_1: 31, XREAL_1: 50;

      then (((pW / EW) * (2 |^ n)) + 1) >= ( 0 + 1) by A4, XREAL_1: 6;

      then 1 < (K + 2) by A5, XXREAL_0: 2;

      hence thesis by A2, INT_1: 28;

    end;

    theorem :: JORDAN1C:11

    

     Th11: for C be compact non vertical Subset of ( TOP-REAL 2) holds for I be Integer st p in ( BDD C) & I = [\(((((p `1 ) - ( W-bound C)) / (( E-bound C) - ( W-bound C))) * (2 |^ n)) + 2)/] holds (I + 1) <= ( len ( Gauge (C,n)))

    proof

      let C be compact non vertical Subset of ( TOP-REAL 2);

      set W = ( W-bound C), E = ( E-bound C);

      set EW = (E - W), pW = ((p `1 ) - W);

      let I be Integer;

      assume that

       A1: p in ( BDD C) and

       A2: I = [\(((pW / EW) * (2 |^ n)) + 2)/];

      

       A3: E >= ( E-bound ( BDD C)) by A1, Th7;

      ( BDD C) is bounded by JORDAN2C: 106;

      then (p `1 ) <= ( E-bound ( BDD C)) by A1, Th5;

      then (p `1 ) <= E by A3, XXREAL_0: 2;

      then

       A4: ((p `1 ) - W) <= EW by XREAL_1: 9;

      EW > 0 by SPRECT_1: 31, XREAL_1: 50;

      then (pW / EW) <= 1 by A4, XREAL_1: 185;

      then ((pW / EW) * (2 |^ n)) <= (1 * (2 |^ n)) by XREAL_1: 64;

      then

       A5: (((pW / EW) * (2 |^ n)) + 3) <= ((2 |^ n) + 3) by XREAL_1: 7;

      I <= (((pW / EW) * (2 |^ n)) + 2) by A2, INT_1:def 6;

      then

       A6: (I + 1) <= ((((pW / EW) * (2 |^ n)) + 2) + 1) by XREAL_1: 6;

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

      hence thesis by A5, A6, XXREAL_0: 2;

    end;

    theorem :: JORDAN1C:12

    

     Th12: for C be compact non horizontal Subset of ( TOP-REAL 2) holds for J be Integer st p in ( BDD C) & J = [\(((((p `2 ) - ( S-bound C)) / (( N-bound C) - ( S-bound C))) * (2 |^ n)) + 2)/] holds 1 < J & (J + 1) <= ( width ( Gauge (C,n)))

    proof

      let C be compact non horizontal Subset of ( TOP-REAL 2);

      set W = ( S-bound C), E = ( N-bound C);

      set EW = (E - W), pW = ((p `2 ) - W);

      let I be Integer;

      assume that

       A1: p in ( BDD C) and

       A2: I = [\(((pW / EW) * (2 |^ n)) + 2)/];

      

       A3: EW > 0 by SPRECT_1: 32, XREAL_1: 50;

      set K = [\((pW / EW) * (2 |^ n))/];

      (((pW / EW) * (2 |^ n)) - 1) < K by INT_1:def 6;

      then

       A4: ((((pW / EW) * (2 |^ n)) - 1) + 2) < (K + 2) by XREAL_1: 6;

      

       A5: W <= ( S-bound ( BDD C)) by A1, Th8;

      ( BDD C) is bounded by JORDAN2C: 106;

      then (p `2 ) >= ( S-bound ( BDD C)) by A1, Th5;

      then (p `2 ) >= W by A5, XXREAL_0: 2;

      then pW >= 0 by XREAL_1: 48;

      then (((pW / EW) * (2 |^ n)) + 1) >= ( 0 + 1) by A3, XREAL_1: 6;

      then 1 < (K + 2) by A4, XXREAL_0: 2;

      hence 1 < I by A2, INT_1: 28;

      

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

      

       A7: E >= ( N-bound ( BDD C)) by A1, Th9;

      ( BDD C) is bounded by JORDAN2C: 106;

      then (p `2 ) <= ( N-bound ( BDD C)) by A1, Th5;

      then (p `2 ) <= E by A7, XXREAL_0: 2;

      then ((p `2 ) - W) <= EW by XREAL_1: 9;

      then (pW / EW) <= 1 by A3, XREAL_1: 185;

      then ((pW / EW) * (2 |^ n)) <= (1 * (2 |^ n)) by XREAL_1: 64;

      then

       A8: (((pW / EW) * (2 |^ n)) + 3) <= ((2 |^ n) + 3) by XREAL_1: 7;

      I <= (((pW / EW) * (2 |^ n)) + 2) by A2, INT_1:def 6;

      then

       A9: (I + 1) <= ((((pW / EW) * (2 |^ n)) + 2) + 1) by XREAL_1: 6;

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

      hence thesis by A6, A8, A9, XXREAL_0: 2;

    end;

    theorem :: JORDAN1C:13

    

     Th13: for I be Integer st I = [\(((((p `1 ) - ( W-bound C)) / (( E-bound C) - ( W-bound C))) * (2 |^ n)) + 2)/] holds (( W-bound C) + (((( E-bound C) - ( W-bound C)) / (2 |^ n)) * (I - 2))) <= (p `1 )

    proof

      set W = ( W-bound C), EW = (( E-bound C) - ( W-bound C));

      set PW = ((p `1 ) - W);

      set KI = [\((PW / EW) * (2 |^ n))/];

      let I be Integer;

      

       A1: EW > 0 by TOPREAL5: 17, XREAL_1: 50;

      (2 |^ n) > 0 by NEWTON: 83;

      then

       A2: ((EW / (2 |^ n)) * ((PW / EW) * (2 |^ n))) = PW by A1, Lm2;

      assume I = [\(((PW / EW) * (2 |^ n)) + 2)/];

      then

       A3: (I - 2) = [\((PW / EW) * (2 |^ n))/] by Lm1;

      KI <= ((PW / EW) * (2 |^ n)) by INT_1:def 6;

      then

       A4: ((EW / (2 |^ n)) * KI) <= ((EW / (2 |^ n)) * ((PW / EW) * (2 |^ n))) by A1, XREAL_1: 64;

      (W + PW) = (p `1 );

      hence thesis by A3, A2, A4, XREAL_1: 6;

    end;

    theorem :: JORDAN1C:14

    

     Th14: for I be Integer st I = [\(((((p `1 ) - ( W-bound C)) / (( E-bound C) - ( W-bound C))) * (2 |^ n)) + 2)/] holds (p `1 ) < (( W-bound C) + (((( E-bound C) - ( W-bound C)) / (2 |^ n)) * (I - 1)))

    proof

      set W = ( W-bound C), E = ( E-bound C);

      set EW = (E - W), PW = ((p `1 ) - W);

      let I be Integer;

      set KI = (I - 1);

      

       A1: (2 |^ n) > 0 by NEWTON: 83;

      assume I = [\(((PW / EW) * (2 |^ n)) + 2)/];

      then I > ((((PW / EW) * (2 |^ n)) + 2) - 1) by INT_1:def 6;

      then

       A2: (I - 1) > ((((PW / EW) * (2 |^ n)) + 1) - 1) by XREAL_1: 9;

      

       A3: EW > 0 by TOPREAL5: 17, XREAL_1: 50;

      then (EW / (2 |^ n)) > 0 by A1, XREAL_1: 139;

      then

       A4: ((EW / (2 |^ n)) * KI) > ((EW / (2 |^ n)) * ((PW / EW) * (2 |^ n))) by A2, XREAL_1: 68;

      

       A5: (W + PW) = (p `1 );

      ((EW / (2 |^ n)) * ((PW / EW) * (2 |^ n))) = PW by A3, A1, Lm2;

      hence thesis by A5, A4, XREAL_1: 6;

    end;

    theorem :: JORDAN1C:15

    

     Th15: for J be Integer st J = [\(((((p `2 ) - ( S-bound C)) / (( N-bound C) - ( S-bound C))) * (2 |^ n)) + 2)/] holds (( S-bound C) + (((( N-bound C) - ( S-bound C)) / (2 |^ n)) * (J - 2))) <= (p `2 )

    proof

      set W = ( S-bound C), EW = (( N-bound C) - ( S-bound C));

      set PW = ((p `2 ) - W);

      set KI = [\((PW / EW) * (2 |^ n))/];

      let I be Integer;

      

       A1: EW > 0 by TOPREAL5: 16, XREAL_1: 50;

      (2 |^ n) > 0 by NEWTON: 83;

      then

       A2: ((EW / (2 |^ n)) * ((PW / EW) * (2 |^ n))) = PW by A1, Lm2;

      assume I = [\(((PW / EW) * (2 |^ n)) + 2)/];

      then

       A3: (I - 2) = [\((PW / EW) * (2 |^ n))/] by Lm1;

      KI <= ((PW / EW) * (2 |^ n)) by INT_1:def 6;

      then

       A4: ((EW / (2 |^ n)) * KI) <= ((EW / (2 |^ n)) * ((PW / EW) * (2 |^ n))) by A1, XREAL_1: 64;

      (W + PW) = (p `2 );

      hence thesis by A3, A2, A4, XREAL_1: 6;

    end;

    theorem :: JORDAN1C:16

    

     Th16: for J be Integer st J = [\(((((p `2 ) - ( S-bound C)) / (( N-bound C) - ( S-bound C))) * (2 |^ n)) + 2)/] holds (p `2 ) < (( S-bound C) + (((( N-bound C) - ( S-bound C)) / (2 |^ n)) * (J - 1)))

    proof

      set W = ( S-bound C), E = ( N-bound C);

      set EW = (E - W), PW = ((p `2 ) - W);

      let I be Integer;

      set KI = (I - 1);

      

       A1: (2 |^ n) > 0 by NEWTON: 83;

      assume I = [\(((PW / EW) * (2 |^ n)) + 2)/];

      then I > ((((PW / EW) * (2 |^ n)) + 2) - 1) by INT_1:def 6;

      then

       A2: (I - 1) > ((((PW / EW) * (2 |^ n)) + 1) - 1) by XREAL_1: 9;

      

       A3: (W + PW) = (p `2 );

      

       A4: EW > 0 by TOPREAL5: 16, XREAL_1: 50;

      then

       A5: (EW / (2 |^ n)) > 0 by A1, XREAL_1: 139;

      ((EW / (2 |^ n)) * ((PW / EW) * (2 |^ n))) = PW by A4, A1, Lm2;

      then ((EW / (2 |^ n)) * KI) > PW by A2, A5, XREAL_1: 68;

      hence thesis by A3, XREAL_1: 6;

    end;

    theorem :: JORDAN1C:17

    

     Th17: for C be closed Subset of ( TOP-REAL 2), p be Point of ( Euclid 2) st p in ( BDD C) holds ex r be Real st r > 0 & ( Ball (p,r)) c= ( BDD C)

    proof

      let C be closed Subset of ( TOP-REAL 2), p be Point of ( Euclid 2);

      set W = ( Int ( BDD C));

      assume p in ( BDD C);

      then p in W by TOPS_1: 23;

      then

      consider r be Real such that

       A1: r > 0 and

       A2: ( Ball (p,r)) c= ( BDD C) by GOBOARD6: 5;

      reconsider r as Real;

      take r;

      thus thesis by A1, A2;

    end;

    theorem :: JORDAN1C:18

    for p,q be Point of ( TOP-REAL 2), r be Real st ( dist ((( Gauge (C,n)) * (1,1)),(( Gauge (C,n)) * (1,2)))) < r & ( dist ((( Gauge (C,n)) * (1,1)),(( Gauge (C,n)) * (2,1)))) < r & p in ( cell (( Gauge (C,n)),i,j)) & q in ( cell (( Gauge (C,n)),i,j)) & 1 <= i & (i + 1) <= ( len ( Gauge (C,n))) & 1 <= j & (j + 1) <= ( width ( Gauge (C,n))) holds ( dist (p,q)) < (2 * r)

    proof

      set G = ( Gauge (C,n));

      let p,q be Point of ( TOP-REAL 2), r be Real;

      assume that

       A1: ( dist ((G * (1,1)),(G * (1,2)))) < r and

       A2: ( dist ((G * (1,1)),(G * (2,1)))) < r and

       A3: p in ( cell (G,i,j)) and

       A4: q in ( cell (G,i,j)) and

       A5: 1 <= i and

       A6: (i + 1) <= ( len G) and

       A7: 1 <= j and

       A8: (j + 1) <= ( width G);

      

       A9: (p `1 ) <= ((G * ((i + 1),j)) `1 ) by A3, A5, A6, A7, A8, JORDAN9: 17;

      

       A10: (p `2 ) <= ((G * (i,(j + 1))) `2 ) by A3, A5, A6, A7, A8, JORDAN9: 17;

      

       A11: ((G * (i,j)) `2 ) <= (p `2 ) by A3, A5, A6, A7, A8, JORDAN9: 17;

      j <= (j + 1) by NAT_1: 11;

      then

       A12: j <= ( width G) by A8, XXREAL_0: 2;

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

      then

       A13: i <= ( len G) by A6, XXREAL_0: 2;

      then

       A14: [i, j] in ( Indices G) by A5, A7, A12, MATRIX_0: 30;

      

       A15: (q `2 ) <= ((G * (i,(j + 1))) `2 ) by A4, A5, A6, A7, A8, JORDAN9: 17;

      

       A16: ((G * (i,j)) `2 ) <= (q `2 ) by A4, A5, A6, A7, A8, JORDAN9: 17;

      

       A17: (q `1 ) <= ((G * ((i + 1),j)) `1 ) by A4, A5, A6, A7, A8, JORDAN9: 17;

      

       A18: ((G * (i,j)) `1 ) <= (q `1 ) by A4, A5, A6, A7, A8, JORDAN9: 17;

      1 <= (j + 1) by NAT_1: 11;

      then [i, (j + 1)] in ( Indices G) by A5, A8, A13, MATRIX_0: 30;

      then

       A19: (((G * (i,(j + 1))) `2 ) - ((G * (i,j)) `2 )) < r by A1, A14, Th2;

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

      then [(i + 1), j] in ( Indices G) by A6, A7, A12, MATRIX_0: 30;

      then (((G * ((i + 1),j)) `1 ) - ((G * (i,j)) `1 )) < r by A2, A14, Th1;

      then

       A20: ((((G * ((i + 1),j)) `1 ) - ((G * (i,j)) `1 )) + (((G * (i,(j + 1))) `2 ) - ((G * (i,j)) `2 ))) < (r + r) by A19, XREAL_1: 8;

      ((G * (i,j)) `1 ) <= (p `1 ) by A3, A5, A6, A7, A8, JORDAN9: 17;

      then ( dist (p,q)) <= ((((G * ((i + 1),j)) `1 ) - ((G * (i,j)) `1 )) + (((G * (i,(j + 1))) `2 ) - ((G * (i,j)) `2 ))) by A9, A11, A10, A18, A17, A16, A15, TOPREAL6: 95;

      hence thesis by A20, XXREAL_0: 2;

    end;

    theorem :: JORDAN1C:19

    for C be compact Subset of ( TOP-REAL 2) holds p in ( BDD C) implies (p `2 ) <> ( N-bound ( BDD C))

    proof

      reconsider P = p as Point of ( Euclid 2) by Lm3;

      let C be compact Subset of ( TOP-REAL 2);

      

       A1: ( BDD C) is bounded by JORDAN2C: 106;

      assume p in ( BDD C);

      then

      consider r be Real such that

       A2: r > 0 and

       A3: ( Ball (P,r)) c= ( BDD C) by Th17;

      set EX = |[(p `1 ), ((p `2 ) + (r / 2))]|;

       0 < (r / 2) by A2, XREAL_1: 139;

      then

       A4: ((p `2 ) + (r / 2)) > ((p `2 ) + 0 ) by XREAL_1: 6;

      assume

       A5: (p `2 ) = ( N-bound ( BDD C));

      

       A6: not EX in ( BDD C)

      proof

        assume EX in ( BDD C);

        then (EX `2 ) <= ( N-bound ( BDD C)) by A1, Th5;

        hence thesis by A5, A4, EUCLID: 52;

      end;

      

       A7: P = |[(p `1 ), (p `2 )]| by EUCLID: 53;

      (r / 2) < r by A2, XREAL_1: 216;

      then EX in ( Ball (P,r)) by A2, A7, GOBOARD6: 8;

      hence thesis by A3, A6;

    end;

    theorem :: JORDAN1C:20

    for C be compact Subset of ( TOP-REAL 2) holds p in ( BDD C) implies (p `1 ) <> ( E-bound ( BDD C))

    proof

      reconsider P = p as Point of ( Euclid 2) by Lm3;

      let C be compact Subset of ( TOP-REAL 2);

      

       A1: ( BDD C) is bounded by JORDAN2C: 106;

      assume p in ( BDD C);

      then

      consider r be Real such that

       A2: r > 0 and

       A3: ( Ball (P,r)) c= ( BDD C) by Th17;

      set EX = |[((p `1 ) + (r / 2)), (p `2 )]|;

       0 < (r / 2) by A2, XREAL_1: 139;

      then

       A4: ((p `1 ) + (r / 2)) > ((p `1 ) + 0 ) by XREAL_1: 6;

      assume

       A5: (p `1 ) = ( E-bound ( BDD C));

      

       A6: not EX in ( BDD C)

      proof

        assume EX in ( BDD C);

        then (EX `1 ) <= ( E-bound ( BDD C)) by A1, Th5;

        hence thesis by A5, A4, EUCLID: 52;

      end;

      

       A7: P = |[(p `1 ), (p `2 )]| by EUCLID: 53;

      (r / 2) < r by A2, XREAL_1: 216;

      then EX in ( Ball (P,r)) by A2, A7, GOBOARD6: 7;

      hence thesis by A3, A6;

    end;

    theorem :: JORDAN1C:21

    for C be compact Subset of ( TOP-REAL 2) holds p in ( BDD C) implies (p `2 ) <> ( S-bound ( BDD C))

    proof

      reconsider P = p as Point of ( Euclid 2) by Lm3;

      let C be compact Subset of ( TOP-REAL 2);

      

       A1: ( BDD C) is bounded by JORDAN2C: 106;

      assume p in ( BDD C);

      then

      consider r be Real such that

       A2: r > 0 and

       A3: ( Ball (P,r)) c= ( BDD C) by Th17;

      set EX = |[(p `1 ), ((p `2 ) - (r / 2))]|;

       0 < (r / 2) by A2, XREAL_1: 139;

      then ((p `2 ) + (r / 2)) > ((p `2 ) + 0 ) by XREAL_1: 6;

      then

       A4: ((p `2 ) - (r / 2)) < (p `2 ) by XREAL_1: 19;

      assume

       A5: (p `2 ) = ( S-bound ( BDD C));

      

       A6: not EX in ( BDD C)

      proof

        assume EX in ( BDD C);

        then (EX `2 ) >= ( S-bound ( BDD C)) by A1, Th5;

        hence thesis by A5, A4, EUCLID: 52;

      end;

      

       A7: P = |[(p `1 ), (p `2 )]| by EUCLID: 53;

      (r / 2) < r by A2, XREAL_1: 216;

      then EX in ( Ball (P,r)) by A2, A7, GOBOARD6: 10;

      hence thesis by A3, A6;

    end;

    theorem :: JORDAN1C:22

    

     Th22: for C be compact Subset of ( TOP-REAL 2) holds p in ( BDD C) implies (p `1 ) <> ( W-bound ( BDD C))

    proof

      reconsider P = p as Point of ( Euclid 2) by Lm3;

      let C be compact Subset of ( TOP-REAL 2);

      

       A1: ( BDD C) is bounded by JORDAN2C: 106;

      assume p in ( BDD C);

      then

      consider r be Real such that

       A2: r > 0 and

       A3: ( Ball (P,r)) c= ( BDD C) by Th17;

      set EX = |[((p `1 ) - (r / 2)), (p `2 )]|;

       0 < (r / 2) by A2, XREAL_1: 139;

      then ((p `1 ) + (r / 2)) > ((p `1 ) + 0 ) by XREAL_1: 6;

      then

       A4: ((p `1 ) - (r / 2)) < (p `1 ) by XREAL_1: 19;

      assume

       A5: (p `1 ) = ( W-bound ( BDD C));

      

       A6: not EX in ( BDD C)

      proof

        assume EX in ( BDD C);

        then (EX `1 ) >= ( W-bound ( BDD C)) by A1, Th5;

        hence thesis by A5, A4, EUCLID: 52;

      end;

      

       A7: P = |[(p `1 ), (p `2 )]| by EUCLID: 53;

      (r / 2) < r by A2, XREAL_1: 216;

      then EX in ( Ball (P,r)) by A2, A7, GOBOARD6: 9;

      hence thesis by A3, A6;

    end;

    theorem :: JORDAN1C:23

    p in ( BDD C) implies ex n,i,j be Nat st 1 < i & i < ( len ( Gauge (C,n))) & 1 < j & j < ( width ( Gauge (C,n))) & (p `1 ) <> ((( Gauge (C,n)) * (i,j)) `1 ) & p in ( cell (( Gauge (C,n)),i,j)) & ( cell (( Gauge (C,n)),i,j)) c= ( BDD C)

    proof

      reconsider P = p as Point of ( Euclid 2) by Lm3;

      set W = ( W-bound C), E = ( E-bound C), S = ( S-bound C), N = ( N-bound C);

      set EW = (E - W), NS = (N - S);

      assume

       A1: p in ( BDD C);

      then

      consider r be Real such that

       A2: r > 0 and

       A3: ( Ball (P,r)) c= ( BDD C) by Th17;

      set l = (r / 4);

      l > 0 by A2, XREAL_1: 139;

      then

      consider n be Nat such that 1 < n and

       A4: ( dist ((( Gauge (C,n)) * (1,1)),(( Gauge (C,n)) * (1,2)))) < l and

       A5: ( dist ((( Gauge (C,n)) * (1,1)),(( Gauge (C,n)) * (2,1)))) < l by GOBRD14: 11;

      set I = [\(((((p `1 ) - W) / EW) * (2 |^ n)) + 2)/], J = [\(((((p `2 ) - S) / NS) * (2 |^ n)) + 2)/];

      

       A6: 1 < J by A1, Th12;

      set G = ( Gauge (C,n));

      

       A7: (I + 1) <= ( len G) by A1, Th11;

      

       A8: (J + 1) <= ( width G) by A1, Th12;

      take n;

      

       A9: 1 < I by A1, Th10;

      then

      reconsider I, J as Element of NAT by A6, INT_1: 3;

      

       A10: I < (I + 1) by XREAL_1: 29;

      then

       A11: I <= ( len G) by A7, XXREAL_0: 2;

      1 <= (J + 1) by NAT_1: 11;

      then [I, (J + 1)] in ( Indices G) by A9, A8, A11, MATRIX_0: 30;

      then (G * (I,(J + 1))) = |[(W + ((EW / (2 |^ n)) * (I - 2))), (S + ((NS / (2 |^ n)) * ((J + 1) - 2)))]| by JORDAN8:def 1;

      then

       A12: ((G * (I,(J + 1))) `2 ) = (S + ((NS / (2 |^ n)) * (J - 1))) by EUCLID: 52;

      then

       A13: (p `2 ) < ((G * (I,(J + 1))) `2 ) by Th16;

      

       A14: J < (J + 1) by XREAL_1: 29;

      then

       A15: J <= ( width G) by A8, XXREAL_0: 2;

      then [I, J] in ( Indices G) by A9, A6, A11, MATRIX_0: 30;

      then

       A16: (G * (I,J)) = |[(W + ((EW / (2 |^ n)) * (I - 2))), (S + ((NS / (2 |^ n)) * (J - 2)))]| by JORDAN8:def 1;

      then ((G * (I,J)) `1 ) = (W + ((EW / (2 |^ n)) * (I - 2))) by EUCLID: 52;

      then

       A17: ((G * (I,J)) `1 ) <= (p `1 ) by Th13;

      1 <= (I + 1) by NAT_1: 11;

      then [(I + 1), J] in ( Indices G) by A7, A6, A15, MATRIX_0: 30;

      then (G * ((I + 1),J)) = |[(W + ((EW / (2 |^ n)) * ((I + 1) - 2))), (S + ((NS / (2 |^ n)) * (J - 2)))]| by JORDAN8:def 1;

      then ((G * ((I + 1),J)) `1 ) = (W + ((EW / (2 |^ n)) * (I - 1))) by EUCLID: 52;

      then

       A18: (p `1 ) < ((G * ((I + 1),J)) `1 ) by Th14;

      ((G * (I,J)) `2 ) = (S + ((NS / (2 |^ n)) * (J - 2))) by A16, EUCLID: 52;

      then

       A19: ((G * (I,J)) `2 ) <= (p `2 ) by Th15;

      

       A20: (S + ((NS / (2 |^ n)) * (J - 1))) > (p `2 ) by Th16;

      then

       A21: p in ( cell (G,I,J)) by A9, A7, A6, A8, A17, A19, A18, A12, JORDAN9: 17;

      per cases ;

        suppose

         A22: (p `1 ) <> ((G * (I,J)) `1 );

        take I, J;

        thus 1 < I & I < ( len G) & 1 < J & J < ( width G) by A1, A7, A8, A10, A14, Th10, Th12, XXREAL_0: 2;

        ( cell (G,I,J)) c= ( Ball (P,r)) by A2, A4, A5, A9, A7, A6, A8, A21, Lm6;

        hence thesis by A3, A9, A7, A6, A8, A20, A17, A19, A18, A12, A22, JORDAN9: 17;

      end;

        suppose

         A23: (p `1 ) = ((G * (I,J)) `1 );

        then

         A24: (p `1 ) <= ((G * (((I -' 1) + 1),J)) `1 ) by A9, XREAL_1: 235;

        

         A25: ((I -' 1) + 1) <= ( len G) by A9, A11, XREAL_1: 235;

        

         A26: 1 <= J by A1, Th12;

        

         A27: 1 <= (I -' 1) by A1, Th10, NAT_D: 49;

        then (I -' 1) < I by NAT_D: 51;

        then

         A28: (p `1 ) > ((G * ((I -' 1),J)) `1 ) by A11, A15, A23, A27, A26, GOBOARD5: 3;

        take (I -' 1), J;

        

         A29: (J + 1) <= ( width G) by A1, Th12;

        

         A30: 1 <= (I -' 1) by A1, Th10, NAT_D: 49;

        then

         A31: (I -' 1) < I by NAT_D: 51;

        ( len G) = ( width G) by JORDAN8:def 1;

        then

         A32: J <= ( len G) by A8, A14, XXREAL_0: 2;

        (I -' 1) <> 1

        proof

          assume (I -' 1) = 1;

          then 1 = (I - 1) by NAT_D: 39;

          then ((G * (I,J)) `1 ) = ( W-bound C) by A6, A32, JORDAN8: 11;

          then (p `1 ) <= ( W-bound ( BDD C)) by A1, A23, Th6;

          then

           A33: (p `1 ) < ( W-bound ( BDD C)) by A1, Th22, XXREAL_0: 1;

          ( BDD C) is bounded by JORDAN2C: 106;

          hence thesis by A1, A33, Th5;

        end;

        hence 1 < (I -' 1) & (I -' 1) < ( len G) & 1 < J & J < ( width G) by A1, A14, A11, A30, A29, A31, Th12, XXREAL_0: 1, XXREAL_0: 2;

        

         A34: ((I -' 1) + 1) <= ( len G) by A9, A11, XREAL_1: 235;

        

         A35: (J + 1) <= ( width G) by A1, Th12;

        

         A36: (p `1 ) <= ((G * (((I -' 1) + 1),J)) `1 ) by A9, A23, XREAL_1: 235;

        

         A37: 1 <= J by A1, Th12;

        

         A38: ((I -' 1) + 1) = I by A9, XREAL_1: 235;

        then

         A39: ((G * ((I -' 1),J)) `2 ) = ((G * (I,J)) `2 ) by A11, A30, A37, A29, JORDAN9: 16;

        

         A40: ((G * ((I -' 1),(J + 1))) `2 ) = ((G * (I,(J + 1))) `2 ) by A11, A38, A30, A37, A29, JORDAN9: 16;

        (p `1 ) > ((G * ((I -' 1),J)) `1 ) by A11, A15, A23, A30, A37, A31, GOBOARD5: 3;

        then p in ( cell (G,(I -' 1),J)) by A19, A13, A30, A34, A37, A29, A36, A39, A40, JORDAN9: 17;

        then ( cell (G,(I -' 1),J)) c= ( Ball (P,r)) by A2, A4, A5, A27, A25, A26, A35, Lm6;

        hence thesis by A3, A19, A13, A39, A40, A27, A25, A26, A35, A24, A28, JORDAN9: 17;

      end;

    end;

    theorem :: JORDAN1C:24

    for C be Subset of ( TOP-REAL 2) st C is bounded holds ( UBD C) is non empty by Lm13;