let n be Nat; :: thesis: for C being non empty connected compact non horizontal non vertical Subset of (TOP-REAL 2) holds W-min C in right_cell ((Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))),1)

let C be non empty connected compact non horizontal non vertical Subset of (TOP-REAL 2); :: thesis: W-min C in right_cell ((Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))),1)

set f = Cage (C,n);

set G = Gauge (C,n);

consider j being Nat such that

A1: 1 <= j and

A2: j <= width (Gauge (C,n)) and

A3: W-min (L~ (Cage (C,n))) = (Gauge (C,n)) * (1,j) by JORDAN1D:30;

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

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

set k = (W-min (L~ (Cage (C,n)))) .. (Cage (C,n));

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

then A7: ( (W-min (L~ (Cage (C,n)))) .. (Cage (C,n)) in dom (Cage (C,n)) & (Cage (C,n)) . ((W-min (L~ (Cage (C,n)))) .. (Cage (C,n))) = W-min (L~ (Cage (C,n))) ) by FINSEQ_4:19, FINSEQ_4:20;

then A8: (Cage (C,n)) /. ((W-min (L~ (Cage (C,n)))) .. (Cage (C,n))) = W-min (L~ (Cage (C,n))) by PARTFUN1:def 6;

then A12: [1,j] in Indices (Gauge (C,n)) by A1, A2, MATRIX_0:30;

then A13: [1,j] in Indices (GoB (Cage (C,n))) by JORDAN1H:44;

(W-min (L~ (Cage (C,n)))) .. (Cage (C,n)) <= len (Cage (C,n)) by A6, FINSEQ_4:21;

then (W-min (L~ (Cage (C,n)))) .. (Cage (C,n)) < len (Cage (C,n)) by A9, XXREAL_0:1;

then A14: ((W-min (L~ (Cage (C,n)))) .. (Cage (C,n))) + 1 <= len (Cage (C,n)) by NAT_1:13;

(Cage (C,n)) /. ((W-min (L~ (Cage (C,n)))) .. (Cage (C,n))) = (Gauge (C,n)) * (1,j) by A3, A7, PARTFUN1:def 6;

then A15: (Cage (C,n)) /. ((W-min (L~ (Cage (C,n)))) .. (Cage (C,n))) = (GoB (Cage (C,n))) * (1,j) by JORDAN1H:44;

set p = W-min C;

A16: Cage (C,n) is_sequence_on Gauge (C,n) by JORDAN9:def 1;

A17: 1 <= ((W-min (L~ (Cage (C,n)))) .. (Cage (C,n))) + 1 by NAT_1:11;

then A18: ((W-min (L~ (Cage (C,n)))) .. (Cage (C,n))) + 1 in dom (Cage (C,n)) by A14, FINSEQ_3:25;

A19: ((W-min (L~ (Cage (C,n)))) .. (Cage (C,n))) + 1 in dom (Cage (C,n)) by A14, A17, FINSEQ_3:25;

then consider ki, kj being Nat such that

A20: [ki,kj] in Indices (Gauge (C,n)) and

A21: (Cage (C,n)) /. (((W-min (L~ (Cage (C,n)))) .. (Cage (C,n))) + 1) = (Gauge (C,n)) * (ki,kj) by A16, GOBOARD1:def 9;

A22: ( 1 <= kj & ki <= len (Gauge (C,n)) ) by A20, MATRIX_0:32;

A23: 1 <= (W-min (L~ (Cage (C,n)))) .. (Cage (C,n)) by Th1;

