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

Last_Point ((L~ (Lower_Seq (C,n))),(E-max (L~ (Cage (C,n)))),(W-min (L~ (Cage (C,n)))),(Vertical_Line (((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2))) in rng (Lower_Seq (C,n))

let n be Nat; :: thesis: ( n > 0 implies Last_Point ((L~ (Lower_Seq (C,n))),(E-max (L~ (Cage (C,n)))),(W-min (L~ (Cage (C,n)))),(Vertical_Line (((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2))) in rng (Lower_Seq (C,n)) )

assume A1: n > 0 ; :: thesis: Last_Point ((L~ (Lower_Seq (C,n))),(E-max (L~ (Cage (C,n)))),(W-min (L~ (Cage (C,n)))),(Vertical_Line (((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2))) in rng (Lower_Seq (C,n))

set sr = ((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2;

set Ebo = E-bound (L~ (Cage (C,n)));

set Wbo = W-bound (L~ (Cage (C,n)));

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

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

set LaP = Last_Point ((L~ (Lower_Seq (C,n))),(E-max (L~ (Cage (C,n)))),(W-min (L~ (Cage (C,n)))),(Vertical_Line (((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2)));

A2: ( (Lower_Seq (C,n)) /. 1 = E-max (L~ (Cage (C,n))) & (Lower_Seq (C,n)) /. (len (Lower_Seq (C,n))) = W-min (L~ (Cage (C,n))) ) by JORDAN1F:6, JORDAN1F:8;

then A3: L~ (Lower_Seq (C,n)) is_an_arc_of E-max (L~ (Cage (C,n))), W-min (L~ (Cage (C,n))) by TOPREAL1:25;

A4: W-bound (L~ (Cage (C,n))) <= E-bound (L~ (Cage (C,n))) by SPRECT_1:21;

then W-bound (L~ (Cage (C,n))) <= ((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2 by JORDAN6:1;

then A5: (W-min (L~ (Cage (C,n)))) `1 <= ((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2 by EUCLID:52;

((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2 <= E-bound (L~ (Cage (C,n))) by A4, JORDAN6:1;

then A6: ((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2 <= (E-max (L~ (Cage (C,n)))) `1 by EUCLID:52;

A7: L~ (Lower_Seq (C,n)) is_an_arc_of W-min (L~ (Cage (C,n))), E-max (L~ (Cage (C,n))) by A2, JORDAN5B:14, TOPREAL1:25;

then A8: L~ (Lower_Seq (C,n)) meets Vertical_Line (((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2) by A5, A6, JORDAN6:49;

(L~ (Lower_Seq (C,n))) /\ (Vertical_Line (((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2)) is closed by A7, A5, A6, JORDAN6:49;

then A9: Last_Point ((L~ (Lower_Seq (C,n))),(E-max (L~ (Cage (C,n)))),(W-min (L~ (Cage (C,n)))),(Vertical_Line (((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2))) in (L~ (Lower_Seq (C,n))) /\ (Vertical_Line (((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2)) by A3, A8, JORDAN5C:def 2;

then Last_Point ((L~ (Lower_Seq (C,n))),(E-max (L~ (Cage (C,n)))),(W-min (L~ (Cage (C,n)))),(Vertical_Line (((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2))) in L~ (Lower_Seq (C,n)) by XBOOLE_0:def 4;

then consider t being Nat such that

A10: 1 <= t and

A11: t + 1 <= len (Lower_Seq (C,n)) and

A12: Last_Point ((L~ (Lower_Seq (C,n))),(E-max (L~ (Cage (C,n)))),(W-min (L~ (Cage (C,n)))),(Vertical_Line (((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2))) in LSeg ((Lower_Seq (C,n)),t) by SPPOL_2:13;

A13: LSeg ((Lower_Seq (C,n)),t) = LSeg (((Lower_Seq (C,n)) /. t),((Lower_Seq (C,n)) /. (t + 1))) by A10, A11, TOPREAL1:def 3;

1 <= t + 1 by A10, NAT_1:13;

then A14: t + 1 in dom (Lower_Seq (C,n)) by A11, FINSEQ_3:25;

t < len (Lower_Seq (C,n)) by A11, NAT_1:13;

then A15: t in dom (Lower_Seq (C,n)) by A10, FINSEQ_3:25;

Last_Point ((L~ (Lower_Seq (C,n))),(E-max (L~ (Cage (C,n)))),(W-min (L~ (Cage (C,n)))),(Vertical_Line (((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2))) in Vertical_Line (((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2) by A9, XBOOLE_0:def 4;

then A16: (Last_Point ((L~ (Lower_Seq (C,n))),(E-max (L~ (Cage (C,n)))),(W-min (L~ (Cage (C,n)))),(Vertical_Line (((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2)))) `1 = ((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2 by JORDAN6:31;

A17: Last_Point ((L~ (Lower_Seq (C,n))),(E-max (L~ (Cage (C,n)))),(W-min (L~ (Cage (C,n)))),(Vertical_Line (((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2))) = Last_Point ((LSeg ((Lower_Seq (C,n)),t)),((Lower_Seq (C,n)) /. t),((Lower_Seq (C,n)) /. (t + 1)),(Vertical_Line (((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2))) by A2, A8, A10, A11, A12, JORDAN5C:20, JORDAN6:30;

Last_Point ((L~ (Lower_Seq (C,n))),(E-max (L~ (Cage (C,n)))),(W-min (L~ (Cage (C,n)))),(Vertical_Line (((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2))) in rng (Lower_Seq (C,n))

let n be Nat; :: thesis: ( n > 0 implies Last_Point ((L~ (Lower_Seq (C,n))),(E-max (L~ (Cage (C,n)))),(W-min (L~ (Cage (C,n)))),(Vertical_Line (((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2))) in rng (Lower_Seq (C,n)) )

assume A1: n > 0 ; :: thesis: Last_Point ((L~ (Lower_Seq (C,n))),(E-max (L~ (Cage (C,n)))),(W-min (L~ (Cage (C,n)))),(Vertical_Line (((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2))) in rng (Lower_Seq (C,n))

set sr = ((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2;

set Ebo = E-bound (L~ (Cage (C,n)));

set Wbo = W-bound (L~ (Cage (C,n)));

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

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

set LaP = Last_Point ((L~ (Lower_Seq (C,n))),(E-max (L~ (Cage (C,n)))),(W-min (L~ (Cage (C,n)))),(Vertical_Line (((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2)));

A2: ( (Lower_Seq (C,n)) /. 1 = E-max (L~ (Cage (C,n))) & (Lower_Seq (C,n)) /. (len (Lower_Seq (C,n))) = W-min (L~ (Cage (C,n))) ) by JORDAN1F:6, JORDAN1F:8;

then A3: L~ (Lower_Seq (C,n)) is_an_arc_of E-max (L~ (Cage (C,n))), W-min (L~ (Cage (C,n))) by TOPREAL1:25;

A4: W-bound (L~ (Cage (C,n))) <= E-bound (L~ (Cage (C,n))) by SPRECT_1:21;

then W-bound (L~ (Cage (C,n))) <= ((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2 by JORDAN6:1;

then A5: (W-min (L~ (Cage (C,n)))) `1 <= ((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2 by EUCLID:52;

((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2 <= E-bound (L~ (Cage (C,n))) by A4, JORDAN6:1;

then A6: ((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2 <= (E-max (L~ (Cage (C,n)))) `1 by EUCLID:52;

A7: L~ (Lower_Seq (C,n)) is_an_arc_of W-min (L~ (Cage (C,n))), E-max (L~ (Cage (C,n))) by A2, JORDAN5B:14, TOPREAL1:25;

then A8: L~ (Lower_Seq (C,n)) meets Vertical_Line (((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2) by A5, A6, JORDAN6:49;

(L~ (Lower_Seq (C,n))) /\ (Vertical_Line (((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2)) is closed by A7, A5, A6, JORDAN6:49;

then A9: Last_Point ((L~ (Lower_Seq (C,n))),(E-max (L~ (Cage (C,n)))),(W-min (L~ (Cage (C,n)))),(Vertical_Line (((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2))) in (L~ (Lower_Seq (C,n))) /\ (Vertical_Line (((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2)) by A3, A8, JORDAN5C:def 2;

then Last_Point ((L~ (Lower_Seq (C,n))),(E-max (L~ (Cage (C,n)))),(W-min (L~ (Cage (C,n)))),(Vertical_Line (((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2))) in L~ (Lower_Seq (C,n)) by XBOOLE_0:def 4;

then consider t being Nat such that

A10: 1 <= t and

A11: t + 1 <= len (Lower_Seq (C,n)) and

A12: Last_Point ((L~ (Lower_Seq (C,n))),(E-max (L~ (Cage (C,n)))),(W-min (L~ (Cage (C,n)))),(Vertical_Line (((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2))) in LSeg ((Lower_Seq (C,n)),t) by SPPOL_2:13;

A13: LSeg ((Lower_Seq (C,n)),t) = LSeg (((Lower_Seq (C,n)) /. t),((Lower_Seq (C,n)) /. (t + 1))) by A10, A11, TOPREAL1:def 3;

1 <= t + 1 by A10, NAT_1:13;

then A14: t + 1 in dom (Lower_Seq (C,n)) by A11, FINSEQ_3:25;

t < len (Lower_Seq (C,n)) by A11, NAT_1:13;

then A15: t in dom (Lower_Seq (C,n)) by A10, FINSEQ_3:25;

Last_Point ((L~ (Lower_Seq (C,n))),(E-max (L~ (Cage (C,n)))),(W-min (L~ (Cage (C,n)))),(Vertical_Line (((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2))) in Vertical_Line (((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2) by A9, XBOOLE_0:def 4;

then A16: (Last_Point ((L~ (Lower_Seq (C,n))),(E-max (L~ (Cage (C,n)))),(W-min (L~ (Cage (C,n)))),(Vertical_Line (((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2)))) `1 = ((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2 by JORDAN6:31;

A17: Last_Point ((L~ (Lower_Seq (C,n))),(E-max (L~ (Cage (C,n)))),(W-min (L~ (Cage (C,n)))),(Vertical_Line (((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2))) = Last_Point ((LSeg ((Lower_Seq (C,n)),t)),((Lower_Seq (C,n)) /. t),((Lower_Seq (C,n)) /. (t + 1)),(Vertical_Line (((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2))) by A2, A8, A10, A11, A12, JORDAN5C:20, JORDAN6:30;

now :: thesis: Last_Point ((L~ (Lower_Seq (C,n))),(E-max (L~ (Cage (C,n)))),(W-min (L~ (Cage (C,n)))),(Vertical_Line (((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2))) in rng (Lower_Seq (C,n))end;

hence
Last_Point ((L~ (Lower_Seq (C,n))),(E-max (L~ (Cage (C,n)))),(W-min (L~ (Cage (C,n)))),(Vertical_Line (((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2))) in rng (Lower_Seq (C,n))
; :: thesis: verumper cases
( LSeg ((Lower_Seq (C,n)),t) is vertical or LSeg ((Lower_Seq (C,n)),t) is horizontal )
by SPPOL_1:19;

end;

suppose A18:
LSeg ((Lower_Seq (C,n)),t) is vertical
; :: thesis: Last_Point ((L~ (Lower_Seq (C,n))),(E-max (L~ (Cage (C,n)))),(W-min (L~ (Cage (C,n)))),(Vertical_Line (((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2))) in rng (Lower_Seq (C,n))

then
((Lower_Seq (C,n)) /. (t + 1)) `1 = ((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2
by A12, A13, A16, SPPOL_1:41;

then (Lower_Seq (C,n)) /. (t + 1) in { p where p is Point of (TOP-REAL 2) : p `1 = ((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2 } ;

then A19: (Lower_Seq (C,n)) /. (t + 1) in Vertical_Line (((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2) by JORDAN6:def 6;

A20: ( LSeg ((Lower_Seq (C,n)),t) is closed & LSeg ((Lower_Seq (C,n)),t) is_an_arc_of (Lower_Seq (C,n)) /. t,(Lower_Seq (C,n)) /. (t + 1) ) by A13, A15, A14, GOBOARD7:29, TOPREAL1:9;

((Lower_Seq (C,n)) /. t) `1 = ((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2 by A12, A13, A16, A18, SPPOL_1:41;

then (Lower_Seq (C,n)) /. t in { p where p is Point of (TOP-REAL 2) : p `1 = ((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2 } ;

then (Lower_Seq (C,n)) /. t in Vertical_Line (((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2) by JORDAN6:def 6;

then LSeg ((Lower_Seq (C,n)),t) c= Vertical_Line (((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2) by A13, A19, JORDAN1A:13;

then Last_Point ((LSeg ((Lower_Seq (C,n)),t)),((Lower_Seq (C,n)) /. t),((Lower_Seq (C,n)) /. (t + 1)),(Vertical_Line (((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2))) = (Lower_Seq (C,n)) /. (t + 1) by A20, JORDAN5C:7;

hence Last_Point ((L~ (Lower_Seq (C,n))),(E-max (L~ (Cage (C,n)))),(W-min (L~ (Cage (C,n)))),(Vertical_Line (((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2))) in rng (Lower_Seq (C,n)) by A17, A14, PARTFUN2:2; :: thesis: verum

end;then (Lower_Seq (C,n)) /. (t + 1) in { p where p is Point of (TOP-REAL 2) : p `1 = ((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2 } ;

then A19: (Lower_Seq (C,n)) /. (t + 1) in Vertical_Line (((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2) by JORDAN6:def 6;

A20: ( LSeg ((Lower_Seq (C,n)),t) is closed & LSeg ((Lower_Seq (C,n)),t) is_an_arc_of (Lower_Seq (C,n)) /. t,(Lower_Seq (C,n)) /. (t + 1) ) by A13, A15, A14, GOBOARD7:29, TOPREAL1:9;

((Lower_Seq (C,n)) /. t) `1 = ((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2 by A12, A13, A16, A18, SPPOL_1:41;

then (Lower_Seq (C,n)) /. t in { p where p is Point of (TOP-REAL 2) : p `1 = ((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2 } ;

then (Lower_Seq (C,n)) /. t in Vertical_Line (((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2) by JORDAN6:def 6;

then LSeg ((Lower_Seq (C,n)),t) c= Vertical_Line (((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2) by A13, A19, JORDAN1A:13;

then Last_Point ((LSeg ((Lower_Seq (C,n)),t)),((Lower_Seq (C,n)) /. t),((Lower_Seq (C,n)) /. (t + 1)),(Vertical_Line (((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2))) = (Lower_Seq (C,n)) /. (t + 1) by A20, JORDAN5C:7;

hence Last_Point ((L~ (Lower_Seq (C,n))),(E-max (L~ (Cage (C,n)))),(W-min (L~ (Cage (C,n)))),(Vertical_Line (((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2))) in rng (Lower_Seq (C,n)) by A17, A14, PARTFUN2:2; :: thesis: verum

suppose
LSeg ((Lower_Seq (C,n)),t) is horizontal
; :: thesis: Last_Point ((L~ (Lower_Seq (C,n))),(E-max (L~ (Cage (C,n)))),(W-min (L~ (Cage (C,n)))),(Vertical_Line (((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2))) in rng (Lower_Seq (C,n))

then A21:
((Lower_Seq (C,n)) /. t) `2 = ((Lower_Seq (C,n)) /. (t + 1)) `2
by A13, SPPOL_1:15;

then A22: (Last_Point ((L~ (Lower_Seq (C,n))),(E-max (L~ (Cage (C,n)))),(W-min (L~ (Cage (C,n)))),(Vertical_Line (((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2)))) `2 = ((Lower_Seq (C,n)) /. t) `2 by A12, A13, GOBOARD7:6;

Lower_Seq (C,n) is_sequence_on Gauge (C,n) by Th5;

then consider i1, j1, i2, j2 being Nat such that

A23: [i1,j1] in Indices (Gauge (C,n)) and

A24: (Lower_Seq (C,n)) /. t = (Gauge (C,n)) * (i1,j1) and

A25: [i2,j2] in Indices (Gauge (C,n)) and

A26: (Lower_Seq (C,n)) /. (t + 1) = (Gauge (C,n)) * (i2,j2) and

A27: ( ( i1 = i2 & j1 + 1 = j2 ) or ( i1 + 1 = i2 & j1 = j2 ) or ( i1 = i2 + 1 & j1 = j2 ) or ( i1 = i2 & j1 = j2 + 1 ) ) by A10, A11, JORDAN8:3;

A28: 1 <= i1 by A23, MATRIX_0:32;

A29: j1 = j2 by A21, A23, A24, A25, A26, Th6;

A30: i2 <= len (Gauge (C,n)) by A25, MATRIX_0:32;

A31: i1 <= len (Gauge (C,n)) by A23, MATRIX_0:32;

A32: 1 <= i2 by A25, MATRIX_0:32;

A33: Center (Gauge (C,n)) <= len (Gauge (C,n)) by JORDAN1B:13;

A34: ( 1 <= j1 & j1 <= width (Gauge (C,n)) ) by A23, MATRIX_0:32;

then A35: ((Gauge (C,n)) * ((Center (Gauge (C,n))),j1)) `1 = ((W-bound C) + (E-bound C)) / 2 by A1, Th35

.= (Last_Point ((L~ (Lower_Seq (C,n))),(E-max (L~ (Cage (C,n)))),(W-min (L~ (Cage (C,n)))),(Vertical_Line (((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2)))) `1 by A16, Th33 ;

A36: 1 <= Center (Gauge (C,n)) by JORDAN1B:11;

then ((Gauge (C,n)) * ((Center (Gauge (C,n))),j1)) `2 = ((Gauge (C,n)) * (1,j1)) `2 by A34, A33, GOBOARD5:1

.= (Last_Point ((L~ (Lower_Seq (C,n))),(E-max (L~ (Cage (C,n)))),(W-min (L~ (Cage (C,n)))),(Vertical_Line (((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2)))) `2 by A22, A24, A28, A31, A34, GOBOARD5:1 ;

then A37: Last_Point ((L~ (Lower_Seq (C,n))),(E-max (L~ (Cage (C,n)))),(W-min (L~ (Cage (C,n)))),(Vertical_Line (((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2))) = (Gauge (C,n)) * ((Center (Gauge (C,n))),j1) by A35, TOPREAL3:6;

end;then A22: (Last_Point ((L~ (Lower_Seq (C,n))),(E-max (L~ (Cage (C,n)))),(W-min (L~ (Cage (C,n)))),(Vertical_Line (((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2)))) `2 = ((Lower_Seq (C,n)) /. t) `2 by A12, A13, GOBOARD7:6;

Lower_Seq (C,n) is_sequence_on Gauge (C,n) by Th5;

then consider i1, j1, i2, j2 being Nat such that

A23: [i1,j1] in Indices (Gauge (C,n)) and

A24: (Lower_Seq (C,n)) /. t = (Gauge (C,n)) * (i1,j1) and

A25: [i2,j2] in Indices (Gauge (C,n)) and

A26: (Lower_Seq (C,n)) /. (t + 1) = (Gauge (C,n)) * (i2,j2) and

A27: ( ( i1 = i2 & j1 + 1 = j2 ) or ( i1 + 1 = i2 & j1 = j2 ) or ( i1 = i2 + 1 & j1 = j2 ) or ( i1 = i2 & j1 = j2 + 1 ) ) by A10, A11, JORDAN8:3;

A28: 1 <= i1 by A23, MATRIX_0:32;

A29: j1 = j2 by A21, A23, A24, A25, A26, Th6;

A30: i2 <= len (Gauge (C,n)) by A25, MATRIX_0:32;

A31: i1 <= len (Gauge (C,n)) by A23, MATRIX_0:32;

A32: 1 <= i2 by A25, MATRIX_0:32;

A33: Center (Gauge (C,n)) <= len (Gauge (C,n)) by JORDAN1B:13;

A34: ( 1 <= j1 & j1 <= width (Gauge (C,n)) ) by A23, MATRIX_0:32;

then A35: ((Gauge (C,n)) * ((Center (Gauge (C,n))),j1)) `1 = ((W-bound C) + (E-bound C)) / 2 by A1, Th35

.= (Last_Point ((L~ (Lower_Seq (C,n))),(E-max (L~ (Cage (C,n)))),(W-min (L~ (Cage (C,n)))),(Vertical_Line (((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2)))) `1 by A16, Th33 ;

A36: 1 <= Center (Gauge (C,n)) by JORDAN1B:11;

then ((Gauge (C,n)) * ((Center (Gauge (C,n))),j1)) `2 = ((Gauge (C,n)) * (1,j1)) `2 by A34, A33, GOBOARD5:1

.= (Last_Point ((L~ (Lower_Seq (C,n))),(E-max (L~ (Cage (C,n)))),(W-min (L~ (Cage (C,n)))),(Vertical_Line (((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2)))) `2 by A22, A24, A28, A31, A34, GOBOARD5:1 ;

then A37: Last_Point ((L~ (Lower_Seq (C,n))),(E-max (L~ (Cage (C,n)))),(W-min (L~ (Cage (C,n)))),(Vertical_Line (((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2))) = (Gauge (C,n)) * ((Center (Gauge (C,n))),j1) by A35, TOPREAL3:6;

now :: thesis: Last_Point ((L~ (Lower_Seq (C,n))),(E-max (L~ (Cage (C,n)))),(W-min (L~ (Cage (C,n)))),(Vertical_Line (((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2))) in rng (Lower_Seq (C,n))end;

hence
Last_Point ((L~ (Lower_Seq (C,n))),(E-max (L~ (Cage (C,n)))),(W-min (L~ (Cage (C,n)))),(Vertical_Line (((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2))) in rng (Lower_Seq (C,n))
; :: thesis: verumper cases
( i1 + 1 = i2 or i1 = i2 + 1 )
by A27, A29;

end;

suppose A38:
i1 + 1 = i2
; :: thesis: Last_Point ((L~ (Lower_Seq (C,n))),(E-max (L~ (Cage (C,n)))),(W-min (L~ (Cage (C,n)))),(Vertical_Line (((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2))) in rng (Lower_Seq (C,n))

i1 < i1 + 1
by NAT_1:13;

then A39: ((Gauge (C,n)) * (i1,j1)) `1 <= ((Gauge (C,n)) * ((i1 + 1),j1)) `1 by A28, A34, A30, A38, SPRECT_3:13;

then ((Gauge (C,n)) * (i1,j1)) `1 <= (Last_Point ((L~ (Lower_Seq (C,n))),(E-max (L~ (Cage (C,n)))),(W-min (L~ (Cage (C,n)))),(Vertical_Line (((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2)))) `1 by A12, A13, A24, A26, A29, A38, TOPREAL1:3;

then i1 <= Center (Gauge (C,n)) by A31, A34, A36, A35, GOBOARD5:3;

then ( i1 = Center (Gauge (C,n)) or i1 < Center (Gauge (C,n)) ) by XXREAL_0:1;

then A40: ( i1 = Center (Gauge (C,n)) or i1 + 1 <= Center (Gauge (C,n)) ) by NAT_1:13;

(Last_Point ((L~ (Lower_Seq (C,n))),(E-max (L~ (Cage (C,n)))),(W-min (L~ (Cage (C,n)))),(Vertical_Line (((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2)))) `1 <= ((Gauge (C,n)) * ((i1 + 1),j1)) `1 by A12, A13, A24, A26, A29, A38, A39, TOPREAL1:3;

then Center (Gauge (C,n)) <= i1 + 1 by A34, A32, A33, A35, A38, GOBOARD5:3;

then ( i1 = Center (Gauge (C,n)) or i1 + 1 = Center (Gauge (C,n)) ) by A40, XXREAL_0:1;

hence Last_Point ((L~ (Lower_Seq (C,n))),(E-max (L~ (Cage (C,n)))),(W-min (L~ (Cage (C,n)))),(Vertical_Line (((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2))) in rng (Lower_Seq (C,n)) by A15, A14, A24, A26, A29, A37, A38, PARTFUN2:2; :: thesis: verum

end;then A39: ((Gauge (C,n)) * (i1,j1)) `1 <= ((Gauge (C,n)) * ((i1 + 1),j1)) `1 by A28, A34, A30, A38, SPRECT_3:13;

then ((Gauge (C,n)) * (i1,j1)) `1 <= (Last_Point ((L~ (Lower_Seq (C,n))),(E-max (L~ (Cage (C,n)))),(W-min (L~ (Cage (C,n)))),(Vertical_Line (((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2)))) `1 by A12, A13, A24, A26, A29, A38, TOPREAL1:3;

then i1 <= Center (Gauge (C,n)) by A31, A34, A36, A35, GOBOARD5:3;

then ( i1 = Center (Gauge (C,n)) or i1 < Center (Gauge (C,n)) ) by XXREAL_0:1;

then A40: ( i1 = Center (Gauge (C,n)) or i1 + 1 <= Center (Gauge (C,n)) ) by NAT_1:13;

(Last_Point ((L~ (Lower_Seq (C,n))),(E-max (L~ (Cage (C,n)))),(W-min (L~ (Cage (C,n)))),(Vertical_Line (((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2)))) `1 <= ((Gauge (C,n)) * ((i1 + 1),j1)) `1 by A12, A13, A24, A26, A29, A38, A39, TOPREAL1:3;

then Center (Gauge (C,n)) <= i1 + 1 by A34, A32, A33, A35, A38, GOBOARD5:3;

then ( i1 = Center (Gauge (C,n)) or i1 + 1 = Center (Gauge (C,n)) ) by A40, XXREAL_0:1;

hence Last_Point ((L~ (Lower_Seq (C,n))),(E-max (L~ (Cage (C,n)))),(W-min (L~ (Cage (C,n)))),(Vertical_Line (((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2))) in rng (Lower_Seq (C,n)) by A15, A14, A24, A26, A29, A37, A38, PARTFUN2:2; :: thesis: verum

suppose A41:
i1 = i2 + 1
; :: thesis: Last_Point ((L~ (Lower_Seq (C,n))),(E-max (L~ (Cage (C,n)))),(W-min (L~ (Cage (C,n)))),(Vertical_Line (((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2))) in rng (Lower_Seq (C,n))

i2 < i2 + 1
by NAT_1:13;

then A42: ((Gauge (C,n)) * (i2,j1)) `1 <= ((Gauge (C,n)) * ((i2 + 1),j1)) `1 by A31, A34, A32, A41, SPRECT_3:13;

then ((Gauge (C,n)) * (i2,j1)) `1 <= (Last_Point ((L~ (Lower_Seq (C,n))),(E-max (L~ (Cage (C,n)))),(W-min (L~ (Cage (C,n)))),(Vertical_Line (((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2)))) `1 by A12, A13, A24, A26, A29, A41, TOPREAL1:3;

then i2 <= Center (Gauge (C,n)) by A34, A30, A36, A35, GOBOARD5:3;

then ( i2 = Center (Gauge (C,n)) or i2 < Center (Gauge (C,n)) ) by XXREAL_0:1;

then A43: ( i2 = Center (Gauge (C,n)) or i2 + 1 <= Center (Gauge (C,n)) ) by NAT_1:13;

(Last_Point ((L~ (Lower_Seq (C,n))),(E-max (L~ (Cage (C,n)))),(W-min (L~ (Cage (C,n)))),(Vertical_Line (((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2)))) `1 <= ((Gauge (C,n)) * ((i2 + 1),j1)) `1 by A12, A13, A24, A26, A29, A41, A42, TOPREAL1:3;

then Center (Gauge (C,n)) <= i2 + 1 by A28, A34, A33, A35, A41, GOBOARD5:3;

then ( i2 = Center (Gauge (C,n)) or i2 + 1 = Center (Gauge (C,n)) ) by A43, XXREAL_0:1;

hence Last_Point ((L~ (Lower_Seq (C,n))),(E-max (L~ (Cage (C,n)))),(W-min (L~ (Cage (C,n)))),(Vertical_Line (((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2))) in rng (Lower_Seq (C,n)) by A15, A14, A24, A26, A29, A37, A41, PARTFUN2:2; :: thesis: verum

end;then A42: ((Gauge (C,n)) * (i2,j1)) `1 <= ((Gauge (C,n)) * ((i2 + 1),j1)) `1 by A31, A34, A32, A41, SPRECT_3:13;

then ((Gauge (C,n)) * (i2,j1)) `1 <= (Last_Point ((L~ (Lower_Seq (C,n))),(E-max (L~ (Cage (C,n)))),(W-min (L~ (Cage (C,n)))),(Vertical_Line (((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2)))) `1 by A12, A13, A24, A26, A29, A41, TOPREAL1:3;

then i2 <= Center (Gauge (C,n)) by A34, A30, A36, A35, GOBOARD5:3;

then ( i2 = Center (Gauge (C,n)) or i2 < Center (Gauge (C,n)) ) by XXREAL_0:1;

then A43: ( i2 = Center (Gauge (C,n)) or i2 + 1 <= Center (Gauge (C,n)) ) by NAT_1:13;

(Last_Point ((L~ (Lower_Seq (C,n))),(E-max (L~ (Cage (C,n)))),(W-min (L~ (Cage (C,n)))),(Vertical_Line (((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2)))) `1 <= ((Gauge (C,n)) * ((i2 + 1),j1)) `1 by A12, A13, A24, A26, A29, A41, A42, TOPREAL1:3;

then Center (Gauge (C,n)) <= i2 + 1 by A28, A34, A33, A35, A41, GOBOARD5:3;

then ( i2 = Center (Gauge (C,n)) or i2 + 1 = Center (Gauge (C,n)) ) by A43, XXREAL_0:1;

hence Last_Point ((L~ (Lower_Seq (C,n))),(E-max (L~ (Cage (C,n)))),(W-min (L~ (Cage (C,n)))),(Vertical_Line (((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2))) in rng (Lower_Seq (C,n)) by A15, A14, A24, A26, A29, A37, A41, PARTFUN2:2; :: thesis: verum