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