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;
N-min (L~ f) in rng f by SPRECT_2:43;
then A2: (Rotate f,(N-min (L~ f))) /. 1 = N-min (L~ (Rotate f,(N-min (L~ f)))) by A1, FINSEQ_6:98;
reconsider u = p as Point of (Euclid 2) by XX;
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
A3: r > 0 and
A4: Ball u,r c= RightComp (Rotate f,(N-min (L~ f))) by GOBOARD6:8;
reconsider r = r as Real by XREAL_0:def 1;
A5: N-bound (L~ (SpStSeq (L~ (Rotate f,(N-min (L~ f)))))) = N-bound (L~ (Rotate f,(N-min (L~ f)))) by SPRECT_1:68;
A6: N-bound (L~ (SpStSeq (L~ (Rotate f,(N-min (L~ f)))))) = sup (proj2 .: (L~ (SpStSeq (L~ (Rotate f,(N-min (L~ f))))))) by SPRECT_1:50;
A7: proj2 .: (L~ (SpStSeq (L~ (Rotate f,(N-min (L~ f)))))) is bounded_above by SPRECT_1:47;
set x = |[(E-bound (L~ (SpStSeq (L~ (Rotate f,(N-min (L~ f))))))),((p `2 ) + (r / 2))]|;
reconsider k = |[(p `1 ),((p `2 ) + (r / 2))]| as Point of (Euclid 2) by XX;
A8: r / 2 > 0 by A3, XREAL_1:141;
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 A8, SQUARE_1:89 ;
then dist u,k < r / 1 by A3, XREAL_1:78;
then A9: 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 A10: not |[(p `1 ),((p `2 ) + (r / 2))]| in LeftComp (Rotate f,(N-min (L~ f))) by A4, A9, XBOOLE_0:3;
then |[(p `1 ),((p `2 ) + (r / 2))]| `2 <= N-bound (L~ (Rotate f,(N-min (L~ f)))) by A2, JORDAN2C:121;
then (p `2 ) + (r / 2) <= N-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 <= N-bound (L~ (Rotate f,(N-min (L~ f)))) by EUCLID:56;
|[(p `1 ),((p `2 ) + (r / 2))]| `2 >= S-bound (L~ (Rotate f,(N-min (L~ f)))) by A2, A10, JORDAN2C:120;
then (p `2 ) + (r / 2) >= S-bound (L~ (Rotate f,(N-min (L~ f)))) by EUCLID:56;
then A12: |[(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;
|[(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 A13: |[(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;
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 A14: |[(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 A11, A12, A13;
A15: 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;
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 ;
then (p `2 ) + (r / 2) in proj2 .: (L~ (SpStSeq (L~ (Rotate f,(N-min (L~ f)))))) by A14, A15, FUNCT_2:43;
then A16: sup (proj2 .: (L~ (SpStSeq (L~ (Rotate f,(N-min (L~ f))))))) >= (p `2 ) + (r / 2) by A7, SEQ_4:def 4;
(p `2 ) + (r / 2) > (p `2 ) + 0 by A8, XREAL_1:8;
hence N-bound (L~ f) > p `2 by A1, A5, A6, A16, XXREAL_0:2; :: thesis: verum