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:
assume that
A1: 1 < i and
A2: i <= len (Gauge C,n) and
A3: (Gauge C,n) * i,1 in rng (Upper_Seq C,n) ; :: thesis:
consider i2 being Nat such that
A4: i2 in dom (Upper_Seq C,n) and
A5: (Upper_Seq C,n) . i2 = (Gauge C,n) * i,1 by A3, FINSEQ_2:11;
reconsider i2 = i2 as Element of NAT by ORDINAL1:def 13;
set i1 = (N-min (L~ (Cage C,n))) .. (Upper_Seq C,n);
A6: (W-min (L~ (Cage C,n))) .. (Upper_Seq C,n) = 1 by Th27;
(W-max (L~ (Cage C,n))) .. (Upper_Seq C,n) <= (N-min (L~ (Cage C,n))) .. (Upper_Seq C,n) by Th29;
then A7: (N-min (L~ (Cage C,n))) .. (Upper_Seq C,n) > 1 by A6, Th28, XXREAL_0:2;
(E-max (L~ (Cage C,n))) .. (Upper_Seq C,n) = len (Upper_Seq C,n) by Th32;
then (N-max (L~ (Cage C,n))) .. (Upper_Seq C,n) <= len (Upper_Seq C,n) by Th31;
then A8: (N-min (L~ (Cage C,n))) .. (Upper_Seq C,n) < len (Upper_Seq C,n) by Th30, XXREAL_0:2;
A9: ( 1 <= i2 & i2 <= len (Upper_Seq C,n) ) by A4, FINSEQ_3:27;
A10: (N-min (L~ (Cage C,n))) .. (Upper_Seq C,n) in dom (Upper_Seq C,n) by A7, A8, FINSEQ_3:27;
set f = Rotate (Cage C,n),(W-min (L~ (Cage C,n)));
A11: Upper_Seq C,n = (Rotate (Cage C,n),(W-min (L~ (Cage C,n)))) -: (E-max (L~ (Cage C,n))) by JORDAN1E:def 1;
A12: N-min (L~ (Cage C,n)) in rng (Cage C,n) by SPRECT_2:43;
A13: E-max (L~ (Cage C,n)) in rng (Cage C,n) by SPRECT_2:50;
A14: W-min (L~ (Cage C,n)) in rng (Cage C,n) by SPRECT_2:47;
A15: rng (Rotate (Cage C,n),(W-min (L~ (Cage C,n)))) = rng (Cage C,n) by FINSEQ_6:96, SPRECT_2:47;
A16: (Rotate (Cage C,n),(W-min (L~ (Cage C,n)))) /. 1 = W-min (L~ (Cage C,n)) by A14, FINSEQ_6:98;
A17: L~ (Cage C,n) = L~ (Rotate (Cage C,n),(W-min (L~ (Cage C,n)))) by REVROT_1:33;
then A18: (N-min (L~ (Cage C,n))) .. (Rotate (Cage C,n),(W-min (L~ (Cage C,n)))) < (N-max (L~ (Cage C,n))) .. (Rotate (Cage C,n),(W-min (L~ (Cage C,n)))) by A16, SPRECT_5:25;
(N-max (L~ (Cage C,n))) .. (Rotate (Cage C,n),(W-min (L~ (Cage C,n)))) <= (E-max (L~ (Cage C,n))) .. (Rotate (Cage C,n),(W-min (L~ (Cage C,n)))) by A16, A17, SPRECT_5:26;
then A19: N-min (L~ (Cage C,n)) in rng (Upper_Seq C,n) by A11, A12, A13, A15, A18, FINSEQ_5:49, XXREAL_0:2;
then A20: (Upper_Seq C,n) /. ((N-min (L~ (Cage C,n))) .. (Upper_Seq C,n)) = N-min (L~ (Cage C,n)) by FINSEQ_5:41;
A21: (N-min (L~ (Cage C,n))) .. (Upper_Seq C,n) <> i2

proof

