let C be connected compact non horizontal non vertical Subset of (TOP-REAL 2); for n being Element of 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 Element of NAT ; ( 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
; 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:12;
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:31;
A5:
W-bound (L~ (Cage C,n)) < E-bound (L~ (Cage C,n))
by SPRECT_1:33;
then
W-bound (L~ (Cage C,n)) < ((W-bound (L~ (Cage C,n))) + (E-bound (L~ (Cage C,n)))) / 2
by XREAL_1:228;
then A6:
(W-min (L~ (Cage C,n))) `1 <= ((W-bound (L~ (Cage C,n))) + (E-bound (L~ (Cage C,n)))) / 2
by EUCLID:56;
A7:
Center (Gauge C,n) <= len (Gauge C,n)
by JORDAN1B:14;
((W-bound (L~ (Cage C,n))) + (E-bound (L~ (Cage C,n)))) / 2 < E-bound (L~ (Cage C,n))
by A5, XREAL_1:228;
then A8:
((W-bound (L~ (Cage C,n))) + (E-bound (L~ (Cage C,n)))) / 2 <= (E-max (L~ (Cage C,n))) `1
by EUCLID:56;
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:64;
(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:64;
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 Element of 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 5;
t < len (Upper_Seq C,n)
by A12, NAT_1:13;
then A15:
t in dom (Upper_Seq C,n)
by A11, FINSEQ_3:27;
1 <= t + 1
by A11, NAT_1:13;
then A16:
t + 1 in dom (Upper_Seq C,n)
by A12, FINSEQ_3:27;
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:34;
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:33;
now per cases
( LSeg (Upper_Seq C,n),t is vertical or LSeg (Upper_Seq C,n),t is horizontal )
by SPPOL_1:41;
suppose A19:
LSeg (Upper_Seq C,n),
t is
vertical
;
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:64;
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:31, SPPOL_1:40, TOPREAL1:15;
((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:64;
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:23;
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:4;
verum end; suppose
LSeg (Upper_Seq C,n),
t is
horizontal
;
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:36;
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
Element of
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:6;
A29:
1
<= i1
by A24, MATRIX_1:39;
A30:
1
<= i2
by A26, MATRIX_1:39;
A31:
i1 <= len (Gauge C,n)
by A24, MATRIX_1:39;
A32:
j1 = j2
by A22, A24, A25, A26, A27, Th6;
A33:
i2 <= len (Gauge C,n)
by A26, MATRIX_1:39;
A34:
( 1
<= j1 &
j1 <= width (Gauge C,n) )
by A24, MATRIX_1:39;
then A35:
((Gauge C,n) * (Center (Gauge C,n)),j1) `1 =
((W-bound C) + (E-bound C)) / 2
by A1, Th43
.=
(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, Th41
;
((Gauge C,n) * (Center (Gauge C,n)),j1) `2 =
((Gauge C,n) * 1,j1) `2
by A2, A7, A34, GOBOARD5:2
.=
(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:2
;
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:11;
now per cases
( i1 + 1 = i2 or i1 = i2 + 1 )
by A28, A32;
suppose A37:
i1 + 1
= i2
;
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:25;
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:9;
then
i1 <= Center (Gauge C,n)
by A2, A31, A34, A35, GOBOARD5:4;
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:9;
then
Center (Gauge C,n) <= i1 + 1
by A7, A34, A30, A35, A37, GOBOARD5:4;
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:4;
verum end; suppose A40:
i1 = i2 + 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)) 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:25;
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:9;
then
i2 <= Center (Gauge C,n)
by A2, A34, A33, A35, GOBOARD5:4;
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:9;
then
Center (Gauge C,n) <= i2 + 1
by A7, A29, A34, A35, A40, GOBOARD5:4;
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:4;
verum 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)
;
verum 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)
; verum