let f be rectangular special_circular_sequence; :: thesis: ( LeftComp f = { p where p is Point of (TOP-REAL 2) : ( not W-bound (L~ f) <= p `1 or not p `1 <= E-bound (L~ f) or not S-bound (L~ f) <= p `2 or not p `2 <= N-bound (L~ f) ) } & RightComp f = { q where q is Point of (TOP-REAL 2) : ( W-bound (L~ f) < q `1 & q `1 < E-bound (L~ f) & S-bound (L~ f) < q `2 & q `2 < N-bound (L~ f) ) } )

defpred S_{1}[ Element of (TOP-REAL 2)] means ( not W-bound (L~ f) <= $1 `1 or not $1 `1 <= E-bound (L~ f) or not S-bound (L~ f) <= $1 `2 or not $1 `2 <= N-bound (L~ f) );

defpred S_{2}[ Element of (TOP-REAL 2)] means ( W-bound (L~ f) < $1 `1 & $1 `1 < E-bound (L~ f) & S-bound (L~ f) < $1 `2 & $1 `2 < N-bound (L~ f) );

defpred S_{3}[ Element of (TOP-REAL 2)] means ( ( $1 `1 = W-bound (L~ f) & $1 `2 <= N-bound (L~ f) & $1 `2 >= S-bound (L~ f) ) or ( $1 `1 <= E-bound (L~ f) & $1 `1 >= W-bound (L~ f) & $1 `2 = N-bound (L~ f) ) or ( $1 `1 <= E-bound (L~ f) & $1 `1 >= W-bound (L~ f) & $1 `2 = S-bound (L~ f) ) or ( $1 `1 = E-bound (L~ f) & $1 `2 <= N-bound (L~ f) & $1 `2 >= S-bound (L~ f) ) );

set LC = { p where p is Point of (TOP-REAL 2) : S_{1}[p] } ;

set RC = { q where q is Point of (TOP-REAL 2) : S_{2}[q] } ;

set Lf = { p where p is Point of (TOP-REAL 2) : S_{3}[p] } ;

A1: S-bound (L~ f) < N-bound (L~ f) by SPRECT_1:32;

A2: { p where p is Point of (TOP-REAL 2) : S_{3}[p] } is Subset of (TOP-REAL 2)
from DOMAIN_1:sch 7();

A3: { q where q is Point of (TOP-REAL 2) : S_{2}[q] } is Subset of (TOP-REAL 2)
from DOMAIN_1:sch 7();

A4: L~ f = { p where p is Point of (TOP-REAL 2) : S_{3}[p] }
by Th35;

{ p where p is Point of (TOP-REAL 2) : S_{1}[p] } is Subset of (TOP-REAL 2)
from DOMAIN_1:sch 7();

then reconsider Lc9 = { p where p is Point of (TOP-REAL 2) : S_{1}[p] } , Rc9 = { q where q is Point of (TOP-REAL 2) : S_{2}[q] } , Lf = { p where p is Point of (TOP-REAL 2) : S_{3}[p] } as Subset of (TOP-REAL 2) by A3, A2;

reconsider Lf = Lf as Subset of (TOP-REAL 2) ;

reconsider Lc9 = Lc9, Rc9 = Rc9 as Subset of (TOP-REAL 2) ;

A5: W-bound (L~ f) < E-bound (L~ f) by SPRECT_1:31;

then reconsider Lc = Lc9, Rc = Rc9 as Subset of ((TOP-REAL 2) | (Lf `)) by A1, JORDAN1:39, JORDAN1:41;

reconsider Lc = Lc, Rc = Rc as Subset of ((TOP-REAL 2) | (Lf `)) ;

A6: ((1 / 2) * (S-bound (L~ f))) + ((1 / 2) * (S-bound (L~ f))) = S-bound (L~ f) ;

Rc = Rc9 ;

then Lc is a_component by A5, A1, JORDAN1:36;

