let f be V22() standard clockwise_oriented special_circular_sequence; :: thesis: ( f /. 1 = N-min (L~ f) implies LeftComp (SpStSeq (L~ f)) c= LeftComp f )
assume A1: f /. 1 = N-min (L~ f) ; :: thesis: 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
proof
let p be Point of (TOP-REAL 2); :: thesis: ( p in P2 implies p `2 > ((GoB f) * (1,(width (GoB f)))) `2 )
assume p in P2 ; :: thesis: p `2 > ((GoB f) * (1,(width (GoB f)))) `2
then ex q being Point of (TOP-REAL 2) st
( p = q & q `2 > N-bound (L~ f) ) ;
hence p `2 > ((GoB f) * (1,(width (GoB f)))) `2 by JORDAN5D:40; :: thesis: verum
end;
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
proof
let p be Point of (TOP-REAL 2); :: thesis: ( p in P4 implies p `1 < ((GoB f) * (1,1)) `1 )
assume p in P4 ; :: thesis: p `1 < ((GoB f) * (1,1)) `1
then ex q being Point of (TOP-REAL 2) st
( p = q & q `1 < W-bound (L~ f) ) ;
hence p `1 < ((GoB f) * (1,1)) `1 by JORDAN5D:37; :: thesis: verum
end;
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
proof
let p be Point of (TOP-REAL 2); :: thesis: ( p in P3 implies p `1 > ((GoB f) * ((len (GoB f)),1)) `1 )
assume p in P3 ; :: thesis: p `1 > ((GoB f) * ((len (GoB f)),1)) `1
then ex q being Point of (TOP-REAL 2) st
( p = q & q `1 > E-bound (L~ f) ) ;
hence p `1 > ((GoB f) * ((len (GoB f)),1)) `1 by JORDAN5D:39; :: thesis: verum
end;
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)
proof
thus LeftComp (SpStSeq (L~ f)) c= (P1 \/ P2) \/ (P3 \/ P4) :: according to XBOOLE_0:def 10 :: thesis: (P1 \/ P2) \/ (P3 \/ P4) c= LeftComp (SpStSeq (L~ f))
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in LeftComp (SpStSeq (L~ f)) or x in (P1 \/ P2) \/ (P3 \/ P4) )
assume x in LeftComp (SpStSeq (L~ f)) ; :: thesis: x in (P1 \/ P2) \/ (P3 \/ P4)
then x in { 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) ) } by A28, A2, A21, A27, Th37;
then ex p being Point of (TOP-REAL 2) st
( p = x & ( 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) ) ) ;
then ( x in P1 or x in P2 or x in P3 or x in P4 ) ;
then ( x in P1 \/ P2 or x in P3 \/ P4 ) by XBOOLE_0:def 3;
hence x in (P1 \/ P2) \/ (P3 \/ P4) by XBOOLE_0:def 3; :: thesis: verum
end;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (P1 \/ P2) \/ (P3 \/ P4) or x in LeftComp (SpStSeq (L~ f)) )
assume x in (P1 \/ P2) \/ (P3 \/ P4) ; :: thesis: x in LeftComp (SpStSeq (L~ f))
then A30: ( x in P1 \/ P2 or x in P3 \/ P4 ) by XBOOLE_0:def 3;
per cases ( x in P1 or x in P2 or x in P3 or x in P4 ) by A30, XBOOLE_0:def 3;
end;
end;
for p being Point of (TOP-REAL 2) st p in P1 holds
p `2 < ((GoB f) * (1,1)) `2
proof
let p be Point of (TOP-REAL 2); :: thesis: ( p in P1 implies p `2 < ((GoB f) * (1,1)) `2 )
assume p in P1 ; :: thesis: p `2 < ((GoB f) * (1,1)) `2
then ex q being Point of (TOP-REAL 2) st
( p = q & q `2 < S-bound (L~ f) ) ;
hence p `2 < ((GoB f) * (1,1)) `2 by JORDAN5D:38; :: thesis: verum
end;
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; :: thesis: verum