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 W-most C & p in west_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 W-most C & p in west_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 W-most C & p in west_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 W-most C
and
A2:
p in west_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;
p in L~ (Cage (C,n))
by A5, SPPOL_2:17;
then A10:
p in (west_halfline x) /\ (L~ (Cage (C,n)))
by A2, XBOOLE_0:def 4;
A11:
Cage (C,n) is_sequence_on Gauge (C,n)
by JORDAN9:def 1;
A12: x `2 =
p `2
by A2, TOPREAL1:def 13
.=
((Cage (C,n)) /. i) `2
by A5, A8, A6, SPPOL_1:19, SPPOL_1:40
;
i in Seg (len (Cage (C,n)))
by A3, A4, FINSEQ_1:1;
then A13:
i in dom (Cage (C,n))
by FINSEQ_1:def 3;
A14: x `2 =
p `2
by A2, TOPREAL1:def 13
.=
((Cage (C,n)) /. (i + 1)) `2
by A5, A8, A6, SPPOL_1:19, SPPOL_1:40
;
A15:
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 A16:
((Cage (C,n)) /. i) `1 <= ((Cage (C,n)) /. (i + 1)) `1
;
contradictionconsider i1,
i2 being
Nat such that A17:
[i1,i2] in Indices (Gauge (C,n))
and A18:
(Cage (C,n)) /. i = (Gauge (C,n)) * (
i1,
i2)
by A11, A13, GOBOARD1:def 9;
A19:
1
<= i2
by A17, MATRIX_0:32;
A20:
i2 <= width (Gauge (C,n))
by A17, MATRIX_0:32;
then A21:
i2 <= len (Gauge (C,n))
by JORDAN8:def 1;
consider j1,
j2 being
Nat such that A22:
[j1,j2] in Indices (Gauge (C,n))
and A23:
(Cage (C,n)) /. (i + 1) = (Gauge (C,n)) * (
j1,
j2)
by A11, A9, GOBOARD1:def 9;
A24:
( 1
<= j2 &
j2 <= width (Gauge (C,n)) )
by A22, 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 A25:
(Cage (C,n)) /. i = (Cage (C,n)) /. (i + 1)
by A14, A12, TOPREAL3:6;
then A26:
i1 = j1
by A17, A18, A22, A23, GOBOARD1:5;
A27:
i2 = j2
by A17, A18, A22, A23, A25, GOBOARD1:5;
|.(i1 - j1).| + |.(i2 - j2).| = 1
by A11, A13, A9, A17, A18, A22, A23, GOBOARD1:def 9;
then 1 =
0 + |.(i2 - j2).|
by A26, GOBOARD7:2
.=
0 + 0
by A27, GOBOARD7:2
;
hence
contradiction
;
verum end; then A28:
((Cage (C,n)) /. i) `1 < ((Cage (C,n)) /. (i + 1)) `1
by A16, XXREAL_0:1;
((Cage (C,n)) /. i) `1 <= p `1
by A5, A8, A16, TOPREAL1:3;
then A29:
((Cage (C,n)) /. i) `1 < x `1
by A15, A10, Th77, XXREAL_0:2;
A30:
1
<= i1
by A17, MATRIX_0:32;
A31:
i1 <= len (Gauge (C,n))
by A17, MATRIX_0:32;
A32:
x `1 =
(W-min C) `1
by A1, PSCOMP_1:31
.=
W-bound C
by EUCLID:52
.=
((Gauge (C,n)) * (2,i2)) `1
by A19, A21, JORDAN8:11
;
then
i1 < 1
+ 1
by A29, A18, A19, A20, A31, SPRECT_3:13;
then A33:
i1 <= 1
by NAT_1:13;
A34:
j1 <= len (Gauge (C,n))
by A22, MATRIX_0:32;
1
<= j1
by A22, MATRIX_0:32;
then
i1 < j1
by A18, A19, A20, A31, A23, A24, A28, Th18;
then
1
< j1
by A30, A33, XXREAL_0:1;
then
1
+ 1
<= j1
by NAT_1:13;
then
x `1 <= ((Cage (C,n)) /. (i + 1)) `1
by A19, A20, A32, A23, A24, A34, Th18;
then
x in L~ (Cage (C,n))
by A8, A14, A12, A29, GOBOARD7:8, SPPOL_2:17;
then
x in (L~ (Cage (C,n))) /\ C
by A15, XBOOLE_0:def 4;
then
L~ (Cage (C,n)) meets C
;
hence
contradiction
by JORDAN10:5;
verum end; suppose A35:
((Cage (C,n)) /. i) `1 >= ((Cage (C,n)) /. (i + 1)) `1
;
contradictionconsider i1,
i2 being
Nat such that A36:
[i1,i2] in Indices (Gauge (C,n))
and A37:
(Cage (C,n)) /. (i + 1) = (Gauge (C,n)) * (
i1,
i2)
by A11, A9, GOBOARD1:def 9;
A38:
1
<= i2
by A36, MATRIX_0:32;
A39:
i2 <= width (Gauge (C,n))
by A36, MATRIX_0:32;
then A40:
i2 <= len (Gauge (C,n))
by JORDAN8:def 1;
consider j1,
j2 being
Nat such that A41:
[j1,j2] in Indices (Gauge (C,n))
and A42:
(Cage (C,n)) /. i = (Gauge (C,n)) * (
j1,
j2)
by A11, A13, GOBOARD1:def 9;
A43:
( 1
<= j2 &
j2 <= width (Gauge (C,n)) )
by A41, 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 A44:
(Cage (C,n)) /. i = (Cage (C,n)) /. (i + 1)
by A14, A12, TOPREAL3:6;
then A45:
i1 = j1
by A36, A37, A41, A42, GOBOARD1:5;
A46:
i2 = j2
by A36, A37, A41, A42, A44, GOBOARD1:5;
|.(j1 - i1).| + |.(j2 - i2).| = 1
by A11, A13, A9, A36, A37, A41, A42, GOBOARD1:def 9;
then 1 =
0 + |.(i2 - j2).|
by A45, A46, GOBOARD7:2
.=
0 + 0
by A46, GOBOARD7:2
;
hence
contradiction
;
verum end; then A47:
((Cage (C,n)) /. (i + 1)) `1 < ((Cage (C,n)) /. i) `1
by A35, XXREAL_0:1;
((Cage (C,n)) /. (i + 1)) `1 <= p `1
by A5, A8, A35, TOPREAL1:3;
then A48:
((Cage (C,n)) /. (i + 1)) `1 < x `1
by A15, A10, Th77, XXREAL_0:2;
A49:
1
<= i1
by A36, MATRIX_0:32;
A50:
i1 <= len (Gauge (C,n))
by A36, MATRIX_0:32;
A51:
x `1 =
(W-min C) `1
by A1, PSCOMP_1:31
.=
W-bound C
by EUCLID:52
.=
((Gauge (C,n)) * (2,i2)) `1
by A38, A40, JORDAN8:11
;
then
i1 < 1
+ 1
by A48, A37, A38, A39, A50, SPRECT_3:13;
then A52:
i1 <= 1
by NAT_1:13;
A53:
j1 <= len (Gauge (C,n))
by A41, MATRIX_0:32;
1
<= j1
by A41, MATRIX_0:32;
then
i1 < j1
by A37, A38, A39, A50, A42, A43, A47, Th18;
then
1
< j1
by A49, A52, XXREAL_0:1;
then
1
+ 1
<= j1
by NAT_1:13;
then
x `1 <= ((Cage (C,n)) /. i) `1
by A38, A39, A51, A42, A43, A53, Th18;
then
x in L~ (Cage (C,n))
by A8, A14, A12, A48, GOBOARD7:8, SPPOL_2:17;
then
x in (L~ (Cage (C,n))) /\ C
by A15, XBOOLE_0:def 4;
then
L~ (Cage (C,n)) meets C
;
hence
contradiction
by JORDAN10:5;
verum end; end;