let f be V22() standard clockwise_oriented special_circular_sequence; ( f /. 1 = N-min (L~ f) implies LeftComp (SpStSeq (L~ f)) c= LeftComp f )
assume A1:
f /. 1 = N-min (L~ f)
; LeftComp (SpStSeq (L~ f)) c= LeftComp f
defpred S1[ Element of (TOP-REAL 2)] means $1 `2 < S-bound (L~ f);
reconsider P1 = { p where p is Point of (TOP-REAL 2) : S1[p] } as Subset of (TOP-REAL 2) from DOMAIN_1:sch 7();
defpred S2[ Element of (TOP-REAL 2)] means $1 `2 > N-bound (L~ f);
reconsider P2 = { p where p is Point of (TOP-REAL 2) : S2[p] } as Subset of (TOP-REAL 2) from DOMAIN_1:sch 7();
defpred S3[ Element of (TOP-REAL 2)] means $1 `1 > E-bound (L~ f);
reconsider P3 = { p where p is Point of (TOP-REAL 2) : S3[p] } as Subset of (TOP-REAL 2) from DOMAIN_1:sch 7();
defpred S4[ Element of (TOP-REAL 2)] means $1 `1 < W-bound (L~ f);
reconsider P4 = { p where p is Point of (TOP-REAL 2) : S4[p] } as Subset of (TOP-REAL 2) from DOMAIN_1:sch 7();
A2:
W-bound (L~ (SpStSeq (L~ f))) = W-bound (L~ f)
by SPRECT_1:58;
for p being Point of (TOP-REAL 2) st p in P2 holds
p `2 > ((GoB f) * (1,(width (GoB f)))) `2
then A3:
P2 misses L~ f
by GOBOARD8:24;
A4:
1 + 1 <= len f
by GOBOARD7:34, XXREAL_0:2;
A5:
((width (GoB f)) -' 1) + 1 = width (GoB f)
by GOBRD11:34, XREAL_1:235;
consider i being Nat such that
A6:
1 <= i
and
A7:
i < len (GoB f)
and
A8:
N-min (L~ f) = (GoB f) * (i,(width (GoB f)))
by Th28;
A9:
i + 1 <= len (GoB f)
by A7, NAT_1:13;
A10:
i in dom (GoB f)
by A6, A7, FINSEQ_3:25;
then A11:
f /. 2 = (GoB f) * ((i + 1),(width (GoB f)))
by A1, A8, Th29;
A12:
width (GoB f) >= 1
by GOBRD11:34;
then A13:
[i,(width (GoB f))] in Indices (GoB f)
by A6, A7, MATRIX_0:30;
A14:
1 <= i + 1
by A6, NAT_1:13;
then A15: (f /. 2) `2 =
((GoB f) * (1,(width (GoB f)))) `2
by A11, A12, A9, GOBOARD5:1
.=
(N-min (L~ f)) `2
by A6, A7, A8, A12, GOBOARD5:1
.=
N-bound (L~ f)
by EUCLID:52
;
set a = ((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))) + |[0,1]|;
set q = (1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))));
A16: (((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))) + |[0,1]|) `2 =
(((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))) `2) + (|[0,1]| `2)
by TOPREAL3:2
.=
(((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))) `2) + 1
by EUCLID:52
;
((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))) `2 =
((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + (f /. 2))) `2
by A1, A8, A10, Th29
.=
(1 / 2) * (((f /. 1) + (f /. 2)) `2)
by A1, A8, TOPREAL3:4
.=
(1 / 2) * (((f /. 1) `2) + ((f /. 2) `2))
by TOPREAL3:2
.=
(1 / 2) * ((N-bound (L~ f)) + (N-bound (L~ f)))
by A1, A15, EUCLID:52
.=
N-bound (L~ f)
;
then
(((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))) + |[0,1]|) `2 > 0 + (N-bound (L~ f))
by A16, XREAL_1:8;
then A17:
(((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))) + |[0,1]|) `2 > N-bound (L~ (SpStSeq (L~ f)))
by SPRECT_1:60;
LeftComp (SpStSeq (L~ f)) = { p where p is Point of (TOP-REAL 2) : ( not W-bound (L~ (SpStSeq (L~ f))) <= p `1 or not p `1 <= E-bound (L~ (SpStSeq (L~ f))) or not S-bound (L~ (SpStSeq (L~ f))) <= p `2 or not p `2 <= N-bound (L~ (SpStSeq (L~ f))) ) }
by Th37;
then A18:
((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))) + |[0,1]| in LeftComp (SpStSeq (L~ f))
by A17;
[(i + 1),(width (GoB f))] in Indices (GoB f)
by A12, A14, A9, MATRIX_0:30;
then
left_cell (f,1) = cell ((GoB f),i,(width (GoB f)))
by A1, A8, A11, A5, A4, A13, GOBOARD5:28;
then A19:
Int (cell ((GoB f),i,(width (GoB f)))) c= LeftComp f
by GOBOARD9:def 1;
((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))) + |[0,1]| in Int (cell ((GoB f),i,(width (GoB f))))
by A6, A9, GOBOARD6:32;
then A20:
LeftComp f meets LeftComp (SpStSeq (L~ f))
by A19, A18, XBOOLE_0:3;
A21:
S-bound (L~ (SpStSeq (L~ f))) = S-bound (L~ f)
by SPRECT_1:59;
for p being Point of (TOP-REAL 2) st p in P4 holds
p `1 < ((GoB f) * (1,1)) `1
then A22:
P4 misses L~ f
by GOBOARD8:21;
for p being Point of (TOP-REAL 2) st p in P3 holds
p `1 > ((GoB f) * ((len (GoB f)),1)) `1
then
P3 misses L~ f
by GOBOARD8:22;
then A23:
P3 \/ P4 misses L~ f
by A22, XBOOLE_1:70;
LeftComp (SpStSeq (L~ f)) is_a_component_of (L~ (SpStSeq (L~ f))) `
by GOBOARD9:def 1;
then consider B1 being Subset of ((TOP-REAL 2) | ((L~ (SpStSeq (L~ f))) `)) such that
A24:
B1 = LeftComp (SpStSeq (L~ f))
and
A25:
B1 is a_component
by CONNSP_1:def 6;
B1 is connected
by A25, CONNSP_1:def 5;
then A26:
LeftComp (SpStSeq (L~ f)) is connected
by A24, CONNSP_1:23;
A27:
E-bound (L~ (SpStSeq (L~ f))) = E-bound (L~ f)
by SPRECT_1:61;
A28:
N-bound (L~ (SpStSeq (L~ f))) = N-bound (L~ f)
by SPRECT_1:60;
A29:
LeftComp (SpStSeq (L~ f)) = (P1 \/ P2) \/ (P3 \/ P4)
for p being Point of (TOP-REAL 2) st p in P1 holds
p `2 < ((GoB f) * (1,1)) `2
then
P1 misses L~ f
by GOBOARD8:23;
then
P1 \/ P2 misses L~ f
by A3, XBOOLE_1:70;
then
LeftComp (SpStSeq (L~ f)) misses L~ f
by A29, A23, XBOOLE_1:70;
then A31:
LeftComp (SpStSeq (L~ f)) c= (L~ f) `
by SUBSET_1:23;
LeftComp f is_a_component_of (L~ f) `
by GOBOARD9:def 1;
hence
LeftComp (SpStSeq (L~ f)) c= LeftComp f
by A26, A20, A31, GOBOARD9:4; verum