let p be Point of (TOP-REAL 2); :: thesis: for f being V8() standard clockwise_oriented special_circular_sequence st p in RightComp f holds

E-bound (L~ f) > p `1

let f be V8() standard clockwise_oriented special_circular_sequence; :: thesis: ( p in RightComp f implies E-bound (L~ f) > p `1 )

set g = Rotate (f,(N-min (L~ f)));

A1: L~ f = L~ (Rotate (f,(N-min (L~ f)))) by REVROT_1:33;

reconsider u = p as Point of (Euclid 2) by EUCLID:22;

assume p in RightComp f ; :: thesis: E-bound (L~ f) > p `1

then p in RightComp (Rotate (f,(N-min (L~ f)))) by REVROT_1:37;

then u in Int (RightComp (Rotate (f,(N-min (L~ f))))) by TOPS_1:23;

then consider r being Real such that

A2: r > 0 and

A3: Ball (u,r) c= RightComp (Rotate (f,(N-min (L~ f)))) by GOBOARD6:5;

reconsider r = r as Real ;

reconsider k = |[((p `1) + (r / 2)),(p `2)]| as Point of (Euclid 2) by EUCLID:22;

dist (u,k) = (Pitag_dist 2) . (u,k) by METRIC_1:def 1

.= sqrt ((((p `1) - (|[((p `1) + (r / 2)),(p `2)]| `1)) ^2) + (((p `2) - (|[((p `1) + (r / 2)),(p `2)]| `2)) ^2)) by TOPREAL3:7

.= sqrt ((((p `1) - ((p `1) + (r / 2))) ^2) + (((p `2) - (|[((p `1) + (r / 2)),(p `2)]| `2)) ^2)) by EUCLID:52

.= sqrt ((((p `1) - ((p `1) + (r / 2))) ^2) + (((p `2) - (p `2)) ^2)) by EUCLID:52

.= sqrt ((r / 2) ^2)

.= r / 2 by A2, SQUARE_1:22 ;

then dist (u,k) < r / 1 by A2, XREAL_1:76;

then A4: k in Ball (u,r) by METRIC_1:11;

RightComp (Rotate (f,(N-min (L~ f)))) misses LeftComp (Rotate (f,(N-min (L~ f)))) by Th14;

then A5: not |[((p `1) + (r / 2)),(p `2)]| in LeftComp (Rotate (f,(N-min (L~ f)))) by A3, A4, XBOOLE_0:3;

set x = |[((p `1) + (r / 2)),(N-bound (L~ (SpStSeq (L~ (Rotate (f,(N-min (L~ f))))))))]|;

A6: LSeg ((NW-corner (L~ (Rotate (f,(N-min (L~ f)))))),(NE-corner (L~ (Rotate (f,(N-min (L~ f))))))) c= L~ (SpStSeq (L~ (Rotate (f,(N-min (L~ f)))))) by SPRECT_3:14;

A7: proj1 . |[((p `1) + (r / 2)),(N-bound (L~ (SpStSeq (L~ (Rotate (f,(N-min (L~ f))))))))]| = |[((p `1) + (r / 2)),(N-bound (L~ (SpStSeq (L~ (Rotate (f,(N-min (L~ f))))))))]| `1 by PSCOMP_1:def 5

.= (p `1) + (r / 2) by EUCLID:52 ;

N-min (L~ f) in rng f by SPRECT_2:39;

then A8: (Rotate (f,(N-min (L~ f)))) /. 1 = N-min (L~ (Rotate (f,(N-min (L~ f))))) by A1, FINSEQ_6:92;

then |[((p `1) + (r / 2)),(p `2)]| `1 <= E-bound (L~ (Rotate (f,(N-min (L~ f))))) by A5, JORDAN2C:111;

then (p `1) + (r / 2) <= E-bound (L~ (Rotate (f,(N-min (L~ f))))) by EUCLID:52;

then A9: |[((p `1) + (r / 2)),(N-bound (L~ (SpStSeq (L~ (Rotate (f,(N-min (L~ f))))))))]| `1 <= E-bound (L~ (Rotate (f,(N-min (L~ f))))) by EUCLID:52;

|[((p `1) + (r / 2)),(N-bound (L~ (SpStSeq (L~ (Rotate (f,(N-min (L~ f))))))))]| `2 = N-bound (L~ (SpStSeq (L~ (Rotate (f,(N-min (L~ f))))))) by EUCLID:52;

then A10: |[((p `1) + (r / 2)),(N-bound (L~ (SpStSeq (L~ (Rotate (f,(N-min (L~ f))))))))]| `2 = N-bound (L~ (Rotate (f,(N-min (L~ f))))) by SPRECT_1:60;

|[((p `1) + (r / 2)),(p `2)]| `1 >= W-bound (L~ (Rotate (f,(N-min (L~ f))))) by A8, A5, JORDAN2C:110;

then (p `1) + (r / 2) >= W-bound (L~ (Rotate (f,(N-min (L~ f))))) by EUCLID:52;

then A11: |[((p `1) + (r / 2)),(N-bound (L~ (SpStSeq (L~ (Rotate (f,(N-min (L~ f))))))))]| `1 >= W-bound (L~ (Rotate (f,(N-min (L~ f))))) by EUCLID:52;

LSeg ((NW-corner (L~ (Rotate (f,(N-min (L~ f)))))),(NE-corner (L~ (Rotate (f,(N-min (L~ f))))))) = { q where q is Point of (TOP-REAL 2) : ( q `1 <= E-bound (L~ (Rotate (f,(N-min (L~ f))))) & q `1 >= W-bound (L~ (Rotate (f,(N-min (L~ f))))) & q `2 = N-bound (L~ (Rotate (f,(N-min (L~ f))))) ) } by SPRECT_1:25;

then |[((p `1) + (r / 2)),(N-bound (L~ (SpStSeq (L~ (Rotate (f,(N-min (L~ f))))))))]| in LSeg ((NW-corner (L~ (Rotate (f,(N-min (L~ f)))))),(NE-corner (L~ (Rotate (f,(N-min (L~ f))))))) by A9, A11, A10;

then ( proj1 .: (L~ (SpStSeq (L~ (Rotate (f,(N-min (L~ f))))))) is bounded_above & (p `1) + (r / 2) in proj1 .: (L~ (SpStSeq (L~ (Rotate (f,(N-min (L~ f))))))) ) by A6, A7, FUNCT_2:35;

then A12: upper_bound (proj1 .: (L~ (SpStSeq (L~ (Rotate (f,(N-min (L~ f)))))))) >= (p `1) + (r / 2) by SEQ_4:def 1;

r / 2 > 0 by A2, XREAL_1:139;

then A13: (p `1) + (r / 2) > (p `1) + 0 by XREAL_1:6;

( E-bound (L~ (SpStSeq (L~ (Rotate (f,(N-min (L~ f))))))) = E-bound (L~ (Rotate (f,(N-min (L~ f))))) & E-bound (L~ (SpStSeq (L~ (Rotate (f,(N-min (L~ f))))))) = upper_bound (proj1 .: (L~ (SpStSeq (L~ (Rotate (f,(N-min (L~ f)))))))) ) by SPRECT_1:46, SPRECT_1:61;

hence E-bound (L~ f) > p `1 by A1, A12, A13, XXREAL_0:2; :: thesis: verum

E-bound (L~ f) > p `1

let f be V8() standard clockwise_oriented special_circular_sequence; :: thesis: ( p in RightComp f implies E-bound (L~ f) > p `1 )

set g = Rotate (f,(N-min (L~ f)));

A1: L~ f = L~ (Rotate (f,(N-min (L~ f)))) by REVROT_1:33;

reconsider u = p as Point of (Euclid 2) by EUCLID:22;

assume p in RightComp f ; :: thesis: E-bound (L~ f) > p `1

then p in RightComp (Rotate (f,(N-min (L~ f)))) by REVROT_1:37;

then u in Int (RightComp (Rotate (f,(N-min (L~ f))))) by TOPS_1:23;

then consider r being Real such that

A2: r > 0 and

A3: Ball (u,r) c= RightComp (Rotate (f,(N-min (L~ f)))) by GOBOARD6:5;

reconsider r = r as Real ;

reconsider k = |[((p `1) + (r / 2)),(p `2)]| as Point of (Euclid 2) by EUCLID:22;

dist (u,k) = (Pitag_dist 2) . (u,k) by METRIC_1:def 1

.= sqrt ((((p `1) - (|[((p `1) + (r / 2)),(p `2)]| `1)) ^2) + (((p `2) - (|[((p `1) + (r / 2)),(p `2)]| `2)) ^2)) by TOPREAL3:7

.= sqrt ((((p `1) - ((p `1) + (r / 2))) ^2) + (((p `2) - (|[((p `1) + (r / 2)),(p `2)]| `2)) ^2)) by EUCLID:52

.= sqrt ((((p `1) - ((p `1) + (r / 2))) ^2) + (((p `2) - (p `2)) ^2)) by EUCLID:52

.= sqrt ((r / 2) ^2)

.= r / 2 by A2, SQUARE_1:22 ;

then dist (u,k) < r / 1 by A2, XREAL_1:76;

then A4: k in Ball (u,r) by METRIC_1:11;

RightComp (Rotate (f,(N-min (L~ f)))) misses LeftComp (Rotate (f,(N-min (L~ f)))) by Th14;

then A5: not |[((p `1) + (r / 2)),(p `2)]| in LeftComp (Rotate (f,(N-min (L~ f)))) by A3, A4, XBOOLE_0:3;

set x = |[((p `1) + (r / 2)),(N-bound (L~ (SpStSeq (L~ (Rotate (f,(N-min (L~ f))))))))]|;

A6: LSeg ((NW-corner (L~ (Rotate (f,(N-min (L~ f)))))),(NE-corner (L~ (Rotate (f,(N-min (L~ f))))))) c= L~ (SpStSeq (L~ (Rotate (f,(N-min (L~ f)))))) by SPRECT_3:14;

A7: proj1 . |[((p `1) + (r / 2)),(N-bound (L~ (SpStSeq (L~ (Rotate (f,(N-min (L~ f))))))))]| = |[((p `1) + (r / 2)),(N-bound (L~ (SpStSeq (L~ (Rotate (f,(N-min (L~ f))))))))]| `1 by PSCOMP_1:def 5

.= (p `1) + (r / 2) by EUCLID:52 ;

N-min (L~ f) in rng f by SPRECT_2:39;

then A8: (Rotate (f,(N-min (L~ f)))) /. 1 = N-min (L~ (Rotate (f,(N-min (L~ f))))) by A1, FINSEQ_6:92;

then |[((p `1) + (r / 2)),(p `2)]| `1 <= E-bound (L~ (Rotate (f,(N-min (L~ f))))) by A5, JORDAN2C:111;

then (p `1) + (r / 2) <= E-bound (L~ (Rotate (f,(N-min (L~ f))))) by EUCLID:52;

then A9: |[((p `1) + (r / 2)),(N-bound (L~ (SpStSeq (L~ (Rotate (f,(N-min (L~ f))))))))]| `1 <= E-bound (L~ (Rotate (f,(N-min (L~ f))))) by EUCLID:52;

|[((p `1) + (r / 2)),(N-bound (L~ (SpStSeq (L~ (Rotate (f,(N-min (L~ f))))))))]| `2 = N-bound (L~ (SpStSeq (L~ (Rotate (f,(N-min (L~ f))))))) by EUCLID:52;

then A10: |[((p `1) + (r / 2)),(N-bound (L~ (SpStSeq (L~ (Rotate (f,(N-min (L~ f))))))))]| `2 = N-bound (L~ (Rotate (f,(N-min (L~ f))))) by SPRECT_1:60;

|[((p `1) + (r / 2)),(p `2)]| `1 >= W-bound (L~ (Rotate (f,(N-min (L~ f))))) by A8, A5, JORDAN2C:110;

then (p `1) + (r / 2) >= W-bound (L~ (Rotate (f,(N-min (L~ f))))) by EUCLID:52;

then A11: |[((p `1) + (r / 2)),(N-bound (L~ (SpStSeq (L~ (Rotate (f,(N-min (L~ f))))))))]| `1 >= W-bound (L~ (Rotate (f,(N-min (L~ f))))) by EUCLID:52;

LSeg ((NW-corner (L~ (Rotate (f,(N-min (L~ f)))))),(NE-corner (L~ (Rotate (f,(N-min (L~ f))))))) = { q where q is Point of (TOP-REAL 2) : ( q `1 <= E-bound (L~ (Rotate (f,(N-min (L~ f))))) & q `1 >= W-bound (L~ (Rotate (f,(N-min (L~ f))))) & q `2 = N-bound (L~ (Rotate (f,(N-min (L~ f))))) ) } by SPRECT_1:25;

then |[((p `1) + (r / 2)),(N-bound (L~ (SpStSeq (L~ (Rotate (f,(N-min (L~ f))))))))]| in LSeg ((NW-corner (L~ (Rotate (f,(N-min (L~ f)))))),(NE-corner (L~ (Rotate (f,(N-min (L~ f))))))) by A9, A11, A10;

then ( proj1 .: (L~ (SpStSeq (L~ (Rotate (f,(N-min (L~ f))))))) is bounded_above & (p `1) + (r / 2) in proj1 .: (L~ (SpStSeq (L~ (Rotate (f,(N-min (L~ f))))))) ) by A6, A7, FUNCT_2:35;

then A12: upper_bound (proj1 .: (L~ (SpStSeq (L~ (Rotate (f,(N-min (L~ f)))))))) >= (p `1) + (r / 2) by SEQ_4:def 1;

r / 2 > 0 by A2, XREAL_1:139;

then A13: (p `1) + (r / 2) > (p `1) + 0 by XREAL_1:6;

( E-bound (L~ (SpStSeq (L~ (Rotate (f,(N-min (L~ f))))))) = E-bound (L~ (Rotate (f,(N-min (L~ f))))) & E-bound (L~ (SpStSeq (L~ (Rotate (f,(N-min (L~ f))))))) = upper_bound (proj1 .: (L~ (SpStSeq (L~ (Rotate (f,(N-min (L~ f)))))))) ) by SPRECT_1:46, SPRECT_1:61;

hence E-bound (L~ f) > p `1 by A1, A12, A13, XXREAL_0:2; :: thesis: verum