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

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

A3: E-max (L~ (Cage (C,n))) = (Gauge (C,n)) * ((len (Gauge (C,n))),j) by JORDAN1D:25;

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

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

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

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

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

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

then A12: (Cage (C,n)) /. ((E-max (L~ (Cage (C,n)))) .. (Cage (C,n))) = (GoB (Cage (C,n))) * ((len (Gauge (C,n))),j) by JORDAN1H:44;

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

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

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

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

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

( 1 <= (j -' 1) + 1 & (j -' 1) + 1 <= width (Gauge (C,n)) ) by A1, A2, XREAL_1:235;

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

set p = E-max C;

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

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

then A19: ((E-max (L~ (Cage (C,n)))) .. (Cage (C,n))) + 1 in dom (Cage (C,n)) by A13, FINSEQ_3:25;

A20: ((E-max (L~ (Cage (C,n)))) .. (Cage (C,n))) + 1 in dom (Cage (C,n)) by A13, A18, FINSEQ_3:25;

then consider ki, kj being Nat such that

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

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

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

A24: 1 <= (E-max (L~ (Cage (C,n)))) .. (Cage (C,n)) by Th2;

then A25: ((Cage (C,n)) /. (((E-max (L~ (Cage (C,n)))) .. (Cage (C,n))) + 1)) `1 = E-bound (L~ (Cage (C,n))) by A8, A13, JORDAN1E:20;

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

then A26: ki = len (Gauge (C,n)) by A21, A15, JORDAN1G:7;

A27: ( kj <= width (Gauge (C,n)) & 1 <= ki ) by A21, MATRIX_0:32;

[(len (Gauge (C,n))),j] in Indices (GoB (Cage (C,n))) by A15, JORDAN1H:44;

then |.((len (Gauge (C,n))) - ki).| + |.(j - kj).| = 1 by A6, A19, A12, A23, FINSEQ_4:20, GOBOARD5:12;

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

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

then (Cage (C,n)) /. (((E-max (L~ (Cage (C,n)))) .. (Cage (C,n))) + 1) in E-most (L~ (Cage (C,n))) by A25, A20, GOBOARD1:1, SPRECT_2:13;

then ((Gauge (C,n)) * ((len (Gauge (C,n))),j)) `2 >= ((Gauge (C,n)) * (ki,kj)) `2 by A3, A22, PSCOMP_1:47;

then j >= kj by A1, A26, A27, GOBOARD5:4;

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

then kj = j - 1 ;

then A29: kj = j -' 1 by A1, XREAL_1:233;

then A30: 1 <= j -' 1 by A21, MATRIX_0:32;

A31: j -' 1 <= width (Gauge (C,n)) by A21, A29, MATRIX_0:32;

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

then A32: right_cell ((Cage (C,n)),((E-max (L~ (Cage (C,n)))) .. (Cage (C,n))),(Gauge (C,n))) = cell ((Gauge (C,n)),((len (Gauge (C,n))) -' 1),(j -' 1)) by A17, A24, A13, A21, A22, A26, A29, A16, GOBRD13:28;

then E-max C in right_cell ((Cage (C,n)),((E-max (L~ (Cage (C,n)))) .. (Cage (C,n)))) by A24, A13, A33, JORDAN1H:23;

hence E-max C in right_cell ((Rotate ((Cage (C,n)),(E-max (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: E-max C in right_cell ((Rotate ((Cage (C,n)),(E-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 <= width (Gauge (C,n)) and

A3: E-max (L~ (Cage (C,n))) = (Gauge (C,n)) * ((len (Gauge (C,n))),j) by JORDAN1D:25;

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

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

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

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

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

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

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

(Cage (C,n)) /. ((E-max (L~ (Cage (C,n)))) .. (Cage (C,n))) = (Gauge (C,n)) * ((len (Gauge (C,n))),j)
by A3, A7, PARTFUN1:def 6;A10:
1 < (E-max (L~ (Cage (C,n)))) .. (Cage (C,n))
by Th2;

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

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

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

then (Cage (C,n)) . 1 = E-max (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 (E-max (L~ (Cage (C,n)))) .. (Cage (C,n)) = len (Cage (C,n)) ; :: thesis: contradiction

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

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

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

then A12: (Cage (C,n)) /. ((E-max (L~ (Cage (C,n)))) .. (Cage (C,n))) = (GoB (Cage (C,n))) * ((len (Gauge (C,n))),j) by JORDAN1H:44;

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

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

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

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

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

( 1 <= (j -' 1) + 1 & (j -' 1) + 1 <= width (Gauge (C,n)) ) by A1, A2, XREAL_1:235;

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

set p = E-max C;

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

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

then A19: ((E-max (L~ (Cage (C,n)))) .. (Cage (C,n))) + 1 in dom (Cage (C,n)) by A13, FINSEQ_3:25;

A20: ((E-max (L~ (Cage (C,n)))) .. (Cage (C,n))) + 1 in dom (Cage (C,n)) by A13, A18, FINSEQ_3:25;

then consider ki, kj being Nat such that

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

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

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

A24: 1 <= (E-max (L~ (Cage (C,n)))) .. (Cage (C,n)) by Th2;

then A25: ((Cage (C,n)) /. (((E-max (L~ (Cage (C,n)))) .. (Cage (C,n))) + 1)) `1 = E-bound (L~ (Cage (C,n))) by A8, A13, JORDAN1E:20;

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

then A26: ki = len (Gauge (C,n)) by A21, A15, JORDAN1G:7;

A27: ( kj <= width (Gauge (C,n)) & 1 <= ki ) by A21, MATRIX_0:32;

[(len (Gauge (C,n))),j] in Indices (GoB (Cage (C,n))) by A15, JORDAN1H:44;

then |.((len (Gauge (C,n))) - ki).| + |.(j - kj).| = 1 by A6, A19, A12, A23, FINSEQ_4:20, GOBOARD5:12;

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

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

then (Cage (C,n)) /. (((E-max (L~ (Cage (C,n)))) .. (Cage (C,n))) + 1) in E-most (L~ (Cage (C,n))) by A25, A20, GOBOARD1:1, SPRECT_2:13;

then ((Gauge (C,n)) * ((len (Gauge (C,n))),j)) `2 >= ((Gauge (C,n)) * (ki,kj)) `2 by A3, A22, PSCOMP_1:47;

then j >= kj by A1, A26, A27, GOBOARD5:4;

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

then kj = j - 1 ;

then A29: kj = j -' 1 by A1, XREAL_1:233;

then A30: 1 <= j -' 1 by A21, MATRIX_0:32;

A31: j -' 1 <= width (Gauge (C,n)) by A21, A29, MATRIX_0:32;

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

then A32: right_cell ((Cage (C,n)),((E-max (L~ (Cage (C,n)))) .. (Cage (C,n))),(Gauge (C,n))) = cell ((Gauge (C,n)),((len (Gauge (C,n))) -' 1),(j -' 1)) by A17, A24, A13, A21, A22, A26, A29, A16, GOBRD13:28;

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

GoB (Cage (C,n)) = Gauge (C,n)
by JORDAN1H:44;
j -' 1 <= len (Gauge (C,n))
by A31, JORDAN8:def 1;

then A34: ((Gauge (C,n)) * (((len (Gauge (C,n))) -' 1),(j -' 1))) `1 = E-bound C by A30, JORDAN8:12;

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

then A35: ((Gauge (C,n)) * (((len (Gauge (C,n))) -' 1),j)) `1 = E-bound C by A1, JORDAN8:12;

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

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

then A38: 1 <= (len (Gauge (C,n))) -' 1 by NAT_D:49;

A39: (len (Gauge (C,n))) -' 1 <= len (Gauge (C,n)) by NAT_D:50;

then A40: ( ((Gauge (C,n)) * (1,j)) `2 = ((Gauge (C,n)) * (((len (Gauge (C,n))) -' 1),j)) `2 & ((Gauge (C,n)) * (1,(j -' 1))) `2 = ((Gauge (C,n)) * (((len (Gauge (C,n))) -' 1),(j -' 1))) `2 ) by A1, A2, A30, A31, A38, GOBOARD5:1;

j -' 1 < j by A30, NAT_D:51;

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

then LSeg (((Gauge (C,n)) * (((len (Gauge (C,n))) -' 1),(j -' 1))),((Gauge (C,n)) * (((len (Gauge (C,n))) -' 1),((j -' 1) + 1)))) c= cell ((Gauge (C,n)),((len (Gauge (C,n))) -' 1),(j -' 1)) by A30, A38, A39, GOBOARD5:19;

then not E-max C in LSeg (((Gauge (C,n)) * (((len (Gauge (C,n))) -' 1),(j -' 1))),((Gauge (C,n)) * (((len (Gauge (C,n))) -' 1),((j -' 1) + 1)))) by A32, A36;

then A41: not E-max C in LSeg (((Gauge (C,n)) * (((len (Gauge (C,n))) -' 1),(j -' 1))),((Gauge (C,n)) * (((len (Gauge (C,n))) -' 1),j))) by A1, XREAL_1:235;

(E-max C) `1 = E-bound C by EUCLID:52;

then A42: ( (E-max C) `2 > ((Gauge (C,n)) * (((len (Gauge (C,n))) -' 1),j)) `2 or (E-max C) `2 < ((Gauge (C,n)) * (((len (Gauge (C,n))) -' 1),(j -' 1))) `2 ) by A41, A34, A35, GOBOARD7:7;

end;then A34: ((Gauge (C,n)) * (((len (Gauge (C,n))) -' 1),(j -' 1))) `1 = E-bound C by A30, JORDAN8:12;

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

then A35: ((Gauge (C,n)) * (((len (Gauge (C,n))) -' 1),j)) `1 = E-bound C by A1, JORDAN8:12;

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

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

then A38: 1 <= (len (Gauge (C,n))) -' 1 by NAT_D:49;

A39: (len (Gauge (C,n))) -' 1 <= len (Gauge (C,n)) by NAT_D:50;

then A40: ( ((Gauge (C,n)) * (1,j)) `2 = ((Gauge (C,n)) * (((len (Gauge (C,n))) -' 1),j)) `2 & ((Gauge (C,n)) * (1,(j -' 1))) `2 = ((Gauge (C,n)) * (((len (Gauge (C,n))) -' 1),(j -' 1))) `2 ) by A1, A2, A30, A31, A38, GOBOARD5:1;

j -' 1 < j by A30, NAT_D:51;

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

then LSeg (((Gauge (C,n)) * (((len (Gauge (C,n))) -' 1),(j -' 1))),((Gauge (C,n)) * (((len (Gauge (C,n))) -' 1),((j -' 1) + 1)))) c= cell ((Gauge (C,n)),((len (Gauge (C,n))) -' 1),(j -' 1)) by A30, A38, A39, GOBOARD5:19;

then not E-max C in LSeg (((Gauge (C,n)) * (((len (Gauge (C,n))) -' 1),(j -' 1))),((Gauge (C,n)) * (((len (Gauge (C,n))) -' 1),((j -' 1) + 1)))) by A32, A36;

then A41: not E-max C in LSeg (((Gauge (C,n)) * (((len (Gauge (C,n))) -' 1),(j -' 1))),((Gauge (C,n)) * (((len (Gauge (C,n))) -' 1),j))) by A1, XREAL_1:235;

(E-max C) `1 = E-bound C by EUCLID:52;

then A42: ( (E-max C) `2 > ((Gauge (C,n)) * (((len (Gauge (C,n))) -' 1),j)) `2 or (E-max C) `2 < ((Gauge (C,n)) * (((len (Gauge (C,n))) -' 1),(j -' 1))) `2 ) by A41, A34, A35, GOBOARD7:7;

per cases
( (E-max C) `2 < ((Gauge (C,n)) * ((len (Gauge (C,n))),(j -' 1))) `2 or (E-max C) `2 > ((Gauge (C,n)) * ((len (Gauge (C,n))),j)) `2 )
by A1, A2, A5, A30, A31, A42, A40, GOBOARD5:1;

end;

suppose A43:
(E-max C) `2 < ((Gauge (C,n)) * ((len (Gauge (C,n))),(j -' 1))) `2
; :: thesis: contradiction

A44:
( 1 <= j -' 1 & (j -' 1) + 1 <= width (Gauge (C,n)) )
by A1, A2, A21, A29, MATRIX_0:32, XREAL_1:235;

cell ((Gauge (C,n)),((len (Gauge (C,n))) -' 1),(j -' 1)) meets C by A24, A13, A32, JORDAN9:31;

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

then consider c being object such that

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

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

A46: ( 1 <= (len (Gauge (C,n))) -' 1 & ((len (Gauge (C,n))) -' 1) + 1 <= len (Gauge (C,n)) ) by A37, NAT_D:49, XREAL_1:235;

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

then A48: ((Gauge (C,n)) * (((len (Gauge (C,n))) -' 1),(j -' 1))) `1 <= c `1 by A46, A44, JORDAN9:17;

A49: c in C by A45, XBOOLE_0:def 4;

then c `1 <= E-bound C by PSCOMP_1:24;

then c in E-most C by A34, A49, A48, SPRECT_2:13, XXREAL_0:1;

then A50: c `2 <= (E-max C) `2 by PSCOMP_1:47;

((Gauge (C,n)) * (((len (Gauge (C,n))) -' 1),(j -' 1))) `2 <= c `2 by A47, A46, A44, JORDAN9:17;

then ((Gauge (C,n)) * (1,(j -' 1))) `2 <= c `2 by A30, A31, A38, A39, GOBOARD5:1;

then ((Gauge (C,n)) * ((len (Gauge (C,n))),(j -' 1))) `2 <= c `2 by A5, A30, A31, GOBOARD5:1;

hence contradiction by A43, A50, XXREAL_0:2; :: thesis: verum

end;cell ((Gauge (C,n)),((len (Gauge (C,n))) -' 1),(j -' 1)) meets C by A24, A13, A32, JORDAN9:31;

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

then consider c being object such that

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

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

A46: ( 1 <= (len (Gauge (C,n))) -' 1 & ((len (Gauge (C,n))) -' 1) + 1 <= len (Gauge (C,n)) ) by A37, NAT_D:49, XREAL_1:235;

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

then A48: ((Gauge (C,n)) * (((len (Gauge (C,n))) -' 1),(j -' 1))) `1 <= c `1 by A46, A44, JORDAN9:17;

A49: c in C by A45, XBOOLE_0:def 4;

then c `1 <= E-bound C by PSCOMP_1:24;

then c in E-most C by A34, A49, A48, SPRECT_2:13, XXREAL_0:1;

then A50: c `2 <= (E-max C) `2 by PSCOMP_1:47;

((Gauge (C,n)) * (((len (Gauge (C,n))) -' 1),(j -' 1))) `2 <= c `2 by A47, A46, A44, JORDAN9:17;

then ((Gauge (C,n)) * (1,(j -' 1))) `2 <= c `2 by A30, A31, A38, A39, GOBOARD5:1;

then ((Gauge (C,n)) * ((len (Gauge (C,n))),(j -' 1))) `2 <= c `2 by A5, A30, A31, GOBOARD5:1;

hence contradiction by A43, A50, XXREAL_0:2; :: thesis: verum

suppose A51:
(E-max C) `2 > ((Gauge (C,n)) * ((len (Gauge (C,n))),j)) `2
; :: thesis: contradiction

east_halfline (E-max C) meets L~ (Cage (C,n))
by JORDAN1A:52, SPRECT_1:14;

then consider r being object such that

A52: r in east_halfline (E-max C) and

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

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

r in (east_halfline (E-max C)) /\ (L~ (Cage (C,n))) by A52, A53, XBOOLE_0:def 4;

then r `1 = E-bound (L~ (Cage (C,n))) by JORDAN1A:83, PSCOMP_1:50;

then r in E-most (L~ (Cage (C,n))) by A53, SPRECT_2:13;

then (E-max (L~ (Cage (C,n)))) `2 >= r `2 by PSCOMP_1:47;

hence contradiction by A3, A51, A52, TOPREAL1:def 11; :: thesis: verum

end;then consider r being object such that

A52: r in east_halfline (E-max C) and

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

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

r in (east_halfline (E-max C)) /\ (L~ (Cage (C,n))) by A52, A53, XBOOLE_0:def 4;

then r `1 = E-bound (L~ (Cage (C,n))) by JORDAN1A:83, PSCOMP_1:50;

then r in E-most (L~ (Cage (C,n))) by A53, SPRECT_2:13;

then (E-max (L~ (Cage (C,n)))) `2 >= r `2 by PSCOMP_1:47;

hence contradiction by A3, A51, A52, TOPREAL1:def 11; :: thesis: verum

then E-max C in right_cell ((Cage (C,n)),((E-max (L~ (Cage (C,n)))) .. (Cage (C,n)))) by A24, A13, A33, JORDAN1H:23;

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