then A24: ((Cage (C,n)) /. (((W-min (L~ (Cage (C,n)))) .. (Cage (C,n))) + 1)) `1 = W-bound (L~ (Cage (C,n))) by A8, A14, JORDAN1E:22;

then ((Gauge (C,n)) * (1,j)) `1 = ((Gauge (C,n)) * (ki,kj)) `1 by A3, A21, EUCLID:52;

then A25: ki = 1 by A20, A12, JORDAN1G:7;

2 <= len (Cage (C,n)) by GOBOARD7:34, XXREAL_0:2;

then (Cage (C,n)) /. (((W-min (L~ (Cage (C,n)))) .. (Cage (C,n))) + 1) in W-most (L~ (Cage (C,n))) by A24, A19, GOBOARD1:1, SPRECT_2:12;

then ((Gauge (C,n)) * (1,j)) `2 <= ((Gauge (C,n)) * (ki,kj)) `2 by A3, A21, PSCOMP_1:31;

then A26: j <= kj by A2, A25, A22, GOBOARD5:4;

( [ki,kj] in Indices (GoB (Cage (C,n))) & (Cage (C,n)) /. (((W-min (L~ (Cage (C,n)))) .. (Cage (C,n))) + 1) = (GoB (Cage (C,n))) * (ki,kj) ) by A20, A21, JORDAN1H:44;

then |.(1 - ki).| + |.(j - kj).| = 1 by A6, A18, A13, A15, FINSEQ_4:20, GOBOARD5:12;

then A27: 0 + |.(j - kj).| = 1 by A25, ABSVALUE:2;

then A28: (Cage (C,n)) /. (((W-min (L~ (Cage (C,n)))) .. (Cage (C,n))) + 1) = (Gauge (C,n)) * (1,(j + 1)) by A21, A25, A26, SEQM_3:41;

A29: kj = j + 1 by A26, A27, SEQM_3:41;

then ( 1 <= j + 1 & j + 1 <= width (Gauge (C,n)) ) by A20, MATRIX_0:32;

then [1,(j + 1)] in Indices (Gauge (C,n)) by A5, MATRIX_0:30;

then A30: right_cell ((Cage (C,n)),((W-min (L~ (Cage (C,n)))) .. (Cage (C,n))),(Gauge (C,n))) = cell ((Gauge (C,n)),1,j) by A3, A16, A23, A8, A14, A12, A28, GOBRD13:22;

then W-min C in right_cell ((Cage (C,n)),((W-min (L~ (Cage (C,n)))) .. (Cage (C,n)))) by A23, A14, A31, JORDAN1H:23;

hence W-min C in right_cell ((Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))),1) by A6, Th5; :: thesis: verum

let C be non empty connected compact non horizontal non vertical Subset of (TOP-REAL 2); :: thesis: W-min C in right_cell ((Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))),1)

set f = Cage (C,n);

set G = Gauge (C,n);

consider j being Nat such that

A1: 1 <= j and

A2: j <= width (Gauge (C,n)) and

A3: W-min (L~ (Cage (C,n))) = (Gauge (C,n)) * (1,j) by JORDAN1D:30;

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

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

set k = (W-min (L~ (Cage (C,n)))) .. (Cage (C,n));

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

then A7: ( (W-min (L~ (Cage (C,n)))) .. (Cage (C,n)) in dom (Cage (C,n)) & (Cage (C,n)) . ((W-min (L~ (Cage (C,n)))) .. (Cage (C,n))) = W-min (L~ (Cage (C,n))) ) by FINSEQ_4:19, FINSEQ_4:20;

then A8: (Cage (C,n)) /. ((W-min (L~ (Cage (C,n)))) .. (Cage (C,n))) = W-min (L~ (Cage (C,n))) by PARTFUN1:def 6;

A9: now :: thesis: not (W-min (L~ (Cage (C,n)))) .. (Cage (C,n)) = len (Cage (C,n))

1 <= len (Gauge (C,n))
by A4, XXREAL_0:2;A10:
1 < (W-min (L~ (Cage (C,n)))) .. (Cage (C,n))
by Th1;

A11: 1 in dom (Cage (C,n)) by A6, FINSEQ_3:31;

assume (W-min (L~ (Cage (C,n)))) .. (Cage (C,n)) = len (Cage (C,n)) ; :: thesis: contradiction

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

then (Cage (C,n)) . 1 = W-min (L~ (Cage (C,n))) by A11, PARTFUN1:def 6;

hence contradiction by A11, A10, FINSEQ_4:24; :: thesis: verum

end;A11: 1 in dom (Cage (C,n)) by A6, FINSEQ_3:31;

assume (W-min (L~ (Cage (C,n)))) .. (Cage (C,n)) = len (Cage (C,n)) ; :: thesis: contradiction

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

then (Cage (C,n)) . 1 = W-min (L~ (Cage (C,n))) by A11, PARTFUN1:def 6;

hence contradiction by A11, A10, FINSEQ_4:24; :: thesis: verum

then A12: [1,j] in Indices (Gauge (C,n)) by A1, A2, MATRIX_0:30;

then A13: [1,j] in Indices (GoB (Cage (C,n))) by JORDAN1H:44;

(W-min (L~ (Cage (C,n)))) .. (Cage (C,n)) <= len (Cage (C,n)) by A6, FINSEQ_4:21;

then (W-min (L~ (Cage (C,n)))) .. (Cage (C,n)) < len (Cage (C,n)) by A9, XXREAL_0:1;

then A14: ((W-min (L~ (Cage (C,n)))) .. (Cage (C,n))) + 1 <= len (Cage (C,n)) by NAT_1:13;

(Cage (C,n)) /. ((W-min (L~ (Cage (C,n)))) .. (Cage (C,n))) = (Gauge (C,n)) * (1,j) by A3, A7, PARTFUN1:def 6;

then A15: (Cage (C,n)) /. ((W-min (L~ (Cage (C,n)))) .. (Cage (C,n))) = (GoB (Cage (C,n))) * (1,j) by JORDAN1H:44;

set p = W-min C;

A16: Cage (C,n) is_sequence_on Gauge (C,n) by JORDAN9:def 1;

A17: 1 <= ((W-min (L~ (Cage (C,n)))) .. (Cage (C,n))) + 1 by NAT_1:11;

then A18: ((W-min (L~ (Cage (C,n)))) .. (Cage (C,n))) + 1 in dom (Cage (C,n)) by A14, FINSEQ_3:25;

A19: ((W-min (L~ (Cage (C,n)))) .. (Cage (C,n))) + 1 in dom (Cage (C,n)) by A14, A17, FINSEQ_3:25;

then consider ki, kj being Nat such that

A20: [ki,kj] in Indices (Gauge (C,n)) and

A21: (Cage (C,n)) /. (((W-min (L~ (Cage (C,n)))) .. (Cage (C,n))) + 1) = (Gauge (C,n)) * (ki,kj) by A16, GOBOARD1:def 9;

A22: ( 1 <= kj & ki <= len (Gauge (C,n)) ) by A20, MATRIX_0:32;

A23: 1 <= (W-min (L~ (Cage (C,n)))) .. (Cage (C,n)) by Th1;

then A24: ((Cage (C,n)) /. (((W-min (L~ (Cage (C,n)))) .. (Cage (C,n))) + 1)) `1 = W-bound (L~ (Cage (C,n))) by A8, A14, JORDAN1E:22;

