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,(width (Gauge (C,n)))) in rng (Lower_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,(width (Gauge (C,n)))) in rng (Lower_Seq (C,n))

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

set wi = width (Gauge (C,n));

assume that

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

A2: (Gauge (C,n)) * (i,(width (Gauge (C,n)))) in rng (Lower_Seq (C,n)) ; :: thesis: contradiction

consider i2 being Nat such that

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

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

reconsider i2 = i2 as Nat ;

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

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

then A6: 2 <= len (Upper_Seq (C,n)) by XXREAL_0:2;

set f = Rotate ((Cage (C,n)),(E-max (L~ (Cage (C,n)))));

set i1 = (S-max (L~ (Cage (C,n)))) .. (Lower_Seq (C,n));

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

E-max (L~ (Cage (C,n))) in rng (Cage (C,n)) by SPRECT_2:46;

then A8: (Rotate ((Cage (C,n)),(E-max (L~ (Cage (C,n)))))) /. 1 = E-max (L~ (Cage (C,n))) by FINSEQ_6:92;

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

then A9: ( (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)))))) & (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 A8, SPRECT_5:40, SPRECT_5:41;

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

(W-min (L~ (Cage (C,n)))) .. (Lower_Seq (C,n)) = len (Lower_Seq (C,n)) by Th30;

then (S-min (L~ (Cage (C,n)))) .. (Lower_Seq (C,n)) <= len (Lower_Seq (C,n)) by Th29;

then A11: (S-max (L~ (Cage (C,n)))) .. (Lower_Seq (C,n)) < len (Lower_Seq (C,n)) by Th28, XXREAL_0:2;

( (E-max (L~ (Cage (C,n)))) .. (Lower_Seq (C,n)) = 1 & (E-min (L~ (Cage (C,n)))) .. (Lower_Seq (C,n)) <= (S-max (L~ (Cage (C,n)))) .. (Lower_Seq (C,n)) ) by Th25, Th27;

then A12: (S-max (L~ (Cage (C,n)))) .. (Lower_Seq (C,n)) > 1 by Th26, XXREAL_0:2;

then A13: (S-max (L~ (Cage (C,n)))) .. (Lower_Seq (C,n)) in dom (Lower_Seq (C,n)) by A11, FINSEQ_3:25;

( Lower_Seq (C,n) = (Rotate ((Cage (C,n)),(E-max (L~ (Cage (C,n)))))) -: (W-min (L~ (Cage (C,n)))) & S-max (L~ (Cage (C,n))) in rng (Cage (C,n)) ) by Th18, SPRECT_2:42;

then A14: S-max (L~ (Cage (C,n))) in rng (Lower_Seq (C,n)) by A10, A9, FINSEQ_5:46, XXREAL_0:2;

then A15: (Lower_Seq (C,n)) /. ((S-max (L~ (Cage (C,n)))) .. (Lower_Seq (C,n))) = S-max (L~ (Cage (C,n))) by FINSEQ_5:38;

A16: ( (S-max (L~ (Cage (C,n)))) .. (Lower_Seq (C,n)) in NAT & i2 in NAT ) by ORDINAL1:def 12;

A17: (S-max (L~ (Cage (C,n)))) .. (Lower_Seq (C,n)) <> i2

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) ;

A18: (h /. 1) `2 = ((Lower_Seq (C,n)) /. ((S-max (L~ (Cage (C,n)))) .. (Lower_Seq (C,n)))) `2 by A3, A13, SPRECT_2:8

