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