then ((Gauge (C,n)) * (1,j)) `1 = ((Gauge (C,n)) * (ki,kj)) `1 by A3, A21, EUCLID:52;

then A25: ki = 1 by A20, A12, JORDAN1G:7;

2 <= len (Cage (C,n)) by GOBOARD7:34, XXREAL_0:2;

then (Cage (C,n)) /. (((W-min (L~ (Cage (C,n)))) .. (Cage (C,n))) + 1) in W-most (L~ (Cage (C,n))) by A24, A19, GOBOARD1:1, SPRECT_2:12;

then ((Gauge (C,n)) * (1,j)) `2 <= ((Gauge (C,n)) * (ki,kj)) `2 by A3, A21, PSCOMP_1:31;

then A26: j <= kj by A2, A25, A22, GOBOARD5:4;

( [ki,kj] in Indices (GoB (Cage (C,n))) & (Cage (C,n)) /. (((W-min (L~ (Cage (C,n)))) .. (Cage (C,n))) + 1) = (GoB (Cage (C,n))) * (ki,kj) ) by A20, A21, JORDAN1H:44;

then |.(1 - ki).| + |.(j - kj).| = 1 by A6, A18, A13, A15, FINSEQ_4:20, GOBOARD5:12;

then A27: 0 + |.(j - kj).| = 1 by A25, ABSVALUE:2;

then A28: (Cage (C,n)) /. (((W-min (L~ (Cage (C,n)))) .. (Cage (C,n))) + 1) = (Gauge (C,n)) * (1,(j + 1)) by A21, A25, A26, SEQM_3:41;

A29: kj = j + 1 by A26, A27, SEQM_3:41;

then ( 1 <= j + 1 & j + 1 <= width (Gauge (C,n)) ) by A20, MATRIX_0:32;

then [1,(j + 1)] in Indices (Gauge (C,n)) by A5, MATRIX_0:30;

then A30: right_cell ((Cage (C,n)),((W-min (L~ (Cage (C,n)))) .. (Cage (C,n))),(Gauge (C,n))) = cell ((Gauge (C,n)),1,j) by A3, A16, A23, A8, A14, A12, A28, GOBRD13:22;

A31: now :: thesis: W-min C in right_cell ((Cage (C,n)),((W-min (L~ (Cage (C,n)))) .. (Cage (C,n))),(Gauge (C,n)))

