let p be Point of (TOP-REAL 2); :: thesis: for f being non constant standard clockwise_oriented special_circular_sequence st p in RightComp f holds
N-bound (L~ f) > p `2
let f be non constant standard clockwise_oriented special_circular_sequence; :: thesis: ( 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:25;
assume p in RightComp f ; :: thesis: 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:55;
then consider r being real number such that
A2: r > 0 and
A3: Ball (u,r) c= RightComp (Rotate (f,(N-min (L~ f)))) by GOBOARD6:8;
reconsider r = r as Real by XREAL_0:def 1;
reconsider k = |[(p `1),((p `2) + (r / 2))]| as Point of (Euclid 2) by EUCLID:25;
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:12
.= sqrt ((((p `1) - (p `1)) ^2) + (((p `2) - (|[(p `1),((p `2) + (r / 2))]| `2)) ^2)) by EUCLID:56
.= sqrt (((p `2) - ((p `2) + (r / 2))) ^2) by EUCLID:56
.= sqrt ((r / 2) ^2)
.= r / 2 by A2, SQUARE_1:89 ;
then dist (u,k) < r / 1 by A2, XREAL_1:78;
then A4: k in Ball (u,r) by METRIC_1:12;
RightComp (Rotate (f,(N-min (L~ f)))) misses LeftComp (Rotate (f,(N-min (L~ f)))) by Th24;
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:43;
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 29
.= (p `2) + (r / 2) by EUCLID:56 ;
N-min (L~ f) in rng f by SPRECT_2:43;
then A8: (Rotate (f,(N-min (L~ f)))) /. 1 = N-min (L~ (Rotate (f,(N-min (L~ f))))) by A1, FINSEQ_6:98;
then |[(p `1),((p `2) + (r / 2))]| `2 <= N-bound (L~ (Rotate (f,(N-min (L~ f))))) by A5, JORDAN2C:121;
then (p `2) + (r / 2) <= N-bound (L~ (Rotate (f,(N-min (L~ f))))) by EUCLID:56;
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:56;
|[(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:56;
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:69;
|[(p `1),((p `2) + (r / 2))]| `2 >= S-bound (L~ (Rotate (f,(N-min (L~ f))))) by A8, A5, JORDAN2C:120;
then (p `2) + (r / 2) >= S-bound (L~ (Rotate (f,(N-min (L~ f))))) by EUCLID:56;
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:56;
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:25;
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:43;
then A12: upper_bound (proj2 .: (L~ (SpStSeq (L~ (Rotate (f,(N-min (L~ f)))))))) >= (p `2) + (r / 2) by SEQ_4:def 4;
r / 2 > 0 by A2, XREAL_1:141;
then A13: (p `2) + (r / 2) > (p `2) + 0 by XREAL_1:8;
( 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:50, SPRECT_1:68;
hence N-bound (L~ f) > p `2 by A1, A12, A13, XXREAL_0:2; :: thesis: verum