let n be Element of NAT ; :: thesis:
let C be connected compact non horizontal non vertical Subset of (TOP-REAL 2); :: thesis:
let i be Element of NAT ; :: thesis:
set wi = width (Gauge C,n);
assume that
A1: 1 <= i and
A2: i < len (Gauge C,n) and
A3: (Gauge C,n) * i,(width (Gauge C,n)) in rng (Lower_Seq C,n) ; :: thesis:
consider i2 being Nat such that
A4: i2 in dom (Lower_Seq C,n) and
A5: (Lower_Seq C,n) . i2 = (Gauge C,n) * i,(width (Gauge C,n)) by A3, FINSEQ_2:11;
reconsider i2 = i2 as Element of NAT by ORDINAL1:def 13;
set i1 = (S-max (L~ (Cage C,n))) .. (Lower_Seq C,n);
A6: len (Gauge C,n) = width (Gauge C,n) by JORDAN8:def 1;
A7: (E-max (L~ (Cage C,n))) .. (Lower_Seq C,n) = 1 by Th33;
(E-min (L~ (Cage C,n))) .. (Lower_Seq C,n) <= (S-max (L~ (Cage C,n))) .. (Lower_Seq C,n) by Th35;
then A8: (S-max (L~ (Cage C,n))) .. (Lower_Seq C,n) > 1 by A7, Th34, XXREAL_0:2;
(W-min (L~ (Cage C,n))) .. (Lower_Seq C,n) = len (Lower_Seq C,n) by Th38;
then (S-min (L~ (Cage C,n))) .. (Lower_Seq C,n) <= len (Lower_Seq C,n) by Th37;
then A9: (S-max (L~ (Cage C,n))) .. (Lower_Seq C,n) < len (Lower_Seq C,n) by Th36, XXREAL_0:2;
A10: ( 1 <= i2 & i2 <= len (Lower_Seq C,n) ) by A4, FINSEQ_3:27;
A11: (S-max (L~ (Cage C,n))) .. (Lower_Seq C,n) in dom (Lower_Seq C,n) by A8, A9, FINSEQ_3:27;
set f = Rotate (Cage C,n),(E-max (L~ (Cage C,n)));
A12: Lower_Seq C,n = (Rotate (Cage C,n),(E-max (L~ (Cage C,n)))) -: (W-min (L~ (Cage C,n))) by Th26;
A13: S-max (L~ (Cage C,n)) in rng (Cage C,n) by SPRECT_2:46;
A14: W-min (L~ (Cage C,n)) in rng (Cage C,n) by SPRECT_2:47;
A15: E-max (L~ (Cage C,n)) in rng (Cage C,n) by SPRECT_2:50;
A16: rng (Rotate (Cage C,n),(E-max (L~ (Cage C,n)))) = rng (Cage C,n) by FINSEQ_6:96, SPRECT_2:50;
A17: (Rotate (Cage C,n),(E-max (L~ (Cage C,n)))) /. 1 = E-max (L~ (Cage C,n)) by A15, FINSEQ_6:98;
A18: L~ (Cage C,n) = L~ (Rotate (Cage C,n),(E-max (L~ (Cage C,n)))) by REVROT_1:33;
then A19: (S-max (L~ (Cage C,n))) .. (Rotate (Cage C,n),(E-max (L~ (Cage C,n)))) < (S-min (L~ (Cage C,n))) .. (Rotate (Cage C,n),(E-max (L~ (Cage C,n)))) by A17, SPRECT_5:41;
(S-min (L~ (Cage C,n))) .. (Rotate (Cage C,n),(E-max (L~ (Cage C,n)))) <= (W-min (L~ (Cage C,n))) .. (Rotate (Cage C,n),(E-max (L~ (Cage C,n)))) by A17, A18, SPRECT_5:42;
then A20: S-max (L~ (Cage C,n)) in rng (Lower_Seq C,n) by A12, A13, A14, A16, A19, FINSEQ_5:49, XXREAL_0:2;
then A21: (Lower_Seq C,n) /. ((S-max (L~ (Cage C,n))) .. (Lower_Seq C,n)) = S-max (L~ (Cage C,n)) by FINSEQ_5:41;
A22: (S-max (L~ (Cage C,n))) .. (Lower_Seq C,n) <> i2

proof