GoB (Cage (C,n)) = Gauge (C,n)
by JORDAN1H:44;
len (Gauge (C,n)) = width (Gauge (C,n))
by JORDAN8:def 1;

then A32: j + 1 <= len (Gauge (C,n)) by A20, A29, MATRIX_0:32;

1 <= j + 1 by A20, A29, MATRIX_0:32;

then A33: ((Gauge (C,n)) * (2,(j + 1))) `1 = W-bound C by A32, JORDAN8:11;

assume A34: not W-min C in right_cell ((Cage (C,n)),((W-min (L~ (Cage (C,n)))) .. (Cage (C,n))),(Gauge (C,n))) ; :: thesis: contradiction

j + 1 <= width (Gauge (C,n)) by A20, A29, MATRIX_0:32;

then A35: j < width (Gauge (C,n)) by NAT_1:13;

A36: 2 <= len (Gauge (C,n)) by A4, XXREAL_0:2;

1 < len (Gauge (C,n)) by A4, XXREAL_0:2;

then LSeg (((Gauge (C,n)) * ((1 + 1),j)),((Gauge (C,n)) * ((1 + 1),(j + 1)))) c= cell ((Gauge (C,n)),1,j) by A1, A35, GOBOARD5:18;

then A37: not W-min C in LSeg (((Gauge (C,n)) * (2,j)),((Gauge (C,n)) * (2,(j + 1)))) by A30, A34;

A38: ( 1 <= j + 1 & j + 1 <= width (Gauge (C,n)) ) by A20, A29, MATRIX_0:32;

j <= len (Gauge (C,n)) by A2, JORDAN8:def 1;

then A39: ((Gauge (C,n)) * (2,j)) `1 = W-bound C by A1, JORDAN8:11;

(W-min C) `1 = W-bound C by EUCLID:52;

then A40: ( (W-min C) `2 > ((Gauge (C,n)) * (2,(j + 1))) `2 or (W-min C) `2 < ((Gauge (C,n)) * (2,j)) `2 ) by A37, A39, A33, GOBOARD7:7;

end;then A32: j + 1 <= len (Gauge (C,n)) by A20, A29, MATRIX_0:32;

1 <= j + 1 by A20, A29, MATRIX_0:32;

then A33: ((Gauge (C,n)) * (2,(j + 1))) `1 = W-bound C by A32, JORDAN8:11;

assume A34: not W-min C in right_cell ((Cage (C,n)),((W-min (L~ (Cage (C,n)))) .. (Cage (C,n))),(Gauge (C,n))) ; :: thesis: contradiction

j + 1 <= width (Gauge (C,n)) by A20, A29, MATRIX_0:32;

then A35: j < width (Gauge (C,n)) by NAT_1:13;

A36: 2 <= len (Gauge (C,n)) by A4, XXREAL_0:2;

1 < len (Gauge (C,n)) by A4, XXREAL_0:2;

then LSeg (((Gauge (C,n)) * ((1 + 1),j)),((Gauge (C,n)) * ((1 + 1),(j + 1)))) c= cell ((Gauge (C,n)),1,j) by A1, A35, GOBOARD5:18;

then A37: not W-min C in LSeg (((Gauge (C,n)) * (2,j)),((Gauge (C,n)) * (2,(j + 1)))) by A30, A34;

A38: ( 1 <= j + 1 & j + 1 <= width (Gauge (C,n)) ) by A20, A29, MATRIX_0:32;

j <= len (Gauge (C,n)) by A2, JORDAN8:def 1;

then A39: ((Gauge (C,n)) * (2,j)) `1 = W-bound C by A1, JORDAN8:11;

(W-min C) `1 = W-bound C by EUCLID:52;

then A40: ( (W-min C) `2 > ((Gauge (C,n)) * (2,(j + 1))) `2 or (W-min C) `2 < ((Gauge (C,n)) * (2,j)) `2 ) by A37, A39, A33, GOBOARD7:7;

per cases
( (W-min C) `2 > ((Gauge (C,n)) * (1,(j + 1))) `2 or (W-min C) `2 < ((Gauge (C,n)) * (1,j)) `2 )
by A1, A2, A40, A38, A36, GOBOARD5:1;

end;

suppose A41:
(W-min C) `2 > ((Gauge (C,n)) * (1,(j + 1))) `2
; :: thesis: contradiction

cell ((Gauge (C,n)),1,j) meets C
by A23, A14, A30, JORDAN9:31;

then (cell ((Gauge (C,n)),1,j)) /\ C <> {} by XBOOLE_0:def 7;