.= (S-max (L~ (Cage (C,n)))) `2 by A14, FINSEQ_5:38

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

len h >= 1 by A3, A13, SPRECT_2:5;

then len h > 1 by A3, A13, A17, SPRECT_2:6, XXREAL_0:1;

then A19: 1 + 1 <= len h by NAT_1:13;

A20: h is_in_the_area_of Cage (C,n) by A3, A13, JORDAN1E:18, SPRECT_2:22;

(h /. (len h)) `2 = ((Lower_Seq (C,n)) /. i2) `2 by A3, A13, SPRECT_2:9

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

.= N-bound (L~ (Cage (C,n))) by A1, A7, JORDAN1A:70 ;

then h is_a_v.c._for Cage (C,n) by A20, A18, SPRECT_2:def 3;

then L~ (Upper_Seq (C,n)) meets L~ h by A6, A19, Th40, SPRECT_2:29;

then consider x being object such that

A21: x in L~ (Upper_Seq (C,n)) and

A22: 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 A12, A11, A5, JORDAN4:35;

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

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

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

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

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

not (Gauge (C,n)) * (i,(width (Gauge (C,n)))) in rng (Lower_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,(width (Gauge (C,n)))) in rng (Lower_Seq (C,n))

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

set wi = width (Gauge (C,n));

assume that

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

A2: (Gauge (C,n)) * (i,(width (Gauge (C,n)))) in rng (Lower_Seq (C,n)) ; :: thesis: contradiction

consider i2 being Nat such that

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

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

reconsider i2 = i2 as Nat ;

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

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

then A6: 2 <= len (Upper_Seq (C,n)) by XXREAL_0:2;

set f = Rotate ((Cage (C,n)),(E-max (L~ (Cage (C,n)))));

set i1 = (S-max (L~ (Cage (C,n)))) .. (Lower_Seq (C,n));

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

E-max (L~ (Cage (C,n))) in rng (Cage (C,n)) by SPRECT_2:46;

then A8: (Rotate ((Cage (C,n)),(E-max (L~ (Cage (C,n)))))) /. 1 = E-max (L~ (Cage (C,n))) by FINSEQ_6:92;

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

then A9: ( (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)))))) & (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 A8, SPRECT_5:40, SPRECT_5:41;

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

(W-min (L~ (Cage (C,n)))) .. (Lower_Seq (C,n)) = len (Lower_Seq (C,n)) by Th30;

then (S-min (L~ (Cage (C,n)))) .. (Lower_Seq (C,n)) <= len (Lower_Seq (C,n)) by Th29;

then A11: (S-max (L~ (Cage (C,n)))) .. (Lower_Seq (C,n)) < len (Lower_Seq (C,n)) by Th28, XXREAL_0:2;

( (E-max (L~ (Cage (C,n)))) .. (Lower_Seq (C,n)) = 1 & (E-min (L~ (Cage (C,n)))) .. (Lower_Seq (C,n)) <= (S-max (L~ (Cage (C,n)))) .. (Lower_Seq (C,n)) ) by Th25, Th27;

then A12: (S-max (L~ (Cage (C,n)))) .. (Lower_Seq (C,n)) > 1 by Th26, XXREAL_0:2;

then A13: (S-max (L~ (Cage (C,n)))) .. (Lower_Seq (C,n)) in dom (Lower_Seq (C,n)) by A11, FINSEQ_3:25;

( Lower_Seq (C,n) = (Rotate ((Cage (C,n)),(E-max (L~ (Cage (C,n)))))) -: (W-min (L~ (Cage (C,n)))) & S-max (L~ (Cage (C,n))) in rng (Cage (C,n)) ) by Th18, SPRECT_2:42;

then A14: S-max (L~ (Cage (C,n))) in rng (Lower_Seq (C,n)) by A10, A9, FINSEQ_5:46, XXREAL_0:2;

then A15: (Lower_Seq (C,n)) /. ((S-max (L~ (Cage (C,n)))) .. (Lower_Seq (C,n))) = S-max (L~ (Cage (C,n))) by FINSEQ_5:38;

A16: ( (S-max (L~ (Cage (C,n)))) .. (Lower_Seq (C,n)) in NAT & i2 in NAT ) by ORDINAL1:def 12;

A17: (S-max (L~ (Cage (C,n)))) .. (Lower_Seq (C,n)) <> i2

proof

then
mid ((Lower_Seq (C,n)),((S-max (L~ (Cage (C,n)))) .. (Lower_Seq (C,n))),i2) is being_S-Seq
by A12, A11, A5, JORDAN3:6, A16;
assume
(S-max (L~ (Cage (C,n)))) .. (Lower_Seq (C,n)) = i2
; :: thesis: contradiction

then (Gauge (C,n)) * (i,(width (Gauge (C,n)))) = S-max (L~ (Cage (C,n))) by A4, A13, A15, PARTFUN1:def 6;

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

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

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

end;then (Gauge (C,n)) * (i,(width (Gauge (C,n)))) = S-max (L~ (Cage (C,n))) by A4, A13, A15, PARTFUN1:def 6;

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

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

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

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) ;

A18: (h /. 1) `2 = ((Lower_Seq (C,n)) /. ((S-max (L~ (Cage (C,n)))) .. (Lower_Seq (C,n)))) `2 by A3, A13, SPRECT_2:8

.= (S-max (L~ (Cage (C,n)))) `2 by A14, FINSEQ_5:38

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

len h >= 1 by A3, A13, SPRECT_2:5;

then len h > 1 by A3, A13, A17, SPRECT_2:6, XXREAL_0:1;

then A19: 1 + 1 <= len h by NAT_1:13;

A20: h is_in_the_area_of Cage (C,n) by A3, A13, JORDAN1E:18, SPRECT_2:22;

(h /. (len h)) `2 = ((Lower_Seq (C,n)) /. i2) `2 by A3, A13, SPRECT_2:9

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

.= N-bound (L~ (Cage (C,n))) by A1, A7, JORDAN1A:70 ;

then h is_a_v.c._for Cage (C,n) by A20, A18, SPRECT_2:def 3;

then L~ (Upper_Seq (C,n)) meets L~ h by A6, A19, Th40, SPRECT_2:29;

then consider x being object such that

A21: x in L~ (Upper_Seq (C,n)) and

A22: 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 A12, A11, A5, JORDAN4:35;

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

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

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

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

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

end;

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

then
x = (Lower_Seq (C,n)) /. 1
by JORDAN1F:6;

then i2 = 1 by A12, A11, A5, A22, Th37;

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

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

.= ((Gauge (C,n)) * ((len (Gauge (C,n))),(width (Gauge (C,n))))) `1 by A7, A24, JORDAN1A:71 ;

hence contradiction by A1, A7, A24, GOBOARD5:3; :: thesis: verum

end;then i2 = 1 by A12, A11, A5, A22, Th37;

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

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

.= ((Gauge (C,n)) * ((len (Gauge (C,n))),(width (Gauge (C,n))))) `1 by A7, A24, JORDAN1A:71 ;

hence contradiction by A1, A7, A24, GOBOARD5:3; :: thesis: verum

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

then
x = (Lower_Seq (C,n)) /. (len (Lower_Seq (C,n)))
by JORDAN1F:8;

then i2 = len (Lower_Seq (C,n)) by A12, A11, A5, A22, Th38;

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

then A25: 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:30;

then (NW-corner (L~ (Cage (C,n)))) `2 > (W-min (L~ (Cage (C,n)))) `2 by SPRECT_2:57, XXREAL_0:2;

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

hence contradiction by A1, A7, JORDAN1A:70; :: thesis: verum

end;then i2 = len (Lower_Seq (C,n)) by A12, A11, A5, A22, Th38;

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

then A25: 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:30;

then (NW-corner (L~ (Cage (C,n)))) `2 > (W-min (L~ (Cage (C,n)))) `2 by SPRECT_2:57, XXREAL_0:2;

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

hence contradiction by A1, A7, JORDAN1A:70; :: thesis: verum