assume (S-max (L~ (Cage C,n))) .. (Lower_Seq C,n) = i2 ; :: thesis:
then (Gauge C,n) * i,(width (Gauge C,n)) = S-max (L~ (Cage C,n)) by A5, A11, A21, PARTFUN1:def 8;
then ((Gauge C,n) * i,(width (Gauge C,n))) `2 = S-bound (L~ (Cage C,n)) by EUCLID:56;
then N-bound (L~ (Cage C,n)) = S-bound (L~ (Cage C,n)) by A1, A2, A6, JORDAN1A:91;
hence contradiction by SPRECT_1:18; :: thesis:

end;

then mid (Lower_Seq C,n),((S-max (L~ (Cage C,n))) .. (Lower_Seq C,n)),i2 is being_S-Seq by A8, A9, A10, JORDAN3:39;
then reconsider h = mid (Lower_Seq C,n),((S-max (L~ (Cage C,n))) .. (Lower_Seq C,n)),i2 as one-to-one special FinSequence of (TOP-REAL 2) ;
3 <= len (Upper_Seq C,n) by JORDAN1E:19;
then A23: 2 <= len (Upper_Seq C,n) by XXREAL_0:2;
A24: len h <> 1 by A4, A11, A22, SPRECT_2:10;
len h >= 1 by A4, A11, SPRECT_2:9;
then len h > 1 by A24, XXREAL_0:1;
then A25: 1 + 1 <= len h by NAT_1:13;
A26: h is_in_the_area_of Cage C,n by A4, A11, JORDAN1E:22, SPRECT_2:26;
A27: (h /. (len h)) `2 = ((Lower_Seq C,n) /. i2) `2 by A4, A11, SPRECT_2:13
.= ((Gauge C,n) * i,(width (Gauge C,n))) `2 by A4, A5, PARTFUN1:def 8
.= N-bound (L~ (Cage C,n)) by A1, A2, A6, JORDAN1A:91 ;
(h /. 1) `2 = ((Lower_Seq C,n) /. ((S-max (L~ (Cage C,n))) .. (Lower_Seq C,n))) `2 by A4, A11, SPRECT_2:12
.= (S-max (L~ (Cage C,n))) `2 by A20, FINSEQ_5:41
.= S-bound (L~ (Cage C,n)) by EUCLID:56 ;
then h is_a_v.c._for Cage C,n by A26, A27, SPRECT_2:def 3;
then L~ (Upper_Seq C,n) meets L~ h by A23, A25, Th48, SPRECT_2:33;
then consider x being set such that
A28: x in L~ (Upper_Seq C,n) and
A29: x in L~ h by XBOOLE_0:3;
L~ (mid (Lower_Seq C,n),((S-max (L~ (Cage C,n))) .. (Lower_Seq C,n)),i2) c= L~ (Lower_Seq C,n) by A8, A9, A10, JORDAN4:47;
then x in (L~ (Lower_Seq C,n)) /\ (L~ (Upper_Seq C,n)) by A28, A29, XBOOLE_0:def 4;
then A30: x in {(W-min (L~ (Cage C,n))),(E-max (L~ (Cage C,n)))} by JORDAN1E:20;
4 <= len (Gauge C,n) by JORDAN8:13;
then A31: 1 <= len (Gauge C,n) by XXREAL_0:2;

per cases by A30, TARSKI:def 2;

suppose x = E-max (L~ (Cage C,n)) ; :: thesis:

then x = (Lower_Seq C,n) /. 1 by JORDAN1F:6;
then i2 = 1 by A8, A9, A10, A29, Th45;
then (Lower_Seq C,n) /. 1 = (Gauge C,n) * i,(width (Gauge C,n)) by A4, A5, PARTFUN1:def 8;
then E-max (L~ (Cage C,n)) = (Gauge C,n) * i,(width (Gauge C,n)) by JORDAN1F:6;
then ((Gauge C,n) * i,(width (Gauge C,n))) `1 = E-bound (L~ (Cage C,n)) by EUCLID:56
.= ((Gauge C,n) * (len (Gauge C,n)),(width (Gauge C,n))) `1 by A6, A31, JORDAN1A:92 ;
hence contradiction by A1, A2, A6, A31, GOBOARD5:4; :: thesis:

end;

suppose x = W-min (L~ (Cage C,n)) ; :: thesis:

then x = (Lower_Seq C,n) /. (len (Lower_Seq C,n)) by JORDAN1F:8;
then i2 = len (Lower_Seq C,n) by A8, A9, A10, A29, Th46;
then (Lower_Seq C,n) /. (len (Lower_Seq C,n)) = (Gauge C,n) * i,(width (Gauge C,n)) by A4, A5, PARTFUN1:def 8;
then A32: W-min (L~ (Cage C,n)) = (Gauge C,n) * i,(width (Gauge C,n)) by JORDAN1F:8;
(NW-corner (L~ (Cage C,n))) `2 >= (W-max (L~ (Cage C,n))) `2 by PSCOMP_1:87;
then (NW-corner (L~ (Cage C,n))) `2 > (W-min (L~ (Cage C,n))) `2 by SPRECT_2:61, XXREAL_0:2;
then N-bound (L~ (Cage C,n)) > ((Gauge C,n) * i,(width (Gauge C,n))) `2 by A32, EUCLID:56;
hence contradiction by A1, A2, A6, JORDAN1A:91; :: thesis:

end;