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

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

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

assume A1: n > 0 ; :: thesis: First_Point ((L~ (Upper_Seq (C,n))),(W-min (L~ (Cage (C,n)))),(E-max (L~ (Cage (C,n)))),(Vertical_Line (((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2))) in rng (Upper_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 FiP = First_Point ((L~ (Upper_Seq (C,n))),(W-min (L~ (Cage (C,n)))),(E-max (L~ (Cage (C,n)))),(Vertical_Line (((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2)));

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

A3: ( (Upper_Seq (C,n)) /. 1 = W-min (L~ (Cage (C,n))) & (Upper_Seq (C,n)) /. (len (Upper_Seq (C,n))) = E-max (L~ (Cage (C,n))) ) by JORDAN1F:5, JORDAN1F:7;

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

A5: W-bound (L~ (Cage (C,n))) < E-bound (L~ (Cage (C,n))) by SPRECT_1:31;

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

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

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

((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2 < E-bound (L~ (Cage (C,n))) by A5, XREAL_1:226;

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

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

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

then A10: First_Point ((L~ (Upper_Seq (C,n))),(W-min (L~ (Cage (C,n)))),(E-max (L~ (Cage (C,n)))),(Vertical_Line (((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2))) in (L~ (Upper_Seq (C,n))) /\ (Vertical_Line (((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2)) by A4, A9, JORDAN5C:def 1;

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

then consider t being Nat such that

A11: 1 <= t and

A12: t + 1 <= len (Upper_Seq (C,n)) and

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

A14: LSeg ((Upper_Seq (C,n)),t) = LSeg (((Upper_Seq (C,n)) /. t),((Upper_Seq (C,n)) /. (t + 1))) by A11, A12, TOPREAL1:def 3;

t < len (Upper_Seq (C,n)) by A12, NAT_1:13;

then A15: t in dom (Upper_Seq (C,n)) by A11, FINSEQ_3:25;

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

then A16: t + 1 in dom (Upper_Seq (C,n)) by A12, FINSEQ_3:25;

First_Point ((L~ (Upper_Seq (C,n))),(W-min (L~ (Cage (C,n)))),(E-max (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 A10, XBOOLE_0:def 4;

then A17: (First_Point ((L~ (Upper_Seq (C,n))),(W-min (L~ (Cage (C,n)))),(E-max (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;

A18: First_Point ((L~ (Upper_Seq (C,n))),(W-min (L~ (Cage (C,n)))),(E-max (L~ (Cage (C,n)))),(Vertical_Line (((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2))) = First_Point ((LSeg ((Upper_Seq (C,n)),t)),((Upper_Seq (C,n)) /. t),((Upper_Seq (C,n)) /. (t + 1)),(Vertical_Line (((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2))) by A3, A9, A11, A12, A13, JORDAN5C:19, JORDAN6:30;

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

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

assume A1: n > 0 ; :: thesis: First_Point ((L~ (Upper_Seq (C,n))),(W-min (L~ (Cage (C,n)))),(E-max (L~ (Cage (C,n)))),(Vertical_Line (((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2))) in rng (Upper_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 FiP = First_Point ((L~ (Upper_Seq (C,n))),(W-min (L~ (Cage (C,n)))),(E-max (L~ (Cage (C,n)))),(Vertical_Line (((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2)));

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

A3: ( (Upper_Seq (C,n)) /. 1 = W-min (L~ (Cage (C,n))) & (Upper_Seq (C,n)) /. (len (Upper_Seq (C,n))) = E-max (L~ (Cage (C,n))) ) by JORDAN1F:5, JORDAN1F:7;

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

A5: W-bound (L~ (Cage (C,n))) < E-bound (L~ (Cage (C,n))) by SPRECT_1:31;

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

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

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

((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2 < E-bound (L~ (Cage (C,n))) by A5, XREAL_1:226;

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

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

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

then A10: First_Point ((L~ (Upper_Seq (C,n))),(W-min (L~ (Cage (C,n)))),(E-max (L~ (Cage (C,n)))),(Vertical_Line (((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2))) in (L~ (Upper_Seq (C,n))) /\ (Vertical_Line (((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2)) by A4, A9, JORDAN5C:def 1;

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

then consider t being Nat such that

A11: 1 <= t and

A12: t + 1 <= len (Upper_Seq (C,n)) and

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

A14: LSeg ((Upper_Seq (C,n)),t) = LSeg (((Upper_Seq (C,n)) /. t),((Upper_Seq (C,n)) /. (t + 1))) by A11, A12, TOPREAL1:def 3;

t < len (Upper_Seq (C,n)) by A12, NAT_1:13;

then A15: t in dom (Upper_Seq (C,n)) by A11, FINSEQ_3:25;

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

then A16: t + 1 in dom (Upper_Seq (C,n)) by A12, FINSEQ_3:25;

First_Point ((L~ (Upper_Seq (C,n))),(W-min (L~ (Cage (C,n)))),(E-max (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 A10, XBOOLE_0:def 4;

then A17: (First_Point ((L~ (Upper_Seq (C,n))),(W-min (L~ (Cage (C,n)))),(E-max (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;

A18: First_Point ((L~ (Upper_Seq (C,n))),(W-min (L~ (Cage (C,n)))),(E-max (L~ (Cage (C,n)))),(Vertical_Line (((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2))) = First_Point ((LSeg ((Upper_Seq (C,n)),t)),((Upper_Seq (C,n)) /. t),((Upper_Seq (C,n)) /. (t + 1)),(Vertical_Line (((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2))) by A3, A9, A11, A12, A13, JORDAN5C:19, JORDAN6:30;

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

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

end;

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

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

then (Upper_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 A20: (Upper_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;

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

((Upper_Seq (C,n)) /. t) `1 = ((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2 by A13, A14, A17, A19, SPPOL_1:41;

then (Upper_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 (Upper_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 ((Upper_Seq (C,n)),t) c= Vertical_Line (((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2) by A14, A20, JORDAN1A:13;

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

hence First_Point ((L~ (Upper_Seq (C,n))),(W-min (L~ (Cage (C,n)))),(E-max (L~ (Cage (C,n)))),(Vertical_Line (((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2))) in rng (Upper_Seq (C,n)) by A18, A15, PARTFUN2:2; :: thesis: verum

end;then (Upper_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 A20: (Upper_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;

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

((Upper_Seq (C,n)) /. t) `1 = ((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2 by A13, A14, A17, A19, SPPOL_1:41;

then (Upper_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 (Upper_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 ((Upper_Seq (C,n)),t) c= Vertical_Line (((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2) by A14, A20, JORDAN1A:13;

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

hence First_Point ((L~ (Upper_Seq (C,n))),(W-min (L~ (Cage (C,n)))),(E-max (L~ (Cage (C,n)))),(Vertical_Line (((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2))) in rng (Upper_Seq (C,n)) by A18, A15, PARTFUN2:2; :: thesis: verum

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

then A22:
((Upper_Seq (C,n)) /. t) `2 = ((Upper_Seq (C,n)) /. (t + 1)) `2
by A14, SPPOL_1:15;

then A23: (First_Point ((L~ (Upper_Seq (C,n))),(W-min (L~ (Cage (C,n)))),(E-max (L~ (Cage (C,n)))),(Vertical_Line (((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2)))) `2 = ((Upper_Seq (C,n)) /. t) `2 by A13, A14, GOBOARD7:6;

Upper_Seq (C,n) is_sequence_on Gauge (C,n) by Th4;

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

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

A25: (Upper_Seq (C,n)) /. t = (Gauge (C,n)) * (i1,j1) and

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

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

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

A29: 1 <= i1 by A24, MATRIX_0:32;

A30: 1 <= i2 by A26, MATRIX_0:32;

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

A32: j1 = j2 by A22, A24, A25, A26, A27, Th6;

A33: i2 <= len (Gauge (C,n)) by A26, MATRIX_0:32;

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

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

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

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

.= (First_Point ((L~ (Upper_Seq (C,n))),(W-min (L~ (Cage (C,n)))),(E-max (L~ (Cage (C,n)))),(Vertical_Line (((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2)))) `2 by A23, A25, A29, A31, A34, GOBOARD5:1 ;

then A36: First_Point ((L~ (Upper_Seq (C,n))),(W-min (L~ (Cage (C,n)))),(E-max (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 A23: (First_Point ((L~ (Upper_Seq (C,n))),(W-min (L~ (Cage (C,n)))),(E-max (L~ (Cage (C,n)))),(Vertical_Line (((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2)))) `2 = ((Upper_Seq (C,n)) /. t) `2 by A13, A14, GOBOARD7:6;

Upper_Seq (C,n) is_sequence_on Gauge (C,n) by Th4;

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

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

A25: (Upper_Seq (C,n)) /. t = (Gauge (C,n)) * (i1,j1) and

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

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

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

A29: 1 <= i1 by A24, MATRIX_0:32;

A30: 1 <= i2 by A26, MATRIX_0:32;

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

A32: j1 = j2 by A22, A24, A25, A26, A27, Th6;

A33: i2 <= len (Gauge (C,n)) by A26, MATRIX_0:32;

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

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

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

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

.= (First_Point ((L~ (Upper_Seq (C,n))),(W-min (L~ (Cage (C,n)))),(E-max (L~ (Cage (C,n)))),(Vertical_Line (((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2)))) `2 by A23, A25, A29, A31, A34, GOBOARD5:1 ;

then A36: First_Point ((L~ (Upper_Seq (C,n))),(W-min (L~ (Cage (C,n)))),(E-max (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: First_Point ((L~ (Upper_Seq (C,n))),(W-min (L~ (Cage (C,n)))),(E-max (L~ (Cage (C,n)))),(Vertical_Line (((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2))) in rng (Upper_Seq (C,n))end;

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

end;

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

i1 < i1 + 1
by NAT_1:13;

then A38: ((Gauge (C,n)) * (i1,j1)) `1 <= ((Gauge (C,n)) * ((i1 + 1),j1)) `1 by A29, A34, A33, A37, SPRECT_3:13;

then ((Gauge (C,n)) * (i1,j1)) `1 <= (First_Point ((L~ (Upper_Seq (C,n))),(W-min (L~ (Cage (C,n)))),(E-max (L~ (Cage (C,n)))),(Vertical_Line (((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2)))) `1 by A13, A14, A25, A27, A32, A37, TOPREAL1:3;

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

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

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

(First_Point ((L~ (Upper_Seq (C,n))),(W-min (L~ (Cage (C,n)))),(E-max (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 A13, A14, A25, A27, A32, A37, A38, TOPREAL1:3;

then Center (Gauge (C,n)) <= i1 + 1 by A7, A34, A30, A35, A37, GOBOARD5:3;

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

hence First_Point ((L~ (Upper_Seq (C,n))),(W-min (L~ (Cage (C,n)))),(E-max (L~ (Cage (C,n)))),(Vertical_Line (((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2))) in rng (Upper_Seq (C,n)) by A15, A16, A25, A27, A32, A36, A37, PARTFUN2:2; :: thesis: verum

end;then A38: ((Gauge (C,n)) * (i1,j1)) `1 <= ((Gauge (C,n)) * ((i1 + 1),j1)) `1 by A29, A34, A33, A37, SPRECT_3:13;

then ((Gauge (C,n)) * (i1,j1)) `1 <= (First_Point ((L~ (Upper_Seq (C,n))),(W-min (L~ (Cage (C,n)))),(E-max (L~ (Cage (C,n)))),(Vertical_Line (((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2)))) `1 by A13, A14, A25, A27, A32, A37, TOPREAL1:3;

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

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

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

(First_Point ((L~ (Upper_Seq (C,n))),(W-min (L~ (Cage (C,n)))),(E-max (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 A13, A14, A25, A27, A32, A37, A38, TOPREAL1:3;

then Center (Gauge (C,n)) <= i1 + 1 by A7, A34, A30, A35, A37, GOBOARD5:3;

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

hence First_Point ((L~ (Upper_Seq (C,n))),(W-min (L~ (Cage (C,n)))),(E-max (L~ (Cage (C,n)))),(Vertical_Line (((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2))) in rng (Upper_Seq (C,n)) by A15, A16, A25, A27, A32, A36, A37, PARTFUN2:2; :: thesis: verum

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

i2 < i2 + 1
by NAT_1:13;

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

then ((Gauge (C,n)) * (i2,j1)) `1 <= (First_Point ((L~ (Upper_Seq (C,n))),(W-min (L~ (Cage (C,n)))),(E-max (L~ (Cage (C,n)))),(Vertical_Line (((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2)))) `1 by A13, A14, A25, A27, A32, A40, TOPREAL1:3;

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

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

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

(First_Point ((L~ (Upper_Seq (C,n))),(W-min (L~ (Cage (C,n)))),(E-max (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 A13, A14, A25, A27, A32, A40, A41, TOPREAL1:3;

then Center (Gauge (C,n)) <= i2 + 1 by A7, A29, A34, A35, A40, GOBOARD5:3;

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

hence First_Point ((L~ (Upper_Seq (C,n))),(W-min (L~ (Cage (C,n)))),(E-max (L~ (Cage (C,n)))),(Vertical_Line (((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2))) in rng (Upper_Seq (C,n)) by A15, A16, A25, A27, A32, A36, A40, PARTFUN2:2; :: thesis: verum

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

then ((Gauge (C,n)) * (i2,j1)) `1 <= (First_Point ((L~ (Upper_Seq (C,n))),(W-min (L~ (Cage (C,n)))),(E-max (L~ (Cage (C,n)))),(Vertical_Line (((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2)))) `1 by A13, A14, A25, A27, A32, A40, TOPREAL1:3;

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

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

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

(First_Point ((L~ (Upper_Seq (C,n))),(W-min (L~ (Cage (C,n)))),(E-max (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 A13, A14, A25, A27, A32, A40, A41, TOPREAL1:3;

then Center (Gauge (C,n)) <= i2 + 1 by A7, A29, A34, A35, A40, GOBOARD5:3;

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

hence First_Point ((L~ (Upper_Seq (C,n))),(W-min (L~ (Cage (C,n)))),(E-max (L~ (Cage (C,n)))),(Vertical_Line (((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2))) in rng (Upper_Seq (C,n)) by A15, A16, A25, A27, A32, A36, A40, PARTFUN2:2; :: thesis: verum