let p be Point of (TOP-REAL 2); :: thesis:
let f be non constant standard clockwise_oriented special_circular_sequence; :: thesis:
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:
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 ) - (r / 2)),(p `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 ) - (r / 2)),(p `2 )]| `1 )) ^2 ) + (((p `2 ) - (|[((p `1 ) - (r / 2)),(p `2 )]| `2 )) ^2 )) by TOPREAL3:12
.= sqrt ((((p `1 ) - ((p `1 ) - (r / 2))) ^2 ) + (((p `2 ) - (|[((p `1 ) - (r / 2)),(p `2 )]| `2 )) ^2 )) by EUCLID:56
.= sqrt ((((p `1 ) - ((p `1 ) - (r / 2))) ^2 ) + (((p `2 ) - (p `2 )) ^2 )) by EUCLID:56
.= 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 ) - (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:26;
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 28
.= (p `1 ) - (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 ) - (r / 2)),(p `2 )]| `1 <= E-bound (L~ (Rotate f,(N-min (L~ f)))) by A5, JORDAN2C:119;
then (p `1 ) - (r / 2) <= E-bound (L~ (Rotate f,(N-min (L~ f)))) by EUCLID:56;
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:56;
|[((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:56;
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:68;
|[((p `1 ) - (r / 2)),(p `2 )]| `1 >= W-bound (L~ (Rotate f,(N-min (L~ f)))) by A8, A5, JORDAN2C:118;
then (p `1 ) - (r / 2) >= W-bound (L~ (Rotate f,(N-min (L~ f)))) by EUCLID:56;
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:56;
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:27;
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_below & (p `1 ) - (r / 2) in proj1 .: (L~ (SpStSeq (L~ (Rotate f,(N-min (L~ f)))))) ) by A6, A7, FUNCT_2:43, SPRECT_1:46;
then A12: lower_bound (proj1 .: (L~ (SpStSeq (L~ (Rotate f,(N-min (L~ f))))))) <= (p `1 ) - (r / 2) by SEQ_4:def 5;
r / 2 > 0 by A2, XREAL_1:141;
then A13: (p `1 ) - (r / 2) < (p `1 ) - 0 by XREAL_1:17;
( W-bound (L~ (SpStSeq (L~ (Rotate f,(N-min (L~ f)))))) = W-bound (L~ (Rotate f,(N-min (L~ f)))) & W-bound (L~ (SpStSeq (L~ (Rotate f,(N-min (L~ f)))))) = lower_bound (proj1 .: (L~ (SpStSeq (L~ (Rotate f,(N-min (L~ f))))))) ) by SPRECT_1:48, SPRECT_1:66;
hence W-bound (L~ f) < p `1 by A1, A12, A13, XXREAL_0:2; :: thesis: