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

let C be non empty connected compact non horizontal non vertical Subset of (TOP-REAL 2); :: thesis: S-max C in right_cell ((Rotate ((Cage (C,n)),(S-max (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 <= len (Gauge (C,n)) and

A3: S-max (L~ (Cage (C,n))) = (Gauge (C,n)) * (j,1) by JORDAN1D:28;

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

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

A5: S-max (L~ (Cage (C,n))) in rng (Cage (C,n)) by SPRECT_2:42;

then A6: ( (S-max (L~ (Cage (C,n)))) .. (Cage (C,n)) in dom (Cage (C,n)) & (Cage (C,n)) . ((S-max (L~ (Cage (C,n)))) .. (Cage (C,n))) = S-max (L~ (Cage (C,n))) ) by FINSEQ_4:19, FINSEQ_4:20;

then A7: (Cage (C,n)) /. ((S-max (L~ (Cage (C,n)))) .. (Cage (C,n))) = S-max (L~ (Cage (C,n))) by PARTFUN1:def 6;

then (S-max (L~ (Cage (C,n)))) .. (Cage (C,n)) < len (Cage (C,n)) by A8, XXREAL_0:1;

then A11: ((S-max (L~ (Cage (C,n)))) .. (Cage (C,n))) + 1 <= len (Cage (C,n)) by NAT_1:13;

A12: (Cage (C,n)) /. ((S-max (L~ (Cage (C,n)))) .. (Cage (C,n))) = (Gauge (C,n)) * (((j -' 1) + 1),1) by A1, A3, A7, XREAL_1:235;

(Cage (C,n)) /. ((S-max (L~ (Cage (C,n)))) .. (Cage (C,n))) = (Gauge (C,n)) * (j,1) by A3, A6, PARTFUN1:def 6;

then A13: (Cage (C,n)) /. ((S-max (L~ (Cage (C,n)))) .. (Cage (C,n))) = (GoB (Cage (C,n))) * (j,1) by JORDAN1H:44;

set p = S-max C;

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

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

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

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

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

A19: ((S-max (L~ (Cage (C,n)))) .. (Cage (C,n))) + 1 in dom (Cage (C,n)) by A11, A17, FINSEQ_3:25;

then consider kj, ki being Nat such that

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

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

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

A23: ki <= width (Gauge (C,n)) by A20, MATRIX_0:32;

A24: 1 <= kj by A20, MATRIX_0:32;

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

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

then A26: [((j -' 1) + 1),1] in Indices (Gauge (C,n)) by A1, XREAL_1:235;

A27: 1 <= (S-max (L~ (Cage (C,n)))) .. (Cage (C,n)) by Th3;

then A28: ((Cage (C,n)) /. (((S-max (L~ (Cage (C,n)))) .. (Cage (C,n))) + 1)) `2 = S-bound (L~ (Cage (C,n))) by A7, A11, JORDAN1E:21;

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

then A29: ki = 1 by A20, A25, JORDAN1G:6;

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

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

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

A31: kj <= len (Gauge (C,n)) by A20, MATRIX_0:32;

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

then (Cage (C,n)) /. (((S-max (L~ (Cage (C,n)))) .. (Cage (C,n))) + 1) in S-most (L~ (Cage (C,n))) by A28, A19, GOBOARD1:1, SPRECT_2:11;

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

then kj <= j by A1, A29, A23, A31, GOBOARD5:3;

then kj + 1 = j by A30, SEQM_3:41;

then A32: kj = j - 1 ;

then kj = j -' 1 by A24, NAT_D:39;

then A33: [(j -' 1),1] in Indices (Gauge (C,n)) by A16, A24, A31, A14, MATRIX_0:30;

(Cage (C,n)) /. (((S-max (L~ (Cage (C,n)))) .. (Cage (C,n))) + 1) = (Gauge (C,n)) * ((j -' 1),1) by A21, A29, A24, A32, NAT_D:39;

then A34: right_cell ((Cage (C,n)),((S-max (L~ (Cage (C,n)))) .. (Cage (C,n))),(Gauge (C,n))) = cell ((Gauge (C,n)),(j -' 1),1) by A4, A27, A11, A33, A26, A12, GOBRD13:26;

then S-max C in right_cell ((Cage (C,n)),((S-max (L~ (Cage (C,n)))) .. (Cage (C,n)))) by A27, A11, A35, JORDAN1H:23;

hence S-max C in right_cell ((Rotate ((Cage (C,n)),(S-max (L~ (Cage (C,n)))))),1) by A5, Th5; :: thesis: verum

let C be non empty connected compact non horizontal non vertical Subset of (TOP-REAL 2); :: thesis: S-max C in right_cell ((Rotate ((Cage (C,n)),(S-max (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 <= len (Gauge (C,n)) and

A3: S-max (L~ (Cage (C,n))) = (Gauge (C,n)) * (j,1) by JORDAN1D:28;

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

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

A5: S-max (L~ (Cage (C,n))) in rng (Cage (C,n)) by SPRECT_2:42;

then A6: ( (S-max (L~ (Cage (C,n)))) .. (Cage (C,n)) in dom (Cage (C,n)) & (Cage (C,n)) . ((S-max (L~ (Cage (C,n)))) .. (Cage (C,n))) = S-max (L~ (Cage (C,n))) ) by FINSEQ_4:19, FINSEQ_4:20;

then A7: (Cage (C,n)) /. ((S-max (L~ (Cage (C,n)))) .. (Cage (C,n))) = S-max (L~ (Cage (C,n))) by PARTFUN1:def 6;

A8: now :: thesis: not (S-max (L~ (Cage (C,n)))) .. (Cage (C,n)) = len (Cage (C,n))

(S-max (L~ (Cage (C,n)))) .. (Cage (C,n)) <= len (Cage (C,n))
by A5, FINSEQ_4:21;A9:
1 < (S-max (L~ (Cage (C,n)))) .. (Cage (C,n))
by Th3;

A10: 1 in dom (Cage (C,n)) by A5, FINSEQ_3:31;

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

then (Cage (C,n)) /. 1 = S-max (L~ (Cage (C,n))) by A7, FINSEQ_6:def 1;

then (Cage (C,n)) . 1 = S-max (L~ (Cage (C,n))) by A10, PARTFUN1:def 6;

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

end;A10: 1 in dom (Cage (C,n)) by A5, FINSEQ_3:31;

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

then (Cage (C,n)) /. 1 = S-max (L~ (Cage (C,n))) by A7, FINSEQ_6:def 1;

then (Cage (C,n)) . 1 = S-max (L~ (Cage (C,n))) by A10, PARTFUN1:def 6;

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

then (S-max (L~ (Cage (C,n)))) .. (Cage (C,n)) < len (Cage (C,n)) by A8, XXREAL_0:1;

then A11: ((S-max (L~ (Cage (C,n)))) .. (Cage (C,n))) + 1 <= len (Cage (C,n)) by NAT_1:13;

A12: (Cage (C,n)) /. ((S-max (L~ (Cage (C,n)))) .. (Cage (C,n))) = (Gauge (C,n)) * (((j -' 1) + 1),1) by A1, A3, A7, XREAL_1:235;

(Cage (C,n)) /. ((S-max (L~ (Cage (C,n)))) .. (Cage (C,n))) = (Gauge (C,n)) * (j,1) by A3, A6, PARTFUN1:def 6;

then A13: (Cage (C,n)) /. ((S-max (L~ (Cage (C,n)))) .. (Cage (C,n))) = (GoB (Cage (C,n))) * (j,1) by JORDAN1H:44;

set p = S-max C;

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

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

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

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

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

A19: ((S-max (L~ (Cage (C,n)))) .. (Cage (C,n))) + 1 in dom (Cage (C,n)) by A11, A17, FINSEQ_3:25;

then consider kj, ki being Nat such that

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

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

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

A23: ki <= width (Gauge (C,n)) by A20, MATRIX_0:32;

A24: 1 <= kj by A20, MATRIX_0:32;

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

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

then A26: [((j -' 1) + 1),1] in Indices (Gauge (C,n)) by A1, XREAL_1:235;

A27: 1 <= (S-max (L~ (Cage (C,n)))) .. (Cage (C,n)) by Th3;

then A28: ((Cage (C,n)) /. (((S-max (L~ (Cage (C,n)))) .. (Cage (C,n))) + 1)) `2 = S-bound (L~ (Cage (C,n))) by A7, A11, JORDAN1E:21;

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

then A29: ki = 1 by A20, A25, JORDAN1G:6;

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

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

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

A31: kj <= len (Gauge (C,n)) by A20, MATRIX_0:32;

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

then (Cage (C,n)) /. (((S-max (L~ (Cage (C,n)))) .. (Cage (C,n))) + 1) in S-most (L~ (Cage (C,n))) by A28, A19, GOBOARD1:1, SPRECT_2:11;

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

then kj <= j by A1, A29, A23, A31, GOBOARD5:3;

then kj + 1 = j by A30, SEQM_3:41;

then A32: kj = j - 1 ;

then kj = j -' 1 by A24, NAT_D:39;

then A33: [(j -' 1),1] in Indices (Gauge (C,n)) by A16, A24, A31, A14, MATRIX_0:30;

(Cage (C,n)) /. (((S-max (L~ (Cage (C,n)))) .. (Cage (C,n))) + 1) = (Gauge (C,n)) * ((j -' 1),1) by A21, A29, A24, A32, NAT_D:39;

then A34: right_cell ((Cage (C,n)),((S-max (L~ (Cage (C,n)))) .. (Cage (C,n))),(Gauge (C,n))) = cell ((Gauge (C,n)),(j -' 1),1) by A4, A27, A11, A33, A26, A12, GOBRD13:26;

A35: now :: thesis: S-max C in right_cell ((Cage (C,n)),((S-max (L~ (Cage (C,n)))) .. (Cage (C,n))),(Gauge (C,n)))

GoB (Cage (C,n)) = Gauge (C,n)
by JORDAN1H:44;
1 < len (Gauge (C,n))
by A15, XXREAL_0:2;

then A36: 1 < width (Gauge (C,n)) by JORDAN8:def 1;

assume A37: not S-max C in right_cell ((Cage (C,n)),((S-max (L~ (Cage (C,n)))) .. (Cage (C,n))),(Gauge (C,n))) ; :: thesis: contradiction

A38: 1 <= j -' 1 by A24, A32, NAT_D:39;

then j -' 1 < j by NAT_D:51;

then j -' 1 < len (Gauge (C,n)) by A2, XXREAL_0:2;

then LSeg (((Gauge (C,n)) * ((j -' 1),(1 + 1))),((Gauge (C,n)) * (((j -' 1) + 1),(1 + 1)))) c= cell ((Gauge (C,n)),(j -' 1),1) by A36, A38, GOBOARD5:21;

then LSeg (((Gauge (C,n)) * ((j -' 1),2)),((Gauge (C,n)) * (j,2))) c= cell ((Gauge (C,n)),(j -' 1),1) by A1, XREAL_1:235;

then A39: not S-max C in LSeg (((Gauge (C,n)) * ((j -' 1),2)),((Gauge (C,n)) * (j,2))) by A34, A37;

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

then A40: 2 <= width (Gauge (C,n)) by A15, XXREAL_0:2;

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

A42: j -' 1 <= len (Gauge (C,n)) by A24, A31, A32, NAT_D:39;

then A43: ((Gauge (C,n)) * ((j -' 1),2)) `2 = S-bound C by A38, JORDAN8:13;

( ((Gauge (C,n)) * (j,2)) `2 = S-bound C & (S-max C) `2 = S-bound C ) by A1, A2, EUCLID:52, JORDAN8:13;

then A44: ( (S-max C) `1 > ((Gauge (C,n)) * (j,2)) `1 or (S-max C) `1 < ((Gauge (C,n)) * ((j -' 1),2)) `1 ) by A39, A43, GOBOARD7:8;

end;then A36: 1 < width (Gauge (C,n)) by JORDAN8:def 1;

assume A37: not S-max C in right_cell ((Cage (C,n)),((S-max (L~ (Cage (C,n)))) .. (Cage (C,n))),(Gauge (C,n))) ; :: thesis: contradiction

A38: 1 <= j -' 1 by A24, A32, NAT_D:39;

then j -' 1 < j by NAT_D:51;

then j -' 1 < len (Gauge (C,n)) by A2, XXREAL_0:2;

then LSeg (((Gauge (C,n)) * ((j -' 1),(1 + 1))),((Gauge (C,n)) * (((j -' 1) + 1),(1 + 1)))) c= cell ((Gauge (C,n)),(j -' 1),1) by A36, A38, GOBOARD5:21;

then LSeg (((Gauge (C,n)) * ((j -' 1),2)),((Gauge (C,n)) * (j,2))) c= cell ((Gauge (C,n)),(j -' 1),1) by A1, XREAL_1:235;

then A39: not S-max C in LSeg (((Gauge (C,n)) * ((j -' 1),2)),((Gauge (C,n)) * (j,2))) by A34, A37;

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

then A40: 2 <= width (Gauge (C,n)) by A15, XXREAL_0:2;

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

A42: j -' 1 <= len (Gauge (C,n)) by A24, A31, A32, NAT_D:39;

then A43: ((Gauge (C,n)) * ((j -' 1),2)) `2 = S-bound C by A38, JORDAN8:13;

( ((Gauge (C,n)) * (j,2)) `2 = S-bound C & (S-max C) `2 = S-bound C ) by A1, A2, EUCLID:52, JORDAN8:13;

then A44: ( (S-max C) `1 > ((Gauge (C,n)) * (j,2)) `1 or (S-max C) `1 < ((Gauge (C,n)) * ((j -' 1),2)) `1 ) by A39, A43, GOBOARD7:8;

per cases
( (S-max C) `1 < ((Gauge (C,n)) * ((j -' 1),1)) `1 or (S-max C) `1 > ((Gauge (C,n)) * (j,1)) `1 )
by A1, A2, A38, A42, A44, A40, GOBOARD5:2;

end;

suppose A45:
(S-max C) `1 < ((Gauge (C,n)) * ((j -' 1),1)) `1
; :: thesis: contradiction

cell ((Gauge (C,n)),(j -' 1),1) meets C
by A27, A11, A34, JORDAN9:31;

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

then consider c being object such that

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

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

A47: c in cell ((Gauge (C,n)),(j -' 1),1) by A46, XBOOLE_0:def 4;

A48: c in C by A46, XBOOLE_0:def 4;

then A49: c `2 >= S-bound C by PSCOMP_1:24;

A50: ( (j -' 1) + 1 <= len (Gauge (C,n)) & 1 + 1 <= width (Gauge (C,n)) ) by A1, A2, A15, A41, XREAL_1:235, XXREAL_0:2;

then c `2 <= ((Gauge (C,n)) * ((j -' 1),(1 + 1))) `2 by A38, A47, JORDAN9:17;

then c in S-most C by A43, A48, A49, SPRECT_2:11, XXREAL_0:1;

then A51: c `1 <= (S-max C) `1 by PSCOMP_1:55;

((Gauge (C,n)) * ((j -' 1),1)) `1 <= c `1 by A38, A47, A50, JORDAN9:17;

hence contradiction by A45, A51, XXREAL_0:2; :: thesis: verum

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

then consider c being object such that

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

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

A47: c in cell ((Gauge (C,n)),(j -' 1),1) by A46, XBOOLE_0:def 4;

A48: c in C by A46, XBOOLE_0:def 4;

then A49: c `2 >= S-bound C by PSCOMP_1:24;

A50: ( (j -' 1) + 1 <= len (Gauge (C,n)) & 1 + 1 <= width (Gauge (C,n)) ) by A1, A2, A15, A41, XREAL_1:235, XXREAL_0:2;

then c `2 <= ((Gauge (C,n)) * ((j -' 1),(1 + 1))) `2 by A38, A47, JORDAN9:17;

then c in S-most C by A43, A48, A49, SPRECT_2:11, XXREAL_0:1;

then A51: c `1 <= (S-max C) `1 by PSCOMP_1:55;

((Gauge (C,n)) * ((j -' 1),1)) `1 <= c `1 by A38, A47, A50, JORDAN9:17;

hence contradiction by A45, A51, XXREAL_0:2; :: thesis: verum

suppose A52:
(S-max C) `1 > ((Gauge (C,n)) * (j,1)) `1
; :: thesis: contradiction

south_halfline (S-max C) meets L~ (Cage (C,n))
by JORDAN1A:53, SPRECT_1:12;

then consider r being object such that

A53: r in south_halfline (S-max C) and

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

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

r in (south_halfline (S-max C)) /\ (L~ (Cage (C,n))) by A53, A54, XBOOLE_0:def 4;

then r `2 = S-bound (L~ (Cage (C,n))) by JORDAN1A:84, PSCOMP_1:58;

then r in S-most (L~ (Cage (C,n))) by A54, SPRECT_2:11;

then (S-max (L~ (Cage (C,n)))) `1 >= r `1 by PSCOMP_1:55;

hence contradiction by A3, A52, A53, TOPREAL1:def 12; :: thesis: verum

end;then consider r being object such that

A53: r in south_halfline (S-max C) and

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

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

r in (south_halfline (S-max C)) /\ (L~ (Cage (C,n))) by A53, A54, XBOOLE_0:def 4;

then r `2 = S-bound (L~ (Cage (C,n))) by JORDAN1A:84, PSCOMP_1:58;

then r in S-most (L~ (Cage (C,n))) by A54, SPRECT_2:11;

then (S-max (L~ (Cage (C,n)))) `1 >= r `1 by PSCOMP_1:55;

hence contradiction by A3, A52, A53, TOPREAL1:def 12; :: thesis: verum

then S-max C in right_cell ((Cage (C,n)),((S-max (L~ (Cage (C,n)))) .. (Cage (C,n)))) by A27, A11, A35, JORDAN1H:23;

hence S-max C in right_cell ((Rotate ((Cage (C,n)),(S-max (L~ (Cage (C,n)))))),1) by A5, Th5; :: thesis: verum