assume (N-min (L~ (Cage C,n))) .. (Upper_Seq C,n) = i2 ; :: thesis:
then (Gauge C,n) * i,1 = N-min (L~ (Cage C,n)) by A5, A10, A20, PARTFUN1:def 8;
then ((Gauge C,n) * i,1) `2 = N-bound (L~ (Cage C,n)) by EUCLID:56;
then S-bound (L~ (Cage C,n)) = N-bound (L~ (Cage C,n)) by A1, A2, JORDAN1A:93;
hence contradiction by SPRECT_1:18; :: thesis:

end;

then mid (Upper_Seq C,n),((N-min (L~ (Cage C,n))) .. (Upper_Seq C,n)),i2 is being_S-Seq by A7, A8, A9, JORDAN3:39;
then reconsider h1 = mid (Upper_Seq C,n),((N-min (L~ (Cage C,n))) .. (Upper_Seq C,n)),i2 as one-to-one special FinSequence of (TOP-REAL 2) ;
set h = Rev h1;
3 <= len (Lower_Seq C,n) by JORDAN1E:19;
then A22: 2 <= len (Lower_Seq C,n) by XXREAL_0:2;
A23: len (Lower_Seq C,n) = len (Rev (Lower_Seq C,n)) by FINSEQ_5:def 3;
A24: len h1 = len (Rev h1) by FINSEQ_5:def 3;
then A25: len (Rev h1) <> 1 by A4, A10, A21, SPRECT_2:10;
A26: len (Rev h1) >= 1 by A4, A10, A24, SPRECT_2:9;
then len (Rev h1) > 1 by A25, XXREAL_0:1;
then A27: 1 + 1 <= len (Rev h1) by NAT_1:13;
A28: Rev h1 is special by SPPOL_2:42;
h1 is_in_the_area_of Cage C,n by A4, A10, JORDAN1E:21, SPRECT_2:26;
then A29: Rev h1 is_in_the_area_of Cage C,n by SPRECT_3:68;
A30: not h1 is empty by A26;
A31: Rev (Lower_Seq C,n) is special by SPPOL_2:42;
A32: L~ (Rev (Lower_Seq C,n)) = L~ (Lower_Seq C,n) by SPPOL_2:22;
A33: ((Rev h1) /. 1) `2 = (h1 /. (len h1)) `2 by A30, FINSEQ_5:68
.= ((Upper_Seq C,n) /. i2) `2 by A4, A10, SPRECT_2:13
.= ((Gauge C,n) * i,1) `2 by A4, A5, PARTFUN1:def 8
.= S-bound (L~ (Cage C,n)) by A1, A2, JORDAN1A:93 ;
((Rev h1) /. (len (Rev h1))) `2 = (h1 /. 1) `2 by A24, A30, FINSEQ_5:68
.= ((Upper_Seq C,n) /. ((N-min (L~ (Cage C,n))) .. (Upper_Seq C,n))) `2 by A4, A10, SPRECT_2:12
.= (N-min (L~ (Cage C,n))) `2 by A19, FINSEQ_5:41
.= N-bound (L~ (Cage C,n)) by EUCLID:56 ;
then Rev h1 is_a_v.c._for Cage C,n by A29, A33, SPRECT_2:def 3;
then L~ (Rev (Lower_Seq C,n)) meets L~ (Rev h1) by A22, A23, A27, A28, A31, Th49, SPRECT_2:33;
then consider x being set such that
A34: x in L~ (Lower_Seq C,n) and
A35: x in L~ (Rev h1) by A32, XBOOLE_0:3;
A36: L~ (Rev h1) = L~ h1 by SPPOL_2:22;
L~ (mid (Upper_Seq C,n),((N-min (L~ (Cage C,n))) .. (Upper_Seq C,n)),i2) c= L~ (Upper_Seq C,n) by A7, A8, A9, JORDAN4:47;
then x in (L~ (Upper_Seq C,n)) /\ (L~ (Lower_Seq C,n)) by A34, A35, A36, XBOOLE_0:def 4;
then A37: 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 A38: 1 <= len (Gauge C,n) by XXREAL_0:2;
A39: len (Gauge C,n) = width (Gauge C,n) by JORDAN8:def 1;

per cases by A37, TARSKI:def 2;

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

then x = (Upper_Seq C,n) /. 1 by JORDAN1F:5;
then i2 = 1 by A7, A8, A9, A35, A36, Th45;
then (Upper_Seq C,n) /. 1 = (Gauge C,n) * i,1 by A4, A5, PARTFUN1:def 8;
then W-min (L~ (Cage C,n)) = (Gauge C,n) * i,1 by JORDAN1F:5;
then ((Gauge C,n) * i,1) `1 = W-bound (L~ (Cage C,n)) by EUCLID:56
.= ((Gauge C,n) * 1,1) `1 by A38, JORDAN1A:94 ;
hence contradiction by A1, A2, A38, A39, GOBOARD5:4; :: thesis:

end;

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

then x = (Upper_Seq C,n) /. (len (Upper_Seq C,n)) by JORDAN1F:7;
then i2 = len (Upper_Seq C,n) by A7, A8, A9, A35, A36, Th46;
then (Upper_Seq C,n) /. (len (Upper_Seq C,n)) = (Gauge C,n) * i,1 by A4, A5, PARTFUN1:def 8;
then A40: E-max (L~ (Cage C,n)) = (Gauge C,n) * i,1 by JORDAN1F:7;
(SE-corner (L~ (Cage C,n))) `2 <= (E-min (L~ (Cage C,n))) `2 by PSCOMP_1:107;
then (SE-corner (L~ (Cage C,n))) `2 < (E-max (L~ (Cage C,n))) `2 by SPRECT_2:57, XXREAL_0:2;
then S-bound (L~ (Cage C,n)) < ((Gauge C,n) * i,1) `2 by A40, EUCLID:56;
hence contradiction by A1, A2, JORDAN1A:93; :: thesis:

end;