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)) & W-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)) & W-max C in right_cell ((Cage (C,n)),i,(Gauge (C,n))) )
consider p being Point of (TOP-REAL 2) such that
A1:
(west_halfline (W-max C)) /\ (L~ (Cage (C,n))) = {p}
by JORDAN1A:89, PSCOMP_1:34;
A2:
p in (west_halfline (W-max C)) /\ (L~ (Cage (C,n)))
by A1, TARSKI:def 1;
then A3:
p in west_halfline (W-max C)
by XBOOLE_0:def 4;
A4:
W-max C = |[((W-max C) `1),((W-max C) `2)]|
by EUCLID:53;
A5:
len (Gauge (C,n)) >= 4
by JORDAN8:10;
then A6:
1 < len (Gauge (C,n))
by XXREAL_0:2;
A7: (W-max C) `1 =
W-bound C
by EUCLID:52
.=
((Gauge (C,n)) * (2,1)) `1
by A6, JORDAN8:11
;
A8:
len (Gauge (C,n)) = width (Gauge (C,n))
by JORDAN8:def 1;
A9:
W-max C in W-most C
by PSCOMP_1:34;
p in L~ (Cage (C,n))
by A2, XBOOLE_0:def 4;
then consider i being Nat such that
A10:
1 <= i
and
A11:
i + 1 <= len (Cage (C,n))
and
A12:
p in LSeg ((Cage (C,n)),i)
by SPPOL_2:13;
take
i
; ( 1 <= i & i < len (Cage (C,n)) & W-max C in right_cell ((Cage (C,n)),i,(Gauge (C,n))) )
A13:
LSeg ((Cage (C,n)),i) = LSeg (((Cage (C,n)) /. i),((Cage (C,n)) /. (i + 1)))
by A10, A11, TOPREAL1:def 3;
thus A14:
( 1 <= i & i < len (Cage (C,n)) )
by A10, A11, NAT_1:13; W-max C in right_cell ((Cage (C,n)),i,(Gauge (C,n)))
then A15:
((Cage (C,n)) /. i) `1 = p `1
by A3, A12, A9, A13, JORDAN1A:81, SPPOL_1:41;
A16:
((Cage (C,n)) /. (i + 1)) `1 = p `1
by A3, A12, A14, A9, A13, JORDAN1A:81, SPPOL_1:41;
A17:
Cage (C,n) is_sequence_on Gauge (C,n)
by JORDAN9:def 1;
then consider i1, j1, i2, j2 being Nat such that
A18:
[i1,j1] in Indices (Gauge (C,n))
and
A19:
(Cage (C,n)) /. i = (Gauge (C,n)) * (i1,j1)
and
A20:
[i2,j2] in Indices (Gauge (C,n))
and
A21:
(Cage (C,n)) /. (i + 1) = (Gauge (C,n)) * (i2,j2)
and
A22:
( ( i1 = i2 & j1 + 1 = j2 ) or ( i1 + 1 = i2 & j1 = j2 ) or ( i1 = i2 + 1 & j1 = j2 ) or ( i1 = i2 & j1 = j2 + 1 ) )
by A10, A11, JORDAN8:3;
A23:
i1 <= len (Gauge (C,n))
by A18, MATRIX_0:32;
A24:
i2 <= len (Gauge (C,n))
by A20, MATRIX_0:32;
A25:
j2 <= width (Gauge (C,n))
by A20, MATRIX_0:32;
A26:
j1 <= width (Gauge (C,n))
by A18, MATRIX_0:32;
A27:
1 <= j1
by A18, MATRIX_0:32;
p `1 = W-bound (L~ (Cage (C,n)))
by A2, JORDAN1A:85, PSCOMP_1:34;
then
((Gauge (C,n)) * (i1,j1)) `1 = ((Gauge (C,n)) * (1,j1)) `1
by A19, A15, A8, A27, A26, JORDAN1A:73;
then A28:
1 >= i1
by A23, A27, A26, GOBOARD5:3;
A29:
1 <= i1
by A18, MATRIX_0:32;
then A30:
i1 = 1
by A28, XXREAL_0:1;
A31:
1 <= i2
by A20, MATRIX_0:32;
A32:
i1 = i2
proof
assume
i1 <> i2
;
contradiction
then
(
i1 < i2 or
i2 < i1 )
by XXREAL_0:1;
hence
contradiction
by A19, A21, A22, A15, A16, A29, A23, A31, A24, A27, A25, GOBOARD5:3;
verum
end;
then A33:
j1 < width (Gauge (C,n))
by A10, A11, A18, A19, A20, A21, A22, A25, A28, JORDAN10:2, NAT_1:13;
j1 <= j1 + 1
by NAT_1:11;
then A34:
((Cage (C,n)) /. i) `2 <= ((Cage (C,n)) /. (i + 1)) `2
by A10, A11, A18, A19, A20, A21, A22, A29, A23, A27, A25, A32, A28, JORDAN10:2, JORDAN1A:19;
then
p `2 <= ((Cage (C,n)) /. (i + 1)) `2
by A12, A13, TOPREAL1:4;
then A35:
(W-max C) `2 <= ((Gauge (C,n)) * (1,(j1 + 1))) `2
by A3, A10, A11, A18, A19, A20, A21, A22, A32, A30, JORDAN10:2, TOPREAL1:def 13;
((Cage (C,n)) /. i) `2 <= p `2
by A12, A13, A34, TOPREAL1:4;
then A36:
((Gauge (C,n)) * (1,j1)) `2 <= (W-max C) `2
by A3, A19, A30, TOPREAL1:def 13;
1 + 1 <= len (Gauge (C,n))
by A5, XXREAL_0:2;
then
((Gauge (C,n)) * (i1,1)) `1 <= (W-max C) `1
by A8, A30, A6, A7, SPRECT_3:13;
then
W-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)) `2 <= s & s <= ((Gauge (C,n)) * (1,(j1 + 1))) `2 ) }
by A30, A7, A36, A35, A4;
then
W-max C in cell ((Gauge (C,n)),i1,j1)
by A27, A30, A33, A6, GOBRD11:32;
hence
W-max C in right_cell ((Cage (C,n)),i,(Gauge (C,n)))
by A10, A11, A17, A18, A19, A20, A21, A22, A32, A28, GOBRD13:22, JORDAN10:2; verum