let C be connected compact non horizontal non vertical Subset of (TOP-REAL 2); 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; ( 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: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 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))per cases
( LSeg ((Lower_Seq (C,n)),t) is vertical or LSeg ((Lower_Seq (C,n)),t) is horizontal )
by SPPOL_1:19;
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: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;
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: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;
now 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))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: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;
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: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;
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