let f be rectangular special_circular_sequence; :: thesis: ( LeftComp f = { p where p is Point of () : ( 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 () : ( 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 ()] 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 ()] 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 ()] 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 () : S1[p] } ;
set RC = { q where q is Point of () : S2[q] } ;
set Lf = { p where p is Point of () : S3[p] } ;
A1: S-bound (L~ f) < N-bound (L~ f) by SPRECT_1:32;
A2: { p where p is Point of () : S3[p] } is Subset of () from A3: { q where q is Point of () : S2[q] } is Subset of () from A4: L~ f = { p where p is Point of () : S3[p] } by Th35;
{ p where p is Point of () : S1[p] } is Subset of () from then reconsider Lc9 = { p where p is Point of () : S1[p] } , Rc9 = { q where q is Point of () : S2[q] } , Lf = { p where p is Point of () : S3[p] } as Subset of () by A3, A2;
reconsider Lf = Lf as Subset of () ;
reconsider Lc9 = Lc9, Rc9 = Rc9 as Subset of () ;
A5: W-bound (L~ f) < E-bound (L~ f) by SPRECT_1:31;
then reconsider Lc = Lc9, Rc = Rc9 as Subset of (() | (Lf `)) by ;
reconsider Lc = Lc, Rc = Rc as Subset of (() | (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 ;
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 ;
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
.= ((1 / 2) * ((f /. 1) + (f /. 2))) `2 by
.= (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 ;
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 () : S1[p] } ;
A13: 1 + 1 = len (GoB f) by ;
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 ;
A15: f /. (1 + 1) = (GoB f) * ((1 + 1),(1 + 1)) by ;
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 ;
1 <= len (GoB f) by GOBOARD7:32;
then A18: [1,(1 + 1)] in Indices (GoB f) by ;
A19: f /. 1 = (GoB f) * (1,(1 + 1)) by ;
then right_cell (f,1) = cell ((GoB f),1,1) by ;
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 ;
then Int (cell ((GoB f),1,(1 + 1))) c= LeftComp f by GOBOARD9:def 1;
then A21: { p where p is Point of () : S1[p] } meets LeftComp f by ;
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 ;
A24: (1 / 2) * (((GoB f) * (1,1)) + ((GoB f) * (2,2))) = (1 / 2) * (((GoB f) * (1,1)) + (f /. 2)) by
.= (1 / 2) * ((f /. 4) + (f /. 2)) by ;
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 () : S1[p] } by ; :: thesis: RightComp f = { q where q is Point of () : ( 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 ;
then A30: ((1 / 2) * (((GoB f) * (1,1)) + ((GoB f) * (2,2)))) `1 < E-bound (L~ f) by ;
A31: ((1 / 2) * (((GoB f) * (1,1)) + ((GoB f) * (2,2)))) `2 = (1 / 2) * (((f /. 4) + (f /. 2)) `2) by
.= (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 ;
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 ;
then A35: ((1 / 2) * (((GoB f) * (1,1)) + ((GoB f) * (2,2)))) `2 < N-bound (L~ f) by ;
(1 / 2) * ((f /. 2) `2) > (1 / 2) * (S-bound (L~ f)) by ;
then A36: S-bound (L~ f) < ((1 / 2) * (((GoB f) * (1,1)) + ((GoB f) * (2,2)))) `2 by ;
(1 / 2) * ((f /. 2) `1) > (1 / 2) * (W-bound (L~ f)) by ;
then W-bound (L~ f) < ((1 / 2) * (((GoB f) * (1,1)) + ((GoB f) * (2,2)))) `1 by ;
then (1 / 2) * (((GoB f) * (1,1)) + ((GoB f) * (2,2))) in { q where q is Point of () : S2[q] } by ;
then A37: { q where q is Point of () : S2[q] } meets RightComp f by ;
RightComp f is_a_component_of (L~ f) ` by GOBOARD9:def 2;
hence RightComp f = { q where q is Point of () : ( 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 ; :: thesis: verum