let n be Nat; for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) ex i being Nat st
( 1 <= i & i < len (Cage (C,n)) & N-max C in right_cell ((Cage (C,n)),i,(Gauge (C,n))) )
let C be connected compact non horizontal non vertical Subset of (TOP-REAL 2); ex i being Nat st
( 1 <= i & i < len (Cage (C,n)) & N-max C in right_cell ((Cage (C,n)),i,(Gauge (C,n))) )
consider p being Point of (TOP-REAL 2) such that
A1:
(north_halfline (N-max C)) /\ (L~ (Cage (C,n))) = {p}
by JORDAN1A:86, PSCOMP_1:42;
A2:
p in (north_halfline (N-max C)) /\ (L~ (Cage (C,n)))
by A1, TARSKI:def 1;
then A3:
p in north_halfline (N-max C)
by XBOOLE_0:def 4;
p in L~ (Cage (C,n))
by A2, XBOOLE_0:def 4;
then consider i being Nat such that
A4:
1 <= i
and
A5:
i + 1 <= len (Cage (C,n))
and
A6:
p in LSeg ((Cage (C,n)),i)
by SPPOL_2:13;
take
i
; ( 1 <= i & i < len (Cage (C,n)) & N-max C in right_cell ((Cage (C,n)),i,(Gauge (C,n))) )
A7:
LSeg ((Cage (C,n)),i) = LSeg (((Cage (C,n)) /. i),((Cage (C,n)) /. (i + 1)))
by A4, A5, TOPREAL1:def 3;
A8:
len (Gauge (C,n)) >= 4
by JORDAN8:10;
then A9:
1 < len (Gauge (C,n))
by XXREAL_0:2;
A10:
((len (Gauge (C,n))) -' 1) + 1 = len (Gauge (C,n))
by A8, XREAL_1:235, XXREAL_0:2;
then A11:
(len (Gauge (C,n))) -' 1 < len (Gauge (C,n))
by NAT_1:13;
A12:
N-max C = |[((N-max C) `1),((N-max C) `2)]|
by EUCLID:53;
A13:
(len (Gauge (C,n))) -' 1 <= len (Gauge (C,n))
by NAT_D:44;
A14: (N-max C) `2 =
N-bound C
by EUCLID:52
.=
((Gauge (C,n)) * (1,((len (Gauge (C,n))) -' 1))) `2
by A9, JORDAN8:14
;
A15:
N-max C in N-most C
by PSCOMP_1:42;
A16:
len (Gauge (C,n)) = width (Gauge (C,n))
by JORDAN8:def 1;
thus A17:
( 1 <= i & i < len (Cage (C,n)) )
by A4, A5, NAT_1:13; N-max C in right_cell ((Cage (C,n)),i,(Gauge (C,n)))
then A18:
((Cage (C,n)) /. i) `2 = p `2
by A3, A6, A15, A7, JORDAN1A:78, SPPOL_1:40;
A19:
((Cage (C,n)) /. (i + 1)) `2 = p `2
by A3, A6, A17, A15, A7, JORDAN1A:78, SPPOL_1:40;
A20:
Cage (C,n) is_sequence_on Gauge (C,n)
by JORDAN9:def 1;
then consider i1, j1, i2, j2 being Nat such that
A21:
[i1,j1] in Indices (Gauge (C,n))
and
A22:
(Cage (C,n)) /. i = (Gauge (C,n)) * (i1,j1)
and
A23:
[i2,j2] in Indices (Gauge (C,n))
and
A24:
(Cage (C,n)) /. (i + 1) = (Gauge (C,n)) * (i2,j2)
and
A25:
( ( i1 = i2 & j1 + 1 = j2 ) or ( i1 + 1 = i2 & j1 = j2 ) or ( i1 = i2 + 1 & j1 = j2 ) or ( i1 = i2 & j1 = j2 + 1 ) )
by A4, A5, JORDAN8:3;
A26:
1 <= i1
by A21, MATRIX_0:32;
A27:
j2 <= width (Gauge (C,n))
by A23, MATRIX_0:32;
A28:
i1 <= len (Gauge (C,n))
by A21, MATRIX_0:32;
A29:
1 <= j1
by A21, MATRIX_0:32;
p `2 = N-bound (L~ (Cage (C,n)))
by A2, JORDAN1A:82, PSCOMP_1:42;
then
((Gauge (C,n)) * (i1,j1)) `2 = ((Gauge (C,n)) * (i1,(len (Gauge (C,n))))) `2
by A22, A18, A26, A28, JORDAN1A:70;
then A30:
len (Gauge (C,n)) <= j1
by A16, A26, A28, A29, GOBOARD5:4;
A31:
j1 <= width (Gauge (C,n))
by A21, MATRIX_0:32;
then A32:
j1 = len (Gauge (C,n))
by A16, A30, XXREAL_0:1;
A33:
1 <= j2
by A23, MATRIX_0:32;
A34:
j1 = j2
proof
assume
j1 <> j2
;
contradiction
then
(
j1 < j2 or
j2 < j1 )
by XXREAL_0:1;
hence
contradiction
by A22, A24, A25, A18, A19, A26, A28, A29, A27, A33, A31, GOBOARD5:4;
verum
end;
A35:
1 <= i2
by A23, MATRIX_0:32;
A36:
i2 <= len (Gauge (C,n))
by A23, MATRIX_0:32;
i1 <= i1 + 1
by NAT_1:11;
then A37:
((Cage (C,n)) /. i) `1 <= ((Cage (C,n)) /. (i + 1)) `1
by A4, A5, A21, A22, A23, A24, A25, A16, A26, A36, A29, A27, A34, A30, JORDAN10:4, JORDAN1A:18;
then
p `1 <= ((Cage (C,n)) /. (i + 1)) `1
by A6, A7, TOPREAL1:3;
then
(N-max C) `1 <= ((Gauge (C,n)) * ((i1 + 1),(len (Gauge (C,n))))) `1
by A3, A4, A5, A21, A22, A23, A24, A25, A16, A34, A32, JORDAN10:4, TOPREAL1:def 10;
then A38:
(N-max C) `1 <= ((Gauge (C,n)) * ((i1 + 1),1)) `1
by A4, A5, A21, A22, A23, A24, A25, A16, A35, A36, A34, A30, A9, GOBOARD5:2, JORDAN10:4;
((Cage (C,n)) /. i) `1 <= p `1
by A6, A7, A37, TOPREAL1:3;
then
((Gauge (C,n)) * (i1,(len (Gauge (C,n))))) `1 <= (N-max C) `1
by A3, A22, A32, TOPREAL1:def 10;
then A39:
((Gauge (C,n)) * (i1,1)) `1 <= (N-max C) `1
by A16, A26, A28, A9, GOBOARD5:2;
len (Gauge (C,n)) >= 1 + 1
by A8, XXREAL_0:2;
then A40:
(len (Gauge (C,n))) - 1 >= 1
by XREAL_1:19;
then
(len (Gauge (C,n))) -' 1 >= 1
by XREAL_0:def 2;
then
((Gauge (C,n)) * (1,j1)) `2 >= (N-max C) `2
by A16, A32, A9, A14, A13, SPRECT_3:12;
then A41:
N-max C in { |[r,s]| where r, s is Real : ( ((Gauge (C,n)) * (i1,1)) `1 <= r & r <= ((Gauge (C,n)) * ((i1 + 1),1)) `1 & ((Gauge (C,n)) * (1,(j1 -' 1))) `2 <= s & s <= ((Gauge (C,n)) * (1,j1)) `2 ) }
by A32, A14, A39, A38, A12;
A42:
1 <= i1
by A21, MATRIX_0:32;
i1 < len (Gauge (C,n))
by A4, A5, A21, A22, A23, A24, A25, A16, A36, A34, A30, JORDAN10:4, NAT_1:13;
then
N-max C in cell ((Gauge (C,n)),i1,(j1 -' 1))
by A16, A32, A42, A40, A10, A11, A41, GOBRD11:32;
hence
N-max C in right_cell ((Cage (C,n)),i,(Gauge (C,n)))
by A4, A5, A20, A21, A22, A23, A24, A25, A16, A34, A30, GOBRD13:24, JORDAN10:4; verum