let z be non constant standard clockwise_oriented special_circular_sequence; :: thesis: ( z /. 1 = N-min (L~ z) & S-min (L~ z) <> W-min (L~ z) implies (S-min (L~ z)) .. z < (W-min (L~ z)) .. z )
set i1 = (E-min (L~ z)) .. z;
set i2 = (W-min (L~ z)) .. z;
set j = (S-min (L~ z)) .. z;
assume that
A1: z /. 1 = N-min (L~ z) and
A2: S-min (L~ z) <> W-min (L~ z) and
A3: (S-min (L~ z)) .. z >= (W-min (L~ z)) .. z ; :: thesis: contradiction
A4: (E-min (L~ z)) .. z < (W-min (L~ z)) .. z by A1, Lm11;
A5: E-min (L~ z) in rng z by Th49;
A6: S-min (L~ z) in rng z by Th45;
A7: W-min (L~ z) in rng z by Th47;
A8: (E-min (L~ z)) .. z in dom z by A5, FINSEQ_4:30;
then A9: ( 1 <= (E-min (L~ z)) .. z & (E-min (L~ z)) .. z <= len z ) by FINSEQ_3:27;
A10: (W-min (L~ z)) .. z in dom z by A7, FINSEQ_4:30;
then A11: ( 1 <= (W-min (L~ z)) .. z & (W-min (L~ z)) .. z <= len z ) by FINSEQ_3:27;
A12: z /. ((W-min (L~ z)) .. z) = z . ((W-min (L~ z)) .. z) by A10, PARTFUN1:def 8
.= W-min (L~ z) by A7, FINSEQ_4:29 ;
A13: z /. (len z) = N-min (L~ z) by A1, FINSEQ_6:def 1;
A14: (S-min (L~ z)) .. z in dom z by A6, FINSEQ_4:30;
then A15: z /. ((S-min (L~ z)) .. z) = z . ((S-min (L~ z)) .. z) by PARTFUN1:def 8
.= S-min (L~ z) by A6, FINSEQ_4:29 ;
A16: z /. ((E-min (L~ z)) .. z) = z . ((E-min (L~ z)) .. z) by A8, PARTFUN1:def 8
.= E-min (L~ z) by A5, FINSEQ_4:29 ;
A17: (S-min (L~ z)) .. z > (W-min (L~ z)) .. z by A2, A3, A12, A15, XXREAL_0:1;
N-max (L~ z) in L~ z by SPRECT_1:13;
then (N-max (L~ z)) `1 <= E-bound (L~ z) by PSCOMP_1:71;
then (N-min (L~ z)) `1 < E-bound (L~ z) by Th55, XXREAL_0:2;
then (N-min (L~ z)) `1 < (E-min (L~ z)) `1 by EUCLID:56;
then A18: (E-min (L~ z)) .. z > 1 by A1, A9, A16, XXREAL_0:1;
A19: len z in dom z by FINSEQ_5:6;
A20: ( 1 <= (S-min (L~ z)) .. z & (S-min (L~ z)) .. z <= len z ) by A14, FINSEQ_3:27;
A21: z /. ((S-min (L~ z)) .. z) = z . ((S-min (L~ z)) .. z) by A14, PARTFUN1:def 8
.= S-min (L~ z) by A6, FINSEQ_4:29 ;
( (N-min (L~ z)) `2 = N-bound (L~ z) & (S-min (L~ z)) `2 = S-bound (L~ z) ) by EUCLID:56;
then N-min (L~ z) <> S-min (L~ z) by TOPREAL5:22;
then A22: (S-min (L~ z)) .. z < len z by A13, A20, A21, XXREAL_0:1;
(S-min (L~ z)) .. z > 1 by A1, A9, Lm9, XXREAL_0:2;
then reconsider h = mid z,((S-min (L~ z)) .. z),(len z) as S-Sequence_in_R2 by A22, Th42;
A23: h is_in_the_area_of z by A14, A19, Th25, Th26;
h /. 1 = S-min (L~ z) by A14, A15, A19, Th12;
then A24: (h /. 1) `2 = S-bound (L~ z) by EUCLID:56;
h /. (len h) = z /. (len z) by A14, A19, Th13;
then (h /. (len h)) `2 = N-bound (L~ z) by A13, EUCLID:56;
then A25: h is_a_v.c._for z by A23, A24, Def3;
reconsider M = mid z,((W-min (L~ z)) .. z),((E-min (L~ z)) .. z) as S-Sequence_in_R2 by A4, A11, A18, Th41;
A26: ( len h >= 2 & len M >= 2 ) by TOPREAL1:def 10;
A27: L~ M misses L~ h by A4, A17, A18, A20, Th54;
A28: M /. (len M) = z /. ((E-min (L~ z)) .. z) by A8, A10, Th13
.= E-min (L~ z) by A5, FINSEQ_5:41 ;
A29: M /. 1 = W-min (L~ z) by A8, A10, A12, Th12;
A30: M is_in_the_area_of z by A8, A10, Th25, Th26;
A31: (M /. 1) `1 = W-bound (L~ z) by A29, EUCLID:56;
(M /. (len M)) `1 = E-bound (L~ z) by A28, EUCLID:56;
then M is_a_h.c._for z by A30, A31, Def2;
hence contradiction by A25, A26, A27, Th33; :: thesis: verum