let z be V22() standard clockwise_oriented special_circular_sequence; :: thesis: ( z /. 1 = N-min (L~ z) implies (S-max (L~ z)) .. z < (S-min (L~ z)) .. z )
set i1 = (S-max (L~ z)) .. z;
set i2 = (S-min (L~ z)) .. z;
set j = (N-max (L~ z)) .. z;
assume that
A1: z /. 1 = N-min (L~ z) and
A2: (S-max (L~ z)) .. z >= (S-min (L~ z)) .. z ; :: thesis: contradiction
A3: z /. 1 = z /. (len z) by FINSEQ_6:def 1;
A4: S-min (L~ z) in rng z by Th41;
then A5: (S-min (L~ z)) .. z in dom z by FINSEQ_4:20;
then A6: (S-min (L~ z)) .. z <= len z by FINSEQ_3:25;
A7: 1 <= (S-min (L~ z)) .. z by A5, FINSEQ_3:25;
A8: S-max (L~ z) in rng z by Th42;
then A9: (S-max (L~ z)) .. z in dom z by FINSEQ_4:20;
then A10: z /. ((S-max (L~ z)) .. z) = z . ((S-max (L~ z)) .. z) by PARTFUN1:def 6
.= S-max (L~ z) by A8, FINSEQ_4:19 ;
A11: (S-max (L~ z)) .. z <= len z by A9, FINSEQ_3:25;
( (N-min (L~ z)) `2 = N-bound (L~ z) & (S-max (L~ z)) `2 = S-bound (L~ z) ) by EUCLID:52;
then N-min (L~ z) <> S-max (L~ z) by TOPREAL5:16;
then A12: (S-max (L~ z)) .. z < len z by A1, A11, A10, A3, XXREAL_0:1;
then ((S-max (L~ z)) .. z) + 1 <= len z by NAT_1:13;
then (len z) - ((S-max (L~ z)) .. z) >= 1 by XREAL_1:19;
then (len z) -' ((S-max (L~ z)) .. z) >= 1 by NAT_D:39;
then A13: ((len z) -' ((S-max (L~ z)) .. z)) + 1 >= 1 + 1 by XREAL_1:6;
A14: N-max (L~ z) in rng z by Th40;
then A15: (N-max (L~ z)) .. z in dom z by FINSEQ_4:20;
then A16: 1 <= (N-max (L~ z)) .. z by FINSEQ_3:25;
then (S-max (L~ z)) .. z > 1 by A1, Lm5, XXREAL_0:2;
then reconsider M = mid (z,(len z),((S-max (L~ z)) .. z)) as S-Sequence_in_R2 by A12, Th37;
A17: z /. ((N-max (L~ z)) .. z) = z . ((N-max (L~ z)) .. z) by A15, PARTFUN1:def 6
.= N-max (L~ z) by A14, FINSEQ_4:19 ;
then A18: (z /. ((N-max (L~ z)) .. z)) `2 = N-bound (L~ z) by EUCLID:52;
N-min (L~ z) <> N-max (L~ z) by Th52;
then A19: 1 < (N-max (L~ z)) .. z by A1, A16, A17, XXREAL_0:1;
A20: len z in dom z by FINSEQ_5:6;
then A21: M /. 1 = z /. (len z) by A9, Th8;
1 <= (S-max (L~ z)) .. z by A9, FINSEQ_3:25;
then A22: len M = ((len z) -' ((S-max (L~ z)) .. z)) + 1 by A11, JORDAN4:9;
then A23: M /. (len M) in L~ M by A13, JORDAN3:1;
A24: 1 in dom M by FINSEQ_5:6;
A25: (N-max (L~ z)) .. z <= len z by A15, FINSEQ_3:25;
A26: (S-min (L~ z)) .. z > (N-max (L~ z)) .. z by A1, Lm6;
then reconsider h = mid (z,((S-min (L~ z)) .. z),((N-max (L~ z)) .. z)) as S-Sequence_in_R2 by A6, A19, Th37;
A27: z /. ((S-min (L~ z)) .. z) = z . ((S-min (L~ z)) .. z) by A5, PARTFUN1:def 6
.= S-min (L~ z) by A4, FINSEQ_4:19 ;
then h /. 1 = S-min (L~ z) by A5, A15, Th8;
then A28: (h /. 1) `2 = S-bound (L~ z) by EUCLID:52;
( h is_in_the_area_of z & h /. (len h) = z /. ((N-max (L~ z)) .. z) ) by A5, A15, Th9, Th21, Th22;
then A29: ( len h >= 2 & h is_a_v.c._for z ) by A18, A28, TOPREAL1:def 8;
S-min (L~ z) <> S-max (L~ z) by Th56;
then (S-max (L~ z)) .. z > (S-min (L~ z)) .. z by A2, A27, A10, XXREAL_0:1;
then A30: L~ h misses L~ M by A11, A26, A19, Th49;
A31: M /. (len M) = S-max (L~ z) by A9, A10, A20, Th9;