let f be rectangular special_circular_sequence; :: thesis:
defpred S₁[ 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₂[ 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₃[ 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₁[p] } ;
set RC = { q where q is Point of (TOP-REAL 2) : S₂[q] } ;
set Lf = { p where p is Point of (TOP-REAL 2) : S₃[p] } ;
A1: L~ f = { p where p is Point of (TOP-REAL 2) : S₃[p] } by Th52;
A2: W-bound (L~ f) < E-bound (L~ f) by SPRECT_1:33;
A3: S-bound (L~ f) < N-bound (L~ f) by SPRECT_1:34;
A4: { p where p is Point of (TOP-REAL 2) : S₁[p] } is Subset of (TOP-REAL 2) from DOMAIN_1:sch 7();
A5: { q where q is Point of (TOP-REAL 2) : S₂[q] } is Subset of (TOP-REAL 2) from DOMAIN_1:sch 7();
{ p where p is Point of (TOP-REAL 2) : S₃[p] } is Subset of (TOP-REAL 2) from DOMAIN_1:sch 7();
then reconsider Lc' = { p where p is Point of (TOP-REAL 2) : S₁[p] } , Rc' = { q where q is Point of (TOP-REAL 2) : S₂[q] } , Lf = { p where p is Point of (TOP-REAL 2) : S₃[p] } as Subset of (TOP-REAL 2) by A4, A5;
reconsider Lc' = Lc', Rc' = Rc' as Subset of (TOP-REAL 2) ;
reconsider Lf = Lf as Subset of (TOP-REAL 2) ;
reconsider Lc = Lc', Rc = Rc' as Subset of ((TOP-REAL 2) | (Lf ` )) by A2, A3, JORDAN1:44, JORDAN1:46;
reconsider Lc = Lc, Rc = Rc as Subset of ((TOP-REAL 2) | (Lf ` )) ;
A6: ( LeftComp f is_a_component_of (L~ f) ` & RightComp f is_a_component_of (L~ f) ` ) by GOBOARD9:def 1, GOBOARD9:def 2;
Rc = Rc' ;
then Lc is_a_component_of (TOP-REAL 2) | (Lf ` ) by A2, A3, JORDAN1:41;
then A7: Lc' is_a_component_of Lf ` by CONNSP_1:def 6;
A8: 1 + 1 <= len f by GOBOARD7:36, XXREAL_0:2;
1 < width (GoB f) by GOBOARD7:35;
then A9: 1 + 1 <= width (GoB f) by NAT_1:13;
1 <= len (GoB f) by GOBOARD7:34;
then A10: [1,(1 + 1)] in Indices (GoB f) by A9, MATRIX_1:37;
A11: GoB f = (f /. 4),(f /. 1) ][ (f /. 3),(f /. 2) by Th53;
then A12: f /. 1 = (GoB f) * 1,(1 + 1) by MATRIX_2:6;
A13: 1 + 1 = len (GoB f) by A11, MATRIX_2:3;
then A14: [(1 + 1),(1 + 1)] in Indices (GoB f) by A9, MATRIX_1:37;
A15: 1 + 1 = width (GoB f) by A11, MATRIX_2:3;
A16: f /. (1 + 1) = (GoB f) * (1 + 1),(1 + 1) by A11, MATRIX_2:6;
then A17: left_cell f,1 = cell (GoB f),1,(1 + 1) by A8, A10, A12, A14, GOBOARD5:29;
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))));
A18: ((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 A13, A15, GOBOARD6:35;
A19: Int (cell (GoB f),1,(1 + 1)) c= LeftComp f by A17, GOBOARD9:def 1;
A20: (((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 ;
((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 A11, A15, MATRIX_2:6
.= ((1 / 2) * ((f /. 1) + (f /. 2))) `2 by A11, A15, 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 A20, XREAL_1:10;
then ((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₁[p] } ;
then { p where p is Point of (TOP-REAL 2) : S₁[p] } meets LeftComp f by A18, A19, XBOOLE_0:3;
hence LeftComp f = { p where p is Point of (TOP-REAL 2) : S₁[p] } by A1, A6, A7, GOBOARD9:3; :: thesis:
Lc = Lc' ;
then Rc is_a_component_of (TOP-REAL 2) | (Lf ` ) by A2, A3, JORDAN1:41;
then A21: Rc' is_a_component_of Lf ` by CONNSP_1:def 6;
A22: right_cell f,1 = cell (GoB f),1,1 by A8, A10, A12, A14, A16, GOBOARD5:29;
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, A15, GOBOARD6:34;
A24: Int (cell (GoB f),1,1) c= RightComp f by A22, GOBOARD9:def 2;
A25: (1 / 2) * (((GoB f) * 1,1) + ((GoB f) * 2,2)) = (1 / 2) * (((GoB f) * 1,1) + (f /. 2)) by A11, MATRIX_2:6
.= (1 / 2) * ((f /. 4) + (f /. 2)) by A11, MATRIX_2:6 ;
A26: ((1 / 2) * (W-bound (L~ f))) + ((1 / 2) * (W-bound (L~ f))) = W-bound (L~ f) ;
A27: ((1 / 2) * (S-bound (L~ f))) + ((1 / 2) * (S-bound (L~ f))) = S-bound (L~ f) ;
A28: ((1 / 2) * (N-bound (L~ f))) + ((1 / 2) * (N-bound (L~ f))) = N-bound (L~ f) ;
A29: ((1 / 2) * (E-bound (L~ f))) + ((1 / 2) * (E-bound (L~ f))) = E-bound (L~ f) ;
A30: ((1 / 2) * (((GoB f) * 1,1) + ((GoB f) * 2,2))) `1 = (1 / 2) * (((f /. 4) + (f /. 2)) `1 ) by A25, TOPREAL3:9
.= (1 / 2) * (((f /. 4) `1 ) + ((f /. 2) `1 )) by TOPREAL3:7
.= ((1 / 2) * ((f /. 4) `1 )) + ((1 / 2) * ((f /. 2) `1 )) ;
A31: ((1 / 2) * (((GoB f) * 1,1) + ((GoB f) * 2,2))) `2 = (1 / 2) * (((f /. 4) + (f /. 2)) `2 ) by A25, TOPREAL3:9
.= (1 / 2) * (((f /. 4) `2 ) + ((f /. 2) `2 )) by TOPREAL3:7
.= ((1 / 2) * ((f /. 4) `2 )) + ((1 / 2) * ((f /. 2) `2 )) ;
A32: (f /. 4) `1 = (W-min (L~ f)) `1 by SPRECT_1:94
.= W-bound (L~ f) by EUCLID:56 ;
A33: (f /. 2) `1 = (E-max (L~ f)) `1 by SPRECT_1:92
.= E-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 ;
A35: (f /. 2) `2 = (N-max (L~ f)) `2 by SPRECT_1:92
.= N-bound (L~ f) by EUCLID:56 ;
(1 / 2) * ((f /. 2) `1 ) > (1 / 2) * (W-bound (L~ f)) by A33, SPRECT_1:33, XREAL_1:70;
then A36: W-bound (L~ f) < ((1 / 2) * (((GoB f) * 1,1) + ((GoB f) * 2,2))) `1 by A26, A30, A32, XREAL_1:8;
(1 / 2) * ((f /. 4) `1 ) < (1 / 2) * (E-bound (L~ f)) by A32, SPRECT_1:33, XREAL_1:70;
then A37: ((1 / 2) * (((GoB f) * 1,1) + ((GoB f) * 2,2))) `1 < E-bound (L~ f) by A29, A30, A33, XREAL_1:8;
(1 / 2) * ((f /. 2) `2 ) > (1 / 2) * (S-bound (L~ f)) by A35, SPRECT_1:34, XREAL_1:70;
then A38: S-bound (L~ f) < ((1 / 2) * (((GoB f) * 1,1) + ((GoB f) * 2,2))) `2 by A27, A31, A34, XREAL_1:8;
(1 / 2) * ((f /. 4) `2 ) < (1 / 2) * (N-bound (L~ f)) by A34, SPRECT_1:34, XREAL_1:70;
then ((1 / 2) * (((GoB f) * 1,1) + ((GoB f) * 2,2))) `2 < N-bound (L~ f) by A28, A31, A35, XREAL_1:8;
then (1 / 2) * (((GoB f) * 1,1) + ((GoB f) * 2,2)) in { q where q is Point of (TOP-REAL 2) : S₂[q] } by A36, A37, A38;
then { q where q is Point of (TOP-REAL 2) : S₂[q] } meets RightComp f by A23, A24, XBOOLE_0:3;
hence RightComp f = { q where q is Point of (TOP-REAL 2) : S₂[q] } by A1, A6, A21, GOBOARD9:3; :: thesis: