let n be Nat; :: thesis: for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2)

for i being Nat st 1 < i & i <= len (Gauge (C,n)) holds

not (Gauge (C,n)) * (i,1) in rng (Upper_Seq (C,n))

let C be connected compact non horizontal non vertical Subset of (TOP-REAL 2); :: thesis: for i being Nat st 1 < i & i <= len (Gauge (C,n)) holds

not (Gauge (C,n)) * (i,1) in rng (Upper_Seq (C,n))

let i be Nat; :: thesis: ( 1 < i & i <= len (Gauge (C,n)) implies not (Gauge (C,n)) * (i,1) in rng (Upper_Seq (C,n)) )

assume that

A1: ( 1 < i & i <= len (Gauge (C,n)) ) and

A2: (Gauge (C,n)) * (i,1) in rng (Upper_Seq (C,n)) ; :: thesis: contradiction

consider i2 being Nat such that

A3: i2 in dom (Upper_Seq (C,n)) and

A4: (Upper_Seq (C,n)) . i2 = (Gauge (C,n)) * (i,1) by A2, FINSEQ_2:10;

reconsider i2 = i2 as Nat ;

A5: ( 1 <= i2 & i2 <= len (Upper_Seq (C,n)) ) by A3, FINSEQ_3:25;

set f = Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))));

set i1 = (N-min (L~ (Cage (C,n)))) .. (Upper_Seq (C,n));

A6: ( E-max (L~ (Cage (C,n))) in rng (Cage (C,n)) & rng (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) = rng (Cage (C,n)) ) by FINSEQ_6:90, SPRECT_2:43, SPRECT_2:46;

W-min (L~ (Cage (C,n))) in rng (Cage (C,n)) by SPRECT_2:43;

then A7: (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) /. 1 = W-min (L~ (Cage (C,n))) by FINSEQ_6:92;

L~ (Cage (C,n)) = L~ (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) by REVROT_1:33;

