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