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