gobrd14.miz



    begin

    reserve i,j,n for Nat,

f for non constant standard special_circular_sequence,

g for clockwise_oriented non constant standard special_circular_sequence,

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

P for Subset of ( TOP-REAL 2),

C for compact non vertical non horizontal Subset of ( TOP-REAL 2),

G for Go-board;

    

     Lm1: the carrier of ( TOP-REAL 2) = ( REAL 2) by EUCLID: 22;

    theorem :: GOBRD14:1

    for p be Point of ( Euclid 2) st p = ( 0.REAL 2) & P is_outside_component_of ( L~ f) holds ex r be Real st r > 0 & (( Ball (p,r)) ` ) c= P

    proof

      let p be Point of ( Euclid 2) such that

       A1: p = ( 0.REAL 2) and

       A2: P is_outside_component_of ( L~ f);

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

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

       A3: 0 < r and c in D and

       A4: for z be Point of ( Euclid 2) st z in D holds ( dist (c,z)) <= r by TBSP_1: 10;

      set rr = ((( dist (p,c)) + r) + 1);

      take rr;

      set L = (( REAL 2) \ { a where a be Point of ( TOP-REAL 2) : |.a.| < rr });

      ((( dist (p,c)) + r) + 0 ) < rr by XREAL_1: 8;

      hence 0 < rr by A3, METRIC_1: 5, XREAL_1: 8;

      then rr = |.rr.| by ABSVALUE:def 1;

      then for a be Point of ( TOP-REAL 2) holds a <> |[ 0 , rr]| or |.a.| >= rr by TOPREAL6: 23;

      then not |[ 0 , rr]| in { a where a be Point of ( TOP-REAL 2) : |.a.| < rr };

      then

      reconsider L as non empty Subset of ( TOP-REAL 2) by Lm1, XBOOLE_0:def 5;

      let x be object;

      assume

       A5: x in (( Ball (p,rr)) ` );

      then

      reconsider y = x as Point of ( Euclid 2);

      reconsider z = y as Point of ( TOP-REAL 2) by EUCLID: 22;

      

       A6: ( dist (p,y)) = |.z.| by A1, TOPREAL6: 25;

      

       A7: D c= ( Ball (p,rr))

      proof

        let x be object;

        

         A8: ((( dist (p,c)) + r) + 0 ) < ((( dist (p,c)) + r) + 1) by XREAL_1: 6;

        assume

         A9: x in D;

        then

        reconsider z = x as Point of ( Euclid 2);

        ( dist (c,z)) <= r by A4, A9;

        then

         A10: (( dist (p,c)) + ( dist (c,z))) <= (( dist (p,c)) + r) by XREAL_1: 7;

        ( dist (p,z)) <= (( dist (p,c)) + ( dist (c,z))) by METRIC_1: 4;

        then ( dist (p,z)) <= (( dist (p,c)) + r) by A10, XXREAL_0: 2;

        then ( dist (p,z)) < ((( dist (p,c)) + r) + 1) by A8, XXREAL_0: 2;

        hence thesis by METRIC_1: 11;

      end;

      

       A11: L c= (( L~ f) ` )

      proof

        let l be object;

        assume

         A12: l in L;

        then

        reconsider j = l as Point of ( TOP-REAL 2);

        reconsider t = j as Point of ( Euclid 2) by EUCLID: 22;

         not l in { a where a be Point of ( TOP-REAL 2) : |.a.| < rr } by A12, XBOOLE_0:def 5;

        then

         A13: |.j.| >= rr;

        now

          assume l in ( L~ f);

          then ( dist (t,p)) < rr by A7, METRIC_1: 11;

          hence contradiction by A1, A13, TOPREAL6: 25;

        end;

        hence thesis by A12, SUBSET_1: 29;

      end;

      L is connected by JORDAN2C: 53;

      then

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

       A14: M is_a_component_of (( L~ f) ` ) and

       A15: L c= M by A11, GOBOARD9: 3;

      M is_outside_component_of ( L~ f)

      proof

        reconsider W = L as Subset of ( Euclid 2);

        thus M is_a_component_of (( L~ f) ` ) by A14;

         not W is bounded by JORDAN2C: 62;

        then not L is bounded by JORDAN2C: 11;

        hence thesis by A15, RLTOPSP1: 42;

      end;

      then

       A16: M in { W where W be Subset of ( TOP-REAL 2) : W is_outside_component_of ( L~ f) };

       not x in ( Ball (p,rr)) by A5, XBOOLE_0:def 5;

      then for k be Point of ( TOP-REAL 2) holds k <> z or |.k.| >= rr by A6, METRIC_1: 11;

      then z in ( REAL 2) & not x in { a where a be Point of ( TOP-REAL 2) : |.a.| < rr };

      then

       A17: x in L by XBOOLE_0:def 5;

      ( UBD ( L~ f)) is_outside_component_of ( L~ f) by JORDAN2C: 68;

      then P = ( UBD ( L~ f)) by A2, JORDAN2C: 119;

      hence thesis by A17, A15, A16, TARSKI:def 4;

    end;

    begin

    theorem :: GOBRD14:2

    for f be FinSequence of ( TOP-REAL n) st ( L~ f) <> {} holds 2 <= ( len f)

    proof

      let f be FinSequence of ( TOP-REAL n);

      assume ( L~ f) <> {} ;

      then ( len f) <> 0 & ( len f) <> 1 by TOPREAL1: 22;

      then ( len f) > 1 by NAT_1: 25;

      then ( len f) >= (1 + 1) by NAT_1: 13;

      hence thesis;

    end;

    theorem :: GOBRD14:3

    

     Th3: 1 <= i & i < ( len G) & 1 <= j & j < ( width G) implies ( cell (G,i,j)) = ( product ((1,2) --> ( [.((G * (i,1)) `1 ), ((G * ((i + 1),1)) `1 ).], [.((G * (1,j)) `2 ), ((G * (1,(j + 1))) `2 ).])))

    proof

      

       A1: [.((G * (1,j)) `2 ), ((G * (1,(j + 1))) `2 ).] = { b where b be Real : ((G * (1,j)) `2 ) <= b & b <= ((G * (1,(j + 1))) `2 ) } by RCOMP_1:def 1;

      set f = ((1,2) --> ( [.((G * (i,1)) `1 ), ((G * ((i + 1),1)) `1 ).], [.((G * (1,j)) `2 ), ((G * (1,(j + 1))) `2 ).]));

      

       A2: ( dom f) = {1, 2} by FUNCT_4: 62;

      assume 1 <= i & i < ( len G) & 1 <= j & j < ( width G);

      then

       A3: ( cell (G,i,j)) = { |[r, s]| where r,s be Real : ((G * (i,1)) `1 ) <= r & r <= ((G * ((i + 1),1)) `1 ) & ((G * (1,j)) `2 ) <= s & s <= ((G * (1,(j + 1))) `2 ) } by GOBRD11: 32;

      

       A4: [.((G * (i,1)) `1 ), ((G * ((i + 1),1)) `1 ).] = { a where a be Real : ((G * (i,1)) `1 ) <= a & a <= ((G * ((i + 1),1)) `1 ) } by RCOMP_1:def 1;

      thus ( cell (G,i,j)) c= ( product f)

      proof

        let c be object;

        assume c in ( cell (G,i,j));

        then

        consider r,s be Real such that

         A5: c = |[r, s]| and

         A6: ((G * (i,1)) `1 ) <= r & r <= ((G * ((i + 1),1)) `1 ) & ((G * (1,j)) `2 ) <= s & s <= ((G * (1,(j + 1))) `2 ) by A3;

        

         A7: r in [.((G * (i,1)) `1 ), ((G * ((i + 1),1)) `1 ).] & s in [.((G * (1,j)) `2 ), ((G * (1,(j + 1))) `2 ).] by A4, A1, A6;

        

         A8: for x be object st x in ( dom f) holds ( <*r, s*> . x) in (f . x)

        proof

          let x be object;

          

           A9: s = ( |[r, s]| `2 ) by EUCLID: 52

          .= ( <*r, s*> . 2);

          assume x in ( dom f);

          then

           A10: x = 1 or x = 2 by TARSKI:def 2;

          r = ( |[r, s]| `1 ) by EUCLID: 52

          .= ( <*r, s*> . 1);

          hence thesis by A7, A10, A9, FUNCT_4: 63;

        end;

        ( dom <*r, s*>) = {1, 2} by FINSEQ_1: 2, FINSEQ_1: 89;

        hence thesis by A2, A5, A8, CARD_3: 9;

      end;

      let c be object;

      assume c in ( product f);

      then

      consider g be Function such that

       A11: c = g and

       A12: ( dom g) = ( dom f) and

       A13: for x be object st x in ( dom f) holds (g . x) in (f . x) by CARD_3:def 5;

      2 in ( dom f) by A2, TARSKI:def 2;

      then (g . 2) in (f . 2) by A13;

      then (g . 2) in [.((G * (1,j)) `2 ), ((G * (1,(j + 1))) `2 ).] by FUNCT_4: 63;

      then

      consider b be Real such that

       A14: (g . 2) = b and

       A15: ((G * (1,j)) `2 ) <= b & b <= ((G * (1,(j + 1))) `2 ) by A1;

      1 in ( dom f) by A2, TARSKI:def 2;

      then (g . 1) in (f . 1) by A13;

      then (g . 1) in [.((G * (i,1)) `1 ), ((G * ((i + 1),1)) `1 ).] by FUNCT_4: 63;

      then

      consider a be Real such that

       A16: (g . 1) = a and

       A17: ((G * (i,1)) `1 ) <= a & a <= ((G * ((i + 1),1)) `1 ) by A4;

      

       A18: for k be object st k in ( dom g) holds (g . k) = ( <*a, b*> . k)

      proof

        let k be object;

        assume k in ( dom g);

        then k = 1 or k = 2 by A12, TARSKI:def 2;

        hence thesis by A16, A14, FINSEQ_1: 44;

      end;

      ( dom <*a, b*>) = {1, 2} by FINSEQ_1: 2, FINSEQ_1: 89;

      then c = |[a, b]| by A11, A12, A18, FUNCT_1: 2, FUNCT_4: 62;

      hence thesis by A3, A17, A15;

    end;

    theorem :: GOBRD14:4

    1 <= i & i < ( len G) & 1 <= j & j < ( width G) implies ( cell (G,i,j)) is compact

    proof

      assume 1 <= i & i < ( len G) & 1 <= j & j < ( width G);

      then ( cell (G,i,j)) = ( product ((1,2) --> ( [.((G * (i,1)) `1 ), ((G * ((i + 1),1)) `1 ).], [.((G * (1,j)) `2 ), ((G * (1,(j + 1))) `2 ).]))) by Th3;

      hence thesis by TOPREAL6: 78;

    end;

    theorem :: GOBRD14:5

     [i, j] in ( Indices G) & [(i + n), j] in ( Indices G) implies ( dist ((G * (i,j)),(G * ((i + n),j)))) = (((G * ((i + n),j)) `1 ) - ((G * (i,j)) `1 ))

    proof

      assume that

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

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

      set x = (G * (i,j)), y = (G * ((i + n),j));

      per cases ;

        suppose n = 0 ;

        hence thesis by TOPREAL6: 93;

      end;

        suppose

         A3: n <> 0 ;

        

         A4: (i + n) <= ( len G) by A2, MATRIX_0: 32;

        

         A5: 1 <= i by A1, MATRIX_0: 32;

        

         A6: 1 <= (i + n) by A2, MATRIX_0: 32;

        

         A7: 1 <= j & j <= ( width G) by A1, MATRIX_0: 32;

        1 <= n by A3, NAT_1: 14;

        then i < (i + n) by NAT_1: 19;

        then (x `1 ) < (y `1 ) by A4, A7, A5, GOBOARD5: 3;

        then

         A8: ((x `1 ) - (x `1 )) < ((y `1 ) - (x `1 )) by XREAL_1: 14;

        i <= ( len G) by A1, MATRIX_0: 32;

        

        then

         A9: (x `2 ) = ((G * (1,j)) `2 ) by A7, A5, GOBOARD5: 1

        .= (y `2 ) by A6, A4, A7, GOBOARD5: 1;

        

        thus ( dist ((G * (i,j)),(G * ((i + n),j)))) = ( sqrt ((((x `1 ) - (y `1 )) ^2 ) + (((x `2 ) - (y `2 )) ^2 ))) by TOPREAL6: 92

        .= |.((x `1 ) - (y `1 )).| by A9, COMPLEX1: 72

        .= |.( - ((x `1 ) - (y `1 ))).| by COMPLEX1: 52

        .= (((G * ((i + n),j)) `1 ) - ((G * (i,j)) `1 )) by A8, ABSVALUE:def 1;

      end;

    end;

    theorem :: GOBRD14:6

     [i, j] in ( Indices G) & [i, (j + n)] in ( Indices G) implies ( dist ((G * (i,j)),(G * (i,(j + n))))) = (((G * (i,(j + n))) `2 ) - ((G * (i,j)) `2 ))

    proof

      assume that

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

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

      set x = (G * (i,j)), y = (G * (i,(j + n)));

      per cases ;

        suppose n = 0 ;

        hence thesis by TOPREAL6: 93;

      end;

        suppose

         A3: n <> 0 ;

        

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

        

         A5: 1 <= i & i <= ( len G) by A1, MATRIX_0: 32;

        

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

        

         A7: 1 <= j by A1, MATRIX_0: 32;

        1 <= n by A3, NAT_1: 14;

        then j < (j + n) by NAT_1: 19;

        then (x `2 ) < (y `2 ) by A4, A7, A5, GOBOARD5: 4;

        then

         A8: ((x `2 ) - (x `2 )) < ((y `2 ) - (x `2 )) by XREAL_1: 14;

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

        

        then

         A9: (x `1 ) = ((G * (i,1)) `1 ) by A7, A5, GOBOARD5: 2

        .= (y `1 ) by A6, A4, A5, GOBOARD5: 2;

        

        thus ( dist ((G * (i,j)),(G * (i,(j + n))))) = ( sqrt ((((x `1 ) - (y `1 )) ^2 ) + (((x `2 ) - (y `2 )) ^2 ))) by TOPREAL6: 92

        .= |.((x `2 ) - (y `2 )).| by A9, COMPLEX1: 72

        .= |.( - ((x `2 ) - (y `2 ))).| by COMPLEX1: 52

        .= (((G * (i,(j + n))) `2 ) - ((G * (i,j)) `2 )) by A8, ABSVALUE:def 1;

      end;

    end;

    theorem :: GOBRD14:7

    3 <= (( len ( Gauge (C,n))) -' 1)

    proof

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

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

      then (4 - 1) <= (( len G) - 1) by XREAL_1: 13;

      hence thesis by XREAL_0:def 2;

    end;

    theorem :: GOBRD14:8

    i <= j implies for a,b be Nat st 2 <= a & a <= (( len ( Gauge (C,i))) - 1) & 2 <= b & b <= (( len ( Gauge (C,i))) - 1) holds ex c,d be Nat st 2 <= c & c <= (( len ( Gauge (C,j))) - 1) & 2 <= d & d <= (( len ( Gauge (C,j))) - 1) & [c, d] in ( Indices ( Gauge (C,j))) & (( Gauge (C,i)) * (a,b)) = (( Gauge (C,j)) * (c,d)) & c = (2 + ((2 |^ (j -' i)) * (a -' 2))) & d = (2 + ((2 |^ (j -' i)) * (b -' 2)))

    proof

      

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

      assume

       A2: i <= j;

      

      then

       A3: ((2 |^ (j -' i)) * (2 |^ i)) = (((2 |^ j) / (2 |^ i)) * (2 |^ i)) by TOPREAL6: 10

      .= (2 |^ j) by A1, XCMPLX_1: 87;

      let a,b be Nat such that

       A4: 2 <= a and

       A5: a <= (( len ( Gauge (C,i))) - 1) and

       A6: 2 <= b and

       A7: b <= (( len ( Gauge (C,i))) - 1);

      

       A8: 1 <= a & 1 <= b by A4, A6, XXREAL_0: 2;

      set c = (2 + ((2 |^ (j -' i)) * (a -' 2))), d = (2 + ((2 |^ (j -' i)) * (b -' 2)));

      

       A9: 0 <= (b - 2) by A6, XREAL_1: 48;

      set n = ( N-bound C), e = ( E-bound C), s = ( S-bound C), w = ( W-bound C);

      

       A10: 0 <> (2 |^ j) by NEWTON: 83;

      

       A11: (((n - s) / (2 |^ j)) * (d - 2)) = (((n - s) / (2 |^ j)) * (((2 |^ j) / (2 |^ i)) * (b -' 2))) by A2, TOPREAL6: 10

      .= ((((n - s) / (2 |^ j)) * ((2 |^ j) / (2 |^ i))) * (b -' 2))

      .= (((n - s) / ((2 |^ j) / ((2 |^ j) / (2 |^ i)))) * (b -' 2)) by XCMPLX_1: 81

      .= (((n - s) / (2 |^ i)) * (b -' 2)) by A10, XCMPLX_1: 52

      .= (((n - s) / (2 |^ i)) * (b - 2)) by A9, XREAL_0:def 2;

      take c, d;

      

       A12: (2 + 0 ) <= (2 + ((2 |^ (j -' i)) * (a -' 2))) by XREAL_1: 6;

      then

       A13: 1 <= c by XXREAL_0: 2;

      (((2 |^ i) + 2) - 2) >= 0 ;

      then

       A14: (((2 |^ i) + 2) -' 2) = ((2 |^ i) + 0 ) by XREAL_0:def 2;

      

       A15: 0 <= (a - 2) by A4, XREAL_1: 48;

      

       A16: (((e - w) / (2 |^ j)) * (c - 2)) = (((e - w) / (2 |^ j)) * (((2 |^ j) / (2 |^ i)) * (a -' 2))) by A2, TOPREAL6: 10

      .= ((((e - w) / (2 |^ j)) * ((2 |^ j) / (2 |^ i))) * (a -' 2))

      .= (((e - w) / ((2 |^ j) / ((2 |^ j) / (2 |^ i)))) * (a -' 2)) by XCMPLX_1: 81

      .= (((e - w) / (2 |^ i)) * (a -' 2)) by A10, XCMPLX_1: 52

      .= (((e - w) / (2 |^ i)) * (a - 2)) by A15, XREAL_0:def 2;

      

       A17: (( len ( Gauge (C,j))) - 1) < (( len ( Gauge (C,j))) - 0 ) by XREAL_1: 15;

      

       A18: (( len ( Gauge (C,i))) - 1) = (((2 |^ i) + 3) - 1) by JORDAN8:def 1

      .= ((2 |^ i) + 2);

      then (a -' 2) <= (((2 |^ i) + 2) -' 2) by A5, NAT_D: 42;

      then

       A19: ((2 |^ (j -' i)) * (a -' 2)) <= (2 |^ j) by A14, A3, XREAL_1: 64;

      (b -' 2) <= (((2 |^ i) + 2) -' 2) by A7, A18, NAT_D: 42;

      then

       A20: ((2 |^ (j -' i)) * (b -' 2)) <= (2 |^ j) by A14, A3, XREAL_1: 64;

      

       A21: (( len ( Gauge (C,i))) - 1) < (( len ( Gauge (C,i))) - 0 ) by XREAL_1: 15;

      then

       A22: a <= ( len ( Gauge (C,i))) by A5, XXREAL_0: 2;

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

      .= ((2 |^ j) + 2);

      hence

       A23: 2 <= c & c <= (( len ( Gauge (C,j))) - 1) & 2 <= d & d <= (( len ( Gauge (C,j))) - 1) by A19, A20, A12, XREAL_1: 6;

      then

       A24: 1 <= d by XXREAL_0: 2;

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

      then

       A25: d <= ( width ( Gauge (C,j))) by A23, A17, XXREAL_0: 2;

      c <= ( len ( Gauge (C,j))) by A23, A17, XXREAL_0: 2;

      hence [c, d] in ( Indices ( Gauge (C,j))) by A13, A24, A25, MATRIX_0: 30;

      then

       A26: (( Gauge (C,j)) * (c,d)) = |[(w + (((e - w) / (2 |^ j)) * (c - 2))), (s + (((n - s) / (2 |^ j)) * (d - 2)))]| by JORDAN8:def 1;

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

      then b <= ( width ( Gauge (C,i))) by A7, A21, XXREAL_0: 2;

      then [a, b] in ( Indices ( Gauge (C,i))) by A22, A8, MATRIX_0: 30;

      then

       A27: (( Gauge (C,i)) * (a,b)) = |[(w + (((e - w) / (2 |^ i)) * (a - 2))), (s + (((n - s) / (2 |^ i)) * (b - 2)))]| by JORDAN8:def 1;

      

      then

       A28: ((( Gauge (C,i)) * (a,b)) `2 ) = (s + (((n - s) / (2 |^ i)) * (b - 2))) by EUCLID: 52

      .= ((( Gauge (C,j)) * (c,d)) `2 ) by A26, A11, EUCLID: 52;

      ((( Gauge (C,i)) * (a,b)) `1 ) = (w + (((e - w) / (2 |^ i)) * (a - 2))) by A27, EUCLID: 52

      .= ((( Gauge (C,j)) * (c,d)) `1 ) by A26, A16, EUCLID: 52;

      hence (( Gauge (C,i)) * (a,b)) = (( Gauge (C,j)) * (c,d)) by A28, TOPREAL3: 6;

      thus thesis;

    end;

    theorem :: GOBRD14:9

    

     Th9: [i, j] in ( Indices ( Gauge (C,n))) & [i, (j + 1)] in ( Indices ( Gauge (C,n))) implies ( dist ((( Gauge (C,n)) * (i,j)),(( Gauge (C,n)) * (i,(j + 1))))) = ((( N-bound C) - ( S-bound C)) / (2 |^ n))

    proof

      set G = ( Gauge (C,n)), a = ( N-bound C), e = ( E-bound C), s = ( S-bound C), w = ( W-bound C), p1 = (G * (i,j)), p2 = (G * (i,(j + 1)));

      assume that

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

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

      

       A3: p2 = |[(w + (((e - w) / (2 |^ n)) * (i - 2))), (s + (((a - s) / (2 |^ n)) * ((j + 1) - 2)))]| by A2, JORDAN8:def 1;

      a >= s by SPRECT_1: 22;

      then

       A4: (a - s) >= (s - s) by XREAL_1: 9;

      set x = ((a - s) / (2 |^ n));

      consider p,q be Point of ( Euclid 2) such that

       A5: p = p1 & q = p2 and

       A6: ( dist (p1,p2)) = ( dist (p,q)) by TOPREAL6:def 1;

      

       A7: p1 = |[(w + (((e - w) / (2 |^ n)) * (i - 2))), (s + (((a - s) / (2 |^ n)) * (j - 2)))]| by A1, JORDAN8:def 1;

      ( dist (p,q)) = (( Pitag_dist 2) . (p,q)) by METRIC_1:def 1

      .= ( sqrt ((((p1 `1 ) - (p2 `1 )) ^2 ) + (((p1 `2 ) - (p2 `2 )) ^2 ))) by A5, TOPREAL3: 7

      .= ( sqrt ((((w + (((e - w) / (2 |^ n)) * (i - 2))) - (p2 `1 )) ^2 ) + (((p1 `2 ) - (p2 `2 )) ^2 ))) by A7, EUCLID: 52

      .= ( sqrt ((((w + (((e - w) / (2 |^ n)) * (i - 2))) - (w + (((e - w) / (2 |^ n)) * (i - 2)))) ^2 ) + (((p1 `2 ) - (p2 `2 )) ^2 ))) by A3, EUCLID: 52

      .= |.((p1 `2 ) - (p2 `2 )).| by COMPLEX1: 72

      .= |.((s + (x * (j - 2))) - (p2 `2 )).| by A7, EUCLID: 52

      .= |.((s + (x * (j - 2))) - (s + (x * ((j + 1) - 2)))).| by A3, EUCLID: 52

      .= |.( - x).|

      .= |.x.| by COMPLEX1: 52

      .= ( |.(a - s).| / |.(2 |^ n).|) by COMPLEX1: 67

      .= ((a - s) / |.(2 |^ n).|) by A4, ABSVALUE:def 1;

      hence thesis by A6, ABSVALUE:def 1;

    end;

    theorem :: GOBRD14:10

    

     Th10: [i, j] in ( Indices ( Gauge (C,n))) & [(i + 1), j] in ( Indices ( Gauge (C,n))) implies ( dist ((( Gauge (C,n)) * (i,j)),(( Gauge (C,n)) * ((i + 1),j)))) = ((( E-bound C) - ( W-bound C)) / (2 |^ n))

    proof

      set G = ( Gauge (C,n)), a = ( N-bound C), e = ( E-bound C), s = ( S-bound C), w = ( W-bound C), p1 = (G * (i,j)), p2 = (G * ((i + 1),j));

      assume that

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

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

      

       A3: p2 = |[(w + (((e - w) / (2 |^ n)) * ((i + 1) - 2))), (s + (((a - s) / (2 |^ n)) * (j - 2)))]| by A2, JORDAN8:def 1;

      e >= w by SPRECT_1: 21;

      then

       A4: (e - w) >= (w - w) by XREAL_1: 9;

      set x = ((e - w) / (2 |^ n));

      consider p,q be Point of ( Euclid 2) such that

       A5: p = p1 & q = p2 and

       A6: ( dist (p1,p2)) = ( dist (p,q)) by TOPREAL6:def 1;

      

       A7: p1 = |[(w + (((e - w) / (2 |^ n)) * (i - 2))), (s + (((a - s) / (2 |^ n)) * (j - 2)))]| by A1, JORDAN8:def 1;

      ( dist (p,q)) = (( Pitag_dist 2) . (p,q)) by METRIC_1:def 1

      .= ( sqrt ((((p1 `1 ) - (p2 `1 )) ^2 ) + (((p1 `2 ) - (p2 `2 )) ^2 ))) by A5, TOPREAL3: 7

      .= ( sqrt ((((p1 `1 ) - (p2 `1 )) ^2 ) + (((s + (((a - s) / (2 |^ n)) * (j - 2))) - (p2 `2 )) ^2 ))) by A7, EUCLID: 52

      .= ( sqrt ((((p1 `1 ) - (p2 `1 )) ^2 ) + (((s + (((a - s) / (2 |^ n)) * (j - 2))) - (s + (((a - s) / (2 |^ n)) * (j - 2)))) ^2 ))) by A3, EUCLID: 52

      .= |.((p1 `1 ) - (p2 `1 )).| by COMPLEX1: 72

      .= |.((w + (x * (i - 2))) - (p2 `1 )).| by A7, EUCLID: 52

      .= |.((w + (x * (i - 2))) - (w + (x * ((i + 1) - 2)))).| by A3, EUCLID: 52

      .= |.( - x).|

      .= |.x.| by COMPLEX1: 52

      .= ( |.(e - w).| / |.(2 |^ n).|) by COMPLEX1: 67

      .= ((e - w) / |.(2 |^ n).|) by A4, ABSVALUE:def 1;

      hence thesis by A6, ABSVALUE:def 1;

    end;

    theorem :: GOBRD14:11

    for r,t be Real holds r > 0 & t > 0 implies ex n be Nat st 1 < n & ( dist ((( Gauge (C,n)) * (1,1)),(( Gauge (C,n)) * (1,2)))) < r & ( dist ((( Gauge (C,n)) * (1,1)),(( Gauge (C,n)) * (2,1)))) < t

    proof

      let r,t be Real;

      assume that

       A1: r > 0 and

       A2: t > 0 ;

      set n = ( N-bound C), e = ( E-bound C), s = ( S-bound C), w = ( W-bound C);

      set a = ( |. [\( log (2,((n - s) / r)))/].| + 1), b = ( |. [\( log (2,((e - w) / t)))/].| + 1);

      take i = (( max (a,b)) + 1);

      

       A3: (2 to_power i) > 0 by POWER: 34;

      then

       A4: (2 |^ i) > 0 by POWER: 41;

       [\( log (2,((n - s) / r)))/] <= |. [\( log (2,((n - s) / r)))/].| by ABSVALUE: 4;

      then

       A5: ( [\( log (2,((n - s) / r)))/] + 1) <= a by XREAL_1: 6;

       [\( log (2,((n - s) / r)))/] > (( log (2,((n - s) / r))) - 1) by INT_1:def 6;

      then ( [\( log (2,((n - s) / r)))/] + 1) > ((( log (2,((n - s) / r))) - 1) + 1) by XREAL_1: 6;

      then

       A6: a > ((( log (2,((n - s) / r))) - 1) + 1) by A5, XXREAL_0: 2;

      a <= ( max (a,b)) by XXREAL_0: 25;

      then

       A7: (a + 1) <= (( max (a,b)) + 1) by XREAL_1: 6;

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

      then i > a by A7, XXREAL_0: 2;

      then i > ( log (2,((n - s) / r))) by A6, XXREAL_0: 2;

      then ( log (2,(2 to_power i))) > ( log (2,((n - s) / r))) by A3, POWER:def 3;

      then (2 to_power i) > ((n - s) / r) by A3, PRE_FF: 10;

      then (2 |^ i) > ((n - s) / r) by POWER: 41;

      then ((2 |^ i) * r) > (((n - s) / r) * r) by A1, XREAL_1: 68;

      then ((2 |^ i) * r) > (n - s) by A1, XCMPLX_1: 87;

      then (((2 |^ i) * r) / (2 |^ i)) > ((n - s) / (2 |^ i)) by A4, XREAL_1: 74;

      then

       A8: ((n - s) / (2 |^ i)) < r by A4, XCMPLX_1: 89;

      a >= ( 0 + 1) & ( max (a,b)) >= a by XREAL_1: 7, XXREAL_0: 25;

      then ( max (a,b)) >= 1 by XXREAL_0: 2;

      then (( max (a,b)) + 1) >= (1 + 1) by XREAL_1: 7;

      hence 1 < i by XXREAL_0: 2;

      

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

      then

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

       [\( log (2,((e - w) / t)))/] <= |. [\( log (2,((e - w) / t)))/].| by ABSVALUE: 4;

      then

       A11: ( [\( log (2,((e - w) / t)))/] + 1) <= b by XREAL_1: 6;

       [\( log (2,((e - w) / t)))/] > (( log (2,((e - w) / t))) - 1) by INT_1:def 6;

      then ( [\( log (2,((e - w) / t)))/] + 1) > ((( log (2,((e - w) / t))) - 1) + 1) by XREAL_1: 6;

      then

       A12: b > ((( log (2,((e - w) / t))) - 1) + 1) by A11, XXREAL_0: 2;

      b <= ( max (a,b)) by XXREAL_0: 25;

      then

       A13: (b + 1) <= (( max (a,b)) + 1) by XREAL_1: 6;

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

      then i > b by A13, XXREAL_0: 2;

      then i > ( log (2,((e - w) / t))) by A12, XXREAL_0: 2;

      then ( log (2,(2 to_power i))) > ( log (2,((e - w) / t))) by A3, POWER:def 3;

      then (2 to_power i) > ((e - w) / t) by A3, PRE_FF: 10;

      then (2 |^ i) > ((e - w) / t) by POWER: 41;

      then ((2 |^ i) * t) > (((e - w) / t) * t) by A2, XREAL_1: 68;

      then ((2 |^ i) * t) > (e - w) by A2, XCMPLX_1: 87;

      then (((2 |^ i) * t) / (2 |^ i)) > ((e - w) / (2 |^ i)) by A4, XREAL_1: 74;

      then

       A14: ((e - w) / (2 |^ i)) < t by A4, XCMPLX_1: 89;

      

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

      then

       A16: [1, 1] in ( Indices ( Gauge (C,i))) by A10, MATRIX_0: 30;

      

       A17: (1 + 1) <= ( width ( Gauge (C,i))) by A15, A9, XXREAL_0: 2;

      then

       A18: [1, (1 + 1)] in ( Indices ( Gauge (C,i))) by A10, MATRIX_0: 30;

       [(1 + 1), 1] in ( Indices ( Gauge (C,i))) by A15, A10, A17, MATRIX_0: 30;

      hence thesis by A8, A14, A16, A18, Th9, Th10;

    end;

    begin

    theorem :: GOBRD14:12

    

     Th12: for P be Subset of (( TOP-REAL 2) | (( L~ f) ` )) st P is a_component holds P = ( RightComp f) or P = ( LeftComp f)

    proof

      let P be Subset of (( TOP-REAL 2) | (( L~ f) ` ));

      assume that

       A1: P is a_component and

       A2: P <> ( RightComp f);

      P <> ( {} (( TOP-REAL 2) | (( L~ f) ` ))) by A1, CONNSP_1: 32;

      then

      consider a be Point of (( TOP-REAL 2) | (( L~ f) ` )) such that

       A3: a in P by SUBSET_1: 4;

      the carrier of (( TOP-REAL 2) | (( L~ f) ` )) = (( L~ f) ` ) & (( L~ f) ` ) = (( LeftComp f) \/ ( RightComp f)) by GOBRD12: 10, PRE_TOPC: 8;

      then

       A4: a in ( LeftComp f) or a in ( RightComp f) by XBOOLE_0:def 3;

      ( LeftComp f) is_a_component_of (( L~ f) ` ) by GOBOARD9:def 1;

      then

       A5: ex L be Subset of (( TOP-REAL 2) | (( L~ f) ` )) st L = ( LeftComp f) & L is a_component by CONNSP_1:def 6;

      ( RightComp f) is_a_component_of (( L~ f) ` ) by GOBOARD9:def 2;

      then

      consider R be Subset of (( TOP-REAL 2) | (( L~ f) ` )) such that

       A6: R = ( RightComp f) and

       A7: R is a_component by CONNSP_1:def 6;

      P misses R by A1, A2, A6, A7, CONNSP_1: 35;

      then P meets ( LeftComp f) by A6, A3, A4, XBOOLE_0: 3;

      hence thesis by A1, A5, CONNSP_1: 35;

    end;

    theorem :: GOBRD14:13

    for A1,A2 be Subset of ( TOP-REAL 2) st (( L~ f) ` ) = (A1 \/ A2) & A1 misses A2 & for C1,C2 be Subset of (( TOP-REAL 2) | (( L~ f) ` )) st C1 = A1 & C2 = A2 holds C1 is a_component & C2 is a_component holds A1 = ( RightComp f) & A2 = ( LeftComp f) or A1 = ( LeftComp f) & A2 = ( RightComp f)

    proof

      let A1,A2 be Subset of ( TOP-REAL 2) such that

       A1: (( L~ f) ` ) = (A1 \/ A2) and

       A2: (A1 /\ A2) = {} and

       A3: for C1,C2 be Subset of (( TOP-REAL 2) | (( L~ f) ` )) st C1 = A1 & C2 = A2 holds C1 is a_component & C2 is a_component;

      the carrier of (( TOP-REAL 2) | (( L~ f) ` )) = (( L~ f) ` ) by PRE_TOPC: 8;

      then

      reconsider C1 = A1, C2 = A2 as Subset of (( TOP-REAL 2) | (( L~ f) ` )) by A1, XBOOLE_1: 7;

      C1 = A1;

      then C2 is a_component by A3;

      then

       A4: C2 = ( RightComp f) or C2 = ( LeftComp f) by Th12;

      C2 = A2;

      then C1 is a_component by A3;

      then

       A5: C1 = ( RightComp f) or C1 = ( LeftComp f) by Th12;

      assume not thesis;

      hence contradiction by A2, A5, A4;

    end;

    theorem :: GOBRD14:14

    

     Th14: ( LeftComp f) misses ( RightComp f)

    proof

      assume (( LeftComp f) /\ ( RightComp f)) <> {} ;

      then

      consider x be object such that

       A1: x in (( LeftComp f) /\ ( RightComp f)) by XBOOLE_0:def 1;

      now

        take x;

        thus x in ( LeftComp f) & x in ( RightComp f) by A1, XBOOLE_0:def 4;

      end;

      then

       A2: ( LeftComp f) meets ( RightComp f) by XBOOLE_0: 3;

      ( LeftComp f) is_a_component_of (( L~ f) ` ) & ( RightComp f) is_a_component_of (( L~ f) ` ) by GOBOARD9:def 1, GOBOARD9:def 2;

      hence thesis by A2, GOBOARD9: 1, SPRECT_4: 6;

    end;

    theorem :: GOBRD14:15

    

     Th15: ((( L~ f) \/ ( RightComp f)) \/ ( LeftComp f)) = the carrier of ( TOP-REAL 2)

    proof

      

       A1: ((( L~ f) ` ) \/ ( L~ f)) = ( [#] the carrier of ( TOP-REAL 2)) by SUBSET_1: 10

      .= the carrier of ( TOP-REAL 2);

      (( L~ f) ` ) = (( RightComp f) \/ ( LeftComp f)) by GOBRD12: 10;

      hence thesis by A1, XBOOLE_1: 4;

    end;

    theorem :: GOBRD14:16

    

     Th16: p in ( L~ f) iff not p in ( LeftComp f) & not p in ( RightComp f)

    proof

      

       A1: p in ( L~ f) iff not p in (( L~ f) ` ) by XBOOLE_0:def 5;

      (( L~ f) ` ) = (( LeftComp f) \/ ( RightComp f)) by GOBRD12: 10;

      hence thesis by A1, XBOOLE_0:def 3;

    end;

    theorem :: GOBRD14:17

    

     Th17: p in ( LeftComp f) iff not p in ( L~ f) & not p in ( RightComp f)

    proof

      ( LeftComp f) misses ( RightComp f) by Th14;

      then

       A1: (( L~ f) ` ) = (( LeftComp f) \/ ( RightComp f)) & (( LeftComp f) /\ ( RightComp f)) = {} by GOBRD12: 10;

      p in ( L~ f) iff not p in (( L~ f) ` ) by XBOOLE_0:def 5;

      hence thesis by A1, XBOOLE_0:def 3, XBOOLE_0:def 4;

    end;

    theorem :: GOBRD14:18

    p in ( RightComp f) iff not p in ( L~ f) & not p in ( LeftComp f) by Th16, Th17;

    theorem :: GOBRD14:19

    

     Th19: ( L~ f) = (( Cl ( RightComp f)) \ ( RightComp f))

    proof

      thus ( L~ f) c= (( Cl ( RightComp f)) \ ( RightComp f))

      proof

        let x be object;

        assume

         A1: x in ( L~ f);

        then

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

        consider i such that

         A2: 1 <= i & (i + 1) <= ( len f) and

         A3: p in ( LSeg (f,i)) by A1, SPPOL_2: 13;

        for O be Subset of ( TOP-REAL 2) st O is open holds p in O implies ( RightComp f) meets O

        proof

          (( left_cell (f,i)) /\ ( right_cell (f,i))) = ( LSeg (f,i)) by A2, GOBOARD5: 31;

          then ( LSeg (f,i)) c= ( right_cell (f,i)) by XBOOLE_1: 17;

          then

           A4: p in ( right_cell (f,i)) by A3;

          f is_sequence_on ( GoB f) by GOBOARD5:def 5;

          then

          consider i1,j1,i2,j2 be Nat such that

           A5: [i1, j1] in ( Indices ( GoB f)) and

           A6: (f /. i) = (( GoB f) * (i1,j1)) and

           A7: [i2, j2] in ( Indices ( GoB f)) and

           A8: (f /. (i + 1)) = (( GoB f) * (i2,j2)) and

           A9: i1 = i2 & (j1 + 1) = j2 or (i1 + 1) = i2 & j1 = j2 or i1 = (i2 + 1) & j1 = j2 or i1 = i2 & j1 = (j2 + 1) by A2, JORDAN8: 3;

          

           A10: 1 <= i1 by A5, MATRIX_0: 32;

          

           A11: j2 <= ( width ( GoB f)) by A7, MATRIX_0: 32;

          

           A12: 1 <= j1 by A5, MATRIX_0: 32;

          

           A13: j1 <= ( width ( GoB f)) by A5, MATRIX_0: 32;

          

           A14: i1 <= ( len ( GoB f)) by A5, MATRIX_0: 32;

          

           A15: i2 <= ( len ( GoB f)) by A7, MATRIX_0: 32;

           A16:

          now

            per cases by A9;

              case

               A17: i1 = i2 & (j1 + 1) = j2;

              set w = (i1 -' 1);

              

               A18: (w + 1) = i1 by A10, XREAL_1: 235;

              then ( right_cell (f,i)) = ( cell (( GoB f),(w + 1),j1)) by A2, A5, A6, A7, A8, A17, GOBOARD5: 27;

              hence p in ( Cl ( Int ( right_cell (f,i)))) by A4, A14, A13, A18, GOBRD11: 35;

            end;

              case

               A19: (i1 + 1) = i2 & j1 = j2;

              set w = (j1 -' 1);

              w <= (w + 1) & (w + 1) <= ( width ( GoB f)) by A12, A13, NAT_1: 11, XREAL_1: 235;

              then

               A20: w <= ( width ( GoB f)) by XXREAL_0: 2;

              (w + 1) = j1 by A12, XREAL_1: 235;

              then ( right_cell (f,i)) = ( cell (( GoB f),i1,w)) by A2, A5, A6, A7, A8, A19, GOBOARD5: 28;

              hence p in ( Cl ( Int ( right_cell (f,i)))) by A4, A14, A20, GOBRD11: 35;

            end;

              case

               A21: i1 = (i2 + 1) & j1 = j2;

              set w = (j1 -' 1);

              

               A22: (w + 1) = j1 by A12, XREAL_1: 235;

              then ( right_cell (f,i)) = ( cell (( GoB f),i2,(w + 1))) by A2, A5, A6, A7, A8, A21, GOBOARD5: 29;

              hence p in ( Cl ( Int ( right_cell (f,i)))) by A4, A13, A15, A22, GOBRD11: 35;

            end;

              case

               A23: i1 = i2 & j1 = (j2 + 1);

              set z = (i1 -' 1);

              z <= (z + 1) & (z + 1) <= ( len ( GoB f)) by A10, A14, NAT_1: 11, XREAL_1: 235;

              then

               A24: z <= ( len ( GoB f)) by XXREAL_0: 2;

              (z + 1) = i1 by A10, XREAL_1: 235;

              then ( right_cell (f,i)) = ( cell (( GoB f),z,j2)) by A2, A5, A6, A7, A8, A23, GOBOARD5: 30;

              hence p in ( Cl ( Int ( right_cell (f,i)))) by A4, A11, A24, GOBRD11: 35;

            end;

          end;

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

          assume O is open & p in O;

          then O meets ( Int ( right_cell (f,i))) by A16, PRE_TOPC:def 7;

          hence thesis by A2, GOBOARD9: 25, XBOOLE_1: 63;

        end;

        then

         A25: p in ( Cl ( RightComp f)) by PRE_TOPC:def 7;

         not x in ( RightComp f) by A1, Th16;

        hence thesis by A25, XBOOLE_0:def 5;

      end;

      assume not (( Cl ( RightComp f)) \ ( RightComp f)) c= ( L~ f);

      then

      consider q be object such that

       A26: q in (( Cl ( RightComp f)) \ ( RightComp f)) and

       A27: not q in ( L~ f);

      reconsider q as Point of ( TOP-REAL 2) by A26;

       not q in ( RightComp f) by A26, XBOOLE_0:def 5;

      then

       A28: q in ( LeftComp f) by A27, Th16;

      q in ( Cl ( RightComp f)) by A26, XBOOLE_0:def 5;

      then ( LeftComp f) meets ( RightComp f) by A28, PRE_TOPC:def 7;

      hence contradiction by Th14;

    end;

    theorem :: GOBRD14:20

    

     Th20: ( L~ f) = (( Cl ( LeftComp f)) \ ( LeftComp f))

    proof

      thus ( L~ f) c= (( Cl ( LeftComp f)) \ ( LeftComp f))

      proof

        let x be object;

        assume

         A1: x in ( L~ f);

        then

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

        consider i such that

         A2: 1 <= i & (i + 1) <= ( len f) and

         A3: p in ( LSeg (f,i)) by A1, SPPOL_2: 13;

        for O be Subset of ( TOP-REAL 2) st O is open holds p in O implies ( LeftComp f) meets O

        proof

          (( left_cell (f,i)) /\ ( right_cell (f,i))) = ( LSeg (f,i)) by A2, GOBOARD5: 31;

          then ( LSeg (f,i)) c= ( left_cell (f,i)) by XBOOLE_1: 17;

          then

           A4: p in ( left_cell (f,i)) by A3;

          f is_sequence_on ( GoB f) by GOBOARD5:def 5;

          then

          consider i1,j1,i2,j2 be Nat such that

           A5: [i1, j1] in ( Indices ( GoB f)) and

           A6: (f /. i) = (( GoB f) * (i1,j1)) and

           A7: [i2, j2] in ( Indices ( GoB f)) and

           A8: (f /. (i + 1)) = (( GoB f) * (i2,j2)) and

           A9: i1 = i2 & (j1 + 1) = j2 or (i1 + 1) = i2 & j1 = j2 or i1 = (i2 + 1) & j1 = j2 or i1 = i2 & j1 = (j2 + 1) by A2, JORDAN8: 3;

          

           A10: 1 <= i1 by A5, MATRIX_0: 32;

          

           A11: j2 <= ( width ( GoB f)) by A7, MATRIX_0: 32;

          

           A12: 1 <= j1 by A5, MATRIX_0: 32;

          

           A13: j1 <= ( width ( GoB f)) by A5, MATRIX_0: 32;

          

           A14: i1 <= ( len ( GoB f)) by A5, MATRIX_0: 32;

          

           A15: i2 <= ( len ( GoB f)) by A7, MATRIX_0: 32;

           A16:

          now

            per cases by A9;

              case

               A17: i1 = i2 & (j1 + 1) = j2;

              set w = (i1 -' 1);

              w <= (w + 1) & (w + 1) <= ( len ( GoB f)) by A10, A14, NAT_1: 11, XREAL_1: 235;

              then

               A18: w <= ( len ( GoB f)) by XXREAL_0: 2;

              (w + 1) = i1 by A10, XREAL_1: 235;

              then ( left_cell (f,i)) = ( cell (( GoB f),w,j1)) by A2, A5, A6, A7, A8, A17, GOBOARD5: 27;

              hence p in ( Cl ( Int ( left_cell (f,i)))) by A4, A13, A18, GOBRD11: 35;

            end;

              case

               A19: (i1 + 1) = i2 & j1 = j2;

              set w = (j1 -' 1);

              (w + 1) = j1 by A12, XREAL_1: 235;

              then

               A20: ( left_cell (f,i)) = ( cell (( GoB f),i1,(w + 1))) by A2, A5, A6, A7, A8, A19, GOBOARD5: 28;

              (w + 1) <= ( width ( GoB f)) by A12, A13, XREAL_1: 235;

              hence p in ( Cl ( Int ( left_cell (f,i)))) by A4, A14, A20, GOBRD11: 35;

            end;

              case

               A21: i1 = (i2 + 1) & j1 = j2;

              set w = (j1 -' 1);

              w <= (w + 1) & (w + 1) <= ( width ( GoB f)) by A12, A13, NAT_1: 11, XREAL_1: 235;

              then

               A22: w <= ( width ( GoB f)) by XXREAL_0: 2;

              (w + 1) = j1 by A12, XREAL_1: 235;

              then ( left_cell (f,i)) = ( cell (( GoB f),i2,w)) by A2, A5, A6, A7, A8, A21, GOBOARD5: 29;

              hence p in ( Cl ( Int ( left_cell (f,i)))) by A4, A15, A22, GOBRD11: 35;

            end;

              case

               A23: i1 = i2 & j1 = (j2 + 1);

              set z = (i1 -' 1);

              (z + 1) = i1 by A10, XREAL_1: 235;

              then

               A24: ( left_cell (f,i)) = ( cell (( GoB f),(z + 1),j2)) by A2, A5, A6, A7, A8, A23, GOBOARD5: 30;

              (z + 1) <= ( len ( GoB f)) by A10, A14, XREAL_1: 235;

              hence p in ( Cl ( Int ( left_cell (f,i)))) by A4, A11, A24, GOBRD11: 35;

            end;

          end;

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

          assume O is open & p in O;

          then O meets ( Int ( left_cell (f,i))) by A16, PRE_TOPC:def 7;

          hence thesis by A2, GOBOARD9: 21, XBOOLE_1: 63;

        end;

        then

         A25: p in ( Cl ( LeftComp f)) by PRE_TOPC:def 7;

         not x in ( LeftComp f) by A1, Th16;

        hence thesis by A25, XBOOLE_0:def 5;

      end;

      assume not (( Cl ( LeftComp f)) \ ( LeftComp f)) c= ( L~ f);

      then

      consider q be object such that

       A26: q in (( Cl ( LeftComp f)) \ ( LeftComp f)) and

       A27: not q in ( L~ f);

      reconsider q as Point of ( TOP-REAL 2) by A26;

       not q in ( LeftComp f) by A26, XBOOLE_0:def 5;

      then

       A28: q in ( RightComp f) by A27, Th16;

      q in ( Cl ( LeftComp f)) by A26, XBOOLE_0:def 5;

      then ( RightComp f) meets ( LeftComp f) by A28, PRE_TOPC:def 7;

      hence contradiction by Th14;

    end;

    theorem :: GOBRD14:21

    

     Th21: ( Cl ( RightComp f)) = (( RightComp f) \/ ( L~ f))

    proof

      thus ( Cl ( RightComp f)) c= (( RightComp f) \/ ( L~ f))

      proof

        let x be object;

        assume

         A1: x in ( Cl ( RightComp f));

        now

           A2:

          now

            assume x in ( LeftComp f);

            then ( LeftComp f) meets ( RightComp f) by A1, TOPS_1: 12;

            hence contradiction by Th14;

          end;

          assume not x in ( RightComp f);

          hence x in ( L~ f) by A1, A2, Th16;

        end;

        hence thesis by XBOOLE_0:def 3;

      end;

      (( Cl ( RightComp f)) \ ( RightComp f)) c= ( Cl ( RightComp f)) by XBOOLE_1: 36;

      then ( RightComp f) c= ( Cl ( RightComp f)) & ( L~ f) c= ( Cl ( RightComp f)) by Th19, PRE_TOPC: 18;

      hence thesis by XBOOLE_1: 8;

    end;

    theorem :: GOBRD14:22

    ( Cl ( LeftComp f)) = (( LeftComp f) \/ ( L~ f))

    proof

      thus ( Cl ( LeftComp f)) c= (( LeftComp f) \/ ( L~ f))

      proof

        let x be object;

        assume

         A1: x in ( Cl ( LeftComp f));

        now

          

           A2: not x in ( RightComp f) by A1, Th14, TOPS_1: 12;

          assume not x in ( LeftComp f);

          hence x in ( L~ f) by A1, A2, Th16;

        end;

        hence thesis by XBOOLE_0:def 3;

      end;

      (( Cl ( LeftComp f)) \ ( LeftComp f)) c= ( Cl ( LeftComp f)) by XBOOLE_1: 36;

      then ( LeftComp f) c= ( Cl ( LeftComp f)) & ( L~ f) c= ( Cl ( LeftComp f)) by Th20, PRE_TOPC: 18;

      hence thesis by XBOOLE_1: 8;

    end;

    registration

      let f be non constant standard special_circular_sequence;

      cluster ( L~ f) -> Jordan;

      coherence

      proof

        thus (( L~ f) ` ) <> {} ;

        take A1 = ( RightComp f), A2 = ( LeftComp f);

        thus (( L~ f) ` ) = (A1 \/ A2) by GOBRD12: 10;

        ( L~ f) = (( Cl A1) \ A1) by Th19;

        hence thesis by Th14, Th20, GOBOARD9:def 1, GOBOARD9:def 2;

      end;

    end

    reserve f for clockwise_oriented non constant standard special_circular_sequence;

    theorem :: GOBRD14:23

    

     Th23: p in ( RightComp f) implies ( W-bound ( L~ f)) < (p `1 )

    proof

      set g = ( Rotate (f,( N-min ( L~ f))));

      

       A1: ( L~ f) = ( L~ g) by REVROT_1: 33;

      reconsider u = p as Point of ( Euclid 2) by EUCLID: 22;

      assume p in ( RightComp f);

      then p in ( RightComp g) by REVROT_1: 37;

      then u in ( Int ( RightComp g)) by TOPS_1: 23;

      then

      consider r be Real such that

       A2: r > 0 and

       A3: ( Ball (u,r)) c= ( RightComp g) by GOBOARD6: 5;

      reconsider r as Real;

      reconsider k = |[((p `1 ) - (r / 2)), (p `2 )]| as Point of ( Euclid 2) by EUCLID: 22;

      ( dist (u,k)) = (( Pitag_dist 2) . (u,k)) by METRIC_1:def 1

      .= ( sqrt ((((p `1 ) - ( |[((p `1 ) - (r / 2)), (p `2 )]| `1 )) ^2 ) + (((p `2 ) - ( |[((p `1 ) - (r / 2)), (p `2 )]| `2 )) ^2 ))) by TOPREAL3: 7

      .= ( sqrt ((((p `1 ) - ((p `1 ) - (r / 2))) ^2 ) + (((p `2 ) - ( |[((p `1 ) - (r / 2)), (p `2 )]| `2 )) ^2 ))) by EUCLID: 52

      .= ( sqrt ((((p `1 ) - ((p `1 ) - (r / 2))) ^2 ) + (((p `2 ) - (p `2 )) ^2 ))) by EUCLID: 52

      .= (r / 2) by A2, SQUARE_1: 22;

      then ( dist (u,k)) < (r / 1) by A2, XREAL_1: 76;

      then

       A4: k in ( Ball (u,r)) by METRIC_1: 11;

      ( RightComp g) misses ( LeftComp g) by Th14;

      then

       A5: not |[((p `1 ) - (r / 2)), (p `2 )]| in ( LeftComp g) by A3, A4, XBOOLE_0: 3;

      set x = |[((p `1 ) - (r / 2)), ( N-bound ( L~ ( SpStSeq ( L~ g))))]|;

      

       A6: ( LSeg (( NW-corner ( L~ g)),( NE-corner ( L~ g)))) c= ( L~ ( SpStSeq ( L~ g))) by SPRECT_3: 14;

      

       A7: ( proj1 . x) = (x `1 ) by PSCOMP_1:def 5

      .= ((p `1 ) - (r / 2)) by EUCLID: 52;

      ( N-min ( L~ f)) in ( rng f) by SPRECT_2: 39;

      then

       A8: (g /. 1) = ( N-min ( L~ g)) by A1, FINSEQ_6: 92;

      then ( |[((p `1 ) - (r / 2)), (p `2 )]| `1 ) <= ( E-bound ( L~ g)) by A5, JORDAN2C: 111;

      then ((p `1 ) - (r / 2)) <= ( E-bound ( L~ g)) by EUCLID: 52;

      then

       A9: (x `1 ) <= ( E-bound ( L~ g)) by EUCLID: 52;

      (x `2 ) = ( N-bound ( L~ ( SpStSeq ( L~ g)))) by EUCLID: 52;

      then

       A10: (x `2 ) = ( N-bound ( L~ g)) by SPRECT_1: 60;

      ( |[((p `1 ) - (r / 2)), (p `2 )]| `1 ) >= ( W-bound ( L~ g)) by A8, A5, JORDAN2C: 110;

      then ((p `1 ) - (r / 2)) >= ( W-bound ( L~ g)) by EUCLID: 52;

      then

       A11: (x `1 ) >= ( W-bound ( L~ g)) by EUCLID: 52;

      ( LSeg (( NW-corner ( L~ g)),( NE-corner ( L~ g)))) = { q : (q `1 ) <= ( E-bound ( L~ g)) & (q `1 ) >= ( W-bound ( L~ g)) & (q `2 ) = ( N-bound ( L~ g)) } by SPRECT_1: 25;

      then x in ( LSeg (( NW-corner ( L~ g)),( NE-corner ( L~ g)))) by A9, A11, A10;

      then ( proj1 .: ( L~ ( SpStSeq ( L~ g)))) is bounded_below & ((p `1 ) - (r / 2)) in ( proj1 .: ( L~ ( SpStSeq ( L~ g)))) by A6, A7, FUNCT_2: 35;

      then

       A12: ( lower_bound ( proj1 .: ( L~ ( SpStSeq ( L~ g))))) <= ((p `1 ) - (r / 2)) by SEQ_4:def 2;

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

      then

       A13: ((p `1 ) - (r / 2)) < ((p `1 ) - 0 ) by XREAL_1: 15;

      ( W-bound ( L~ ( SpStSeq ( L~ g)))) = ( W-bound ( L~ g)) & ( W-bound ( L~ ( SpStSeq ( L~ g)))) = ( lower_bound ( proj1 .: ( L~ ( SpStSeq ( L~ g))))) by SPRECT_1: 43, SPRECT_1: 58;

      hence thesis by A1, A12, A13, XXREAL_0: 2;

    end;

    theorem :: GOBRD14:24

    

     Th24: p in ( RightComp f) implies ( E-bound ( L~ f)) > (p `1 )

    proof

      set g = ( Rotate (f,( N-min ( L~ f))));

      

       A1: ( L~ f) = ( L~ g) by REVROT_1: 33;

      reconsider u = p as Point of ( Euclid 2) by EUCLID: 22;

      assume p in ( RightComp f);

      then p in ( RightComp g) by REVROT_1: 37;

      then u in ( Int ( RightComp g)) by TOPS_1: 23;

      then

      consider r be Real such that

       A2: r > 0 and

       A3: ( Ball (u,r)) c= ( RightComp g) by GOBOARD6: 5;

      reconsider r as Real;

      reconsider k = |[((p `1 ) + (r / 2)), (p `2 )]| as Point of ( Euclid 2) by EUCLID: 22;

      ( dist (u,k)) = (( Pitag_dist 2) . (u,k)) by METRIC_1:def 1

      .= ( sqrt ((((p `1 ) - ( |[((p `1 ) + (r / 2)), (p `2 )]| `1 )) ^2 ) + (((p `2 ) - ( |[((p `1 ) + (r / 2)), (p `2 )]| `2 )) ^2 ))) by TOPREAL3: 7

      .= ( sqrt ((((p `1 ) - ((p `1 ) + (r / 2))) ^2 ) + (((p `2 ) - ( |[((p `1 ) + (r / 2)), (p `2 )]| `2 )) ^2 ))) by EUCLID: 52

      .= ( sqrt ((((p `1 ) - ((p `1 ) + (r / 2))) ^2 ) + (((p `2 ) - (p `2 )) ^2 ))) by EUCLID: 52

      .= ( sqrt ((r / 2) ^2 ))

      .= (r / 2) by A2, SQUARE_1: 22;

      then ( dist (u,k)) < (r / 1) by A2, XREAL_1: 76;

      then

       A4: k in ( Ball (u,r)) by METRIC_1: 11;

      ( RightComp g) misses ( LeftComp g) by Th14;

      then

       A5: not |[((p `1 ) + (r / 2)), (p `2 )]| in ( LeftComp g) by A3, A4, XBOOLE_0: 3;

      set x = |[((p `1 ) + (r / 2)), ( N-bound ( L~ ( SpStSeq ( L~ g))))]|;

      

       A6: ( LSeg (( NW-corner ( L~ g)),( NE-corner ( L~ g)))) c= ( L~ ( SpStSeq ( L~ g))) by SPRECT_3: 14;

      

       A7: ( proj1 . x) = (x `1 ) by PSCOMP_1:def 5

      .= ((p `1 ) + (r / 2)) by EUCLID: 52;

      ( N-min ( L~ f)) in ( rng f) by SPRECT_2: 39;

      then

       A8: (g /. 1) = ( N-min ( L~ g)) by A1, FINSEQ_6: 92;

      then ( |[((p `1 ) + (r / 2)), (p `2 )]| `1 ) <= ( E-bound ( L~ g)) by A5, JORDAN2C: 111;

      then ((p `1 ) + (r / 2)) <= ( E-bound ( L~ g)) by EUCLID: 52;

      then

       A9: (x `1 ) <= ( E-bound ( L~ g)) by EUCLID: 52;

      (x `2 ) = ( N-bound ( L~ ( SpStSeq ( L~ g)))) by EUCLID: 52;

      then

       A10: (x `2 ) = ( N-bound ( L~ g)) by SPRECT_1: 60;

      ( |[((p `1 ) + (r / 2)), (p `2 )]| `1 ) >= ( W-bound ( L~ g)) by A8, A5, JORDAN2C: 110;

      then ((p `1 ) + (r / 2)) >= ( W-bound ( L~ g)) by EUCLID: 52;

      then

       A11: (x `1 ) >= ( W-bound ( L~ g)) by EUCLID: 52;

      ( LSeg (( NW-corner ( L~ g)),( NE-corner ( L~ g)))) = { q : (q `1 ) <= ( E-bound ( L~ g)) & (q `1 ) >= ( W-bound ( L~ g)) & (q `2 ) = ( N-bound ( L~ g)) } by SPRECT_1: 25;

      then x in ( LSeg (( NW-corner ( L~ g)),( NE-corner ( L~ g)))) by A9, A11, A10;

      then ( proj1 .: ( L~ ( SpStSeq ( L~ g)))) is bounded_above & ((p `1 ) + (r / 2)) in ( proj1 .: ( L~ ( SpStSeq ( L~ g)))) by A6, A7, FUNCT_2: 35;

      then

       A12: ( upper_bound ( proj1 .: ( L~ ( SpStSeq ( L~ g))))) >= ((p `1 ) + (r / 2)) by SEQ_4:def 1;

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

      then

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

      ( E-bound ( L~ ( SpStSeq ( L~ g)))) = ( E-bound ( L~ g)) & ( E-bound ( L~ ( SpStSeq ( L~ g)))) = ( upper_bound ( proj1 .: ( L~ ( SpStSeq ( L~ g))))) by SPRECT_1: 46, SPRECT_1: 61;

      hence thesis by A1, A12, A13, XXREAL_0: 2;

    end;

    theorem :: GOBRD14:25

    

     Th25: p in ( RightComp f) implies ( N-bound ( L~ f)) > (p `2 )

    proof

      set g = ( Rotate (f,( N-min ( L~ f))));

      

       A1: ( L~ f) = ( L~ g) by REVROT_1: 33;

      reconsider u = p as Point of ( Euclid 2) by EUCLID: 22;

      assume p in ( RightComp f);

      then p in ( RightComp g) by REVROT_1: 37;

      then u in ( Int ( RightComp g)) by TOPS_1: 23;

      then

      consider r be Real such that

       A2: r > 0 and

       A3: ( Ball (u,r)) c= ( RightComp g) by GOBOARD6: 5;

      reconsider r as Real;

      reconsider k = |[(p `1 ), ((p `2 ) + (r / 2))]| as Point of ( Euclid 2) by EUCLID: 22;

      ( dist (u,k)) = (( Pitag_dist 2) . (u,k)) by METRIC_1:def 1

      .= ( sqrt ((((p `1 ) - ( |[(p `1 ), ((p `2 ) + (r / 2))]| `1 )) ^2 ) + (((p `2 ) - ( |[(p `1 ), ((p `2 ) + (r / 2))]| `2 )) ^2 ))) by TOPREAL3: 7

      .= ( sqrt ((((p `1 ) - (p `1 )) ^2 ) + (((p `2 ) - ( |[(p `1 ), ((p `2 ) + (r / 2))]| `2 )) ^2 ))) by EUCLID: 52

      .= ( sqrt (((p `2 ) - ((p `2 ) + (r / 2))) ^2 )) by EUCLID: 52

      .= ( sqrt ((r / 2) ^2 ))

      .= (r / 2) by A2, SQUARE_1: 22;

      then ( dist (u,k)) < (r / 1) by A2, XREAL_1: 76;

      then

       A4: k in ( Ball (u,r)) by METRIC_1: 11;

      ( RightComp g) misses ( LeftComp g) by Th14;

      then

       A5: not |[(p `1 ), ((p `2 ) + (r / 2))]| in ( LeftComp g) by A3, A4, XBOOLE_0: 3;

      set x = |[( E-bound ( L~ ( SpStSeq ( L~ g)))), ((p `2 ) + (r / 2))]|;

      

       A6: ( LSeg (( SE-corner ( L~ g)),( NE-corner ( L~ g)))) c= ( L~ ( SpStSeq ( L~ g))) by TOPREAL6: 35;

      

       A7: ( proj2 . x) = (x `2 ) by PSCOMP_1:def 6

      .= ((p `2 ) + (r / 2)) by EUCLID: 52;

      ( N-min ( L~ f)) in ( rng f) by SPRECT_2: 39;

      then

       A8: (g /. 1) = ( N-min ( L~ g)) by A1, FINSEQ_6: 92;

      then ( |[(p `1 ), ((p `2 ) + (r / 2))]| `2 ) <= ( N-bound ( L~ g)) by A5, JORDAN2C: 113;

      then ((p `2 ) + (r / 2)) <= ( N-bound ( L~ g)) by EUCLID: 52;

      then

       A9: (x `2 ) <= ( N-bound ( L~ g)) by EUCLID: 52;

      (x `1 ) = ( E-bound ( L~ ( SpStSeq ( L~ g)))) by EUCLID: 52;

      then

       A10: (x `1 ) = ( E-bound ( L~ g)) by SPRECT_1: 61;

      ( |[(p `1 ), ((p `2 ) + (r / 2))]| `2 ) >= ( S-bound ( L~ g)) by A8, A5, JORDAN2C: 112;

      then ((p `2 ) + (r / 2)) >= ( S-bound ( L~ g)) by EUCLID: 52;

      then

       A11: (x `2 ) >= ( S-bound ( L~ g)) by EUCLID: 52;

      ( LSeg (( SE-corner ( L~ g)),( NE-corner ( L~ g)))) = { q : (q `1 ) = ( E-bound ( L~ g)) & (q `2 ) <= ( N-bound ( L~ g)) & (q `2 ) >= ( S-bound ( L~ g)) } by SPRECT_1: 23;

      then x in ( LSeg (( SE-corner ( L~ g)),( NE-corner ( L~ g)))) by A9, A11, A10;

      then ( proj2 .: ( L~ ( SpStSeq ( L~ g)))) is bounded_above & ((p `2 ) + (r / 2)) in ( proj2 .: ( L~ ( SpStSeq ( L~ g)))) by A6, A7, FUNCT_2: 35;

      then

       A12: ( upper_bound ( proj2 .: ( L~ ( SpStSeq ( L~ g))))) >= ((p `2 ) + (r / 2)) by SEQ_4:def 1;

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

      then

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

      ( N-bound ( L~ ( SpStSeq ( L~ g)))) = ( N-bound ( L~ g)) & ( N-bound ( L~ ( SpStSeq ( L~ g)))) = ( upper_bound ( proj2 .: ( L~ ( SpStSeq ( L~ g))))) by SPRECT_1: 45, SPRECT_1: 60;

      hence thesis by A1, A12, A13, XXREAL_0: 2;

    end;

    theorem :: GOBRD14:26

    

     Th26: p in ( RightComp f) implies ( S-bound ( L~ f)) < (p `2 )

    proof

      set g = ( Rotate (f,( N-min ( L~ f))));

      

       A1: ( L~ f) = ( L~ g) by REVROT_1: 33;

      reconsider u = p as Point of ( Euclid 2) by EUCLID: 22;

      assume p in ( RightComp f);

      then p in ( RightComp g) by REVROT_1: 37;

      then u in ( Int ( RightComp g)) by TOPS_1: 23;

      then

      consider r be Real such that

       A2: r > 0 and

       A3: ( Ball (u,r)) c= ( RightComp g) by GOBOARD6: 5;

      reconsider r as Real;

      reconsider k = |[(p `1 ), ((p `2 ) - (r / 2))]| as Point of ( Euclid 2) by EUCLID: 22;

      ( dist (u,k)) = (( Pitag_dist 2) . (u,k)) by METRIC_1:def 1

      .= ( sqrt ((((p `1 ) - ( |[(p `1 ), ((p `2 ) - (r / 2))]| `1 )) ^2 ) + (((p `2 ) - ( |[(p `1 ), ((p `2 ) - (r / 2))]| `2 )) ^2 ))) by TOPREAL3: 7

      .= ( sqrt ((((p `1 ) - (p `1 )) ^2 ) + (((p `2 ) - ( |[(p `1 ), ((p `2 ) - (r / 2))]| `2 )) ^2 ))) by EUCLID: 52

      .= ( sqrt (((p `2 ) - ((p `2 ) - (r / 2))) ^2 )) by EUCLID: 52

      .= (r / 2) by A2, SQUARE_1: 22;

      then ( dist (u,k)) < (r / 1) by A2, XREAL_1: 76;

      then

       A4: k in ( Ball (u,r)) by METRIC_1: 11;

      ( RightComp g) misses ( LeftComp g) by Th14;

      then

       A5: not |[(p `1 ), ((p `2 ) - (r / 2))]| in ( LeftComp g) by A3, A4, XBOOLE_0: 3;

      set x = |[( E-bound ( L~ ( SpStSeq ( L~ g)))), ((p `2 ) - (r / 2))]|;

      

       A6: ( LSeg (( SE-corner ( L~ g)),( NE-corner ( L~ g)))) c= ( L~ ( SpStSeq ( L~ g))) by TOPREAL6: 35;

      

       A7: ( proj2 . x) = (x `2 ) by PSCOMP_1:def 6

      .= ((p `2 ) - (r / 2)) by EUCLID: 52;

      ( N-min ( L~ f)) in ( rng f) by SPRECT_2: 39;

      then

       A8: (g /. 1) = ( N-min ( L~ g)) by A1, FINSEQ_6: 92;

      then ( |[(p `1 ), ((p `2 ) - (r / 2))]| `2 ) <= ( N-bound ( L~ g)) by A5, JORDAN2C: 113;

      then ((p `2 ) - (r / 2)) <= ( N-bound ( L~ g)) by EUCLID: 52;

      then

       A9: (x `2 ) <= ( N-bound ( L~ g)) by EUCLID: 52;

      (x `1 ) = ( E-bound ( L~ ( SpStSeq ( L~ g)))) by EUCLID: 52;

      then

       A10: (x `1 ) = ( E-bound ( L~ g)) by SPRECT_1: 61;

      ( |[(p `1 ), ((p `2 ) - (r / 2))]| `2 ) >= ( S-bound ( L~ g)) by A8, A5, JORDAN2C: 112;

      then ((p `2 ) - (r / 2)) >= ( S-bound ( L~ g)) by EUCLID: 52;

      then

       A11: (x `2 ) >= ( S-bound ( L~ g)) by EUCLID: 52;

      ( LSeg (( SE-corner ( L~ g)),( NE-corner ( L~ g)))) = { q : (q `1 ) = ( E-bound ( L~ g)) & (q `2 ) <= ( N-bound ( L~ g)) & (q `2 ) >= ( S-bound ( L~ g)) } by SPRECT_1: 23;

      then x in ( LSeg (( SE-corner ( L~ g)),( NE-corner ( L~ g)))) by A9, A11, A10;

      then ( proj2 .: ( L~ ( SpStSeq ( L~ g)))) is bounded_below & ((p `2 ) - (r / 2)) in ( proj2 .: ( L~ ( SpStSeq ( L~ g)))) by A6, A7, FUNCT_2: 35;

      then

       A12: ( lower_bound ( proj2 .: ( L~ ( SpStSeq ( L~ g))))) <= ((p `2 ) - (r / 2)) by SEQ_4:def 2;

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

      then

       A13: ((p `2 ) - (r / 2)) < ((p `2 ) - 0 ) by XREAL_1: 15;

      ( S-bound ( L~ ( SpStSeq ( L~ g)))) = ( S-bound ( L~ g)) & ( S-bound ( L~ ( SpStSeq ( L~ g)))) = ( lower_bound ( proj2 .: ( L~ ( SpStSeq ( L~ g))))) by SPRECT_1: 44, SPRECT_1: 59;

      hence thesis by A1, A12, A13, XXREAL_0: 2;

    end;

    theorem :: GOBRD14:27

    

     Th27: p in ( RightComp f) & q in ( LeftComp f) implies ( LSeg (p,q)) meets ( L~ f)

    proof

      assume that

       A1: p in ( RightComp f) and

       A2: q in ( LeftComp f);

      assume ( LSeg (p,q)) misses ( L~ f);

      then ( LSeg (p,q)) c= (( L~ f) ` ) by TDLAT_1: 2;

      then

      reconsider A = ( LSeg (p,q)) as Subset of (( TOP-REAL 2) | (( L~ f) ` )) by PRE_TOPC: 8;

      ( LeftComp f) is_a_component_of (( L~ f) ` ) by GOBOARD9:def 1;

      then

      consider L be Subset of (( TOP-REAL 2) | (( L~ f) ` )) such that

       A3: L = ( LeftComp f) and

       A4: L is a_component by CONNSP_1:def 6;

      q in A by RLTOPSP1: 68;

      then

       A5: L meets A by A2, A3, XBOOLE_0: 3;

      ( RightComp f) is_a_component_of (( L~ f) ` ) by GOBOARD9:def 2;

      then

      consider R be Subset of (( TOP-REAL 2) | (( L~ f) ` )) such that

       A6: R = ( RightComp f) and

       A7: R is a_component by CONNSP_1:def 6;

      p in A by RLTOPSP1: 68;

      then A is connected & R meets A by A1, A6, CONNSP_1: 23, XBOOLE_0: 3;

      hence contradiction by A6, A7, A3, A4, A5, JORDAN2C: 92, SPRECT_4: 6;

    end;

    theorem :: GOBRD14:28

    

     Th28: ( Cl ( RightComp ( SpStSeq C))) = ( product ((1,2) --> ( [.( W-bound ( L~ ( SpStSeq C))), ( E-bound ( L~ ( SpStSeq C))).], [.( S-bound ( L~ ( SpStSeq C))), ( N-bound ( L~ ( SpStSeq C))).])))

    proof

      set g = ((1,2) --> ( [.( W-bound ( L~ ( SpStSeq C))), ( E-bound ( L~ ( SpStSeq C))).], [.( S-bound ( L~ ( SpStSeq C))), ( N-bound ( L~ ( SpStSeq C))).]));

      

       A1: ( dom g) = {1, 2} by FUNCT_4: 62;

      

       A2: ( Cl ( RightComp ( SpStSeq C))) = (( RightComp ( SpStSeq C)) \/ ( L~ ( SpStSeq C))) by Th21;

      hereby

        let a be object;

        assume

         A3: a in ( Cl ( RightComp ( SpStSeq C)));

        then

        reconsider b = a as Point of ( TOP-REAL 2);

        reconsider h = a as FinSequence by A3;

        

         A4: for x be object st x in {1, 2} holds (h . x) in (g . x)

        proof

          let x be object such that

           A5: x in {1, 2};

          per cases by A5, TARSKI:def 2;

            suppose

             A6: x = 1;

            then

             A7: (g . x) = [.( W-bound ( L~ ( SpStSeq C))), ( E-bound ( L~ ( SpStSeq C))).] by FUNCT_4: 63;

            now

              per cases by A2, A3, XBOOLE_0:def 3;

                case a in ( RightComp ( SpStSeq C));

                then ( W-bound ( L~ ( SpStSeq C))) < (b `1 ) & ( E-bound ( L~ ( SpStSeq C))) > (b `1 ) by Th23, Th24;

                hence thesis by A6, A7, XXREAL_1: 1;

              end;

                case a in ( L~ ( SpStSeq C));

                then ( W-bound ( L~ ( SpStSeq C))) <= (b `1 ) & (b `1 ) <= ( E-bound ( L~ ( SpStSeq C))) by PSCOMP_1: 24;

                hence thesis by A6, A7, XXREAL_1: 1;

              end;

            end;

            hence thesis;

          end;

            suppose

             A8: x = 2;

            then

             A9: (g . x) = [.( S-bound ( L~ ( SpStSeq C))), ( N-bound ( L~ ( SpStSeq C))).] by FUNCT_4: 63;

            now

              per cases by A2, A3, XBOOLE_0:def 3;

                case a in ( RightComp ( SpStSeq C));

                then ( S-bound ( L~ ( SpStSeq C))) < (b `2 ) & ( N-bound ( L~ ( SpStSeq C))) > (b `2 ) by Th25, Th26;

                hence thesis by A8, A9, XXREAL_1: 1;

              end;

                case a in ( L~ ( SpStSeq C));

                then ( S-bound ( L~ ( SpStSeq C))) <= (b `2 ) & (b `2 ) <= ( N-bound ( L~ ( SpStSeq C))) by PSCOMP_1: 24;

                hence thesis by A8, A9, XXREAL_1: 1;

              end;

            end;

            hence thesis;

          end;

        end;

        a is Tuple of 2, REAL by A3, Lm1, FINSEQ_2: 131;

        then ex r,s be Element of REAL st a = <*r, s*> by FINSEQ_2: 100;

        then ( dom h) = {1, 2} by FINSEQ_1: 2, FINSEQ_1: 89;

        hence a in ( product g) by A1, A4, CARD_3: 9;

      end;

      let a be object;

      assume a in ( product g);

      then

      consider h be Function such that

       A10: a = h and

       A11: ( dom h) = ( dom g) and

       A12: for x be object st x in ( dom g) holds (h . x) in (g . x) by CARD_3:def 5;

      

       A13: [.( S-bound ( L~ ( SpStSeq C))), ( N-bound ( L~ ( SpStSeq C))).] = { s where s be Real : ( S-bound ( L~ ( SpStSeq C))) <= s & s <= ( N-bound ( L~ ( SpStSeq C))) } by RCOMP_1:def 1;

      2 in ( dom g) by A1, TARSKI:def 2;

      then (h . 2) in (g . 2) by A12;

      then (h . 2) in [.( S-bound ( L~ ( SpStSeq C))), ( N-bound ( L~ ( SpStSeq C))).] by FUNCT_4: 63;

      then

      consider s be Real such that

       A14: (h . 2) = s and

       A15: ( S-bound ( L~ ( SpStSeq C))) <= s & s <= ( N-bound ( L~ ( SpStSeq C))) by A13;

      

       A16: [.( W-bound ( L~ ( SpStSeq C))), ( E-bound ( L~ ( SpStSeq C))).] = { r where r be Real : ( W-bound ( L~ ( SpStSeq C))) <= r & r <= ( E-bound ( L~ ( SpStSeq C))) } by RCOMP_1:def 1;

      1 in ( dom g) by A1, TARSKI:def 2;

      then (h . 1) in (g . 1) by A12;

      then (h . 1) in [.( W-bound ( L~ ( SpStSeq C))), ( E-bound ( L~ ( SpStSeq C))).] by FUNCT_4: 63;

      then

      consider r be Real such that

       A17: (h . 1) = r and

       A18: ( W-bound ( L~ ( SpStSeq C))) <= r & r <= ( E-bound ( L~ ( SpStSeq C))) by A16;

      

       A19: ( LeftComp ( SpStSeq C)) = { q : not (( W-bound ( L~ ( SpStSeq C))) <= (q `1 ) & (q `1 ) <= ( E-bound ( L~ ( SpStSeq C))) & ( S-bound ( L~ ( SpStSeq C))) <= (q `2 ) & (q `2 ) <= ( N-bound ( L~ ( SpStSeq C)))) } by SPRECT_3: 37;

      

       A20: for k be object st k in ( dom h) holds (h . k) = ( <*r, s*> . k)

      proof

        let k be object;

        assume k in ( dom h);

        then k = 1 or k = 2 by A11, TARSKI:def 2;

        hence thesis by A17, A14, FINSEQ_1: 44;

      end;

      ( dom <*r, s*>) = {1, 2} by FINSEQ_1: 2, FINSEQ_1: 89;

      then

       A21: a = |[r, s]| by A10, A11, A20, FUNCT_1: 2, FUNCT_4: 62;

      assume not a in ( Cl ( RightComp ( SpStSeq C)));

      then ( not a in ( RightComp ( SpStSeq C))) & not a in ( L~ ( SpStSeq C)) by A2, XBOOLE_0:def 3;

      then a in ( LeftComp ( SpStSeq C)) by A21, Th16;

      then ex q st q = a & not (( W-bound ( L~ ( SpStSeq C))) <= (q `1 ) & (q `1 ) <= ( E-bound ( L~ ( SpStSeq C))) & ( S-bound ( L~ ( SpStSeq C))) <= (q `2 ) & (q `2 ) <= ( N-bound ( L~ ( SpStSeq C)))) by A19;

      hence contradiction by A18, A15, A21, EUCLID: 52;

    end;

    theorem :: GOBRD14:29

    

     Th29: ( proj1 .: ( Cl ( RightComp f))) = ( proj1 .: ( L~ f))

    proof

      set g = ( Rotate (f,( N-min ( L~ f))));

      

       A1: ( L~ f) = ( L~ g) by REVROT_1: 33;

      ( N-min ( L~ f)) in ( rng f) by SPRECT_2: 39;

      then

       A2: (g /. 1) = ( N-min ( L~ g)) by A1, FINSEQ_6: 92;

      thus ( proj1 .: ( Cl ( RightComp f))) c= ( proj1 .: ( L~ f))

      proof

        

         A3: ( Cl ( RightComp f)) = (( RightComp f) \/ ( L~ f)) by Th21;

        let a be object;

        assume a in ( proj1 .: ( Cl ( RightComp f)));

        then

        consider x be object such that

         A4: x in the carrier of ( TOP-REAL 2) and

         A5: x in ( Cl ( RightComp f)) and

         A6: a = ( proj1 . x) by FUNCT_2: 64;

        per cases by A5, A3, XBOOLE_0:def 3;

          suppose

           A7: x in ( RightComp f);

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

          set b = |[(x `1 ), (( N-bound ( L~ f)) + 1)]|;

          (b `2 ) = (( N-bound ( L~ f)) + 1) & (( N-bound ( L~ f)) + 1) > (( N-bound ( L~ f)) + 0 ) by EUCLID: 52, XREAL_1: 6;

          then b in ( LeftComp g) by A1, A2, JORDAN2C: 113;

          then b in ( LeftComp f) by REVROT_1: 36;

          then ( LSeg (x,b)) meets ( L~ f) by A7, Th27;

          then

          consider c be object such that

           A8: c in ( LSeg (x,b)) and

           A9: c in ( L~ f) by XBOOLE_0: 3;

          reconsider c as Point of ( TOP-REAL 2) by A8;

          

           A10: (b `1 ) = (x `1 ) by EUCLID: 52;

          ( proj1 . c) = (c `1 ) by PSCOMP_1:def 5

          .= (x `1 ) by A8, A10, GOBOARD7: 5

          .= a by A6, PSCOMP_1:def 5;

          hence thesis by A9, FUNCT_2: 35;

        end;

          suppose x in ( L~ f);

          hence thesis by A6, FUNCT_2: 35;

        end;

      end;

      ( L~ f) = (( Cl ( RightComp f)) \ ( RightComp f)) by Th19;

      hence thesis by RELAT_1: 123, XBOOLE_1: 36;

    end;

    theorem :: GOBRD14:30

    

     Th30: ( proj2 .: ( Cl ( RightComp f))) = ( proj2 .: ( L~ f))

    proof

      set g = ( Rotate (f,( N-min ( L~ f))));

      

       A1: ( L~ f) = ( L~ g) by REVROT_1: 33;

      ( N-min ( L~ f)) in ( rng f) by SPRECT_2: 39;

      then

       A2: (g /. 1) = ( N-min ( L~ g)) by A1, FINSEQ_6: 92;

      thus ( proj2 .: ( Cl ( RightComp f))) c= ( proj2 .: ( L~ f))

      proof

        

         A3: ( Cl ( RightComp f)) = (( RightComp f) \/ ( L~ f)) by Th21;

        let a be object;

        assume a in ( proj2 .: ( Cl ( RightComp f)));

        then

        consider x be object such that

         A4: x in the carrier of ( TOP-REAL 2) and

         A5: x in ( Cl ( RightComp f)) and

         A6: a = ( proj2 . x) by FUNCT_2: 64;

        per cases by A5, A3, XBOOLE_0:def 3;

          suppose

           A7: x in ( RightComp f);

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

          set b = |[(( E-bound ( L~ f)) + 1), (x `2 )]|;

          (b `1 ) = (( E-bound ( L~ f)) + 1) & (( E-bound ( L~ f)) + 1) > (( E-bound ( L~ f)) + 0 ) by EUCLID: 52, XREAL_1: 6;

          then b in ( LeftComp g) by A1, A2, JORDAN2C: 111;

          then b in ( LeftComp f) by REVROT_1: 36;

          then ( LSeg (x,b)) meets ( L~ f) by A7, Th27;

          then

          consider c be object such that

           A8: c in ( LSeg (x,b)) and

           A9: c in ( L~ f) by XBOOLE_0: 3;

          reconsider c as Point of ( TOP-REAL 2) by A8;

          

           A10: (b `2 ) = (x `2 ) by EUCLID: 52;

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

          .= (x `2 ) by A8, A10, GOBOARD7: 6

          .= a by A6, PSCOMP_1:def 6;

          hence thesis by A9, FUNCT_2: 35;

        end;

          suppose x in ( L~ f);

          hence thesis by A6, FUNCT_2: 35;

        end;

      end;

      ( L~ f) = (( Cl ( RightComp f)) \ ( RightComp f)) by Th19;

      hence thesis by RELAT_1: 123, XBOOLE_1: 36;

    end;

    theorem :: GOBRD14:31

    

     Th31: ( RightComp g) c= ( RightComp ( SpStSeq ( L~ g)))

    proof

      let a be object;

      assume

       A1: a in ( RightComp g);

      then

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

      (p `1 ) > ( W-bound ( L~ g)) by A1, Th23;

      then

       A2: (p `1 ) > ( W-bound ( L~ ( SpStSeq ( L~ g)))) by SPRECT_1: 58;

      (p `2 ) > ( S-bound ( L~ g)) by A1, Th26;

      then

       A3: (p `2 ) > ( S-bound ( L~ ( SpStSeq ( L~ g)))) by SPRECT_1: 59;

      (p `1 ) < ( E-bound ( L~ g)) by A1, Th24;

      then

       A4: (p `1 ) < ( E-bound ( L~ ( SpStSeq ( L~ g)))) by SPRECT_1: 61;

      (p `2 ) < ( N-bound ( L~ g)) by A1, Th25;

      then

       A5: (p `2 ) < ( N-bound ( L~ ( SpStSeq ( L~ g)))) by SPRECT_1: 60;

      ( RightComp ( SpStSeq ( L~ g))) = { q : ( W-bound ( L~ ( SpStSeq ( L~ g)))) < (q `1 ) & (q `1 ) < ( E-bound ( L~ ( SpStSeq ( L~ g)))) & ( S-bound ( L~ ( SpStSeq ( L~ g)))) < (q `2 ) & (q `2 ) < ( N-bound ( L~ ( SpStSeq ( L~ g)))) } by SPRECT_3: 37;

      hence thesis by A2, A4, A3, A5;

    end;

    theorem :: GOBRD14:32

    

     Th32: ( Cl ( RightComp g)) is compact

    proof

      ( Cl ( RightComp ( SpStSeq ( L~ g)))) = ( product ((1,2) --> ( [.( W-bound ( L~ ( SpStSeq ( L~ g)))), ( E-bound ( L~ ( SpStSeq ( L~ g)))).], [.( S-bound ( L~ ( SpStSeq ( L~ g)))), ( N-bound ( L~ ( SpStSeq ( L~ g)))).]))) by Th28;

      then

       A1: ( Cl ( RightComp ( SpStSeq ( L~ g)))) is compact by TOPREAL6: 78;

      ( RightComp g) c= ( RightComp ( SpStSeq ( L~ g))) by Th31;

      hence thesis by A1, COMPTS_1: 9, PRE_TOPC: 19;

    end;

    theorem :: GOBRD14:33

    

     Th33: ( LeftComp g) is non bounded

    proof

      ( Cl ( RightComp g)) is compact by Th32;

      then ( RightComp g) is bounded by PRE_TOPC: 18, RLTOPSP1: 42;

      then

       A1: (( L~ g) \/ ( RightComp g)) is bounded by TOPREAL6: 67;

      ((( L~ g) \/ ( RightComp g)) \/ ( LeftComp g)) = the carrier of ( TOP-REAL 2) by Th15;

      hence thesis by A1, TOPREAL6: 66;

    end;

    theorem :: GOBRD14:34

    

     Th34: ( LeftComp g) is_outside_component_of ( L~ g) by GOBOARD9:def 1, Th33;

    theorem :: GOBRD14:35

    ( RightComp g) is_inside_component_of ( L~ g)

    proof

      thus ( RightComp g) is_a_component_of (( L~ g) ` ) by GOBOARD9:def 2;

      ( Cl ( RightComp g)) is compact by Th32;

      hence thesis by PRE_TOPC: 18, RLTOPSP1: 42;

    end;

    theorem :: GOBRD14:36

    

     Th36: ( UBD ( L~ g)) = ( LeftComp g)

    proof

      ( UBD ( L~ g)) is_outside_component_of ( L~ g) & ( LeftComp g) is_outside_component_of ( L~ g) by Th34, JORDAN2C: 68;

      hence thesis by JORDAN2C: 119;

    end;

    theorem :: GOBRD14:37

    

     Th37: ( BDD ( L~ g)) = ( RightComp g)

    proof

      

       A1: ( BDD ( L~ g)) misses ( UBD ( L~ g)) by JORDAN2C: 24;

      

       A2: (( L~ g) ` ) = (( BDD ( L~ g)) \/ ( UBD ( L~ g))) & ( LeftComp g) misses ( RightComp g) by Th14, JORDAN2C: 27;

      ( UBD ( L~ g)) = ( LeftComp g) & (( L~ g) ` ) = (( LeftComp g) \/ ( RightComp g)) by Th36, GOBRD12: 10;

      hence thesis by A2, A1, XBOOLE_1: 71;

    end;

    theorem :: GOBRD14:38

    P is_outside_component_of ( L~ g) implies P = ( LeftComp g)

    proof

      assume

       A1: P is_outside_component_of ( L~ g);

      ( UBD ( L~ g)) is_outside_component_of ( L~ g) by JORDAN2C: 68;

      then P = ( UBD ( L~ g)) by A1, JORDAN2C: 119;

      hence thesis by Th36;

    end;

    theorem :: GOBRD14:39

    

     Th39: P is_inside_component_of ( L~ g) implies P meets ( RightComp g)

    proof

      assume P is_inside_component_of ( L~ g);

      then

       A1: P c= ( BDD ( L~ g)) & P is_a_component_of (( L~ g) ` ) by JORDAN2C: 22;

      ( BDD ( L~ g)) = ( RightComp g) by Th37;

      hence thesis by A1, SPRECT_1: 4, XBOOLE_1: 67;

    end;

    theorem :: GOBRD14:40

    P is_inside_component_of ( L~ g) implies P = ( BDD ( L~ g))

    proof

      

       A1: ( RightComp g) = ( BDD ( L~ g)) by Th37;

      ( BDD ( L~ g)) is_inside_component_of ( L~ g) by JORDAN2C: 108;

      then

       A2: ( BDD ( L~ g)) is_a_component_of (( L~ g) ` );

      assume

       A3: P is_inside_component_of ( L~ g);

      thus thesis by A3, A1, A2, Th39, GOBOARD9: 1;

    end;

    theorem :: GOBRD14:41

    ( W-bound ( L~ g)) = ( W-bound ( RightComp g))

    proof

      set A = (( Cl ( RightComp g)) \ ( RightComp g));

      

       A1: ( W-bound ( Cl ( RightComp g))) = ( lower_bound ( proj1 .: ( Cl ( RightComp g)))) by SPRECT_1: 43;

      

       A2: ( L~ g) = A by Th19;

      ( Cl ( RightComp g)) is compact by Th32;

      then

       A3: ( RightComp g) is bounded by PRE_TOPC: 18, RLTOPSP1: 42;

      reconsider A as non empty Subset of ( TOP-REAL 2) by A2;

      ( proj1 .: ( Cl ( RightComp g))) = ( proj1 .: ( L~ g)) & ( W-bound A) = ( lower_bound ( proj1 .: A)) by Th29, SPRECT_1: 43;

      hence thesis by A2, A3, A1, TOPREAL6: 85;

    end;

    theorem :: GOBRD14:42

    ( E-bound ( L~ g)) = ( E-bound ( RightComp g))

    proof

      set A = (( Cl ( RightComp g)) \ ( RightComp g));

      

       A1: ( E-bound ( Cl ( RightComp g))) = ( upper_bound ( proj1 .: ( Cl ( RightComp g)))) by SPRECT_1: 46;

      

       A2: ( L~ g) = A by Th19;

      ( Cl ( RightComp g)) is compact by Th32;

      then

       A3: ( RightComp g) is bounded by PRE_TOPC: 18, RLTOPSP1: 42;

      reconsider A as non empty Subset of ( TOP-REAL 2) by A2;

      ( proj1 .: ( Cl ( RightComp g))) = ( proj1 .: ( L~ g)) & ( E-bound A) = ( upper_bound ( proj1 .: A)) by Th29, SPRECT_1: 46;

      hence thesis by A2, A3, A1, TOPREAL6: 86;

    end;

    theorem :: GOBRD14:43

    ( N-bound ( L~ g)) = ( N-bound ( RightComp g))

    proof

      set A = (( Cl ( RightComp g)) \ ( RightComp g));

      

       A1: ( N-bound ( Cl ( RightComp g))) = ( upper_bound ( proj2 .: ( Cl ( RightComp g)))) by SPRECT_1: 45;

      

       A2: ( L~ g) = A by Th19;

      ( Cl ( RightComp g)) is compact by Th32;

      then

       A3: ( RightComp g) is bounded by PRE_TOPC: 18, RLTOPSP1: 42;

      reconsider A as non empty Subset of ( TOP-REAL 2) by A2;

      ( proj2 .: ( Cl ( RightComp g))) = ( proj2 .: ( L~ g)) & ( N-bound A) = ( upper_bound ( proj2 .: A)) by Th30, SPRECT_1: 45;

      hence thesis by A2, A3, A1, TOPREAL6: 87;

    end;

    theorem :: GOBRD14:44

    ( S-bound ( L~ g)) = ( S-bound ( RightComp g))

    proof

      set A = (( Cl ( RightComp g)) \ ( RightComp g));

      

       A1: ( S-bound ( Cl ( RightComp g))) = ( lower_bound ( proj2 .: ( Cl ( RightComp g)))) by SPRECT_1: 44;

      

       A2: ( L~ g) = A by Th19;

      ( Cl ( RightComp g)) is compact by Th32;

      then

       A3: ( RightComp g) is bounded by PRE_TOPC: 18, RLTOPSP1: 42;

      reconsider A as non empty Subset of ( TOP-REAL 2) by A2;

      ( proj2 .: ( Cl ( RightComp g))) = ( proj2 .: ( L~ g)) & ( S-bound A) = ( lower_bound ( proj2 .: A)) by Th30, SPRECT_1: 44;

      hence thesis by A2, A3, A1, TOPREAL6: 88;

    end;