then A7: Lc9 is_a_component_of Lf ` by CONNSP_1:def 6;

set p = ((1 / 2) * (((GoB f) * (1,(width (GoB f)))) + ((GoB f) * ((1 + 1),(width (GoB f)))))) + |[0,1]|;

set q = (1 / 2) * (((GoB f) * (1,(width (GoB f)))) + ((GoB f) * ((1 + 1),(width (GoB f)))));

A8: 1 + 1 <= len f by GOBOARD7:34, XXREAL_0:2;

A9: (((1 / 2) * (((GoB f) * (1,(width (GoB f)))) + ((GoB f) * ((1 + 1),(width (GoB f)))))) + |[0,1]|) `2 = (((1 / 2) * (((GoB f) * (1,(width (GoB f)))) + ((GoB f) * ((1 + 1),(width (GoB f)))))) `2) + (|[0,1]| `2) by TOPREAL3:2

.= (((1 / 2) * (((GoB f) * (1,(width (GoB f)))) + ((GoB f) * ((1 + 1),(width (GoB f)))))) `2) + 1 by EUCLID:52 ;

A10: GoB f = ((f /. 4),(f /. 1)) ][ ((f /. 3),(f /. 2)) by Th36;

then A11: 1 + 1 = width (GoB f) by MATRIX_0:47;

then ((1 / 2) * (((GoB f) * (1,(width (GoB f)))) + ((GoB f) * ((1 + 1),(width (GoB f)))))) `2 = ((1 / 2) * (((GoB f) * (1,(width (GoB f)))) + (f /. 2))) `2 by A10, MATRIX_0:50

.= ((1 / 2) * ((f /. 1) + (f /. 2))) `2 by A10, A11, MATRIX_0:50

.= (1 / 2) * (((f /. 1) + (f /. 2)) `2) by TOPREAL3:4

.= (1 / 2) * (((f /. 1) `2) + ((f /. 2) `2)) by TOPREAL3:2

.= (1 / 2) * (((N-min (L~ f)) `2) + ((f /. 2) `2)) by SPRECT_1:83

.= (1 / 2) * (((N-min (L~ f)) `2) + ((N-max (L~ f)) `2)) by SPRECT_1:84

.= (1 / 2) * ((N-bound (L~ f)) + ((N-max (L~ f)) `2)) by EUCLID:52

.= (1 / 2) * ((N-bound (L~ f)) + (N-bound (L~ f))) by EUCLID:52

.= N-bound (L~ f) ;

