let i, n be Nat; for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2)
for p, x being Point of (TOP-REAL 2) st x in E-most C & p in east_halfline x & 1 <= i & i < len (Cage (C,n)) & p in LSeg ((Cage (C,n)),i) holds
LSeg ((Cage (C,n)),i) is vertical
let C be connected compact non horizontal non vertical Subset of (TOP-REAL 2); for p, x being Point of (TOP-REAL 2) st x in E-most C & p in east_halfline x & 1 <= i & i < len (Cage (C,n)) & p in LSeg ((Cage (C,n)),i) holds
LSeg ((Cage (C,n)),i) is vertical
let p, x be Point of (TOP-REAL 2); ( x in E-most C & p in east_halfline x & 1 <= i & i < len (Cage (C,n)) & p in LSeg ((Cage (C,n)),i) implies LSeg ((Cage (C,n)),i) is vertical )
set G = Gauge (C,n);
set f = Cage (C,n);
assume that
A1:
x in E-most C
and
A2:
p in east_halfline x
and
A3:
1 <= i
and
A4:
i < len (Cage (C,n))
and
A5:
p in LSeg ((Cage (C,n)),i)
; LSeg ((Cage (C,n)),i) is vertical
assume A6:
not LSeg ((Cage (C,n)),i) is vertical
; contradiction
A7:
i + 1 <= len (Cage (C,n))
by A4, NAT_1:13;
then A8:
LSeg ((Cage (C,n)),i) = LSeg (((Cage (C,n)) /. i),((Cage (C,n)) /. (i + 1)))
by A3, TOPREAL1:def 3;
1 <= i + 1
by A3, NAT_1:13;
then
i + 1 in Seg (len (Cage (C,n)))
by A7, FINSEQ_1:1;
then A9:
i + 1 in dom (Cage (C,n))
by FINSEQ_1:def 3;
i in Seg (len (Cage (C,n)))
by A3, A4, FINSEQ_1:1;
then A10:
i in dom (Cage (C,n))
by FINSEQ_1:def 3;
p in L~ (Cage (C,n))
by A5, SPPOL_2:17;
then A11:
p in (east_halfline x) /\ (L~ (Cage (C,n)))
by A2, XBOOLE_0:def 4;
A12:
Cage (C,n) is_sequence_on Gauge (C,n)
by JORDAN9:def 1;
A13: x `2 =
p `2
by A2, TOPREAL1:def 11
.=
((Cage (C,n)) /. i) `2
by A5, A8, A6, SPPOL_1:19, SPPOL_1:40
;
A14: x `2 =
p `2
by A2, TOPREAL1:def 11
.=
((Cage (C,n)) /. (i + 1)) `2
by A5, A8, A6, SPPOL_1:19, SPPOL_1:40
;
A15:
len (Gauge (C,n)) = width (Gauge (C,n))
by JORDAN8:def 1;
then A16:
(len (Gauge (C,n))) -' 1 <= width (Gauge (C,n))
by NAT_D:35;
A17:
x in C
by A1, XBOOLE_0:def 4;
per cases
( ((Cage (C,n)) /. i) `1 <= ((Cage (C,n)) /. (i + 1)) `1 or ((Cage (C,n)) /. i) `1 >= ((Cage (C,n)) /. (i + 1)) `1 )
;
suppose A18:
((Cage (C,n)) /. i) `1 <= ((Cage (C,n)) /. (i + 1)) `1
;
contradictionthen
p `1 <= ((Cage (C,n)) /. (i + 1)) `1
by A5, A8, TOPREAL1:3;
then A19:
((Cage (C,n)) /. (i + 1)) `1 > x `1
by A17, A11, Th75, XXREAL_0:2;
consider i1,
i2 being
Nat such that A20:
[i1,i2] in Indices (Gauge (C,n))
and A21:
(Cage (C,n)) /. (i + 1) = (Gauge (C,n)) * (
i1,
i2)
by A12, A9, GOBOARD1:def 9;
A22:
( 1
<= i2 &
i2 <= width (Gauge (C,n)) )
by A20, MATRIX_0:32;
consider j1,
j2 being
Nat such that A23:
[j1,j2] in Indices (Gauge (C,n))
and A24:
(Cage (C,n)) /. i = (Gauge (C,n)) * (
j1,
j2)
by A12, A10, GOBOARD1:def 9;
A25:
( 1
<= j2 &
j2 <= width (Gauge (C,n)) )
by A23, MATRIX_0:32;
A26:
i1 <= len (Gauge (C,n))
by A20, MATRIX_0:32;
A27:
1
<= i1
by A20, MATRIX_0:32;
now not ((Cage (C,n)) /. i) `1 = ((Cage (C,n)) /. (i + 1)) `1 assume
((Cage (C,n)) /. i) `1 = ((Cage (C,n)) /. (i + 1)) `1
;
contradictionthen A28:
(Cage (C,n)) /. i = (Cage (C,n)) /. (i + 1)
by A14, A13, TOPREAL3:6;
then A29:
i2 = j2
by A20, A21, A23, A24, GOBOARD1:5;
(
i1 = j1 &
|.(i1 - j1).| + |.(i2 - j2).| = 1 )
by A12, A10, A9, A20, A21, A23, A24, A28, GOBOARD1:5, GOBOARD1:def 9;
then 1 =
0 + |.(i2 - j2).|
by GOBOARD7:2
.=
0 + 0
by A29, GOBOARD7:2
;
hence
contradiction
;
verum end; then A30:
((Cage (C,n)) /. i) `1 < ((Cage (C,n)) /. (i + 1)) `1
by A18, XXREAL_0:1;
A31:
1
<= j1
by A23, MATRIX_0:32;
j1 <= len (Gauge (C,n))
by A23, MATRIX_0:32;
then
i1 > j1
by A21, A22, A27, A24, A25, A30, Th18;
then
len (Gauge (C,n)) > j1
by A26, XXREAL_0:2;
then A32:
(len (Gauge (C,n))) -' 1
>= j1
by NAT_D:49;
x `1 =
(E-min C) `1
by A1, PSCOMP_1:47
.=
E-bound C
by EUCLID:52
.=
((Gauge (C,n)) * (((len (Gauge (C,n))) -' 1),i2)) `1
by A15, A22, JORDAN8:12
;
then
x `1 >= ((Cage (C,n)) /. i) `1
by A15, A16, A22, A24, A25, A31, A32, Th18;
then
x in L~ (Cage (C,n))
by A8, A14, A13, A19, GOBOARD7:8, SPPOL_2:17;
then
x in (L~ (Cage (C,n))) /\ C
by A17, XBOOLE_0:def 4;
then
L~ (Cage (C,n)) meets C
;
hence
contradiction
by JORDAN10:5;
verum end; suppose A33:
((Cage (C,n)) /. i) `1 >= ((Cage (C,n)) /. (i + 1)) `1
;
contradictionthen
p `1 <= ((Cage (C,n)) /. i) `1
by A5, A8, TOPREAL1:3;
then A34:
((Cage (C,n)) /. i) `1 > x `1
by A17, A11, Th75, XXREAL_0:2;
consider i1,
i2 being
Nat such that A35:
[i1,i2] in Indices (Gauge (C,n))
and A36:
(Cage (C,n)) /. i = (Gauge (C,n)) * (
i1,
i2)
by A12, A10, GOBOARD1:def 9;
A37:
( 1
<= i2 &
i2 <= width (Gauge (C,n)) )
by A35, MATRIX_0:32;
consider j1,
j2 being
Nat such that A38:
[j1,j2] in Indices (Gauge (C,n))
and A39:
(Cage (C,n)) /. (i + 1) = (Gauge (C,n)) * (
j1,
j2)
by A12, A9, GOBOARD1:def 9;
A40:
( 1
<= j2 &
j2 <= width (Gauge (C,n)) )
by A38, MATRIX_0:32;
A41:
i1 <= len (Gauge (C,n))
by A35, MATRIX_0:32;
A42:
1
<= i1
by A35, MATRIX_0:32;
now not ((Cage (C,n)) /. i) `1 = ((Cage (C,n)) /. (i + 1)) `1 assume
((Cage (C,n)) /. i) `1 = ((Cage (C,n)) /. (i + 1)) `1
;
contradictionthen A43:
(Cage (C,n)) /. i = (Cage (C,n)) /. (i + 1)
by A14, A13, TOPREAL3:6;
then A44:
i2 = j2
by A35, A36, A38, A39, GOBOARD1:5;
(
i1 = j1 &
|.(j1 - i1).| + |.(j2 - i2).| = 1 )
by A12, A10, A9, A35, A36, A38, A39, A43, GOBOARD1:5, GOBOARD1:def 9;
then 1 =
0 + |.(i2 - j2).|
by A44, GOBOARD7:2
.=
0 + 0
by A44, GOBOARD7:2
;
hence
contradiction
;
verum end; then A45:
((Cage (C,n)) /. (i + 1)) `1 < ((Cage (C,n)) /. i) `1
by A33, XXREAL_0:1;
A46:
1
<= j1
by A38, MATRIX_0:32;
j1 <= len (Gauge (C,n))
by A38, MATRIX_0:32;
then
i1 > j1
by A36, A37, A42, A39, A40, A45, Th18;
then
len (Gauge (C,n)) > j1
by A41, XXREAL_0:2;
then A47:
(len (Gauge (C,n))) -' 1
>= j1
by NAT_D:49;
x `1 =
(E-min C) `1
by A1, PSCOMP_1:47
.=
E-bound C
by EUCLID:52
.=
((Gauge (C,n)) * (((len (Gauge (C,n))) -' 1),i2)) `1
by A15, A37, JORDAN8:12
;
then
x `1 >= ((Cage (C,n)) /. (i + 1)) `1
by A15, A16, A37, A39, A40, A46, A47, Th18;
then
x in L~ (Cage (C,n))
by A8, A14, A13, A34, GOBOARD7:8, SPPOL_2:17;
then
x in (L~ (Cage (C,n))) /\ C
by A17, XBOOLE_0:def 4;
then
L~ (Cage (C,n)) meets C
;
hence
contradiction
by JORDAN10:5;
verum end;