then A8: ( (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)))))) & (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 A7, SPRECT_5:24, SPRECT_5:25;

(E-max (L~ (Cage (C,n)))) .. (Upper_Seq (C,n)) = len (Upper_Seq (C,n)) by Th24;

then (N-max (L~ (Cage (C,n)))) .. (Upper_Seq (C,n)) <= len (Upper_Seq (C,n)) by Th23;

then A9: (N-min (L~ (Cage (C,n)))) .. (Upper_Seq (C,n)) < len (Upper_Seq (C,n)) by Th22, XXREAL_0:2;

3 <= len (Lower_Seq (C,n)) by JORDAN1E:15;

then A10: 2 <= len (Lower_Seq (C,n)) by XXREAL_0:2;

A11: len (Gauge (C,n)) = width (Gauge (C,n)) by JORDAN8:def 1;

4 <= len (Gauge (C,n)) by JORDAN8:10;

then A12: 1 <= len (Gauge (C,n)) by XXREAL_0:2;

( (W-min (L~ (Cage (C,n)))) .. (Upper_Seq (C,n)) = 1 & (W-max (L~ (Cage (C,n)))) .. (Upper_Seq (C,n)) <= (N-min (L~ (Cage (C,n)))) .. (Upper_Seq (C,n)) ) by Th19, Th21;

then A13: (N-min (L~ (Cage (C,n)))) .. (Upper_Seq (C,n)) > 1 by Th20, XXREAL_0:2;

then A14: (N-min (L~ (Cage (C,n)))) .. (Upper_Seq (C,n)) in dom (Upper_Seq (C,n)) by A9, FINSEQ_3:25;

( Upper_Seq (C,n) = (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) -: (E-max (L~ (Cage (C,n)))) & N-min (L~ (Cage (C,n))) in rng (Cage (C,n)) ) by JORDAN1E:def 1, SPRECT_2:39;

then A15: N-min (L~ (Cage (C,n))) in rng (Upper_Seq (C,n)) by A6, A8, FINSEQ_5:46, XXREAL_0:2;

then A16: (Upper_Seq (C,n)) /. ((N-min (L~ (Cage (C,n)))) .. (Upper_Seq (C,n))) = N-min (L~ (Cage (C,n))) by FINSEQ_5:38;

A17: ( (N-min (L~ (Cage (C,n)))) .. (Upper_Seq (C,n)) in NAT & i2 in NAT ) by ORDINAL1:def 12;

A18: (N-min (L~ (Cage (C,n)))) .. (Upper_Seq (C,n)) <> i2

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;

A19: len h1 = len (Rev h1) by FINSEQ_5:def 3;

then A20: not h1 is empty by A3, A14, SPRECT_2:5;

then A21: ((Rev h1) /. (len (Rev h1))) `2 = (h1 /. 1) `2 by A19, FINSEQ_5:65

.= ((Upper_Seq (C,n)) /. ((N-min (L~ (Cage (C,n)))) .. (Upper_Seq (C,n)))) `2 by A3, A14, SPRECT_2:8

.= (N-min (L~ (Cage (C,n)))) `2 by A15, FINSEQ_5:38

.= N-bound (L~ (Cage (C,n))) by EUCLID:52 ;

h1 is_in_the_area_of Cage (C,n) by A3, A14, JORDAN1E:17, SPRECT_2:22;

then A22: Rev h1 is_in_the_area_of Cage (C,n) by SPRECT_3:51;

((Rev h1) /. 1) `2 = (h1 /. (len h1)) `2 by A20, FINSEQ_5:65

.= ((Upper_Seq (C,n)) /. i2) `2 by A3, A14, SPRECT_2:9

.= ((Gauge (C,n)) * (i,1)) `2 by A3, A4, PARTFUN1:def 6

.= S-bound (L~ (Cage (C,n))) by A1, JORDAN1A:72 ;

then A23: ( Rev (Lower_Seq (C,n)) is special & Rev h1 is_a_v.c._for Cage (C,n) ) by A22, A21, SPRECT_2:def 3;

len (Rev h1) >= 1 by A3, A14, A19, SPRECT_2:5;

then len (Rev h1) > 1 by A3, A14, A18, A19, SPRECT_2:6, XXREAL_0:1;

then A24: 1 + 1 <= len (Rev h1) by NAT_1:13;

( len (Lower_Seq (C,n)) = len (Rev (Lower_Seq (C,n))) & Rev h1 is special ) by FINSEQ_5:def 3, SPPOL_2:40;

then ( L~ (Rev (Lower_Seq (C,n))) = L~ (Lower_Seq (C,n)) & L~ (Rev (Lower_Seq (C,n))) meets L~ (Rev h1) ) by A10, A24, A23, Th41, SPPOL_2:22, SPRECT_2:29;

then consider x being object such that

A25: x in L~ (Lower_Seq (C,n)) and

A26: x in L~ (Rev h1) by XBOOLE_0:3;

A27: 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 A13, A9, A5, JORDAN4:35;

then x in (L~ (Upper_Seq (C,n))) /\ (L~ (Lower_Seq (C,n))) by A25, A26, A27, XBOOLE_0:def 4;

then A28: x in {(W-min (L~ (Cage (C,n)))),(E-max (L~ (Cage (C,n))))} by JORDAN1E:16;

for i being Nat st 1 < i & i <= len (Gauge (C,n)) holds

not (Gauge (C,n)) * (i,1) in rng (Upper_Seq (C,n))

let C be connected compact non horizontal non vertical Subset of (TOP-REAL 2); :: thesis: for i being Nat st 1 < i & i <= len (Gauge (C,n)) holds

not (Gauge (C,n)) * (i,1) in rng (Upper_Seq (C,n))

let i be Nat; :: thesis: ( 1 < i & i <= len (Gauge (C,n)) implies not (Gauge (C,n)) * (i,1) in rng (Upper_Seq (C,n)) )

assume that

A1: ( 1 < i & i <= len (Gauge (C,n)) ) and

A2: (Gauge (C,n)) * (i,1) in rng (Upper_Seq (C,n)) ; :: thesis: contradiction

consider i2 being Nat such that

A3: i2 in dom (Upper_Seq (C,n)) and

A4: (Upper_Seq (C,n)) . i2 = (Gauge (C,n)) * (i,1) by A2, FINSEQ_2:10;

reconsider i2 = i2 as Nat ;

A5: ( 1 <= i2 & i2 <= len (Upper_Seq (C,n)) ) by A3, FINSEQ_3:25;

set f = Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))));

set i1 = (N-min (L~ (Cage (C,n)))) .. (Upper_Seq (C,n));

A6: ( E-max (L~ (Cage (C,n))) in rng (Cage (C,n)) & rng (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) = rng (Cage (C,n)) ) by FINSEQ_6:90, SPRECT_2:43, SPRECT_2:46;

W-min (L~ (Cage (C,n))) in rng (Cage (C,n)) by SPRECT_2:43;

then A7: (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) /. 1 = W-min (L~ (Cage (C,n))) by FINSEQ_6:92;

L~ (Cage (C,n)) = L~ (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) by REVROT_1:33;

