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 S_{1}[ Element of (TOP-REAL 2)] means $1 `2 < S-bound (L~ f);

reconsider P1 = { p where p is Point of (TOP-REAL 2) : S_{1}[p] } as Subset of (TOP-REAL 2) from DOMAIN_1:sch 7();

defpred S_{2}[ Element of (TOP-REAL 2)] means $1 `2 > N-bound (L~ f);

reconsider P2 = { p where p is Point of (TOP-REAL 2) : S_{2}[p] } as Subset of (TOP-REAL 2) from DOMAIN_1:sch 7();

defpred S_{3}[ Element of (TOP-REAL 2)] means $1 `1 > E-bound (L~ f);

reconsider P3 = { p where p is Point of (TOP-REAL 2) : S_{3}[p] } as Subset of (TOP-REAL 2) from DOMAIN_1:sch 7();

defpred S_{4}[ Element of (TOP-REAL 2)] means $1 `1 < W-bound (L~ f);

reconsider P4 = { p where p is Point of (TOP-REAL 2) : S_{4}[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

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

for p being Point of (TOP-REAL 2) st p in P3 holds

p `1 > ((GoB f) * ((len (GoB f)),1)) `1

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)

p `2 < ((GoB f) * (1,1)) `2

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

assume A1: f /. 1 = N-min (L~ f) ; :: thesis: LeftComp (SpStSeq (L~ f)) c= LeftComp f

defpred S

reconsider P1 = { p where p is Point of (TOP-REAL 2) : S

defpred S

reconsider P2 = { p where p is Point of (TOP-REAL 2) : S

defpred S

reconsider P3 = { p where p is Point of (TOP-REAL 2) : S

defpred S

reconsider P4 = { p where p is Point of (TOP-REAL 2) : S

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

then A3:
P2 misses L~ f
by GOBOARD8:24;
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;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

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

then A22:
P4 misses L~ f
by GOBOARD8:21;
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;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

for p being Point of (TOP-REAL 2) st p in P3 holds

p `1 > ((GoB f) * ((len (GoB f)),1)) `1

proof

then
P3 misses L~ f
by GOBOARD8:22;
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;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

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

for p being Point of (TOP-REAL 2) st p in P1 holds
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))

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;

end;proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (P1 \/ P2) \/ (P3 \/ P4) or x in LeftComp (SpStSeq (L~ f)) )
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;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

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;

suppose
x in P1
; :: thesis: x in LeftComp (SpStSeq (L~ f))

then
ex p being Point of (TOP-REAL 2) st

( x = p & p `2 < S-bound (L~ f) ) ;

hence x in LeftComp (SpStSeq (L~ f)) by A21, Th40; :: thesis: verum

end;( x = p & p `2 < S-bound (L~ f) ) ;

hence x in LeftComp (SpStSeq (L~ f)) by A21, Th40; :: thesis: verum

suppose
x in P2
; :: thesis: x in LeftComp (SpStSeq (L~ f))

then
ex p being Point of (TOP-REAL 2) st

( x = p & p `2 > N-bound (L~ f) ) ;

hence x in LeftComp (SpStSeq (L~ f)) by A28, Th40; :: thesis: verum

end;( x = p & p `2 > N-bound (L~ f) ) ;

hence x in LeftComp (SpStSeq (L~ f)) by A28, Th40; :: thesis: verum

p `2 < ((GoB f) * (1,1)) `2

proof

then
P1 misses L~ f
by GOBOARD8:23;
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;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

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