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 S-most C & p in south_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 S-most C & p in south_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 S-most C & p in south_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 S-most C
and
A2:
p in south_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;
p in L~ (Cage (C,n))
by A5, SPPOL_2:17;
then A10:
p in (south_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 `1 =
p `1
by A2, TOPREAL1:def 12
.=
((Cage (C,n)) /. i) `1
by A5, A8, A6, SPPOL_1:19, SPPOL_1:41
;
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 `1 =
p `1
by A2, TOPREAL1:def 12
.=
((Cage (C,n)) /. (i + 1)) `1
by A5, A8, A6, SPPOL_1:19, SPPOL_1:41
;
A15:
x in C
by A1, XBOOLE_0:def 4;
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 A16:
((Cage (C,n)) /. i) `2 <= ((Cage (C,n)) /. (i + 1)) `2
;
contradictionthen
((Cage (C,n)) /. i) `2 <= p `2
by A5, A8, TOPREAL1:4;
then A17:
((Cage (C,n)) /. i) `2 < x `2
by A15, A10, Th76, XXREAL_0:2;
consider i1,
i2 being
Nat such that A18:
[i1,i2] in Indices (Gauge (C,n))
and A19:
(Cage (C,n)) /. i = (Gauge (C,n)) * (
i1,
i2)
by A11, A13, GOBOARD1:def 9;
A20:
i2 <= width (Gauge (C,n))
by A18, MATRIX_0:32;
A21:
1
<= i2
by A18, MATRIX_0:32;
A22:
( 1
<= i1 &
i1 <= len (Gauge (C,n)) )
by A18, MATRIX_0:32;
A23:
x `2 =
(S-min C) `2
by A1, PSCOMP_1:55
.=
S-bound C
by EUCLID:52
.=
((Gauge (C,n)) * (i1,2)) `2
by A22, JORDAN8:13
;
then
i2 < 1
+ 1
by A17, A19, A20, A22, SPRECT_3:12;
then A24:
i2 <= 1
by NAT_1:13;
consider j1,
j2 being
Nat such that A25:
[j1,j2] in Indices (Gauge (C,n))
and A26:
(Cage (C,n)) /. (i + 1) = (Gauge (C,n)) * (
j1,
j2)
by A11, A9, GOBOARD1:def 9;
A27:
j2 <= width (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 A14, A12, TOPREAL3:6;
then A29:
i1 = j1
by A18, A19, A25, A26, GOBOARD1:5;
A30:
i2 = j2
by A18, A19, A25, A26, A28, GOBOARD1:5;
|.(i1 - j1).| + |.(i2 - j2).| = 1
by A11, A13, A9, A18, A19, A25, A26, GOBOARD1:def 9;
then 1 =
0 + |.(i2 - j2).|
by A29, GOBOARD7:2
.=
0 + 0
by A30, GOBOARD7:2
;
hence
contradiction
;
verum end; then A31:
((Cage (C,n)) /. i) `2 < ((Cage (C,n)) /. (i + 1)) `2
by A16, XXREAL_0:1;
A32:
( 1
<= j1 &
j1 <= len (Gauge (C,n)) )
by A25, MATRIX_0:32;
1
<= j2
by A25, MATRIX_0:32;
then
i2 < j2
by A19, A20, A22, A26, A32, A31, Th19;
then
1
< j2
by A21, A24, XXREAL_0:1;
then
1
+ 1
<= j2
by NAT_1:13;
then
x `2 <= ((Cage (C,n)) /. (i + 1)) `2
by A22, A23, A26, A27, A32, Th19;
then
x in L~ (Cage (C,n))
by A8, A14, A12, A17, GOBOARD7:7, 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 A33:
((Cage (C,n)) /. i) `2 >= ((Cage (C,n)) /. (i + 1)) `2
;
contradictionthen
((Cage (C,n)) /. (i + 1)) `2 <= p `2
by A5, A8, TOPREAL1:4;
then A34:
((Cage (C,n)) /. (i + 1)) `2 < x `2
by A15, A10, Th76, XXREAL_0:2;
consider i1,
i2 being
Nat such that A35:
[i1,i2] in Indices (Gauge (C,n))
and A36:
(Cage (C,n)) /. (i + 1) = (Gauge (C,n)) * (
i1,
i2)
by A11, A9, GOBOARD1:def 9;
A37:
i2 <= width (Gauge (C,n))
by A35, MATRIX_0:32;
A38:
1
<= i2
by A35, MATRIX_0:32;
A39:
( 1
<= i1 &
i1 <= len (Gauge (C,n)) )
by A35, MATRIX_0:32;
A40:
x `2 =
(S-min C) `2
by A1, PSCOMP_1:55
.=
S-bound C
by EUCLID:52
.=
((Gauge (C,n)) * (i1,2)) `2
by A39, JORDAN8:13
;
then
i2 < 1
+ 1
by A34, A36, A37, A39, SPRECT_3:12;
then A41:
i2 <= 1
by NAT_1:13;
consider j1,
j2 being
Nat such that A42:
[j1,j2] in Indices (Gauge (C,n))
and A43:
(Cage (C,n)) /. i = (Gauge (C,n)) * (
j1,
j2)
by A11, A13, GOBOARD1:def 9;
A44:
j2 <= width (Gauge (C,n))
by A42, 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 A45:
(Cage (C,n)) /. i = (Cage (C,n)) /. (i + 1)
by A14, A12, TOPREAL3:6;
then A46:
i1 = j1
by A35, A36, A42, A43, GOBOARD1:5;
A47:
i2 = j2
by A35, A36, A42, A43, A45, GOBOARD1:5;
|.(j1 - i1).| + |.(j2 - i2).| = 1
by A11, A13, A9, A35, A36, A42, A43, GOBOARD1:def 9;
then 1 =
0 + |.(i2 - j2).|
by A46, A47, GOBOARD7:2
.=
0 + 0
by A47, GOBOARD7:2
;
hence
contradiction
;
verum end; then A48:
((Cage (C,n)) /. (i + 1)) `2 < ((Cage (C,n)) /. i) `2
by A33, XXREAL_0:1;
A49:
( 1
<= j1 &
j1 <= len (Gauge (C,n)) )
by A42, MATRIX_0:32;
1
<= j2
by A42, MATRIX_0:32;
then
i2 < j2
by A36, A37, A39, A43, A49, A48, Th19;
then
1
< j2
by A38, A41, XXREAL_0:1;
then
1
+ 1
<= j2
by NAT_1:13;
then
x `2 <= ((Cage (C,n)) /. i) `2
by A39, A40, A43, A44, A49, Th19;
then
x in L~ (Cage (C,n))
by A8, A14, A12, A34, GOBOARD7:7, 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;