then consider c being object such that

A42: c in (cell ((Gauge (C,n)),1,j)) /\ C by XBOOLE_0:def 1;

reconsider c = c as Element of (TOP-REAL 2) by A42;

A43: c in cell ((Gauge (C,n)),1,j) by A42, XBOOLE_0:def 4;

A44: c in C by A42, XBOOLE_0:def 4;

then A45: c `1 >= W-bound C by PSCOMP_1:24;

A46: ( 1 + 1 <= len (Gauge (C,n)) & j + 1 <= width (Gauge (C,n)) ) by A4, A20, A29, MATRIX_0:32, XXREAL_0:2;

then c `1 <= ((Gauge (C,n)) * ((1 + 1),j)) `1 by A1, A43, JORDAN9:17;

then c in W-most C by A39, A44, A45, SPRECT_2:12, XXREAL_0:1;

then A47: c `2 >= (W-min C) `2 by PSCOMP_1:31;

c `2 <= ((Gauge (C,n)) * (1,(j + 1))) `2 by A1, A43, A46, JORDAN9:17;

hence contradiction by A41, A47, XXREAL_0:2; :: thesis: verum

end;then (cell ((Gauge (C,n)),1,j)) /\ C <> {} by XBOOLE_0:def 7;

then consider c being object such that

A42: c in (cell ((Gauge (C,n)),1,j)) /\ C by XBOOLE_0:def 1;

reconsider c = c as Element of (TOP-REAL 2) by A42;

A43: c in cell ((Gauge (C,n)),1,j) by A42, XBOOLE_0:def 4;

A44: c in C by A42, XBOOLE_0:def 4;

then A45: c `1 >= W-bound C by PSCOMP_1:24;

A46: ( 1 + 1 <= len (Gauge (C,n)) & j + 1 <= width (Gauge (C,n)) ) by A4, A20, A29, MATRIX_0:32, XXREAL_0:2;

then c `1 <= ((Gauge (C,n)) * ((1 + 1),j)) `1 by A1, A43, JORDAN9:17;

then c in W-most C by A39, A44, A45, SPRECT_2:12, XXREAL_0:1;

then A47: c `2 >= (W-min C) `2 by PSCOMP_1:31;

c `2 <= ((Gauge (C,n)) * (1,(j + 1))) `2 by A1, A43, A46, JORDAN9:17;

hence contradiction by A41, A47, XXREAL_0:2; :: thesis: verum

suppose A48:
(W-min C) `2 < ((Gauge (C,n)) * (1,j)) `2
; :: thesis: contradiction

west_halfline (W-min C) meets L~ (Cage (C,n))
by JORDAN1A:54, SPRECT_1:13;

then consider r being object such that

A49: r in west_halfline (W-min C) and

A50: r in L~ (Cage (C,n)) by XBOOLE_0:3;

reconsider r = r as Element of (TOP-REAL 2) by A49;

r in (west_halfline (W-min C)) /\ (L~ (Cage (C,n))) by A49, A50, XBOOLE_0:def 4;

then r `1 = W-bound (L~ (Cage (C,n))) by JORDAN1A:85, PSCOMP_1:34;

then r in W-most (L~ (Cage (C,n))) by A50, SPRECT_2:12;

then (W-min (L~ (Cage (C,n)))) `2 <= r `2 by PSCOMP_1:31;

hence contradiction by A3, A48, A49, TOPREAL1:def 13; :: thesis: verum

end;then consider r being object such that

A49: r in west_halfline (W-min C) and

A50: r in L~ (Cage (C,n)) by XBOOLE_0:3;

reconsider r = r as Element of (TOP-REAL 2) by A49;

r in (west_halfline (W-min C)) /\ (L~ (Cage (C,n))) by A49, A50, XBOOLE_0:def 4;

then r `1 = W-bound (L~ (Cage (C,n))) by JORDAN1A:85, PSCOMP_1:34;

then r in W-most (L~ (Cage (C,n))) by A50, SPRECT_2:12;

then (W-min (L~ (Cage (C,n)))) `2 <= r `2 by PSCOMP_1:31;

hence contradiction by A3, A48, A49, TOPREAL1:def 13; :: thesis: verum

then W-min C in right_cell ((Cage (C,n)),((W-min (L~ (Cage (C,n)))) .. (Cage (C,n)))) by A23, A14, A31, JORDAN1H:23;

hence W-min C in right_cell ((Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))),1) by A6, Th5; :: thesis: verum