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 S1[ 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 S2[ 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 S3[ 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) : S1[p] } ;
set RC = { q where q is Point of (TOP-REAL 2) : S2[q] } ;
set Lf = { p where p is Point of (TOP-REAL 2) : S3[p] } ;
A1: S-bound (L~ f) < N-bound (L~ f) by SPRECT_1:34;
A2: { p where p is Point of (TOP-REAL 2) : S3[p] } is Subset of (TOP-REAL 2) from DOMAIN_1:sch 7();
 A3: { q where q is Point of (TOP-REAL 2) : S2[q] } is Subset of (TOP-REAL 2) from DOMAIN_1:sch 7();
 A4: L~ f = { p where p is Point of (TOP-REAL 2) : S3[p] } by Th52;
{ p where p is Point of (TOP-REAL 2) : S1[p] } is Subset of (TOP-REAL 2) from DOMAIN_1:sch 7();
 then reconsider Lc9 = { p where p is Point of (TOP-REAL 2) : S1[p] } , Rc9 = { q where q is Point of (TOP-REAL 2) : S2[q] } , Lf = { p where p is Point of (TOP-REAL 2) : S3[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:33;
then reconsider Lc = Lc9, Rc = Rc9 as Subset of ((TOP-REAL 2) | (Lf ` )) by A1, JORDAN1:44, JORDAN1:46;
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:41;
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:36, 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:7
.= (((1 / 2) * (((GoB f) * 1,(width (GoB f))) + ((GoB f) * (1 + 1),(width (GoB f))))) `2 ) + 1 by EUCLID:56 ;
A10: GoB f = (f /. 4),(f /. 1) ][ (f /. 3),(f /. 2) by Th53;
then A11: 1 + 1 = width (GoB f) by MATRIX_2:3;
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_2:6
.= ((1 / 2) * ((f /. 1) + (f /. 2))) `2 by A10, A11, MATRIX_2:6
.= (1 / 2) * (((f /. 1) + (f /. 2)) `2 ) by TOPREAL3:9
.= (1 / 2) * (((f /. 1) `2 ) + ((f /. 2) `2 )) by TOPREAL3:7
.= (1 / 2) * (((N-min (L~ f)) `2 ) + ((f /. 2) `2 )) by SPRECT_1:91
.= (1 / 2) * (((N-min (L~ f)) `2 ) + ((N-max (L~ f)) `2 )) by SPRECT_1:92
.= (1 / 2) * ((N-bound (L~ f)) + ((N-max (L~ f)) `2 )) by EUCLID:56
.= (1 / 2) * ((N-bound (L~ f)) + (N-bound (L~ f))) by EUCLID:56
.= 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:10;
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) : S1[p] } ;
A13: 1 + 1 = len (GoB f) by A10, MATRIX_2:3;
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:35;
A15: f /. (1 + 1) = (GoB f) * (1 + 1),(1 + 1) by A10, MATRIX_2:6;
1 < width (GoB f) by GOBOARD7:35;
then A16: 1 + 1 <= width (GoB f) by NAT_1:13;
then A17: [(1 + 1),(1 + 1)] in Indices (GoB f) by A13, MATRIX_1:37;
1 <= len (GoB f) by GOBOARD7:34;
then A18: [1,(1 + 1)] in Indices (GoB f) by A16, MATRIX_1:37;
A19: f /. 1 = (GoB f) * 1,(1 + 1) by A10, MATRIX_2:6;
then right_cell f,1 = cell (GoB f),1,1 by A8, A18, A17, A15, GOBOARD5:29;
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:29;
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) : S1[p] } meets LeftComp f by A14, A12, XBOOLE_0:3;
A22: (f /. 2) `1 = (E-max (L~ f)) `1 by SPRECT_1:92
.= E-bound (L~ f) by EUCLID:56 ;
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:34;
A24: (1 / 2) * (((GoB f) * 1,1) + ((GoB f) * 2,2)) = (1 / 2) * (((GoB f) * 1,1) + (f /. 2)) by A10, MATRIX_2:6
.= (1 / 2) * ((f /. 4) + (f /. 2)) by A10, MATRIX_2:6 ;
then A25: ((1 / 2) * (((GoB f) * 1,1) + ((GoB f) * 2,2))) `1 = (1 / 2) * (((f /. 4) + (f /. 2)) `1 ) by TOPREAL3:9
.= (1 / 2) * (((f /. 4) `1 ) + ((f /. 2) `1 )) by TOPREAL3:7
.= ((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) : S1[p] } by A4, A7, A21, GOBOARD9:3; :: 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:94
.= W-bound (L~ f) by EUCLID:56 ;
then (1 / 2) * ((f /. 4) `1 ) < (1 / 2) * (E-bound (L~ f)) by SPRECT_1:33, XREAL_1:70;
then A30: ((1 / 2) * (((GoB f) * 1,1) + ((GoB f) * 2,2))) `1 < E-bound (L~ f) by A27, A25, A22, XREAL_1:8;
A31: ((1 / 2) * (((GoB f) * 1,1) + ((GoB f) * 2,2))) `2 = (1 / 2) * (((f /. 4) + (f /. 2)) `2 ) by A24, TOPREAL3:9
.= (1 / 2) * (((f /. 4) `2 ) + ((f /. 2) `2 )) by TOPREAL3:7
.= ((1 / 2) * ((f /. 4) `2 )) + ((1 / 2) * ((f /. 2) `2 )) ;
Lc = Lc9 ;
then Rc is a_component by A5, A1, JORDAN1:41;
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:92
.= N-bound (L~ f) by EUCLID:56 ;
A34: (f /. 4) `2 = (S-min (L~ f)) `2 by SPRECT_1:94
.= S-bound (L~ f) by EUCLID:56 ;
then (1 / 2) * ((f /. 4) `2 ) < (1 / 2) * (N-bound (L~ f)) by SPRECT_1:34, XREAL_1:70;
then A35: ((1 / 2) * (((GoB f) * 1,1) + ((GoB f) * 2,2))) `2 < N-bound (L~ f) by A28, A31, A33, XREAL_1:8;
(1 / 2) * ((f /. 2) `2 ) > (1 / 2) * (S-bound (L~ f)) by A33, SPRECT_1:34, XREAL_1:70;
then A36: S-bound (L~ f) < ((1 / 2) * (((GoB f) * 1,1) + ((GoB f) * 2,2))) `2 by A6, A31, A34, XREAL_1:8;
(1 / 2) * ((f /. 2) `1 ) > (1 / 2) * (W-bound (L~ f)) by A22, SPRECT_1:33, XREAL_1:70;
then W-bound (L~ f) < ((1 / 2) * (((GoB f) * 1,1) + ((GoB f) * 2,2))) `1 by A26, A25, A29, XREAL_1:8;
then (1 / 2) * (((GoB f) * 1,1) + ((GoB f) * 2,2)) in { q where q is Point of (TOP-REAL 2) : S2[q] } by A30, A36, A35;
then A37: { q where q is Point of (TOP-REAL 2) : S2[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:3; :: thesis: verum