let p be Point of (TOP-REAL 2); for f being V8() standard clockwise_oriented special_circular_sequence st p in RightComp f holds
N-bound (L~ f) > p `2
let f be V8() standard clockwise_oriented special_circular_sequence; ( p in RightComp f implies N-bound (L~ f) > p `2 )
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
; N-bound (L~ f) > p `2
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),((p `2) + (r / 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),((p `2) + (r / 2))]| `1)) ^2) + (((p `2) - (|[(p `1),((p `2) + (r / 2))]| `2)) ^2))
by TOPREAL3:7
.=
sqrt ((((p `1) - (p `1)) ^2) + (((p `2) - (|[(p `1),((p `2) + (r / 2))]| `2)) ^2))
by EUCLID:52
.=
sqrt (((p `2) - ((p `2) + (r / 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),((p `2) + (r / 2))]| in LeftComp (Rotate (f,(N-min (L~ f))))
by A3, A4, XBOOLE_0:3;
set x = |[(E-bound (L~ (SpStSeq (L~ (Rotate (f,(N-min (L~ f)))))))),((p `2) + (r / 2))]|;
A6:
LSeg ((SE-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 TOPREAL6:35;
A7: proj2 . |[(E-bound (L~ (SpStSeq (L~ (Rotate (f,(N-min (L~ f)))))))),((p `2) + (r / 2))]| =
|[(E-bound (L~ (SpStSeq (L~ (Rotate (f,(N-min (L~ f)))))))),((p `2) + (r / 2))]| `2
by PSCOMP_1:def 6
.=
(p `2) + (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),((p `2) + (r / 2))]| `2 <= N-bound (L~ (Rotate (f,(N-min (L~ f)))))
by A5, JORDAN2C:113;
then
(p `2) + (r / 2) <= N-bound (L~ (Rotate (f,(N-min (L~ f)))))
by EUCLID:52;
then A9:
|[(E-bound (L~ (SpStSeq (L~ (Rotate (f,(N-min (L~ f)))))))),((p `2) + (r / 2))]| `2 <= N-bound (L~ (Rotate (f,(N-min (L~ f)))))
by EUCLID:52;
|[(E-bound (L~ (SpStSeq (L~ (Rotate (f,(N-min (L~ f)))))))),((p `2) + (r / 2))]| `1 = E-bound (L~ (SpStSeq (L~ (Rotate (f,(N-min (L~ f)))))))
by EUCLID:52;
then A10:
|[(E-bound (L~ (SpStSeq (L~ (Rotate (f,(N-min (L~ f)))))))),((p `2) + (r / 2))]| `1 = E-bound (L~ (Rotate (f,(N-min (L~ f)))))
by SPRECT_1:61;
|[(p `1),((p `2) + (r / 2))]| `2 >= S-bound (L~ (Rotate (f,(N-min (L~ f)))))
by A8, A5, JORDAN2C:112;
then
(p `2) + (r / 2) >= S-bound (L~ (Rotate (f,(N-min (L~ f)))))
by EUCLID:52;
then A11:
|[(E-bound (L~ (SpStSeq (L~ (Rotate (f,(N-min (L~ f)))))))),((p `2) + (r / 2))]| `2 >= S-bound (L~ (Rotate (f,(N-min (L~ f)))))
by EUCLID:52;
LSeg ((SE-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 `2 <= N-bound (L~ (Rotate (f,(N-min (L~ f))))) & q `2 >= S-bound (L~ (Rotate (f,(N-min (L~ f))))) ) }
by SPRECT_1:23;
then
|[(E-bound (L~ (SpStSeq (L~ (Rotate (f,(N-min (L~ f)))))))),((p `2) + (r / 2))]| in LSeg ((SE-corner (L~ (Rotate (f,(N-min (L~ f)))))),(NE-corner (L~ (Rotate (f,(N-min (L~ f)))))))
by A9, A11, A10;
then
( proj2 .: (L~ (SpStSeq (L~ (Rotate (f,(N-min (L~ f))))))) is bounded_above & (p `2) + (r / 2) in proj2 .: (L~ (SpStSeq (L~ (Rotate (f,(N-min (L~ f))))))) )
by A6, A7, FUNCT_2:35;
then A12:
upper_bound (proj2 .: (L~ (SpStSeq (L~ (Rotate (f,(N-min (L~ f)))))))) >= (p `2) + (r / 2)
by SEQ_4:def 1;
r / 2 > 0
by A2, XREAL_1:139;
then A13:
(p `2) + (r / 2) > (p `2) + 0
by XREAL_1:6;
( N-bound (L~ (SpStSeq (L~ (Rotate (f,(N-min (L~ f))))))) = N-bound (L~ (Rotate (f,(N-min (L~ f))))) & N-bound (L~ (SpStSeq (L~ (Rotate (f,(N-min (L~ f))))))) = upper_bound (proj2 .: (L~ (SpStSeq (L~ (Rotate (f,(N-min (L~ f)))))))) )
by SPRECT_1:45, SPRECT_1:60;
hence
N-bound (L~ f) > p `2
by A1, A12, A13, XXREAL_0:2; verum