then A8: ( (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)))))) & (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 A7, SPRECT_5:24, SPRECT_5:25;

(E-max (L~ (Cage (C,n)))) .. (Upper_Seq (C,n)) = len (Upper_Seq (C,n)) by Th24;

then (N-max (L~ (Cage (C,n)))) .. (Upper_Seq (C,n)) <= len (Upper_Seq (C,n)) by Th23;

then A9: (N-min (L~ (Cage (C,n)))) .. (Upper_Seq (C,n)) < len (Upper_Seq (C,n)) by Th22, XXREAL_0:2;

3 <= len (Lower_Seq (C,n)) by JORDAN1E:15;

then A10: 2 <= len (Lower_Seq (C,n)) by XXREAL_0:2;

A11: len (Gauge (C,n)) = width (Gauge (C,n)) by JORDAN8:def 1;

4 <= len (Gauge (C,n)) by JORDAN8:10;

then A12: 1 <= len (Gauge (C,n)) by XXREAL_0:2;

( (W-min (L~ (Cage (C,n)))) .. (Upper_Seq (C,n)) = 1 & (W-max (L~ (Cage (C,n)))) .. (Upper_Seq (C,n)) <= (N-min (L~ (Cage (C,n)))) .. (Upper_Seq (C,n)) ) by Th19, Th21;

then A13: (N-min (L~ (Cage (C,n)))) .. (Upper_Seq (C,n)) > 1 by Th20, XXREAL_0:2;

then A14: (N-min (L~ (Cage (C,n)))) .. (Upper_Seq (C,n)) in dom (Upper_Seq (C,n)) by A9, FINSEQ_3:25;

( Upper_Seq (C,n) = (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) -: (E-max (L~ (Cage (C,n)))) & N-min (L~ (Cage (C,n))) in rng (Cage (C,n)) ) by JORDAN1E:def 1, SPRECT_2:39;

then A15: N-min (L~ (Cage (C,n))) in rng (Upper_Seq (C,n)) by A6, A8, FINSEQ_5:46, XXREAL_0:2;

then A16: (Upper_Seq (C,n)) /. ((N-min (L~ (Cage (C,n)))) .. (Upper_Seq (C,n))) = N-min (L~ (Cage (C,n))) by FINSEQ_5:38;

A17: ( (N-min (L~ (Cage (C,n)))) .. (Upper_Seq (C,n)) in NAT & i2 in NAT ) by ORDINAL1:def 12;

A18: (N-min (L~ (Cage (C,n)))) .. (Upper_Seq (C,n)) <> i2

proof

then
mid ((Upper_Seq (C,n)),((N-min (L~ (Cage (C,n)))) .. (Upper_Seq (C,n))),i2) is being_S-Seq
by A13, A9, A5, JORDAN3:6, A17;
assume
(N-min (L~ (Cage (C,n)))) .. (Upper_Seq (C,n)) = i2
; :: thesis: contradiction

then (Gauge (C,n)) * (i,1) = N-min (L~ (Cage (C,n))) by A4, A14, A16, PARTFUN1:def 6;

then ((Gauge (C,n)) * (i,1)) `2 = N-bound (L~ (Cage (C,n))) by EUCLID:52;

then S-bound (L~ (Cage (C,n))) = N-bound (L~ (Cage (C,n))) by A1, JORDAN1A:72;

hence contradiction by SPRECT_1:16; :: thesis: verum

end;then (Gauge (C,n)) * (i,1) = N-min (L~ (Cage (C,n))) by A4, A14, A16, PARTFUN1:def 6;

then ((Gauge (C,n)) * (i,1)) `2 = N-bound (L~ (Cage (C,n))) by EUCLID:52;

then S-bound (L~ (Cage (C,n))) = N-bound (L~ (Cage (C,n))) by A1, JORDAN1A:72;

hence contradiction by SPRECT_1:16; :: thesis: verum

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;

A19: len h1 = len (Rev h1) by FINSEQ_5:def 3;

then A20: not h1 is empty by A3, A14, SPRECT_2:5;

then A21: ((Rev h1) /. (len (Rev h1))) `2 = (h1 /. 1) `2 by A19, FINSEQ_5:65

.= ((Upper_Seq (C,n)) /. ((N-min (L~ (Cage (C,n)))) .. (Upper_Seq (C,n)))) `2 by A3, A14, SPRECT_2:8

.= (N-min (L~ (Cage (C,n)))) `2 by A15, FINSEQ_5:38

.= N-bound (L~ (Cage (C,n))) by EUCLID:52 ;

h1 is_in_the_area_of Cage (C,n) by A3, A14, JORDAN1E:17, SPRECT_2:22;

then A22: Rev h1 is_in_the_area_of Cage (C,n) by SPRECT_3:51;

((Rev h1) /. 1) `2 = (h1 /. (len h1)) `2 by A20, FINSEQ_5:65

.= ((Upper_Seq (C,n)) /. i2) `2 by A3, A14, SPRECT_2:9

.= ((Gauge (C,n)) * (i,1)) `2 by A3, A4, PARTFUN1:def 6

.= S-bound (L~ (Cage (C,n))) by A1, JORDAN1A:72 ;

then A23: ( Rev (Lower_Seq (C,n)) is special & Rev h1 is_a_v.c._for Cage (C,n) ) by A22, A21, SPRECT_2:def 3;

len (Rev h1) >= 1 by A3, A14, A19, SPRECT_2:5;

then len (Rev h1) > 1 by A3, A14, A18, A19, SPRECT_2:6, XXREAL_0:1;

then A24: 1 + 1 <= len (Rev h1) by NAT_1:13;

( len (Lower_Seq (C,n)) = len (Rev (Lower_Seq (C,n))) & Rev h1 is special ) by FINSEQ_5:def 3, SPPOL_2:40;

then ( L~ (Rev (Lower_Seq (C,n))) = L~ (Lower_Seq (C,n)) & L~ (Rev (Lower_Seq (C,n))) meets L~ (Rev h1) ) by A10, A24, A23, Th41, SPPOL_2:22, SPRECT_2:29;

then consider x being object such that

A25: x in L~ (Lower_Seq (C,n)) and

A26: x in L~ (Rev h1) by XBOOLE_0:3;

A27: 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 A13, A9, A5, JORDAN4:35;

then x in (L~ (Upper_Seq (C,n))) /\ (L~ (Lower_Seq (C,n))) by A25, A26, A27, XBOOLE_0:def 4;

then A28: x in {(W-min (L~ (Cage (C,n)))),(E-max (L~ (Cage (C,n))))} by JORDAN1E:16;

per cases
( x = W-min (L~ (Cage (C,n))) or x = E-max (L~ (Cage (C,n))) )
by A28, TARSKI:def 2;

end;

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

then
x = (Upper_Seq (C,n)) /. 1
by JORDAN1F:5;

then i2 = 1 by A13, A9, A5, A26, A27, Th37;

then (Upper_Seq (C,n)) /. 1 = (Gauge (C,n)) * (i,1) by A3, A4, PARTFUN1:def 6;

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:52

.= ((Gauge (C,n)) * (1,1)) `1 by A12, JORDAN1A:73 ;

hence contradiction by A1, A12, A11, GOBOARD5:3; :: thesis: verum

end;then i2 = 1 by A13, A9, A5, A26, A27, Th37;

then (Upper_Seq (C,n)) /. 1 = (Gauge (C,n)) * (i,1) by A3, A4, PARTFUN1:def 6;

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:52

.= ((Gauge (C,n)) * (1,1)) `1 by A12, JORDAN1A:73 ;

hence contradiction by A1, A12, A11, GOBOARD5:3; :: thesis: verum

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

then
x = (Upper_Seq (C,n)) /. (len (Upper_Seq (C,n)))
by JORDAN1F:7;

then i2 = len (Upper_Seq (C,n)) by A13, A9, A5, A26, A27, Th38;

then (Upper_Seq (C,n)) /. (len (Upper_Seq (C,n))) = (Gauge (C,n)) * (i,1) by A3, A4, PARTFUN1:def 6;

then A29: 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:46;

then (SE-corner (L~ (Cage (C,n)))) `2 < (E-max (L~ (Cage (C,n)))) `2 by SPRECT_2:53, XXREAL_0:2;

then S-bound (L~ (Cage (C,n))) < ((Gauge (C,n)) * (i,1)) `2 by A29, EUCLID:52;

hence contradiction by A1, JORDAN1A:72; :: thesis: verum

end;then i2 = len (Upper_Seq (C,n)) by A13, A9, A5, A26, A27, Th38;

then (Upper_Seq (C,n)) /. (len (Upper_Seq (C,n))) = (Gauge (C,n)) * (i,1) by A3, A4, PARTFUN1:def 6;

then A29: 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:46;

then (SE-corner (L~ (Cage (C,n)))) `2 < (E-max (L~ (Cage (C,n)))) `2 by SPRECT_2:53, XXREAL_0:2;

then S-bound (L~ (Cage (C,n))) < ((Gauge (C,n)) * (i,1)) `2 by A29, EUCLID:52;

hence contradiction by A1, JORDAN1A:72; :: thesis: verum