then (((1 / 2) * (((GoB f) * (1,(width (GoB f)))) + ((GoB f) * ((1 + 1),(width (GoB f)))))) + |[0,1]|) `2 > 0 + (N-bound (L~ f)) by A9, XREAL_1:8;

then A12: ((1 / 2) * (((GoB f) * (1,(width (GoB f)))) + ((GoB f) * ((1 + 1),(width (GoB f)))))) + |[0,1]| in { p where p is Point of (TOP-REAL 2) : S_{1}[p] }
;

A13: 1 + 1 = len (GoB f) by A10, MATRIX_0:47;

then A14: ((1 / 2) * (((GoB f) * (1,(width (GoB f)))) + ((GoB f) * ((1 + 1),(width (GoB f)))))) + |[0,1]| in Int (cell ((GoB f),1,(1 + 1))) by A11, GOBOARD6:32;

A15: f /. (1 + 1) = (GoB f) * ((1 + 1),(1 + 1)) by A10, MATRIX_0:50;

1 < width (GoB f) by GOBOARD7:33;

then A16: 1 + 1 <= width (GoB f) by NAT_1:13;

then A17: [(1 + 1),(1 + 1)] in Indices (GoB f) by A13, MATRIX_0:30;

1 <= len (GoB f) by GOBOARD7:32;

then A18: [1,(1 + 1)] in Indices (GoB f) by A16, MATRIX_0:30;

A19: f /. 1 = (GoB f) * (1,(1 + 1)) by A10, MATRIX_0:50;

then right_cell (f,1) = cell ((GoB f),1,1) by A8, A18, A17, A15, GOBOARD5:28;

then A20: Int (cell ((GoB f),1,1)) c= RightComp f by GOBOARD9:def 2;

left_cell (f,1) = cell ((GoB f),1,(1 + 1)) by A8, A18, A19, A17, A15, GOBOARD5:28;

then Int (cell ((GoB f),1,(1 + 1))) c= LeftComp f by GOBOARD9:def 1;

then A21: { p where p is Point of (TOP-REAL 2) : S_{1}[p] } meets LeftComp f
by A14, A12, XBOOLE_0:3;

A22: (f /. 2) `1 = (E-max (L~ f)) `1 by SPRECT_1:84

.= E-bound (L~ f) by EUCLID:52 ;

set p = (1 / 2) * (((GoB f) * (1,1)) + ((GoB f) * (2,2)));

A23: (1 / 2) * (((GoB f) * (1,1)) + ((GoB f) * (2,2))) in Int (cell ((GoB f),1,1)) by A13, A11, GOBOARD6:31;

A24: (1 / 2) * (((GoB f) * (1,1)) + ((GoB f) * (2,2))) = (1 / 2) * (((GoB f) * (1,1)) + (f /. 2)) by A10, MATRIX_0:50

.= (1 / 2) * ((f /. 4) + (f /. 2)) by A10, MATRIX_0:50 ;

then A25: ((1 / 2) * (((GoB f) * (1,1)) + ((GoB f) * (2,2)))) `1 = (1 / 2) * (((f /. 4) + (f /. 2)) `1) by TOPREAL3:4

.= (1 / 2) * (((f /. 4) `1) + ((f /. 2) `1)) by TOPREAL3:2

.= ((1 / 2) * ((f /. 4) `1)) + ((1 / 2) * ((f /. 2) `1)) ;

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

hence LeftComp f = { p where p is Point of (TOP-REAL 2) : S_{1}[p] }
by A4, A7, A21, GOBOARD9:1; :: thesis: RightComp f = { q where q is Point of (TOP-REAL 2) : ( W-bound (L~ f) < q `1 & q `1 < E-bound (L~ f) & S-bound (L~ f) < q `2 & q `2 < N-bound (L~ f) ) }

A26: ((1 / 2) * (W-bound (L~ f))) + ((1 / 2) * (W-bound (L~ f))) = W-bound (L~ f) ;

A27: ((1 / 2) * (E-bound (L~ f))) + ((1 / 2) * (E-bound (L~ f))) = E-bound (L~ f) ;

A28: ((1 / 2) * (N-bound (L~ f))) + ((1 / 2) * (N-bound (L~ f))) = N-bound (L~ f) ;

A29: (f /. 4) `1 = (W-min (L~ f)) `1 by SPRECT_1:86

.= W-bound (L~ f) by EUCLID:52 ;

then (1 / 2) * ((f /. 4) `1) < (1 / 2) * (E-bound (L~ f)) by SPRECT_1:31, XREAL_1:68;

then A30: ((1 / 2) * (((GoB f) * (1,1)) + ((GoB f) * (2,2)))) `1 < E-bound (L~ f) by A27, A25, A22, XREAL_1:6;

A31: ((1 / 2) * (((GoB f) * (1,1)) + ((GoB f) * (2,2)))) `2 = (1 / 2) * (((f /. 4) + (f /. 2)) `2) by A24, TOPREAL3:4

.= (1 / 2) * (((f /. 4) `2) + ((f /. 2) `2)) by TOPREAL3:2

.= ((1 / 2) * ((f /. 4) `2)) + ((1 / 2) * ((f /. 2) `2)) ;

Lc = Lc9 ;

then Rc is a_component by A5, A1, JORDAN1:36;

then A32: Rc9 is_a_component_of Lf ` by CONNSP_1:def 6;

A33: (f /. 2) `2 = (N-max (L~ f)) `2 by SPRECT_1:84

.= N-bound (L~ f) by EUCLID:52 ;

A34: (f /. 4) `2 = (S-min (L~ f)) `2 by SPRECT_1:86

.= S-bound (L~ f) by EUCLID:52 ;

then (1 / 2) * ((f /. 4) `2) < (1 / 2) * (N-bound (L~ f)) by SPRECT_1:32, XREAL_1:68;

then A35: ((1 / 2) * (((GoB f) * (1,1)) + ((GoB f) * (2,2)))) `2 < N-bound (L~ f) by A28, A31, A33, XREAL_1:6;

(1 / 2) * ((f /. 2) `2) > (1 / 2) * (S-bound (L~ f)) by A33, SPRECT_1:32, XREAL_1:68;

then A36: S-bound (L~ f) < ((1 / 2) * (((GoB f) * (1,1)) + ((GoB f) * (2,2)))) `2 by A6, A31, A34, XREAL_1:6;

(1 / 2) * ((f /. 2) `1) > (1 / 2) * (W-bound (L~ f)) by A22, SPRECT_1:31, XREAL_1:68;

then W-bound (L~ f) < ((1 / 2) * (((GoB f) * (1,1)) + ((GoB f) * (2,2)))) `1 by A26, A25, A29, XREAL_1:6;

then (1 / 2) * (((GoB f) * (1,1)) + ((GoB f) * (2,2))) in { q where q is Point of (TOP-REAL 2) : S_{2}[q] }
by A30, A36, A35;

then A37: { q where q is Point of (TOP-REAL 2) : S_{2}[q] } meets RightComp f
by A23, A20, XBOOLE_0:3;

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

hence RightComp f = { q where q is Point of (TOP-REAL 2) : ( W-bound (L~ f) < q `1 & q `1 < E-bound (L~ f) & S-bound (L~ f) < q `2 & q `2 < N-bound (L~ f) ) } by A4, A32, A37, GOBOARD9:1; :: thesis: verum

defpred S

defpred S

defpred S

set LC = { p where p is Point of (TOP-REAL 2) : S

set RC = { q where q is Point of (TOP-REAL 2) : S

set Lf = { p where p is Point of (TOP-REAL 2) : S

A1: S-bound (L~ f) < N-bound (L~ f) by SPRECT_1:32;

A2: { p where p is Point of (TOP-REAL 2) : S

A3: { q where q is Point of (TOP-REAL 2) : S

A4: L~ f = { p where p is Point of (TOP-REAL 2) : S

{ p where p is Point of (TOP-REAL 2) : S

then reconsider Lc9 = { p where p is Point of (TOP-REAL 2) : S

reconsider Lf = Lf as Subset of (TOP-REAL 2) ;

reconsider Lc9 = Lc9, Rc9 = Rc9 as Subset of (TOP-REAL 2) ;

A5: W-bound (L~ f) < E-bound (L~ f) by SPRECT_1:31;

then reconsider Lc = Lc9, Rc = Rc9 as Subset of ((TOP-REAL 2) | (Lf `)) by A1, JORDAN1:39, JORDAN1:41;

reconsider Lc = Lc, Rc = Rc as Subset of ((TOP-REAL 2) | (Lf `)) ;

A6: ((1 / 2) * (S-bound (L~ f))) + ((1 / 2) * (S-bound (L~ f))) = S-bound (L~ f) ;

Rc = Rc9 ;

then Lc is a_component by A5, A1, JORDAN1:36;

then A7: Lc9 is_a_component_of Lf ` by CONNSP_1:def 6;

set p = ((1 / 2) * (((GoB f) * (1,(width (GoB f)))) + ((GoB f) * ((1 + 1),(width (GoB f)))))) + |[0,1]|;

set q = (1 / 2) * (((GoB f) * (1,(width (GoB f)))) + ((GoB f) * ((1 + 1),(width (GoB f)))));

A8: 1 + 1 <= len f by GOBOARD7:34, XXREAL_0:2;

A9: (((1 / 2) * (((GoB f) * (1,(width (GoB f)))) + ((GoB f) * ((1 + 1),(width (GoB f)))))) + |[0,1]|) `2 = (((1 / 2) * (((GoB f) * (1,(width (GoB f)))) + ((GoB f) * ((1 + 1),(width (GoB f)))))) `2) + (|[0,1]| `2) by TOPREAL3:2

.= (((1 / 2) * (((GoB f) * (1,(width (GoB f)))) + ((GoB f) * ((1 + 1),(width (GoB f)))))) `2) + 1 by EUCLID:52 ;

A10: GoB f = ((f /. 4),(f /. 1)) ][ ((f /. 3),(f /. 2)) by Th36;

then A11: 1 + 1 = width (GoB f) by MATRIX_0:47;

then ((1 / 2) * (((GoB f) * (1,(width (GoB f)))) + ((GoB f) * ((1 + 1),(width (GoB f)))))) `2 = ((1 / 2) * (((GoB f) * (1,(width (GoB f)))) + (f /. 2))) `2 by A10, MATRIX_0:50

.= ((1 / 2) * ((f /. 1) + (f /. 2))) `2 by A10, A11, MATRIX_0:50

.= (1 / 2) * (((f /. 1) + (f /. 2)) `2) by TOPREAL3:4

.= (1 / 2) * (((f /. 1) `2) + ((f /. 2) `2)) by TOPREAL3:2

.= (1 / 2) * (((N-min (L~ f)) `2) + ((f /. 2) `2)) by SPRECT_1:83

.= (1 / 2) * (((N-min (L~ f)) `2) + ((N-max (L~ f)) `2)) by SPRECT_1:84

.= (1 / 2) * ((N-bound (L~ f)) + ((N-max (L~ f)) `2)) by EUCLID:52

.= (1 / 2) * ((N-bound (L~ f)) + (N-bound (L~ f))) by EUCLID:52

.= N-bound (L~ f) ;

then (((1 / 2) * (((GoB f) * (1,(width (GoB f)))) + ((GoB f) * ((1 + 1),(width (GoB f)))))) + |[0,1]|) `2 > 0 + (N-bound (L~ f)) by A9, XREAL_1:8;

then A12: ((1 / 2) * (((GoB f) * (1,(width (GoB f)))) + ((GoB f) * ((1 + 1),(width (GoB f)))))) + |[0,1]| in { p where p is Point of (TOP-REAL 2) : S

A13: 1 + 1 = len (GoB f) by A10, MATRIX_0:47;

then A14: ((1 / 2) * (((GoB f) * (1,(width (GoB f)))) + ((GoB f) * ((1 + 1),(width (GoB f)))))) + |[0,1]| in Int (cell ((GoB f),1,(1 + 1))) by A11, GOBOARD6:32;

A15: f /. (1 + 1) = (GoB f) * ((1 + 1),(1 + 1)) by A10, MATRIX_0:50;

1 < width (GoB f) by GOBOARD7:33;

then A16: 1 + 1 <= width (GoB f) by NAT_1:13;

then A17: [(1 + 1),(1 + 1)] in Indices (GoB f) by A13, MATRIX_0:30;

1 <= len (GoB f) by GOBOARD7:32;

then A18: [1,(1 + 1)] in Indices (GoB f) by A16, MATRIX_0:30;

A19: f /. 1 = (GoB f) * (1,(1 + 1)) by A10, MATRIX_0:50;

then right_cell (f,1) = cell ((GoB f),1,1) by A8, A18, A17, A15, GOBOARD5:28;

then A20: Int (cell ((GoB f),1,1)) c= RightComp f by GOBOARD9:def 2;

left_cell (f,1) = cell ((GoB f),1,(1 + 1)) by A8, A18, A19, A17, A15, GOBOARD5:28;

then Int (cell ((GoB f),1,(1 + 1))) c= LeftComp f by GOBOARD9:def 1;

then A21: { p where p is Point of (TOP-REAL 2) : S

A22: (f /. 2) `1 = (E-max (L~ f)) `1 by SPRECT_1:84

.= E-bound (L~ f) by EUCLID:52 ;

set p = (1 / 2) * (((GoB f) * (1,1)) + ((GoB f) * (2,2)));

A23: (1 / 2) * (((GoB f) * (1,1)) + ((GoB f) * (2,2))) in Int (cell ((GoB f),1,1)) by A13, A11, GOBOARD6:31;

A24: (1 / 2) * (((GoB f) * (1,1)) + ((GoB f) * (2,2))) = (1 / 2) * (((GoB f) * (1,1)) + (f /. 2)) by A10, MATRIX_0:50

.= (1 / 2) * ((f /. 4) + (f /. 2)) by A10, MATRIX_0:50 ;

then A25: ((1 / 2) * (((GoB f) * (1,1)) + ((GoB f) * (2,2)))) `1 = (1 / 2) * (((f /. 4) + (f /. 2)) `1) by TOPREAL3:4

.= (1 / 2) * (((f /. 4) `1) + ((f /. 2) `1)) by TOPREAL3:2

.= ((1 / 2) * ((f /. 4) `1)) + ((1 / 2) * ((f /. 2) `1)) ;

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

hence LeftComp f = { p where p is Point of (TOP-REAL 2) : S

A26: ((1 / 2) * (W-bound (L~ f))) + ((1 / 2) * (W-bound (L~ f))) = W-bound (L~ f) ;

A27: ((1 / 2) * (E-bound (L~ f))) + ((1 / 2) * (E-bound (L~ f))) = E-bound (L~ f) ;

A28: ((1 / 2) * (N-bound (L~ f))) + ((1 / 2) * (N-bound (L~ f))) = N-bound (L~ f) ;

A29: (f /. 4) `1 = (W-min (L~ f)) `1 by SPRECT_1:86

.= W-bound (L~ f) by EUCLID:52 ;

then (1 / 2) * ((f /. 4) `1) < (1 / 2) * (E-bound (L~ f)) by SPRECT_1:31, XREAL_1:68;

then A30: ((1 / 2) * (((GoB f) * (1,1)) + ((GoB f) * (2,2)))) `1 < E-bound (L~ f) by A27, A25, A22, XREAL_1:6;

A31: ((1 / 2) * (((GoB f) * (1,1)) + ((GoB f) * (2,2)))) `2 = (1 / 2) * (((f /. 4) + (f /. 2)) `2) by A24, TOPREAL3:4

.= (1 / 2) * (((f /. 4) `2) + ((f /. 2) `2)) by TOPREAL3:2

.= ((1 / 2) * ((f /. 4) `2)) + ((1 / 2) * ((f /. 2) `2)) ;

Lc = Lc9 ;

then Rc is a_component by A5, A1, JORDAN1:36;

then A32: Rc9 is_a_component_of Lf ` by CONNSP_1:def 6;

A33: (f /. 2) `2 = (N-max (L~ f)) `2 by SPRECT_1:84

.= N-bound (L~ f) by EUCLID:52 ;

A34: (f /. 4) `2 = (S-min (L~ f)) `2 by SPRECT_1:86

.= S-bound (L~ f) by EUCLID:52 ;

then (1 / 2) * ((f /. 4) `2) < (1 / 2) * (N-bound (L~ f)) by SPRECT_1:32, XREAL_1:68;

then A35: ((1 / 2) * (((GoB f) * (1,1)) + ((GoB f) * (2,2)))) `2 < N-bound (L~ f) by A28, A31, A33, XREAL_1:6;

(1 / 2) * ((f /. 2) `2) > (1 / 2) * (S-bound (L~ f)) by A33, SPRECT_1:32, XREAL_1:68;

then A36: S-bound (L~ f) < ((1 / 2) * (((GoB f) * (1,1)) + ((GoB f) * (2,2)))) `2 by A6, A31, A34, XREAL_1:6;

(1 / 2) * ((f /. 2) `1) > (1 / 2) * (W-bound (L~ f)) by A22, SPRECT_1:31, XREAL_1:68;

then W-bound (L~ f) < ((1 / 2) * (((GoB f) * (1,1)) + ((GoB f) * (2,2)))) `1 by A26, A25, A29, XREAL_1:6;

then (1 / 2) * (((GoB f) * (1,1)) + ((GoB f) * (2,2))) in { q where q is Point of (TOP-REAL 2) : S

then A37: { q where q is Point of (TOP-REAL 2) : S

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

hence RightComp f = { q where q is Point of (TOP-REAL 2) : ( W-bound (L~ f) < q `1 & q `1 < E-bound (L~ f) & S-bound (L~ f) < q `2 & q `2 < N-bound (L~ f) ) } by A4, A32, A37, GOBOARD9:1; :: thesis: verum