:: JORDAN1F semantic presentation
begin
theorem Th1: :: JORDAN1F:1
for i, j, k being Element of NAT
for f being FinSequence of the carrier of (TOP-REAL 2)
for G being Go-board st f is_sequence_on G & LSeg ((G * (i,j)),(G * (i,k))) meets L~ f & [i,j] in Indices G & [i,k] in Indices G & j <= k holds
ex n being Element of NAT st
( j <= n & n <= k & (G * (i,n)) `2 = lower_bound (proj2 .: ((LSeg ((G * (i,j)),(G * (i,k)))) /\ (L~ f))) )
proof
let i, j, k be Element of NAT ; ::_thesis: for f being FinSequence of the carrier of (TOP-REAL 2)
for G being Go-board st f is_sequence_on G & LSeg ((G * (i,j)),(G * (i,k))) meets L~ f & [i,j] in Indices G & [i,k] in Indices G & j <= k holds
ex n being Element of NAT st
( j <= n & n <= k & (G * (i,n)) `2 = lower_bound (proj2 .: ((LSeg ((G * (i,j)),(G * (i,k)))) /\ (L~ f))) )
let f be FinSequence of the carrier of (TOP-REAL 2); ::_thesis: for G being Go-board st f is_sequence_on G & LSeg ((G * (i,j)),(G * (i,k))) meets L~ f & [i,j] in Indices G & [i,k] in Indices G & j <= k holds
ex n being Element of NAT st
( j <= n & n <= k & (G * (i,n)) `2 = lower_bound (proj2 .: ((LSeg ((G * (i,j)),(G * (i,k)))) /\ (L~ f))) )
let G be Go-board; ::_thesis: ( f is_sequence_on G & LSeg ((G * (i,j)),(G * (i,k))) meets L~ f & [i,j] in Indices G & [i,k] in Indices G & j <= k implies ex n being Element of NAT st
( j <= n & n <= k & (G * (i,n)) `2 = lower_bound (proj2 .: ((LSeg ((G * (i,j)),(G * (i,k)))) /\ (L~ f))) ) )
set X = (LSeg ((G * (i,j)),(G * (i,k)))) /\ (L~ f);
assume that
A1: f is_sequence_on G and
A2: LSeg ((G * (i,j)),(G * (i,k))) meets L~ f and
A3: [i,j] in Indices G and
A4: [i,k] in Indices G and
A5: j <= k ; ::_thesis: ex n being Element of NAT st
( j <= n & n <= k & (G * (i,n)) `2 = lower_bound (proj2 .: ((LSeg ((G * (i,j)),(G * (i,k)))) /\ (L~ f))) )
A6: ( 1 <= i & i <= len G ) by A3, MATRIX_1:38;
ex x being set st
( x in LSeg ((G * (i,j)),(G * (i,k))) & x in L~ f ) by A2, XBOOLE_0:3;
then reconsider X1 = (LSeg ((G * (i,j)),(G * (i,k)))) /\ (L~ f) as non empty compact Subset of (TOP-REAL 2) by XBOOLE_0:def_4;
consider p being set such that
A7: p in S-most X1 by XBOOLE_0:def_1;
reconsider p = p as Point of (TOP-REAL 2) by A7;
A8: p in (LSeg ((G * (i,j)),(G * (i,k)))) /\ (L~ f) by A7, XBOOLE_0:def_4;
then A9: p in LSeg ((G * (i,j)),(G * (i,k))) by XBOOLE_0:def_4;
proj2 .: ((LSeg ((G * (i,j)),(G * (i,k)))) /\ (L~ f)) = (proj2 | ((LSeg ((G * (i,j)),(G * (i,k)))) /\ (L~ f))) .: ((LSeg ((G * (i,j)),(G * (i,k)))) /\ (L~ f)) by RELAT_1:129;
then A10: lower_bound (proj2 .: ((LSeg ((G * (i,j)),(G * (i,k)))) /\ (L~ f))) = lower_bound ((proj2 | ((LSeg ((G * (i,j)),(G * (i,k)))) /\ (L~ f))) .: ([#] ((TOP-REAL 2) | ((LSeg ((G * (i,j)),(G * (i,k)))) /\ (L~ f))))) by PRE_TOPC:def_5
.= S-bound ((LSeg ((G * (i,j)),(G * (i,k)))) /\ (L~ f)) ;
A11: 1 <= k by A4, MATRIX_1:38;
A12: p `2 = (S-min ((LSeg ((G * (i,j)),(G * (i,k)))) /\ (L~ f))) `2 by A7, PSCOMP_1:55
.= lower_bound (proj2 .: ((LSeg ((G * (i,j)),(G * (i,k)))) /\ (L~ f))) by A10, EUCLID:52 ;
A13: ( 1 <= i & i <= len G ) by A3, MATRIX_1:38;
A14: 1 <= j by A3, MATRIX_1:38;
A15: k <= width G by A4, MATRIX_1:38;
then A16: (G * (i,j)) `2 <= (G * (i,k)) `2 by A5, A6, A14, SPRECT_3:12;
then A17: (G * (i,j)) `2 <= p `2 by A9, TOPREAL1:4;
A18: p `2 <= (G * (i,k)) `2 by A9, A16, TOPREAL1:4;
A19: j <= width G by A3, MATRIX_1:38;
then A20: (G * (i,j)) `1 = (G * (i,1)) `1 by A6, A14, GOBOARD5:2
.= (G * (i,k)) `1 by A13, A11, A15, GOBOARD5:2 ;
p in L~ f by A8, XBOOLE_0:def_4;
then p in union { (LSeg (f,k1)) where k1 is Element of NAT : ( 1 <= k1 & k1 + 1 <= len f ) } by TOPREAL1:def_4;
then consider Y being set such that
A21: p in Y and
A22: Y in { (LSeg (f,k1)) where k1 is Element of NAT : ( 1 <= k1 & k1 + 1 <= len f ) } by TARSKI:def_4;
consider i1 being Element of NAT such that
A23: Y = LSeg (f,i1) and
A24: 1 <= i1 and
A25: i1 + 1 <= len f by A22;
A26: p in LSeg ((f /. i1),(f /. (i1 + 1))) by A21, A23, A24, A25, TOPREAL1:def_3;
1 < i1 + 1 by A24, NAT_1:13;
then i1 + 1 in Seg (len f) by A25, FINSEQ_1:1;
then A27: i1 + 1 in dom f by FINSEQ_1:def_3;
then consider io, jo being Element of NAT such that
A28: [io,jo] in Indices G and
A29: f /. (i1 + 1) = G * (io,jo) by A1, GOBOARD1:def_9;
A30: ( 1 <= io & io <= len G ) by A28, MATRIX_1:38;
A31: 1 <= jo by A28, MATRIX_1:38;
i1 <= len f by A25, NAT_1:13;
then i1 in Seg (len f) by A24, FINSEQ_1:1;
then A32: i1 in dom f by FINSEQ_1:def_3;
then consider i0, j0 being Element of NAT such that
A33: [i0,j0] in Indices G and
A34: f /. i1 = G * (i0,j0) by A1, GOBOARD1:def_9;
A35: ( 1 <= i0 & i0 <= len G ) by A33, MATRIX_1:38;
A36: 1 <= j0 by A33, MATRIX_1:38;
A37: j0 <= width G by A33, MATRIX_1:38;
A38: jo <= width G by A28, MATRIX_1:38;
A39: f is special by A1, A32, JORDAN8:4, RELAT_1:38;
ex n being Element of NAT st
( j <= n & n <= k & G * (i,n) = p )
proof
percases ( (f /. i1) `1 = (f /. (i1 + 1)) `1 or (f /. i1) `2 = (f /. (i1 + 1)) `2 ) by A24, A25, A39, TOPREAL1:def_5;
supposeA40: (f /. i1) `1 = (f /. (i1 + 1)) `1 ; ::_thesis: ex n being Element of NAT st
( j <= n & n <= k & G * (i,n) = p )
(G * (io,j)) `1 = (G * (io,1)) `1 by A14, A19, A30, GOBOARD5:2
.= (G * (io,jo)) `1 by A30, A31, A38, GOBOARD5:2
.= p `1 by A26, A29, A40, GOBOARD7:5
.= (G * (i,j)) `1 by A20, A9, GOBOARD7:5 ;
then ( io <= i & io >= i ) by A6, A14, A19, A30, GOBOARD5:3;
then A41: i = io by XXREAL_0:1;
(G * (i0,j)) `1 = (G * (i0,1)) `1 by A14, A19, A35, GOBOARD5:2
.= (G * (i0,j0)) `1 by A35, A36, A37, GOBOARD5:2
.= p `1 by A26, A34, A40, GOBOARD7:5
.= (G * (i,j)) `1 by A20, A9, GOBOARD7:5 ;
then ( i0 <= i & i0 >= i ) by A6, A14, A19, A35, GOBOARD5:3;
then A42: i = i0 by XXREAL_0:1;
thus ex n being Element of NAT st
( j <= n & n <= k & G * (i,n) = p ) ::_thesis: verum
proof
percases ( (f /. i1) `2 <= (f /. (i1 + 1)) `2 or (f /. i1) `2 > (f /. (i1 + 1)) `2 ) ;
supposeA43: (f /. i1) `2 <= (f /. (i1 + 1)) `2 ; ::_thesis: ex n being Element of NAT st
( j <= n & n <= k & G * (i,n) = p )
thus ex n being Element of NAT st
( j <= n & n <= k & G * (i,n) = p ) ::_thesis: verum
proof
percases ( f /. i1 in LSeg ((G * (i,j)),(G * (i,k))) or not f /. i1 in LSeg ((G * (i,j)),(G * (i,k))) ) ;
supposeA44: f /. i1 in LSeg ((G * (i,j)),(G * (i,k))) ; ::_thesis: ex n being Element of NAT st
( j <= n & n <= k & G * (i,n) = p )
1 + 1 <= i1 + 1 by A24, XREAL_1:6;
then f /. i1 in L~ f by A25, A32, GOBOARD1:1, XXREAL_0:2;
then f /. i1 in X1 by A44, XBOOLE_0:def_4;
then A45: p `2 <= (f /. i1) `2 by A10, A12, PSCOMP_1:24;
take n = j0; ::_thesis: ( j <= n & n <= k & G * (i,n) = p )
A46: p in LSeg ((G * (i,j)),(G * (i,k))) by A8, XBOOLE_0:def_4;
p `2 >= (f /. i1) `2 by A26, A43, TOPREAL1:4;
then p `2 = (f /. i1) `2 by A45, XXREAL_0:1;
then A47: p `2 = (G * (1,j0)) `2 by A34, A35, A36, A37, GOBOARD5:1
.= (G * (i,n)) `2 by A6, A36, A37, GOBOARD5:1 ;
A48: (G * (i,j)) `2 <= (G * (i,k)) `2 by A5, A6, A14, A15, SPRECT_3:12;
then (G * (i,j)) `2 <= (G * (i,n)) `2 by A46, A47, TOPREAL1:4;
hence j <= n by A6, A19, A36, GOBOARD5:4; ::_thesis: ( n <= k & G * (i,n) = p )
(G * (i,n)) `2 <= (G * (i,k)) `2 by A46, A47, A48, TOPREAL1:4;
hence n <= k by A13, A11, A37, GOBOARD5:4; ::_thesis: G * (i,n) = p
p `1 = (G * (i,j)) `1 by A20, A46, GOBOARD7:5
.= (G * (i,1)) `1 by A6, A14, A19, GOBOARD5:2
.= (G * (i,n)) `1 by A6, A36, A37, GOBOARD5:2 ;
hence G * (i,n) = p by A47, TOPREAL3:6; ::_thesis: verum
end;
supposeA49: not f /. i1 in LSeg ((G * (i,j)),(G * (i,k))) ; ::_thesis: ex n being Element of NAT st
( j <= n & n <= k & G * (i,n) = p )
A50: (f /. i1) `1 = p `1 by A26, A40, GOBOARD7:5
.= (G * (i,j)) `1 by A20, A9, GOBOARD7:5 ;
thus ex n being Element of NAT st
( j <= n & n <= k & G * (i,n) = p ) ::_thesis: verum
proof
percases ( (f /. i1) `2 < (G * (i,j)) `2 or (f /. i1) `2 > (G * (i,k)) `2 ) by A20, A49, A50, GOBOARD7:7;
supposeA51: (f /. i1) `2 < (G * (i,j)) `2 ; ::_thesis: ex n being Element of NAT st
( j <= n & n <= k & G * (i,n) = p )
p `2 <= (G * (io,jo)) `2 by A26, A29, A43, TOPREAL1:4;
then p `2 <= (G * (1,jo)) `2 by A30, A31, A38, GOBOARD5:1;
then p `2 <= (G * (i,jo)) `2 by A6, A31, A38, GOBOARD5:1;
then (G * (i,j)) `2 <= (G * (i,jo)) `2 by A17, XXREAL_0:2;
then A52: j <= jo by A6, A19, A31, GOBOARD5:4;
(abs (i0 - io)) + (abs (j0 - jo)) = 1 by A1, A32, A27, A33, A34, A28, A29, GOBOARD1:def_9;
then 0 + (abs (j0 - jo)) = 1 by A42, A41, ABSVALUE:2;
then A53: abs (- (j0 - jo)) = 1 by COMPLEX1:52;
j0 <= jo + 0 by A34, A29, A35, A37, A31, A42, A41, A43, GOBOARD5:4;
then j0 - jo <= 0 by XREAL_1:20;
then jo - j0 = 1 by A53, ABSVALUE:def_1;
then A54: j0 + 1 = jo + 0 ;
( (G * (i,j0)) `2 < (G * (i,j)) `2 & j0 <= j ) by A34, A6, A14, A37, A42, A51, GOBOARD5:4;
then j0 < j by XXREAL_0:1;
then jo <= j by A54, NAT_1:13;
then A55: j = jo by A52, XXREAL_0:1;
take n = jo; ::_thesis: ( j <= n & n <= k & G * (i,n) = p )
A56: p `1 = (G * (i,j)) `1 by A20, A9, GOBOARD7:5
.= (G * (i,1)) `1 by A6, A14, A19, GOBOARD5:2
.= (G * (i,n)) `1 by A6, A31, A38, GOBOARD5:2 ;
p `2 <= (G * (io,jo)) `2 by A26, A29, A43, TOPREAL1:4;
then p `2 <= (G * (1,jo)) `2 by A30, A31, A38, GOBOARD5:1;
then p `2 <= (G * (i,jo)) `2 by A6, A31, A38, GOBOARD5:1;
then p `2 = (G * (i,j)) `2 by A17, A55, XXREAL_0:1;
hence ( j <= n & n <= k & G * (i,n) = p ) by A5, A55, A56, TOPREAL3:6; ::_thesis: verum
end;
supposeA57: (f /. i1) `2 > (G * (i,k)) `2 ; ::_thesis: ex n being Element of NAT st
( j <= n & n <= k & G * (i,n) = p )
p `2 >= (f /. i1) `2 by A26, A43, TOPREAL1:4;
hence ex n being Element of NAT st
( j <= n & n <= k & G * (i,n) = p ) by A18, A57, XXREAL_0:2; ::_thesis: verum
end;
end;
end;
end;
end;
end;
end;
supposeA58: (f /. i1) `2 > (f /. (i1 + 1)) `2 ; ::_thesis: ex n being Element of NAT st
( j <= n & n <= k & G * (i,n) = p )
thus ex n being Element of NAT st
( j <= n & n <= k & G * (i,n) = p ) ::_thesis: verum
proof
percases ( f /. (i1 + 1) in LSeg ((G * (i,j)),(G * (i,k))) or not f /. (i1 + 1) in LSeg ((G * (i,j)),(G * (i,k))) ) ;
supposeA59: f /. (i1 + 1) in LSeg ((G * (i,j)),(G * (i,k))) ; ::_thesis: ex n being Element of NAT st
( j <= n & n <= k & G * (i,n) = p )
1 + 1 <= i1 + 1 by A24, XREAL_1:6;
then f /. (i1 + 1) in L~ f by A25, A27, GOBOARD1:1, XXREAL_0:2;
then f /. (i1 + 1) in X1 by A59, XBOOLE_0:def_4;
then A60: p `2 <= (f /. (i1 + 1)) `2 by A10, A12, PSCOMP_1:24;
take n = jo; ::_thesis: ( j <= n & n <= k & G * (i,n) = p )
A61: p in LSeg ((G * (i,j)),(G * (i,k))) by A8, XBOOLE_0:def_4;
p `2 >= (f /. (i1 + 1)) `2 by A26, A58, TOPREAL1:4;
then p `2 = (f /. (i1 + 1)) `2 by A60, XXREAL_0:1;
then A62: p `2 = (G * (1,jo)) `2 by A29, A30, A31, A38, GOBOARD5:1
.= (G * (i,n)) `2 by A6, A31, A38, GOBOARD5:1 ;
A63: (G * (i,j)) `2 <= (G * (i,k)) `2 by A5, A6, A14, A15, SPRECT_3:12;
then (G * (i,j)) `2 <= (G * (i,n)) `2 by A61, A62, TOPREAL1:4;
hence j <= n by A6, A19, A31, GOBOARD5:4; ::_thesis: ( n <= k & G * (i,n) = p )
(G * (i,n)) `2 <= (G * (i,k)) `2 by A61, A62, A63, TOPREAL1:4;
hence n <= k by A13, A11, A38, GOBOARD5:4; ::_thesis: G * (i,n) = p
p `1 = (G * (i,j)) `1 by A20, A61, GOBOARD7:5
.= (G * (i,1)) `1 by A6, A14, A19, GOBOARD5:2
.= (G * (i,n)) `1 by A6, A31, A38, GOBOARD5:2 ;
hence G * (i,n) = p by A62, TOPREAL3:6; ::_thesis: verum
end;
supposeA64: not f /. (i1 + 1) in LSeg ((G * (i,j)),(G * (i,k))) ; ::_thesis: ex n being Element of NAT st
( j <= n & n <= k & G * (i,n) = p )
A65: (f /. (i1 + 1)) `1 = p `1 by A26, A40, GOBOARD7:5
.= (G * (i,j)) `1 by A20, A9, GOBOARD7:5 ;
thus ex n being Element of NAT st
( j <= n & n <= k & G * (i,n) = p ) ::_thesis: verum
proof
percases ( (f /. (i1 + 1)) `2 < (G * (i,j)) `2 or (f /. (i1 + 1)) `2 > (G * (i,k)) `2 ) by A20, A64, A65, GOBOARD7:7;
supposeA66: (f /. (i1 + 1)) `2 < (G * (i,j)) `2 ; ::_thesis: ex n being Element of NAT st
( j <= n & n <= k & G * (i,n) = p )
p `2 <= (G * (i0,j0)) `2 by A26, A34, A58, TOPREAL1:4;
then p `2 <= (G * (1,j0)) `2 by A35, A36, A37, GOBOARD5:1;
then p `2 <= (G * (i,j0)) `2 by A6, A36, A37, GOBOARD5:1;
then (G * (i,j)) `2 <= (G * (i,j0)) `2 by A17, XXREAL_0:2;
then A67: j <= j0 by A6, A19, A36, GOBOARD5:4;
jo <= j0 + 0 by A34, A29, A35, A36, A38, A42, A41, A58, GOBOARD5:4;
then jo - j0 <= 0 by XREAL_1:20;
then A68: - (jo - j0) >= - 0 ;
(abs (i0 - io)) + (abs (j0 - jo)) = 1 by A1, A32, A27, A33, A34, A28, A29, GOBOARD1:def_9;
then 0 + (abs (j0 - jo)) = 1 by A42, A41, ABSVALUE:2;
then j0 - jo = 1 by A68, ABSVALUE:def_1;
then A69: jo + 1 = j0 - 0 ;
( (G * (i,jo)) `2 < (G * (i,j)) `2 & jo <= j ) by A29, A6, A14, A38, A41, A66, GOBOARD5:4;
then jo < j by XXREAL_0:1;
then j0 <= j by A69, NAT_1:13;
then A70: j = j0 by A67, XXREAL_0:1;
take n = j0; ::_thesis: ( j <= n & n <= k & G * (i,n) = p )
A71: p `1 = (G * (i,j)) `1 by A20, A9, GOBOARD7:5
.= (G * (i,1)) `1 by A6, A14, A19, GOBOARD5:2
.= (G * (i,n)) `1 by A6, A36, A37, GOBOARD5:2 ;
p `2 <= (G * (i0,j0)) `2 by A26, A34, A58, TOPREAL1:4;
then p `2 <= (G * (1,j0)) `2 by A35, A36, A37, GOBOARD5:1;
then p `2 <= (G * (i,j0)) `2 by A6, A36, A37, GOBOARD5:1;
then p `2 = (G * (i,j)) `2 by A17, A70, XXREAL_0:1;
hence ( j <= n & n <= k & G * (i,n) = p ) by A5, A70, A71, TOPREAL3:6; ::_thesis: verum
end;
supposeA72: (f /. (i1 + 1)) `2 > (G * (i,k)) `2 ; ::_thesis: ex n being Element of NAT st
( j <= n & n <= k & G * (i,n) = p )
p `2 >= (f /. (i1 + 1)) `2 by A26, A58, TOPREAL1:4;
hence ex n being Element of NAT st
( j <= n & n <= k & G * (i,n) = p ) by A18, A72, XXREAL_0:2; ::_thesis: verum
end;
end;
end;
end;
end;
end;
end;
end;
end;
end;
supposeA73: (f /. i1) `2 = (f /. (i1 + 1)) `2 ; ::_thesis: ex n being Element of NAT st
( j <= n & n <= k & G * (i,n) = p )
take n = j0; ::_thesis: ( j <= n & n <= k & G * (i,n) = p )
p `2 = (f /. i1) `2 by A26, A73, GOBOARD7:6;
then A74: p `2 = (G * (1,j0)) `2 by A34, A35, A36, A37, GOBOARD5:1
.= (G * (i,n)) `2 by A6, A36, A37, GOBOARD5:1 ;
A75: (G * (i,j)) `2 <= (G * (i,k)) `2 by A5, A6, A14, A15, SPRECT_3:12;
then (G * (i,j)) `2 <= (G * (i,n)) `2 by A9, A74, TOPREAL1:4;
hence j <= n by A6, A19, A36, GOBOARD5:4; ::_thesis: ( n <= k & G * (i,n) = p )
(G * (i,n)) `2 <= (G * (i,k)) `2 by A9, A74, A75, TOPREAL1:4;
hence n <= k by A13, A11, A37, GOBOARD5:4; ::_thesis: G * (i,n) = p
p `1 = (G * (i,j)) `1 by A20, A9, GOBOARD7:5
.= (G * (i,1)) `1 by A6, A14, A19, GOBOARD5:2
.= (G * (i,n)) `1 by A6, A36, A37, GOBOARD5:2 ;
hence G * (i,n) = p by A74, TOPREAL3:6; ::_thesis: verum
end;
end;
end;
hence ex n being Element of NAT st
( j <= n & n <= k & (G * (i,n)) `2 = lower_bound (proj2 .: ((LSeg ((G * (i,j)),(G * (i,k)))) /\ (L~ f))) ) by A12; ::_thesis: verum
end;
theorem :: JORDAN1F:2
for i, j, k being Element of NAT
for f being FinSequence of the carrier of (TOP-REAL 2)
for G being Go-board st f is_sequence_on G & LSeg ((G * (i,j)),(G * (i,k))) meets L~ f & [i,j] in Indices G & [i,k] in Indices G & j <= k holds
ex n being Element of NAT st
( j <= n & n <= k & (G * (i,n)) `2 = upper_bound (proj2 .: ((LSeg ((G * (i,j)),(G * (i,k)))) /\ (L~ f))) )
proof
let i, j, k be Element of NAT ; ::_thesis: for f being FinSequence of the carrier of (TOP-REAL 2)
for G being Go-board st f is_sequence_on G & LSeg ((G * (i,j)),(G * (i,k))) meets L~ f & [i,j] in Indices G & [i,k] in Indices G & j <= k holds
ex n being Element of NAT st
( j <= n & n <= k & (G * (i,n)) `2 = upper_bound (proj2 .: ((LSeg ((G * (i,j)),(G * (i,k)))) /\ (L~ f))) )
let f be FinSequence of the carrier of (TOP-REAL 2); ::_thesis: for G being Go-board st f is_sequence_on G & LSeg ((G * (i,j)),(G * (i,k))) meets L~ f & [i,j] in Indices G & [i,k] in Indices G & j <= k holds
ex n being Element of NAT st
( j <= n & n <= k & (G * (i,n)) `2 = upper_bound (proj2 .: ((LSeg ((G * (i,j)),(G * (i,k)))) /\ (L~ f))) )
let G be Go-board; ::_thesis: ( f is_sequence_on G & LSeg ((G * (i,j)),(G * (i,k))) meets L~ f & [i,j] in Indices G & [i,k] in Indices G & j <= k implies ex n being Element of NAT st
( j <= n & n <= k & (G * (i,n)) `2 = upper_bound (proj2 .: ((LSeg ((G * (i,j)),(G * (i,k)))) /\ (L~ f))) ) )
set X = (LSeg ((G * (i,j)),(G * (i,k)))) /\ (L~ f);
assume that
A1: f is_sequence_on G and
A2: LSeg ((G * (i,j)),(G * (i,k))) meets L~ f and
A3: [i,j] in Indices G and
A4: [i,k] in Indices G and
A5: j <= k ; ::_thesis: ex n being Element of NAT st
( j <= n & n <= k & (G * (i,n)) `2 = upper_bound (proj2 .: ((LSeg ((G * (i,j)),(G * (i,k)))) /\ (L~ f))) )
A6: ( 1 <= i & i <= len G ) by A3, MATRIX_1:38;
ex x being set st
( x in LSeg ((G * (i,j)),(G * (i,k))) & x in L~ f ) by A2, XBOOLE_0:3;
then reconsider X1 = (LSeg ((G * (i,j)),(G * (i,k)))) /\ (L~ f) as non empty compact Subset of (TOP-REAL 2) by XBOOLE_0:def_4;
consider p being set such that
A7: p in N-most X1 by XBOOLE_0:def_1;
reconsider p = p as Point of (TOP-REAL 2) by A7;
A8: p in (LSeg ((G * (i,j)),(G * (i,k)))) /\ (L~ f) by A7, XBOOLE_0:def_4;
then A9: p in LSeg ((G * (i,j)),(G * (i,k))) by XBOOLE_0:def_4;
p in L~ f by A8, XBOOLE_0:def_4;
then p in union { (LSeg (f,k1)) where k1 is Element of NAT : ( 1 <= k1 & k1 + 1 <= len f ) } by TOPREAL1:def_4;
then consider Y being set such that
A10: p in Y and
A11: Y in { (LSeg (f,k1)) where k1 is Element of NAT : ( 1 <= k1 & k1 + 1 <= len f ) } by TARSKI:def_4;
consider i1 being Element of NAT such that
A12: Y = LSeg (f,i1) and
A13: 1 <= i1 and
A14: i1 + 1 <= len f by A11;
A15: p in LSeg ((f /. i1),(f /. (i1 + 1))) by A10, A12, A13, A14, TOPREAL1:def_3;
proj2 .: ((LSeg ((G * (i,j)),(G * (i,k)))) /\ (L~ f)) = (proj2 | ((LSeg ((G * (i,j)),(G * (i,k)))) /\ (L~ f))) .: ((LSeg ((G * (i,j)),(G * (i,k)))) /\ (L~ f)) by RELAT_1:129;
then A16: upper_bound (proj2 .: ((LSeg ((G * (i,j)),(G * (i,k)))) /\ (L~ f))) = upper_bound ((proj2 | ((LSeg ((G * (i,j)),(G * (i,k)))) /\ (L~ f))) .: ([#] ((TOP-REAL 2) | ((LSeg ((G * (i,j)),(G * (i,k)))) /\ (L~ f))))) by PRE_TOPC:def_5
.= N-bound ((LSeg ((G * (i,j)),(G * (i,k)))) /\ (L~ f)) ;
A17: 1 <= k by A4, MATRIX_1:38;
A18: 1 <= j by A3, MATRIX_1:38;
1 < i1 + 1 by A13, NAT_1:13;
then i1 + 1 in Seg (len f) by A14, FINSEQ_1:1;
then A19: i1 + 1 in dom f by FINSEQ_1:def_3;
then consider io, jo being Element of NAT such that
A20: [io,jo] in Indices G and
A21: f /. (i1 + 1) = G * (io,jo) by A1, GOBOARD1:def_9;
A22: ( 1 <= io & io <= len G ) by A20, MATRIX_1:38;
A23: 1 <= jo by A20, MATRIX_1:38;
A24: p `2 = (N-min ((LSeg ((G * (i,j)),(G * (i,k)))) /\ (L~ f))) `2 by A7, PSCOMP_1:39
.= upper_bound (proj2 .: ((LSeg ((G * (i,j)),(G * (i,k)))) /\ (L~ f))) by A16, EUCLID:52 ;
A25: ( 1 <= i & i <= len G ) by A3, MATRIX_1:38;
A26: k <= width G by A4, MATRIX_1:38;
then A27: (G * (i,j)) `2 <= (G * (i,k)) `2 by A5, A6, A18, SPRECT_3:12;
then A28: (G * (i,j)) `2 <= p `2 by A9, TOPREAL1:4;
A29: p `2 <= (G * (i,k)) `2 by A9, A27, TOPREAL1:4;
A30: j <= width G by A3, MATRIX_1:38;
then A31: (G * (i,j)) `1 = (G * (i,1)) `1 by A6, A18, GOBOARD5:2
.= (G * (i,k)) `1 by A25, A17, A26, GOBOARD5:2 ;
A32: jo <= width G by A20, MATRIX_1:38;
i1 <= len f by A14, NAT_1:13;
then i1 in Seg (len f) by A13, FINSEQ_1:1;
then A33: i1 in dom f by FINSEQ_1:def_3;
then consider i0, j0 being Element of NAT such that
A34: [i0,j0] in Indices G and
A35: f /. i1 = G * (i0,j0) by A1, GOBOARD1:def_9;
A36: ( 1 <= i0 & i0 <= len G ) by A34, MATRIX_1:38;
A37: 1 <= j0 by A34, MATRIX_1:38;
A38: j0 <= width G by A34, MATRIX_1:38;
A39: f is special by A1, A33, JORDAN8:4, RELAT_1:38;
ex n being Element of NAT st
( j <= n & n <= k & G * (i,n) = p )
proof
percases ( (f /. i1) `1 = (f /. (i1 + 1)) `1 or (f /. i1) `2 = (f /. (i1 + 1)) `2 ) by A13, A14, A39, TOPREAL1:def_5;
supposeA40: (f /. i1) `1 = (f /. (i1 + 1)) `1 ; ::_thesis: ex n being Element of NAT st
( j <= n & n <= k & G * (i,n) = p )
(G * (io,j)) `1 = (G * (io,1)) `1 by A18, A30, A22, GOBOARD5:2
.= (G * (io,jo)) `1 by A22, A23, A32, GOBOARD5:2
.= p `1 by A15, A21, A40, GOBOARD7:5
.= (G * (i,j)) `1 by A31, A9, GOBOARD7:5 ;
then ( io <= i & io >= i ) by A6, A18, A30, A22, GOBOARD5:3;
then A41: i = io by XXREAL_0:1;
(G * (i0,j)) `1 = (G * (i0,1)) `1 by A18, A30, A36, GOBOARD5:2
.= (G * (i0,j0)) `1 by A36, A37, A38, GOBOARD5:2
.= p `1 by A15, A35, A40, GOBOARD7:5
.= (G * (i,j)) `1 by A31, A9, GOBOARD7:5 ;
then ( i0 <= i & i0 >= i ) by A6, A18, A30, A36, GOBOARD5:3;
then A42: i = i0 by XXREAL_0:1;
thus ex n being Element of NAT st
( j <= n & n <= k & G * (i,n) = p ) ::_thesis: verum
proof
percases ( (f /. i1) `2 <= (f /. (i1 + 1)) `2 or (f /. i1) `2 > (f /. (i1 + 1)) `2 ) ;
supposeA43: (f /. i1) `2 <= (f /. (i1 + 1)) `2 ; ::_thesis: ex n being Element of NAT st
( j <= n & n <= k & G * (i,n) = p )
thus ex n being Element of NAT st
( j <= n & n <= k & G * (i,n) = p ) ::_thesis: verum
proof
percases ( f /. (i1 + 1) in LSeg ((G * (i,j)),(G * (i,k))) or not f /. (i1 + 1) in LSeg ((G * (i,j)),(G * (i,k))) ) ;
supposeA44: f /. (i1 + 1) in LSeg ((G * (i,j)),(G * (i,k))) ; ::_thesis: ex n being Element of NAT st
( j <= n & n <= k & G * (i,n) = p )
1 + 1 <= i1 + 1 by A13, XREAL_1:6;
then f /. (i1 + 1) in L~ f by A14, A19, GOBOARD1:1, XXREAL_0:2;
then f /. (i1 + 1) in X1 by A44, XBOOLE_0:def_4;
then A45: p `2 >= (f /. (i1 + 1)) `2 by A16, A24, PSCOMP_1:24;
take n = jo; ::_thesis: ( j <= n & n <= k & G * (i,n) = p )
A46: p in LSeg ((G * (i,j)),(G * (i,k))) by A8, XBOOLE_0:def_4;
p `2 <= (f /. (i1 + 1)) `2 by A15, A43, TOPREAL1:4;
then p `2 = (f /. (i1 + 1)) `2 by A45, XXREAL_0:1;
then A47: p `2 = (G * (1,jo)) `2 by A21, A22, A23, A32, GOBOARD5:1
.= (G * (i,n)) `2 by A6, A23, A32, GOBOARD5:1 ;
A48: (G * (i,j)) `2 <= (G * (i,k)) `2 by A5, A6, A18, A26, SPRECT_3:12;
then (G * (i,j)) `2 <= (G * (i,n)) `2 by A46, A47, TOPREAL1:4;
hence j <= n by A6, A30, A23, GOBOARD5:4; ::_thesis: ( n <= k & G * (i,n) = p )
(G * (i,n)) `2 <= (G * (i,k)) `2 by A46, A47, A48, TOPREAL1:4;
hence n <= k by A25, A17, A32, GOBOARD5:4; ::_thesis: G * (i,n) = p
p `1 = (G * (i,j)) `1 by A31, A46, GOBOARD7:5
.= (G * (i,1)) `1 by A6, A18, A30, GOBOARD5:2
.= (G * (i,n)) `1 by A6, A23, A32, GOBOARD5:2 ;
hence G * (i,n) = p by A47, TOPREAL3:6; ::_thesis: verum
end;
supposeA49: not f /. (i1 + 1) in LSeg ((G * (i,j)),(G * (i,k))) ; ::_thesis: ex n being Element of NAT st
( j <= n & n <= k & G * (i,n) = p )
A50: (f /. (i1 + 1)) `1 = p `1 by A15, A40, GOBOARD7:5
.= (G * (i,j)) `1 by A31, A9, GOBOARD7:5 ;
thus ex n being Element of NAT st
( j <= n & n <= k & G * (i,n) = p ) ::_thesis: verum
proof
percases ( (f /. (i1 + 1)) `2 > (G * (i,k)) `2 or (f /. (i1 + 1)) `2 < (G * (i,j)) `2 ) by A31, A49, A50, GOBOARD7:7;
supposeA51: (f /. (i1 + 1)) `2 > (G * (i,k)) `2 ; ::_thesis: ex n being Element of NAT st
( j <= n & n <= k & G * (i,n) = p )
p `2 >= (G * (i0,j0)) `2 by A15, A35, A43, TOPREAL1:4;
then p `2 >= (G * (1,j0)) `2 by A36, A37, A38, GOBOARD5:1;
then p `2 >= (G * (i,j0)) `2 by A6, A37, A38, GOBOARD5:1;
then (G * (i,k)) `2 >= (G * (i,j0)) `2 by A29, XXREAL_0:2;
then A52: k >= j0 by A25, A17, A38, GOBOARD5:4;
(abs (i0 - io)) + (abs (j0 - jo)) = 1 by A1, A33, A19, A34, A35, A20, A21, GOBOARD1:def_9;
then 0 + (abs (j0 - jo)) = 1 by A42, A41, ABSVALUE:2;
then A53: abs (- (j0 - jo)) = 1 by COMPLEX1:52;
j0 <= jo + 0 by A35, A21, A36, A38, A23, A42, A41, A43, GOBOARD5:4;
then j0 - jo <= 0 by XREAL_1:20;
then jo - j0 = 1 by A53, ABSVALUE:def_1;
then A54: j0 + 1 = jo + 0 ;
( (G * (i,jo)) `2 > (G * (i,k)) `2 & jo >= k ) by A21, A25, A26, A23, A41, A51, GOBOARD5:4;
then jo > k by XXREAL_0:1;
then j0 >= k by A54, NAT_1:13;
then A55: k = j0 by A52, XXREAL_0:1;
take n = j0; ::_thesis: ( j <= n & n <= k & G * (i,n) = p )
A56: p `1 = (G * (i,j)) `1 by A31, A9, GOBOARD7:5
.= (G * (i,1)) `1 by A6, A18, A30, GOBOARD5:2
.= (G * (i,n)) `1 by A6, A37, A38, GOBOARD5:2 ;
p `2 >= (G * (i0,j0)) `2 by A15, A35, A43, TOPREAL1:4;
then p `2 >= (G * (1,j0)) `2 by A36, A37, A38, GOBOARD5:1;
then p `2 >= (G * (i,j0)) `2 by A6, A37, A38, GOBOARD5:1;
then p `2 = (G * (i,k)) `2 by A29, A55, XXREAL_0:1;
hence ( j <= n & n <= k & G * (i,n) = p ) by A5, A55, A56, TOPREAL3:6; ::_thesis: verum
end;
supposeA57: (f /. (i1 + 1)) `2 < (G * (i,j)) `2 ; ::_thesis: ex n being Element of NAT st
( j <= n & n <= k & G * (i,n) = p )
p `2 <= (f /. (i1 + 1)) `2 by A15, A43, TOPREAL1:4;
hence ex n being Element of NAT st
( j <= n & n <= k & G * (i,n) = p ) by A28, A57, XXREAL_0:2; ::_thesis: verum
end;
end;
end;
end;
end;
end;
end;
supposeA58: (f /. i1) `2 > (f /. (i1 + 1)) `2 ; ::_thesis: ex n being Element of NAT st
( j <= n & n <= k & G * (i,n) = p )
thus ex n being Element of NAT st
( j <= n & n <= k & G * (i,n) = p ) ::_thesis: verum
proof
percases ( f /. i1 in LSeg ((G * (i,j)),(G * (i,k))) or not f /. i1 in LSeg ((G * (i,j)),(G * (i,k))) ) ;
supposeA59: f /. i1 in LSeg ((G * (i,j)),(G * (i,k))) ; ::_thesis: ex n being Element of NAT st
( j <= n & n <= k & G * (i,n) = p )
1 + 1 <= i1 + 1 by A13, XREAL_1:6;
then f /. i1 in L~ f by A14, A33, GOBOARD1:1, XXREAL_0:2;
then f /. i1 in X1 by A59, XBOOLE_0:def_4;
then A60: p `2 >= (f /. i1) `2 by A16, A24, PSCOMP_1:24;
take n = j0; ::_thesis: ( j <= n & n <= k & G * (i,n) = p )
A61: p in LSeg ((G * (i,j)),(G * (i,k))) by A8, XBOOLE_0:def_4;
p `2 <= (f /. i1) `2 by A15, A58, TOPREAL1:4;
then p `2 = (f /. i1) `2 by A60, XXREAL_0:1;
then A62: p `2 = (G * (1,j0)) `2 by A35, A36, A37, A38, GOBOARD5:1
.= (G * (i,n)) `2 by A6, A37, A38, GOBOARD5:1 ;
A63: (G * (i,j)) `2 <= (G * (i,k)) `2 by A5, A6, A18, A26, SPRECT_3:12;
then (G * (i,j)) `2 <= (G * (i,n)) `2 by A61, A62, TOPREAL1:4;
hence j <= n by A6, A30, A37, GOBOARD5:4; ::_thesis: ( n <= k & G * (i,n) = p )
(G * (i,n)) `2 <= (G * (i,k)) `2 by A61, A62, A63, TOPREAL1:4;
hence n <= k by A25, A17, A38, GOBOARD5:4; ::_thesis: G * (i,n) = p
p `1 = (G * (i,j)) `1 by A31, A61, GOBOARD7:5
.= (G * (i,1)) `1 by A6, A18, A30, GOBOARD5:2
.= (G * (i,n)) `1 by A6, A37, A38, GOBOARD5:2 ;
hence G * (i,n) = p by A62, TOPREAL3:6; ::_thesis: verum
end;
supposeA64: not f /. i1 in LSeg ((G * (i,j)),(G * (i,k))) ; ::_thesis: ex n being Element of NAT st
( j <= n & n <= k & G * (i,n) = p )
A65: (f /. i1) `1 = p `1 by A15, A40, GOBOARD7:5
.= (G * (i,j)) `1 by A31, A9, GOBOARD7:5 ;
thus ex n being Element of NAT st
( j <= n & n <= k & G * (i,n) = p ) ::_thesis: verum
proof
percases ( (f /. i1) `2 > (G * (i,k)) `2 or (f /. i1) `2 < (G * (i,j)) `2 ) by A31, A64, A65, GOBOARD7:7;
supposeA66: (f /. i1) `2 > (G * (i,k)) `2 ; ::_thesis: ex n being Element of NAT st
( j <= n & n <= k & G * (i,n) = p )
p `2 >= (G * (io,jo)) `2 by A15, A21, A58, TOPREAL1:4;
then p `2 >= (G * (1,jo)) `2 by A22, A23, A32, GOBOARD5:1;
then p `2 >= (G * (i,jo)) `2 by A6, A23, A32, GOBOARD5:1;
then (G * (i,k)) `2 >= (G * (i,jo)) `2 by A29, XXREAL_0:2;
then A67: k >= jo by A25, A17, A32, GOBOARD5:4;
jo <= j0 + 0 by A35, A21, A36, A37, A32, A42, A41, A58, GOBOARD5:4;
then jo - j0 <= 0 by XREAL_1:20;
then A68: - (jo - j0) >= - 0 ;
(abs (i0 - io)) + (abs (j0 - jo)) = 1 by A1, A33, A19, A34, A35, A20, A21, GOBOARD1:def_9;
then 0 + (abs (j0 - jo)) = 1 by A42, A41, ABSVALUE:2;
then j0 - jo = 1 by A68, ABSVALUE:def_1;
then A69: jo + 1 = j0 - 0 ;
( (G * (i,j0)) `2 > (G * (i,k)) `2 & j0 >= k ) by A35, A25, A26, A37, A42, A66, GOBOARD5:4;
then j0 > k by XXREAL_0:1;
then jo >= k by A69, NAT_1:13;
then A70: k = jo by A67, XXREAL_0:1;
take n = jo; ::_thesis: ( j <= n & n <= k & G * (i,n) = p )
A71: p `1 = (G * (i,j)) `1 by A31, A9, GOBOARD7:5
.= (G * (i,1)) `1 by A6, A18, A30, GOBOARD5:2
.= (G * (i,n)) `1 by A6, A23, A32, GOBOARD5:2 ;
p `2 >= (G * (io,jo)) `2 by A15, A21, A58, TOPREAL1:4;
then p `2 >= (G * (1,jo)) `2 by A22, A23, A32, GOBOARD5:1;
then p `2 >= (G * (i,jo)) `2 by A6, A23, A32, GOBOARD5:1;
then p `2 = (G * (i,k)) `2 by A29, A70, XXREAL_0:1;
hence ( j <= n & n <= k & G * (i,n) = p ) by A5, A70, A71, TOPREAL3:6; ::_thesis: verum
end;
supposeA72: (f /. i1) `2 < (G * (i,j)) `2 ; ::_thesis: ex n being Element of NAT st
( j <= n & n <= k & G * (i,n) = p )
p `2 <= (f /. i1) `2 by A15, A58, TOPREAL1:4;
hence ex n being Element of NAT st
( j <= n & n <= k & G * (i,n) = p ) by A28, A72, XXREAL_0:2; ::_thesis: verum
end;
end;
end;
end;
end;
end;
end;
end;
end;
end;
supposeA73: (f /. i1) `2 = (f /. (i1 + 1)) `2 ; ::_thesis: ex n being Element of NAT st
( j <= n & n <= k & G * (i,n) = p )
take n = j0; ::_thesis: ( j <= n & n <= k & G * (i,n) = p )
p `2 = (f /. i1) `2 by A15, A73, GOBOARD7:6;
then A74: p `2 = (G * (1,j0)) `2 by A35, A36, A37, A38, GOBOARD5:1
.= (G * (i,n)) `2 by A6, A37, A38, GOBOARD5:1 ;
A75: (G * (i,j)) `2 <= (G * (i,k)) `2 by A5, A6, A18, A26, SPRECT_3:12;
then (G * (i,j)) `2 <= (G * (i,n)) `2 by A9, A74, TOPREAL1:4;
hence j <= n by A6, A30, A37, GOBOARD5:4; ::_thesis: ( n <= k & G * (i,n) = p )
(G * (i,n)) `2 <= (G * (i,k)) `2 by A9, A74, A75, TOPREAL1:4;
hence n <= k by A25, A17, A38, GOBOARD5:4; ::_thesis: G * (i,n) = p
p `1 = (G * (i,j)) `1 by A31, A9, GOBOARD7:5
.= (G * (i,1)) `1 by A6, A18, A30, GOBOARD5:2
.= (G * (i,n)) `1 by A6, A37, A38, GOBOARD5:2 ;
hence G * (i,n) = p by A74, TOPREAL3:6; ::_thesis: verum
end;
end;
end;
hence ex n being Element of NAT st
( j <= n & n <= k & (G * (i,n)) `2 = upper_bound (proj2 .: ((LSeg ((G * (i,j)),(G * (i,k)))) /\ (L~ f))) ) by A24; ::_thesis: verum
end;
theorem :: JORDAN1F:3
for j, i, k being Element of NAT
for f being FinSequence of the carrier of (TOP-REAL 2)
for G being Go-board st f is_sequence_on G & LSeg ((G * (j,i)),(G * (k,i))) meets L~ f & [j,i] in Indices G & [k,i] in Indices G & j <= k holds
ex n being Element of NAT st
( j <= n & n <= k & (G * (n,i)) `1 = lower_bound (proj1 .: ((LSeg ((G * (j,i)),(G * (k,i)))) /\ (L~ f))) )
proof
let j, i, k be Element of NAT ; ::_thesis: for f being FinSequence of the carrier of (TOP-REAL 2)
for G being Go-board st f is_sequence_on G & LSeg ((G * (j,i)),(G * (k,i))) meets L~ f & [j,i] in Indices G & [k,i] in Indices G & j <= k holds
ex n being Element of NAT st
( j <= n & n <= k & (G * (n,i)) `1 = lower_bound (proj1 .: ((LSeg ((G * (j,i)),(G * (k,i)))) /\ (L~ f))) )
let f be FinSequence of the carrier of (TOP-REAL 2); ::_thesis: for G being Go-board st f is_sequence_on G & LSeg ((G * (j,i)),(G * (k,i))) meets L~ f & [j,i] in Indices G & [k,i] in Indices G & j <= k holds
ex n being Element of NAT st
( j <= n & n <= k & (G * (n,i)) `1 = lower_bound (proj1 .: ((LSeg ((G * (j,i)),(G * (k,i)))) /\ (L~ f))) )
let G be Go-board; ::_thesis: ( f is_sequence_on G & LSeg ((G * (j,i)),(G * (k,i))) meets L~ f & [j,i] in Indices G & [k,i] in Indices G & j <= k implies ex n being Element of NAT st
( j <= n & n <= k & (G * (n,i)) `1 = lower_bound (proj1 .: ((LSeg ((G * (j,i)),(G * (k,i)))) /\ (L~ f))) ) )
set X = (LSeg ((G * (j,i)),(G * (k,i)))) /\ (L~ f);
assume that
A1: f is_sequence_on G and
A2: LSeg ((G * (j,i)),(G * (k,i))) meets L~ f and
A3: [j,i] in Indices G and
A4: [k,i] in Indices G and
A5: j <= k ; ::_thesis: ex n being Element of NAT st
( j <= n & n <= k & (G * (n,i)) `1 = lower_bound (proj1 .: ((LSeg ((G * (j,i)),(G * (k,i)))) /\ (L~ f))) )
A6: 1 <= j by A3, MATRIX_1:38;
ex x being set st
( x in LSeg ((G * (j,i)),(G * (k,i))) & x in L~ f ) by A2, XBOOLE_0:3;
then reconsider X1 = (LSeg ((G * (j,i)),(G * (k,i)))) /\ (L~ f) as non empty compact Subset of (TOP-REAL 2) by XBOOLE_0:def_4;
consider p being set such that
A7: p in W-most X1 by XBOOLE_0:def_1;
reconsider p = p as Point of (TOP-REAL 2) by A7;
A8: p in (LSeg ((G * (j,i)),(G * (k,i)))) /\ (L~ f) by A7, XBOOLE_0:def_4;
then A9: p in LSeg ((G * (j,i)),(G * (k,i))) by XBOOLE_0:def_4;
proj1 .: ((LSeg ((G * (j,i)),(G * (k,i)))) /\ (L~ f)) = (proj1 | ((LSeg ((G * (j,i)),(G * (k,i)))) /\ (L~ f))) .: ((LSeg ((G * (j,i)),(G * (k,i)))) /\ (L~ f)) by RELAT_1:129;
then A10: lower_bound (proj1 .: ((LSeg ((G * (j,i)),(G * (k,i)))) /\ (L~ f))) = lower_bound ((proj1 | ((LSeg ((G * (j,i)),(G * (k,i)))) /\ (L~ f))) .: ([#] ((TOP-REAL 2) | ((LSeg ((G * (j,i)),(G * (k,i)))) /\ (L~ f))))) by PRE_TOPC:def_5
.= W-bound ((LSeg ((G * (j,i)),(G * (k,i)))) /\ (L~ f)) ;
A11: ( 1 <= k & 1 <= i ) by A4, MATRIX_1:38;
A12: p `1 = (W-min ((LSeg ((G * (j,i)),(G * (k,i)))) /\ (L~ f))) `1 by A7, PSCOMP_1:31
.= lower_bound (proj1 .: ((LSeg ((G * (j,i)),(G * (k,i)))) /\ (L~ f))) by A10, EUCLID:52 ;
A13: i <= width G by A3, MATRIX_1:38;
A14: ( 1 <= i & i <= width G ) by A3, MATRIX_1:38;
A15: k <= len G by A4, MATRIX_1:38;
then A16: (G * (j,i)) `1 <= (G * (k,i)) `1 by A5, A6, A14, SPRECT_3:13;
then A17: (G * (j,i)) `1 <= p `1 by A9, TOPREAL1:3;
A18: p `1 <= (G * (k,i)) `1 by A9, A16, TOPREAL1:3;
A19: j <= len G by A3, MATRIX_1:38;
then A20: (G * (j,i)) `2 = (G * (1,i)) `2 by A6, A14, GOBOARD5:1
.= (G * (k,i)) `2 by A15, A11, A13, GOBOARD5:1 ;
p in L~ f by A8, XBOOLE_0:def_4;
then p in union { (LSeg (f,k1)) where k1 is Element of NAT : ( 1 <= k1 & k1 + 1 <= len f ) } by TOPREAL1:def_4;
then consider Y being set such that
A21: p in Y and
A22: Y in { (LSeg (f,k1)) where k1 is Element of NAT : ( 1 <= k1 & k1 + 1 <= len f ) } by TARSKI:def_4;
consider i1 being Element of NAT such that
A23: Y = LSeg (f,i1) and
A24: 1 <= i1 and
A25: i1 + 1 <= len f by A22;
A26: p in LSeg ((f /. i1),(f /. (i1 + 1))) by A21, A23, A24, A25, TOPREAL1:def_3;
1 < i1 + 1 by A24, NAT_1:13;
then i1 + 1 in Seg (len f) by A25, FINSEQ_1:1;
then A27: i1 + 1 in dom f by FINSEQ_1:def_3;
then consider jo, io being Element of NAT such that
A28: [jo,io] in Indices G and
A29: f /. (i1 + 1) = G * (jo,io) by A1, GOBOARD1:def_9;
A30: 1 <= jo by A28, MATRIX_1:38;
i1 <= len f by A25, NAT_1:13;
then i1 in Seg (len f) by A24, FINSEQ_1:1;
then A31: i1 in dom f by FINSEQ_1:def_3;
then consider j0, i0 being Element of NAT such that
A32: [j0,i0] in Indices G and
A33: f /. i1 = G * (j0,i0) by A1, GOBOARD1:def_9;
A34: 1 <= j0 by A32, MATRIX_1:38;
A35: ( 1 <= i0 & i0 <= width G ) by A32, MATRIX_1:38;
A36: j0 <= len G by A32, MATRIX_1:38;
A37: ( 1 <= io & io <= width G ) by A28, MATRIX_1:38;
A38: jo <= len G by A28, MATRIX_1:38;
A39: f is special by A1, A31, JORDAN8:4, RELAT_1:38;
ex n being Element of NAT st
( j <= n & n <= k & G * (n,i) = p )
proof
percases ( (f /. i1) `2 = (f /. (i1 + 1)) `2 or (f /. i1) `1 = (f /. (i1 + 1)) `1 ) by A24, A25, A39, TOPREAL1:def_5;
supposeA40: (f /. i1) `2 = (f /. (i1 + 1)) `2 ; ::_thesis: ex n being Element of NAT st
( j <= n & n <= k & G * (n,i) = p )
(G * (j,io)) `2 = (G * (1,io)) `2 by A6, A19, A37, GOBOARD5:1
.= (G * (jo,io)) `2 by A30, A38, A37, GOBOARD5:1
.= p `2 by A26, A29, A40, GOBOARD7:6
.= (G * (j,i)) `2 by A20, A9, GOBOARD7:6 ;
then ( io <= i & io >= i ) by A6, A19, A14, A37, GOBOARD5:4;
then A41: i = io by XXREAL_0:1;
(G * (j,i0)) `2 = (G * (1,i0)) `2 by A6, A19, A35, GOBOARD5:1
.= (G * (j0,i0)) `2 by A34, A36, A35, GOBOARD5:1
.= p `2 by A26, A33, A40, GOBOARD7:6
.= (G * (j,i)) `2 by A20, A9, GOBOARD7:6 ;
then ( i0 <= i & i0 >= i ) by A6, A19, A14, A35, GOBOARD5:4;
then A42: i = i0 by XXREAL_0:1;
thus ex n being Element of NAT st
( j <= n & n <= k & G * (n,i) = p ) ::_thesis: verum
proof
percases ( (f /. i1) `1 <= (f /. (i1 + 1)) `1 or (f /. i1) `1 > (f /. (i1 + 1)) `1 ) ;
supposeA43: (f /. i1) `1 <= (f /. (i1 + 1)) `1 ; ::_thesis: ex n being Element of NAT st
( j <= n & n <= k & G * (n,i) = p )
thus ex n being Element of NAT st
( j <= n & n <= k & G * (n,i) = p ) ::_thesis: verum
proof
percases ( f /. i1 in LSeg ((G * (j,i)),(G * (k,i))) or not f /. i1 in LSeg ((G * (j,i)),(G * (k,i))) ) ;
supposeA44: f /. i1 in LSeg ((G * (j,i)),(G * (k,i))) ; ::_thesis: ex n being Element of NAT st
( j <= n & n <= k & G * (n,i) = p )
1 + 1 <= i1 + 1 by A24, XREAL_1:6;
then f /. i1 in L~ f by A25, A31, GOBOARD1:1, XXREAL_0:2;
then f /. i1 in X1 by A44, XBOOLE_0:def_4;
then A45: p `1 <= (f /. i1) `1 by A10, A12, PSCOMP_1:24;
take n = j0; ::_thesis: ( j <= n & n <= k & G * (n,i) = p )
A46: p in LSeg ((G * (j,i)),(G * (k,i))) by A8, XBOOLE_0:def_4;
p `1 >= (f /. i1) `1 by A26, A43, TOPREAL1:3;
then p `1 = (f /. i1) `1 by A45, XXREAL_0:1;
then A47: p `1 = (G * (j0,1)) `1 by A33, A34, A36, A35, GOBOARD5:2
.= (G * (n,i)) `1 by A14, A34, A36, GOBOARD5:2 ;
A48: (G * (j,i)) `1 <= (G * (k,i)) `1 by A5, A6, A14, A15, SPRECT_3:13;
then (G * (j,i)) `1 <= (G * (n,i)) `1 by A46, A47, TOPREAL1:3;
hence j <= n by A19, A14, A34, GOBOARD5:3; ::_thesis: ( n <= k & G * (n,i) = p )
(G * (n,i)) `1 <= (G * (k,i)) `1 by A46, A47, A48, TOPREAL1:3;
hence n <= k by A11, A13, A36, GOBOARD5:3; ::_thesis: G * (n,i) = p
p `2 = (G * (j,i)) `2 by A20, A46, GOBOARD7:6
.= (G * (1,i)) `2 by A6, A19, A14, GOBOARD5:1
.= (G * (n,i)) `2 by A14, A34, A36, GOBOARD5:1 ;
hence G * (n,i) = p by A47, TOPREAL3:6; ::_thesis: verum
end;
supposeA49: not f /. i1 in LSeg ((G * (j,i)),(G * (k,i))) ; ::_thesis: ex n being Element of NAT st
( j <= n & n <= k & G * (n,i) = p )
A50: (f /. i1) `2 = p `2 by A26, A40, GOBOARD7:6
.= (G * (j,i)) `2 by A20, A9, GOBOARD7:6 ;
thus ex n being Element of NAT st
( j <= n & n <= k & G * (n,i) = p ) ::_thesis: verum
proof
percases ( (f /. i1) `1 < (G * (j,i)) `1 or (f /. i1) `1 > (G * (k,i)) `1 ) by A20, A49, A50, GOBOARD7:8;
supposeA51: (f /. i1) `1 < (G * (j,i)) `1 ; ::_thesis: ex n being Element of NAT st
( j <= n & n <= k & G * (n,i) = p )
p `1 <= (G * (jo,io)) `1 by A26, A29, A43, TOPREAL1:3;
then p `1 <= (G * (jo,1)) `1 by A30, A38, A37, GOBOARD5:2;
then p `1 <= (G * (jo,i)) `1 by A14, A30, A38, GOBOARD5:2;
then (G * (j,i)) `1 <= (G * (jo,i)) `1 by A17, XXREAL_0:2;
then A52: j <= jo by A19, A14, A30, GOBOARD5:3;
(abs (i0 - io)) + (abs (j0 - jo)) = 1 by A1, A31, A27, A32, A33, A28, A29, GOBOARD1:def_9;
then 0 + (abs (j0 - jo)) = 1 by A42, A41, ABSVALUE:2;
then A53: abs (- (j0 - jo)) = 1 by COMPLEX1:52;
j0 <= jo + 0 by A33, A29, A36, A35, A30, A42, A41, A43, GOBOARD5:3;
then j0 - jo <= 0 by XREAL_1:20;
then jo - j0 = 1 by A53, ABSVALUE:def_1;
then A54: j0 + 1 = jo + 0 ;
( (G * (j0,i)) `1 < (G * (j,i)) `1 & j0 <= j ) by A33, A6, A14, A36, A42, A51, GOBOARD5:3;
then j0 < j by XXREAL_0:1;
then jo <= j by A54, NAT_1:13;
then A55: j = jo by A52, XXREAL_0:1;
take n = jo; ::_thesis: ( j <= n & n <= k & G * (n,i) = p )
A56: p `2 = (G * (j,i)) `2 by A20, A9, GOBOARD7:6
.= (G * (1,i)) `2 by A6, A19, A14, GOBOARD5:1
.= (G * (n,i)) `2 by A14, A30, A38, GOBOARD5:1 ;
p `1 <= (G * (jo,io)) `1 by A26, A29, A43, TOPREAL1:3;
then p `1 <= (G * (jo,1)) `1 by A30, A38, A37, GOBOARD5:2;
then p `1 <= (G * (jo,i)) `1 by A14, A30, A38, GOBOARD5:2;
then p `1 = (G * (j,i)) `1 by A17, A55, XXREAL_0:1;
hence ( j <= n & n <= k & G * (n,i) = p ) by A5, A55, A56, TOPREAL3:6; ::_thesis: verum
end;
supposeA57: (f /. i1) `1 > (G * (k,i)) `1 ; ::_thesis: ex n being Element of NAT st
( j <= n & n <= k & G * (n,i) = p )
p `1 >= (f /. i1) `1 by A26, A43, TOPREAL1:3;
hence ex n being Element of NAT st
( j <= n & n <= k & G * (n,i) = p ) by A18, A57, XXREAL_0:2; ::_thesis: verum
end;
end;
end;
end;
end;
end;
end;
supposeA58: (f /. i1) `1 > (f /. (i1 + 1)) `1 ; ::_thesis: ex n being Element of NAT st
( j <= n & n <= k & G * (n,i) = p )
thus ex n being Element of NAT st
( j <= n & n <= k & G * (n,i) = p ) ::_thesis: verum
proof
percases ( f /. (i1 + 1) in LSeg ((G * (j,i)),(G * (k,i))) or not f /. (i1 + 1) in LSeg ((G * (j,i)),(G * (k,i))) ) ;
supposeA59: f /. (i1 + 1) in LSeg ((G * (j,i)),(G * (k,i))) ; ::_thesis: ex n being Element of NAT st
( j <= n & n <= k & G * (n,i) = p )
1 + 1 <= i1 + 1 by A24, XREAL_1:6;
then f /. (i1 + 1) in L~ f by A25, A27, GOBOARD1:1, XXREAL_0:2;
then f /. (i1 + 1) in X1 by A59, XBOOLE_0:def_4;
then A60: p `1 <= (f /. (i1 + 1)) `1 by A10, A12, PSCOMP_1:24;
take n = jo; ::_thesis: ( j <= n & n <= k & G * (n,i) = p )
A61: p in LSeg ((G * (j,i)),(G * (k,i))) by A8, XBOOLE_0:def_4;
p `1 >= (f /. (i1 + 1)) `1 by A26, A58, TOPREAL1:3;
then p `1 = (f /. (i1 + 1)) `1 by A60, XXREAL_0:1;
then A62: p `1 = (G * (jo,1)) `1 by A29, A30, A38, A37, GOBOARD5:2
.= (G * (n,i)) `1 by A14, A30, A38, GOBOARD5:2 ;
A63: (G * (j,i)) `1 <= (G * (k,i)) `1 by A5, A6, A14, A15, SPRECT_3:13;
then (G * (j,i)) `1 <= (G * (n,i)) `1 by A61, A62, TOPREAL1:3;
hence j <= n by A19, A14, A30, GOBOARD5:3; ::_thesis: ( n <= k & G * (n,i) = p )
(G * (n,i)) `1 <= (G * (k,i)) `1 by A61, A62, A63, TOPREAL1:3;
hence n <= k by A11, A13, A38, GOBOARD5:3; ::_thesis: G * (n,i) = p
p `2 = (G * (j,i)) `2 by A20, A61, GOBOARD7:6
.= (G * (1,i)) `2 by A6, A19, A14, GOBOARD5:1
.= (G * (n,i)) `2 by A14, A30, A38, GOBOARD5:1 ;
hence G * (n,i) = p by A62, TOPREAL3:6; ::_thesis: verum
end;
supposeA64: not f /. (i1 + 1) in LSeg ((G * (j,i)),(G * (k,i))) ; ::_thesis: ex n being Element of NAT st
( j <= n & n <= k & G * (n,i) = p )
A65: (f /. (i1 + 1)) `2 = p `2 by A26, A40, GOBOARD7:6
.= (G * (j,i)) `2 by A20, A9, GOBOARD7:6 ;
thus ex n being Element of NAT st
( j <= n & n <= k & G * (n,i) = p ) ::_thesis: verum
proof
percases ( (f /. (i1 + 1)) `1 < (G * (j,i)) `1 or (f /. (i1 + 1)) `1 > (G * (k,i)) `1 ) by A20, A64, A65, GOBOARD7:8;
supposeA66: (f /. (i1 + 1)) `1 < (G * (j,i)) `1 ; ::_thesis: ex n being Element of NAT st
( j <= n & n <= k & G * (n,i) = p )
p `1 <= (G * (j0,i0)) `1 by A26, A33, A58, TOPREAL1:3;
then p `1 <= (G * (j0,1)) `1 by A34, A36, A35, GOBOARD5:2;
then p `1 <= (G * (j0,i)) `1 by A14, A34, A36, GOBOARD5:2;
then (G * (j,i)) `1 <= (G * (j0,i)) `1 by A17, XXREAL_0:2;
then A67: j <= j0 by A19, A14, A34, GOBOARD5:3;
jo <= j0 + 0 by A33, A29, A34, A35, A38, A42, A41, A58, GOBOARD5:3;
then jo - j0 <= 0 by XREAL_1:20;
then A68: - (jo - j0) >= - 0 ;
(abs (i0 - io)) + (abs (j0 - jo)) = 1 by A1, A31, A27, A32, A33, A28, A29, GOBOARD1:def_9;
then 0 + (abs (j0 - jo)) = 1 by A42, A41, ABSVALUE:2;
then j0 - jo = 1 by A68, ABSVALUE:def_1;
then A69: jo + 1 = j0 - 0 ;
( (G * (jo,i)) `1 < (G * (j,i)) `1 & jo <= j ) by A29, A6, A14, A38, A41, A66, GOBOARD5:3;
then jo < j by XXREAL_0:1;
then j0 <= j by A69, NAT_1:13;
then A70: j = j0 by A67, XXREAL_0:1;
take n = j0; ::_thesis: ( j <= n & n <= k & G * (n,i) = p )
A71: p `2 = (G * (j,i)) `2 by A20, A9, GOBOARD7:6
.= (G * (1,i)) `2 by A6, A19, A14, GOBOARD5:1
.= (G * (n,i)) `2 by A14, A34, A36, GOBOARD5:1 ;
p `1 <= (G * (j0,i0)) `1 by A26, A33, A58, TOPREAL1:3;
then p `1 <= (G * (j0,1)) `1 by A34, A36, A35, GOBOARD5:2;
then p `1 <= (G * (j0,i)) `1 by A14, A34, A36, GOBOARD5:2;
then p `1 = (G * (j,i)) `1 by A17, A70, XXREAL_0:1;
hence ( j <= n & n <= k & G * (n,i) = p ) by A5, A70, A71, TOPREAL3:6; ::_thesis: verum
end;
supposeA72: (f /. (i1 + 1)) `1 > (G * (k,i)) `1 ; ::_thesis: ex n being Element of NAT st
( j <= n & n <= k & G * (n,i) = p )
p `1 >= (f /. (i1 + 1)) `1 by A26, A58, TOPREAL1:3;
hence ex n being Element of NAT st
( j <= n & n <= k & G * (n,i) = p ) by A18, A72, XXREAL_0:2; ::_thesis: verum
end;
end;
end;
end;
end;
end;
end;
end;
end;
end;
supposeA73: (f /. i1) `1 = (f /. (i1 + 1)) `1 ; ::_thesis: ex n being Element of NAT st
( j <= n & n <= k & G * (n,i) = p )
take n = j0; ::_thesis: ( j <= n & n <= k & G * (n,i) = p )
p `1 = (f /. i1) `1 by A26, A73, GOBOARD7:5;
then A74: p `1 = (G * (j0,1)) `1 by A33, A34, A36, A35, GOBOARD5:2
.= (G * (n,i)) `1 by A14, A34, A36, GOBOARD5:2 ;
A75: (G * (j,i)) `1 <= (G * (k,i)) `1 by A5, A6, A14, A15, SPRECT_3:13;
then (G * (j,i)) `1 <= (G * (n,i)) `1 by A9, A74, TOPREAL1:3;
hence j <= n by A19, A14, A34, GOBOARD5:3; ::_thesis: ( n <= k & G * (n,i) = p )
(G * (n,i)) `1 <= (G * (k,i)) `1 by A9, A74, A75, TOPREAL1:3;
hence n <= k by A11, A13, A36, GOBOARD5:3; ::_thesis: G * (n,i) = p
p `2 = (G * (j,i)) `2 by A20, A9, GOBOARD7:6
.= (G * (1,i)) `2 by A6, A19, A14, GOBOARD5:1
.= (G * (n,i)) `2 by A14, A34, A36, GOBOARD5:1 ;
hence G * (n,i) = p by A74, TOPREAL3:6; ::_thesis: verum
end;
end;
end;
hence ex n being Element of NAT st
( j <= n & n <= k & (G * (n,i)) `1 = lower_bound (proj1 .: ((LSeg ((G * (j,i)),(G * (k,i)))) /\ (L~ f))) ) by A12; ::_thesis: verum
end;
theorem :: JORDAN1F:4
for j, i, k being Element of NAT
for f being FinSequence of the carrier of (TOP-REAL 2)
for G being Go-board st f is_sequence_on G & LSeg ((G * (j,i)),(G * (k,i))) meets L~ f & [j,i] in Indices G & [k,i] in Indices G & j <= k holds
ex n being Element of NAT st
( j <= n & n <= k & (G * (n,i)) `1 = upper_bound (proj1 .: ((LSeg ((G * (j,i)),(G * (k,i)))) /\ (L~ f))) )
proof
let j, i, k be Element of NAT ; ::_thesis: for f being FinSequence of the carrier of (TOP-REAL 2)
for G being Go-board st f is_sequence_on G & LSeg ((G * (j,i)),(G * (k,i))) meets L~ f & [j,i] in Indices G & [k,i] in Indices G & j <= k holds
ex n being Element of NAT st
( j <= n & n <= k & (G * (n,i)) `1 = upper_bound (proj1 .: ((LSeg ((G * (j,i)),(G * (k,i)))) /\ (L~ f))) )
let f be FinSequence of the carrier of (TOP-REAL 2); ::_thesis: for G being Go-board st f is_sequence_on G & LSeg ((G * (j,i)),(G * (k,i))) meets L~ f & [j,i] in Indices G & [k,i] in Indices G & j <= k holds
ex n being Element of NAT st
( j <= n & n <= k & (G * (n,i)) `1 = upper_bound (proj1 .: ((LSeg ((G * (j,i)),(G * (k,i)))) /\ (L~ f))) )
let G be Go-board; ::_thesis: ( f is_sequence_on G & LSeg ((G * (j,i)),(G * (k,i))) meets L~ f & [j,i] in Indices G & [k,i] in Indices G & j <= k implies ex n being Element of NAT st
( j <= n & n <= k & (G * (n,i)) `1 = upper_bound (proj1 .: ((LSeg ((G * (j,i)),(G * (k,i)))) /\ (L~ f))) ) )
set X = (LSeg ((G * (j,i)),(G * (k,i)))) /\ (L~ f);
assume that
A1: f is_sequence_on G and
A2: LSeg ((G * (j,i)),(G * (k,i))) meets L~ f and
A3: [j,i] in Indices G and
A4: [k,i] in Indices G and
A5: j <= k ; ::_thesis: ex n being Element of NAT st
( j <= n & n <= k & (G * (n,i)) `1 = upper_bound (proj1 .: ((LSeg ((G * (j,i)),(G * (k,i)))) /\ (L~ f))) )
A6: 1 <= j by A3, MATRIX_1:38;
ex x being set st
( x in LSeg ((G * (j,i)),(G * (k,i))) & x in L~ f ) by A2, XBOOLE_0:3;
then reconsider X1 = (LSeg ((G * (j,i)),(G * (k,i)))) /\ (L~ f) as non empty compact Subset of (TOP-REAL 2) by XBOOLE_0:def_4;
consider p being set such that
A7: p in E-most X1 by XBOOLE_0:def_1;
reconsider p = p as Point of (TOP-REAL 2) by A7;
A8: p in (LSeg ((G * (j,i)),(G * (k,i)))) /\ (L~ f) by A7, XBOOLE_0:def_4;
then A9: p in LSeg ((G * (j,i)),(G * (k,i))) by XBOOLE_0:def_4;
proj1 .: ((LSeg ((G * (j,i)),(G * (k,i)))) /\ (L~ f)) = (proj1 | ((LSeg ((G * (j,i)),(G * (k,i)))) /\ (L~ f))) .: ((LSeg ((G * (j,i)),(G * (k,i)))) /\ (L~ f)) by RELAT_1:129;
then A10: upper_bound (proj1 .: ((LSeg ((G * (j,i)),(G * (k,i)))) /\ (L~ f))) = upper_bound ((proj1 | ((LSeg ((G * (j,i)),(G * (k,i)))) /\ (L~ f))) .: ([#] ((TOP-REAL 2) | ((LSeg ((G * (j,i)),(G * (k,i)))) /\ (L~ f))))) by PRE_TOPC:def_5
.= E-bound ((LSeg ((G * (j,i)),(G * (k,i)))) /\ (L~ f)) ;
A11: ( 1 <= i & i <= width G ) by A3, MATRIX_1:38;
A12: p `1 = (E-min ((LSeg ((G * (j,i)),(G * (k,i)))) /\ (L~ f))) `1 by A7, PSCOMP_1:47
.= upper_bound (proj1 .: ((LSeg ((G * (j,i)),(G * (k,i)))) /\ (L~ f))) by A10, EUCLID:52 ;
A13: 1 <= k by A4, MATRIX_1:38;
A14: ( 1 <= i & i <= width G ) by A3, MATRIX_1:38;
A15: k <= len G by A4, MATRIX_1:38;
then A16: (G * (j,i)) `1 <= (G * (k,i)) `1 by A5, A6, A14, SPRECT_3:13;
then A17: (G * (j,i)) `1 <= p `1 by A9, TOPREAL1:3;
A18: p `1 <= (G * (k,i)) `1 by A9, A16, TOPREAL1:3;
A19: j <= len G by A3, MATRIX_1:38;
then A20: (G * (j,i)) `2 = (G * (1,i)) `2 by A6, A14, GOBOARD5:1
.= (G * (k,i)) `2 by A13, A15, A11, GOBOARD5:1 ;
p in L~ f by A8, XBOOLE_0:def_4;
then p in union { (LSeg (f,k1)) where k1 is Element of NAT : ( 1 <= k1 & k1 + 1 <= len f ) } by TOPREAL1:def_4;
then consider Y being set such that
A21: p in Y and
A22: Y in { (LSeg (f,k1)) where k1 is Element of NAT : ( 1 <= k1 & k1 + 1 <= len f ) } by TARSKI:def_4;
consider i1 being Element of NAT such that
A23: Y = LSeg (f,i1) and
A24: 1 <= i1 and
A25: i1 + 1 <= len f by A22;
A26: p in LSeg ((f /. i1),(f /. (i1 + 1))) by A21, A23, A24, A25, TOPREAL1:def_3;
1 < i1 + 1 by A24, NAT_1:13;
then i1 + 1 in Seg (len f) by A25, FINSEQ_1:1;
then A27: i1 + 1 in dom f by FINSEQ_1:def_3;
then consider jo, io being Element of NAT such that
A28: [jo,io] in Indices G and
A29: f /. (i1 + 1) = G * (jo,io) by A1, GOBOARD1:def_9;
A30: 1 <= jo by A28, MATRIX_1:38;
i1 <= len f by A25, NAT_1:13;
then i1 in Seg (len f) by A24, FINSEQ_1:1;
then A31: i1 in dom f by FINSEQ_1:def_3;
then consider j0, i0 being Element of NAT such that
A32: [j0,i0] in Indices G and
A33: f /. i1 = G * (j0,i0) by A1, GOBOARD1:def_9;
A34: 1 <= j0 by A32, MATRIX_1:38;
A35: ( 1 <= i0 & i0 <= width G ) by A32, MATRIX_1:38;
A36: j0 <= len G by A32, MATRIX_1:38;
A37: ( 1 <= io & io <= width G ) by A28, MATRIX_1:38;
A38: jo <= len G by A28, MATRIX_1:38;
A39: f is special by A1, A31, JORDAN8:4, RELAT_1:38;
ex n being Element of NAT st
( j <= n & n <= k & G * (n,i) = p )
proof
percases ( (f /. i1) `2 = (f /. (i1 + 1)) `2 or (f /. i1) `1 = (f /. (i1 + 1)) `1 ) by A24, A25, A39, TOPREAL1:def_5;
supposeA40: (f /. i1) `2 = (f /. (i1 + 1)) `2 ; ::_thesis: ex n being Element of NAT st
( j <= n & n <= k & G * (n,i) = p )
(G * (j,io)) `2 = (G * (1,io)) `2 by A6, A19, A37, GOBOARD5:1
.= (G * (jo,io)) `2 by A30, A38, A37, GOBOARD5:1
.= p `2 by A26, A29, A40, GOBOARD7:6
.= (G * (j,i)) `2 by A20, A9, GOBOARD7:6 ;
then ( io <= i & io >= i ) by A6, A19, A14, A37, GOBOARD5:4;
then A41: i = io by XXREAL_0:1;
(G * (j,i0)) `2 = (G * (1,i0)) `2 by A6, A19, A35, GOBOARD5:1
.= (G * (j0,i0)) `2 by A34, A36, A35, GOBOARD5:1
.= p `2 by A26, A33, A40, GOBOARD7:6
.= (G * (j,i)) `2 by A20, A9, GOBOARD7:6 ;
then ( i0 <= i & i0 >= i ) by A6, A19, A14, A35, GOBOARD5:4;
then A42: i = i0 by XXREAL_0:1;
thus ex n being Element of NAT st
( j <= n & n <= k & G * (n,i) = p ) ::_thesis: verum
proof
percases ( (f /. i1) `1 <= (f /. (i1 + 1)) `1 or (f /. i1) `1 > (f /. (i1 + 1)) `1 ) ;
supposeA43: (f /. i1) `1 <= (f /. (i1 + 1)) `1 ; ::_thesis: ex n being Element of NAT st
( j <= n & n <= k & G * (n,i) = p )
thus ex n being Element of NAT st
( j <= n & n <= k & G * (n,i) = p ) ::_thesis: verum
proof
percases ( f /. (i1 + 1) in LSeg ((G * (j,i)),(G * (k,i))) or not f /. (i1 + 1) in LSeg ((G * (j,i)),(G * (k,i))) ) ;
supposeA44: f /. (i1 + 1) in LSeg ((G * (j,i)),(G * (k,i))) ; ::_thesis: ex n being Element of NAT st
( j <= n & n <= k & G * (n,i) = p )
1 + 1 <= i1 + 1 by A24, XREAL_1:6;
then f /. (i1 + 1) in L~ f by A25, A27, GOBOARD1:1, XXREAL_0:2;
then f /. (i1 + 1) in X1 by A44, XBOOLE_0:def_4;
then A45: p `1 >= (f /. (i1 + 1)) `1 by A10, A12, PSCOMP_1:24;
take n = jo; ::_thesis: ( j <= n & n <= k & G * (n,i) = p )
A46: p in LSeg ((G * (j,i)),(G * (k,i))) by A8, XBOOLE_0:def_4;
p `1 <= (f /. (i1 + 1)) `1 by A26, A43, TOPREAL1:3;
then p `1 = (f /. (i1 + 1)) `1 by A45, XXREAL_0:1;
then A47: p `1 = (G * (jo,1)) `1 by A29, A30, A38, A37, GOBOARD5:2
.= (G * (n,i)) `1 by A14, A30, A38, GOBOARD5:2 ;
A48: (G * (j,i)) `1 <= (G * (k,i)) `1 by A5, A6, A14, A15, SPRECT_3:13;
then (G * (j,i)) `1 <= (G * (n,i)) `1 by A46, A47, TOPREAL1:3;
hence j <= n by A19, A14, A30, GOBOARD5:3; ::_thesis: ( n <= k & G * (n,i) = p )
(G * (n,i)) `1 <= (G * (k,i)) `1 by A46, A47, A48, TOPREAL1:3;
hence n <= k by A13, A11, A38, GOBOARD5:3; ::_thesis: G * (n,i) = p
p `2 = (G * (j,i)) `2 by A20, A46, GOBOARD7:6
.= (G * (1,i)) `2 by A6, A19, A14, GOBOARD5:1
.= (G * (n,i)) `2 by A14, A30, A38, GOBOARD5:1 ;
hence G * (n,i) = p by A47, TOPREAL3:6; ::_thesis: verum
end;
supposeA49: not f /. (i1 + 1) in LSeg ((G * (j,i)),(G * (k,i))) ; ::_thesis: ex n being Element of NAT st
( j <= n & n <= k & G * (n,i) = p )
A50: (f /. (i1 + 1)) `2 = p `2 by A26, A40, GOBOARD7:6
.= (G * (j,i)) `2 by A20, A9, GOBOARD7:6 ;
thus ex n being Element of NAT st
( j <= n & n <= k & G * (n,i) = p ) ::_thesis: verum
proof
percases ( (f /. (i1 + 1)) `1 > (G * (k,i)) `1 or (f /. (i1 + 1)) `1 < (G * (j,i)) `1 ) by A20, A49, A50, GOBOARD7:8;
supposeA51: (f /. (i1 + 1)) `1 > (G * (k,i)) `1 ; ::_thesis: ex n being Element of NAT st
( j <= n & n <= k & G * (n,i) = p )
p `1 >= (G * (j0,i0)) `1 by A26, A33, A43, TOPREAL1:3;
then p `1 >= (G * (j0,1)) `1 by A34, A36, A35, GOBOARD5:2;
then p `1 >= (G * (j0,i)) `1 by A14, A34, A36, GOBOARD5:2;
then (G * (k,i)) `1 >= (G * (j0,i)) `1 by A18, XXREAL_0:2;
then A52: k >= j0 by A13, A11, A36, GOBOARD5:3;
(abs (i0 - io)) + (abs (j0 - jo)) = 1 by A1, A31, A27, A32, A33, A28, A29, GOBOARD1:def_9;
then 0 + (abs (j0 - jo)) = 1 by A42, A41, ABSVALUE:2;
then A53: abs (- (j0 - jo)) = 1 by COMPLEX1:52;
j0 <= jo + 0 by A33, A29, A36, A35, A30, A42, A41, A43, GOBOARD5:3;
then j0 - jo <= 0 by XREAL_1:20;
then jo - j0 = 1 by A53, ABSVALUE:def_1;
then A54: j0 + 1 = jo + 0 ;
( (G * (jo,i)) `1 > (G * (k,i)) `1 & jo >= k ) by A29, A15, A11, A30, A41, A51, GOBOARD5:3;
then jo > k by XXREAL_0:1;
then j0 >= k by A54, NAT_1:13;
then A55: k = j0 by A52, XXREAL_0:1;
take n = j0; ::_thesis: ( j <= n & n <= k & G * (n,i) = p )
A56: p `2 = (G * (j,i)) `2 by A20, A9, GOBOARD7:6
.= (G * (1,i)) `2 by A6, A19, A14, GOBOARD5:1
.= (G * (n,i)) `2 by A14, A34, A36, GOBOARD5:1 ;
p `1 >= (G * (j0,i0)) `1 by A26, A33, A43, TOPREAL1:3;
then p `1 >= (G * (j0,1)) `1 by A34, A36, A35, GOBOARD5:2;
then p `1 >= (G * (j0,i)) `1 by A14, A34, A36, GOBOARD5:2;
then p `1 = (G * (k,i)) `1 by A18, A55, XXREAL_0:1;
hence ( j <= n & n <= k & G * (n,i) = p ) by A5, A55, A56, TOPREAL3:6; ::_thesis: verum
end;
supposeA57: (f /. (i1 + 1)) `1 < (G * (j,i)) `1 ; ::_thesis: ex n being Element of NAT st
( j <= n & n <= k & G * (n,i) = p )
p `1 <= (f /. (i1 + 1)) `1 by A26, A43, TOPREAL1:3;
hence ex n being Element of NAT st
( j <= n & n <= k & G * (n,i) = p ) by A17, A57, XXREAL_0:2; ::_thesis: verum
end;
end;
end;
end;
end;
end;
end;
supposeA58: (f /. i1) `1 > (f /. (i1 + 1)) `1 ; ::_thesis: ex n being Element of NAT st
( j <= n & n <= k & G * (n,i) = p )
thus ex n being Element of NAT st
( j <= n & n <= k & G * (n,i) = p ) ::_thesis: verum
proof
percases ( f /. i1 in LSeg ((G * (j,i)),(G * (k,i))) or not f /. i1 in LSeg ((G * (j,i)),(G * (k,i))) ) ;
supposeA59: f /. i1 in LSeg ((G * (j,i)),(G * (k,i))) ; ::_thesis: ex n being Element of NAT st
( j <= n & n <= k & G * (n,i) = p )
1 + 1 <= i1 + 1 by A24, XREAL_1:6;
then f /. i1 in L~ f by A25, A31, GOBOARD1:1, XXREAL_0:2;
then f /. i1 in X1 by A59, XBOOLE_0:def_4;
then A60: p `1 >= (f /. i1) `1 by A10, A12, PSCOMP_1:24;
take n = j0; ::_thesis: ( j <= n & n <= k & G * (n,i) = p )
A61: p in LSeg ((G * (j,i)),(G * (k,i))) by A8, XBOOLE_0:def_4;
p `1 <= (f /. i1) `1 by A26, A58, TOPREAL1:3;
then p `1 = (f /. i1) `1 by A60, XXREAL_0:1;
then A62: p `1 = (G * (j0,1)) `1 by A33, A34, A36, A35, GOBOARD5:2
.= (G * (n,i)) `1 by A14, A34, A36, GOBOARD5:2 ;
A63: (G * (j,i)) `1 <= (G * (k,i)) `1 by A5, A6, A14, A15, SPRECT_3:13;
then (G * (j,i)) `1 <= (G * (n,i)) `1 by A61, A62, TOPREAL1:3;
hence j <= n by A19, A14, A34, GOBOARD5:3; ::_thesis: ( n <= k & G * (n,i) = p )
(G * (n,i)) `1 <= (G * (k,i)) `1 by A61, A62, A63, TOPREAL1:3;
hence n <= k by A13, A11, A36, GOBOARD5:3; ::_thesis: G * (n,i) = p
p `2 = (G * (j,i)) `2 by A20, A61, GOBOARD7:6
.= (G * (1,i)) `2 by A6, A19, A14, GOBOARD5:1
.= (G * (n,i)) `2 by A14, A34, A36, GOBOARD5:1 ;
hence G * (n,i) = p by A62, TOPREAL3:6; ::_thesis: verum
end;
supposeA64: not f /. i1 in LSeg ((G * (j,i)),(G * (k,i))) ; ::_thesis: ex n being Element of NAT st
( j <= n & n <= k & G * (n,i) = p )
A65: (f /. i1) `2 = p `2 by A26, A40, GOBOARD7:6
.= (G * (j,i)) `2 by A20, A9, GOBOARD7:6 ;
thus ex n being Element of NAT st
( j <= n & n <= k & G * (n,i) = p ) ::_thesis: verum
proof
percases ( (f /. i1) `1 > (G * (k,i)) `1 or (f /. i1) `1 < (G * (j,i)) `1 ) by A20, A64, A65, GOBOARD7:8;
supposeA66: (f /. i1) `1 > (G * (k,i)) `1 ; ::_thesis: ex n being Element of NAT st
( j <= n & n <= k & G * (n,i) = p )
p `1 >= (G * (jo,io)) `1 by A26, A29, A58, TOPREAL1:3;
then p `1 >= (G * (jo,1)) `1 by A30, A38, A37, GOBOARD5:2;
then p `1 >= (G * (jo,i)) `1 by A14, A30, A38, GOBOARD5:2;
then (G * (k,i)) `1 >= (G * (jo,i)) `1 by A18, XXREAL_0:2;
then A67: k >= jo by A13, A11, A38, GOBOARD5:3;
jo <= j0 + 0 by A33, A29, A34, A35, A38, A42, A41, A58, GOBOARD5:3;
then jo - j0 <= 0 by XREAL_1:20;
then A68: - (jo - j0) >= - 0 ;
(abs (i0 - io)) + (abs (j0 - jo)) = 1 by A1, A31, A27, A32, A33, A28, A29, GOBOARD1:def_9;
then 0 + (abs (j0 - jo)) = 1 by A42, A41, ABSVALUE:2;
then j0 - jo = 1 by A68, ABSVALUE:def_1;
then A69: jo + 1 = j0 - 0 ;
( (G * (j0,i)) `1 > (G * (k,i)) `1 & j0 >= k ) by A33, A15, A11, A34, A42, A66, GOBOARD5:3;
then j0 > k by XXREAL_0:1;
then jo >= k by A69, NAT_1:13;
then A70: k = jo by A67, XXREAL_0:1;
take n = jo; ::_thesis: ( j <= n & n <= k & G * (n,i) = p )
A71: p `2 = (G * (j,i)) `2 by A20, A9, GOBOARD7:6
.= (G * (1,i)) `2 by A6, A19, A14, GOBOARD5:1
.= (G * (n,i)) `2 by A14, A30, A38, GOBOARD5:1 ;
p `1 >= (G * (jo,io)) `1 by A26, A29, A58, TOPREAL1:3;
then p `1 >= (G * (jo,1)) `1 by A30, A38, A37, GOBOARD5:2;
then p `1 >= (G * (jo,i)) `1 by A14, A30, A38, GOBOARD5:2;
then p `1 = (G * (k,i)) `1 by A18, A70, XXREAL_0:1;
hence ( j <= n & n <= k & G * (n,i) = p ) by A5, A70, A71, TOPREAL3:6; ::_thesis: verum
end;
supposeA72: (f /. i1) `1 < (G * (j,i)) `1 ; ::_thesis: ex n being Element of NAT st
( j <= n & n <= k & G * (n,i) = p )
p `1 <= (f /. i1) `1 by A26, A58, TOPREAL1:3;
hence ex n being Element of NAT st
( j <= n & n <= k & G * (n,i) = p ) by A17, A72, XXREAL_0:2; ::_thesis: verum
end;
end;
end;
end;
end;
end;
end;
end;
end;
end;
supposeA73: (f /. i1) `1 = (f /. (i1 + 1)) `1 ; ::_thesis: ex n being Element of NAT st
( j <= n & n <= k & G * (n,i) = p )
take n = j0; ::_thesis: ( j <= n & n <= k & G * (n,i) = p )
p `1 = (f /. i1) `1 by A26, A73, GOBOARD7:5;
then A74: p `1 = (G * (j0,1)) `1 by A33, A34, A36, A35, GOBOARD5:2
.= (G * (n,i)) `1 by A14, A34, A36, GOBOARD5:2 ;
A75: (G * (j,i)) `1 <= (G * (k,i)) `1 by A5, A6, A14, A15, SPRECT_3:13;
then (G * (j,i)) `1 <= (G * (n,i)) `1 by A9, A74, TOPREAL1:3;
hence j <= n by A19, A14, A34, GOBOARD5:3; ::_thesis: ( n <= k & G * (n,i) = p )
(G * (n,i)) `1 <= (G * (k,i)) `1 by A9, A74, A75, TOPREAL1:3;
hence n <= k by A13, A11, A36, GOBOARD5:3; ::_thesis: G * (n,i) = p
p `2 = (G * (j,i)) `2 by A20, A9, GOBOARD7:6
.= (G * (1,i)) `2 by A6, A19, A14, GOBOARD5:1
.= (G * (n,i)) `2 by A14, A34, A36, GOBOARD5:1 ;
hence G * (n,i) = p by A74, TOPREAL3:6; ::_thesis: verum
end;
end;
end;
hence ex n being Element of NAT st
( j <= n & n <= k & (G * (n,i)) `1 = upper_bound (proj1 .: ((LSeg ((G * (j,i)),(G * (k,i)))) /\ (L~ f))) ) by A12; ::_thesis: verum
end;
theorem Th5: :: JORDAN1F:5
for C being compact non horizontal non vertical Subset of (TOP-REAL 2)
for n being Element of NAT holds (Upper_Seq (C,n)) /. 1 = W-min (L~ (Cage (C,n)))
proof
let C be compact non horizontal non vertical Subset of (TOP-REAL 2); ::_thesis: for n being Element of NAT holds (Upper_Seq (C,n)) /. 1 = W-min (L~ (Cage (C,n)))
let n be Element of NAT ; ::_thesis: (Upper_Seq (C,n)) /. 1 = W-min (L~ (Cage (C,n)))
E-max (L~ (Cage (C,n))) in rng (Cage (C,n)) by SPRECT_2:46;
then ( Upper_Seq (C,n) = (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) -: (E-max (L~ (Cage (C,n)))) & E-max (L~ (Cage (C,n))) in rng (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) ) by FINSEQ_6:90, JORDAN1E:def_1, SPRECT_2:43;
then ( W-min (L~ (Cage (C,n))) in rng (Cage (C,n)) & (Upper_Seq (C,n)) /. 1 = (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) /. 1 ) by FINSEQ_5:44, SPRECT_2:43;
hence (Upper_Seq (C,n)) /. 1 = W-min (L~ (Cage (C,n))) by FINSEQ_6:92; ::_thesis: verum
end;
theorem Th6: :: JORDAN1F:6
for C being compact non horizontal non vertical Subset of (TOP-REAL 2)
for n being Element of NAT holds (Lower_Seq (C,n)) /. 1 = E-max (L~ (Cage (C,n)))
proof
let C be compact non horizontal non vertical Subset of (TOP-REAL 2); ::_thesis: for n being Element of NAT holds (Lower_Seq (C,n)) /. 1 = E-max (L~ (Cage (C,n)))
let n be Element of NAT ; ::_thesis: (Lower_Seq (C,n)) /. 1 = E-max (L~ (Cage (C,n)))
Lower_Seq (C,n) = (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) :- (E-max (L~ (Cage (C,n)))) by JORDAN1E:def_2;
hence (Lower_Seq (C,n)) /. 1 = E-max (L~ (Cage (C,n))) by FINSEQ_5:53; ::_thesis: verum
end;
theorem Th7: :: JORDAN1F:7
for C being compact non horizontal non vertical Subset of (TOP-REAL 2)
for n being Element of NAT holds (Upper_Seq (C,n)) /. (len (Upper_Seq (C,n))) = E-max (L~ (Cage (C,n)))
proof
let C be compact non horizontal non vertical Subset of (TOP-REAL 2); ::_thesis: for n being Element of NAT holds (Upper_Seq (C,n)) /. (len (Upper_Seq (C,n))) = E-max (L~ (Cage (C,n)))
let n be Element of NAT ; ::_thesis: (Upper_Seq (C,n)) /. (len (Upper_Seq (C,n))) = E-max (L~ (Cage (C,n)))
A1: ( Upper_Seq (C,n) = (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) -: (E-max (L~ (Cage (C,n)))) & rng (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) = rng (Cage (C,n)) ) by FINSEQ_6:90, JORDAN1E:def_1, SPRECT_2:43;
then len (Upper_Seq (C,n)) = (E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) by FINSEQ_5:42, SPRECT_2:46;
hence (Upper_Seq (C,n)) /. (len (Upper_Seq (C,n))) = E-max (L~ (Cage (C,n))) by A1, FINSEQ_5:45, SPRECT_2:46; ::_thesis: verum
end;
theorem Th8: :: JORDAN1F:8
for C being compact non horizontal non vertical Subset of (TOP-REAL 2)
for n being Element of NAT holds (Lower_Seq (C,n)) /. (len (Lower_Seq (C,n))) = W-min (L~ (Cage (C,n)))
proof
let C be compact non horizontal non vertical Subset of (TOP-REAL 2); ::_thesis: for n being Element of NAT holds (Lower_Seq (C,n)) /. (len (Lower_Seq (C,n))) = W-min (L~ (Cage (C,n)))
let n be Element of NAT ; ::_thesis: (Lower_Seq (C,n)) /. (len (Lower_Seq (C,n))) = W-min (L~ (Cage (C,n)))
A1: W-min (L~ (Cage (C,n))) in rng (Cage (C,n)) by SPRECT_2:43;
E-max (L~ (Cage (C,n))) in rng (Cage (C,n)) by SPRECT_2:46;
then ( Lower_Seq (C,n) = (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) :- (E-max (L~ (Cage (C,n)))) & E-max (L~ (Cage (C,n))) in rng (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) ) by FINSEQ_6:90, JORDAN1E:def_2, SPRECT_2:43;
hence (Lower_Seq (C,n)) /. (len (Lower_Seq (C,n))) = (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) /. (len (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n))))))) by FINSEQ_5:54
.= (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) /. 1 by FINSEQ_6:def_1
.= W-min (L~ (Cage (C,n))) by A1, FINSEQ_6:92 ;
::_thesis: verum
end;
theorem Th9: :: JORDAN1F:9
for C being compact non horizontal non vertical Subset of (TOP-REAL 2)
for n being Element of NAT holds
( ( L~ (Upper_Seq (C,n)) = Upper_Arc (L~ (Cage (C,n))) & L~ (Lower_Seq (C,n)) = Lower_Arc (L~ (Cage (C,n))) ) or ( L~ (Upper_Seq (C,n)) = Lower_Arc (L~ (Cage (C,n))) & L~ (Lower_Seq (C,n)) = Upper_Arc (L~ (Cage (C,n))) ) )
proof
let C be compact non horizontal non vertical Subset of (TOP-REAL 2); ::_thesis: for n being Element of NAT holds
( ( L~ (Upper_Seq (C,n)) = Upper_Arc (L~ (Cage (C,n))) & L~ (Lower_Seq (C,n)) = Lower_Arc (L~ (Cage (C,n))) ) or ( L~ (Upper_Seq (C,n)) = Lower_Arc (L~ (Cage (C,n))) & L~ (Lower_Seq (C,n)) = Upper_Arc (L~ (Cage (C,n))) ) )
let n be Element of NAT ; ::_thesis: ( ( L~ (Upper_Seq (C,n)) = Upper_Arc (L~ (Cage (C,n))) & L~ (Lower_Seq (C,n)) = Lower_Arc (L~ (Cage (C,n))) ) or ( L~ (Upper_Seq (C,n)) = Lower_Arc (L~ (Cage (C,n))) & L~ (Lower_Seq (C,n)) = Upper_Arc (L~ (Cage (C,n))) ) )
set WC = W-min (L~ (Cage (C,n)));
set EC = E-max (L~ (Cage (C,n)));
A1: ( Lower_Arc (L~ (Cage (C,n))) is_an_arc_of W-min (L~ (Cage (C,n))), E-max (L~ (Cage (C,n))) & (Upper_Arc (L~ (Cage (C,n)))) \/ (Lower_Arc (L~ (Cage (C,n)))) = L~ (Cage (C,n)) ) by JORDAN6:50;
( (Upper_Seq (C,n)) /. 1 = W-min (L~ (Cage (C,n))) & (Upper_Seq (C,n)) /. (len (Upper_Seq (C,n))) = E-max (L~ (Cage (C,n))) ) by Th5, Th7;
then A2: L~ (Upper_Seq (C,n)) is_an_arc_of W-min (L~ (Cage (C,n))), E-max (L~ (Cage (C,n))) by TOPREAL1:25;
( (Lower_Seq (C,n)) /. 1 = E-max (L~ (Cage (C,n))) & (Lower_Seq (C,n)) /. (len (Lower_Seq (C,n))) = W-min (L~ (Cage (C,n))) ) by Th6, Th8;
then A3: L~ (Lower_Seq (C,n)) is_an_arc_of W-min (L~ (Cage (C,n))), E-max (L~ (Cage (C,n))) by JORDAN5B:14, TOPREAL1:25;
( (L~ (Upper_Seq (C,n))) \/ (L~ (Lower_Seq (C,n))) = L~ (Cage (C,n)) & Upper_Arc (L~ (Cage (C,n))) is_an_arc_of W-min (L~ (Cage (C,n))), E-max (L~ (Cage (C,n))) ) by JORDAN1E:13, JORDAN6:50;
hence ( ( L~ (Upper_Seq (C,n)) = Upper_Arc (L~ (Cage (C,n))) & L~ (Lower_Seq (C,n)) = Lower_Arc (L~ (Cage (C,n))) ) or ( L~ (Upper_Seq (C,n)) = Lower_Arc (L~ (Cage (C,n))) & L~ (Lower_Seq (C,n)) = Upper_Arc (L~ (Cage (C,n))) ) ) by A2, A3, A1, JORDAN6:48; ::_thesis: verum
end;
theorem Th10: :: JORDAN1F:10
for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2)
for n being Element of NAT holds Upper_Seq (C,n) is_sequence_on Gauge (C,n)
proof
let C be connected compact non horizontal non vertical Subset of (TOP-REAL 2); ::_thesis: for n being Element of NAT holds Upper_Seq (C,n) is_sequence_on Gauge (C,n)
let n be Element of NAT ; ::_thesis: Upper_Seq (C,n) is_sequence_on Gauge (C,n)
Cage (C,n) is_sequence_on Gauge (C,n) by JORDAN9:def_1;
then A1: Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n))))) is_sequence_on Gauge (C,n) by REVROT_1:34;
Upper_Seq (C,n) = (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) -: (E-max (L~ (Cage (C,n)))) by JORDAN1E:def_1
.= (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) | ((E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n))))))) by FINSEQ_5:def_1 ;
hence Upper_Seq (C,n) is_sequence_on Gauge (C,n) by A1, GOBOARD1:22; ::_thesis: verum
end;
theorem Th11: :: JORDAN1F:11
for G being Go-board
for p being Point of (TOP-REAL 2)
for f being FinSequence of (TOP-REAL 2) st f is_sequence_on G & ex i, j being Element of NAT st
( [i,j] in Indices G & p = G * (i,j) ) & ( for i1, j1, i2, j2 being Element of NAT st [i1,j1] in Indices G & [i2,j2] in Indices G & p = G * (i1,j1) & f /. 1 = G * (i2,j2) holds
(abs (i2 - i1)) + (abs (j2 - j1)) = 1 ) holds
<*p*> ^ f is_sequence_on G
proof
let G be Go-board; ::_thesis: for p being Point of (TOP-REAL 2)
for f being FinSequence of (TOP-REAL 2) st f is_sequence_on G & ex i, j being Element of NAT st
( [i,j] in Indices G & p = G * (i,j) ) & ( for i1, j1, i2, j2 being Element of NAT st [i1,j1] in Indices G & [i2,j2] in Indices G & p = G * (i1,j1) & f /. 1 = G * (i2,j2) holds
(abs (i2 - i1)) + (abs (j2 - j1)) = 1 ) holds
<*p*> ^ f is_sequence_on G
let p be Point of (TOP-REAL 2); ::_thesis: for f being FinSequence of (TOP-REAL 2) st f is_sequence_on G & ex i, j being Element of NAT st
( [i,j] in Indices G & p = G * (i,j) ) & ( for i1, j1, i2, j2 being Element of NAT st [i1,j1] in Indices G & [i2,j2] in Indices G & p = G * (i1,j1) & f /. 1 = G * (i2,j2) holds
(abs (i2 - i1)) + (abs (j2 - j1)) = 1 ) holds
<*p*> ^ f is_sequence_on G
let f be FinSequence of (TOP-REAL 2); ::_thesis: ( f is_sequence_on G & ex i, j being Element of NAT st
( [i,j] in Indices G & p = G * (i,j) ) & ( for i1, j1, i2, j2 being Element of NAT st [i1,j1] in Indices G & [i2,j2] in Indices G & p = G * (i1,j1) & f /. 1 = G * (i2,j2) holds
(abs (i2 - i1)) + (abs (j2 - j1)) = 1 ) implies <*p*> ^ f is_sequence_on G )
assume that
A1: f is_sequence_on G and
A2: ex i, j being Element of NAT st
( [i,j] in Indices G & p = G * (i,j) ) and
A3: for i1, j1, i2, j2 being Element of NAT st [i1,j1] in Indices G & [i2,j2] in Indices G & p = G * (i1,j1) & f /. 1 = G * (i2,j2) holds
(abs (i2 - i1)) + (abs (j2 - j1)) = 1 ; ::_thesis: <*p*> ^ f is_sequence_on G
A4: now__::_thesis:_for_m,_k,_i,_j_being_Element_of_NAT_st_[m,k]_in_Indices_G_&_[i,j]_in_Indices_G_&_<*p*>_/._(len_<*p*>)_=_G_*_(m,k)_&_f_/._1_=_G_*_(i,j)_&_len_<*p*>_in_dom_<*p*>_&_1_in_dom_f_holds_
1_=_(abs_(m_-_i))_+_(abs_(k_-_j))
let m, k, i, j be Element of NAT ; ::_thesis: ( [m,k] in Indices G & [i,j] in Indices G & <*p*> /. (len <*p*>) = G * (m,k) & f /. 1 = G * (i,j) & len <*p*> in dom <*p*> & 1 in dom f implies 1 = (abs (m - i)) + (abs (k - j)) )
assume that
A5: ( [m,k] in Indices G & [i,j] in Indices G & <*p*> /. (len <*p*>) = G * (m,k) & f /. 1 = G * (i,j) ) and
A6: len <*p*> in dom <*p*> and
1 in dom f ; ::_thesis: 1 = (abs (m - i)) + (abs (k - j))
len <*p*> = 1 by FINSEQ_1:40;
then <*p*> . (len <*p*>) = p by FINSEQ_1:40;
then <*p*> /. (len <*p*>) = p by A6, PARTFUN1:def_6;
then (abs (i - m)) + (abs (j - k)) = 1 by A3, A5;
hence 1 = (abs (m - i)) + (abs (j - k)) by UNIFORM1:11
.= (abs (m - i)) + (abs (k - j)) by UNIFORM1:11 ;
::_thesis: verum
end;
A7: now__::_thesis:_for_n_being_Element_of_NAT_st_n_in_dom_(<*p*>_^_f)_holds_
ex_i,_j_being_Element_of_NAT_st_
(_[i,j]_in_Indices_G_&_(<*p*>_^_f)_/._n_=_G_*_(i,j)_)
let n be Element of NAT ; ::_thesis: ( n in dom (<*p*> ^ f) implies ex i, j being Element of NAT st
( [j,b3] in Indices G & (<*p*> ^ f) /. i = G * (j,b3) ) )
assume A8: n in dom (<*p*> ^ f) ; ::_thesis: ex i, j being Element of NAT st
( [j,b3] in Indices G & (<*p*> ^ f) /. i = G * (j,b3) )
percases ( n in dom <*p*> or ex l being Nat st
( l in dom f & n = (len <*p*>) + l ) ) by A8, FINSEQ_1:25;
supposeA9: n in dom <*p*> ; ::_thesis: ex i, j being Element of NAT st
( [j,b3] in Indices G & (<*p*> ^ f) /. i = G * (j,b3) )
consider i, j being Element of NAT such that
A10: [i,j] in Indices G and
A11: p = G * (i,j) by A2;
take i = i; ::_thesis: ex j being Element of NAT st
( [i,j] in Indices G & (<*p*> ^ f) /. n = G * (i,j) )
take j = j; ::_thesis: ( [i,j] in Indices G & (<*p*> ^ f) /. n = G * (i,j) )
thus [i,j] in Indices G by A10; ::_thesis: (<*p*> ^ f) /. n = G * (i,j)
n in Seg 1 by A9, FINSEQ_1:38;
then ( 1 <= n & n <= 1 ) by FINSEQ_1:1;
then n = 1 by XXREAL_0:1;
then <*p*> . n = p by FINSEQ_1:40;
then <*p*> /. n = p by A9, PARTFUN1:def_6;
hence (<*p*> ^ f) /. n = G * (i,j) by A9, A11, FINSEQ_4:68; ::_thesis: verum
end;
suppose ex l being Nat st
( l in dom f & n = (len <*p*>) + l ) ; ::_thesis: ex i, j being Element of NAT st
( [j,b3] in Indices G & (<*p*> ^ f) /. i = G * (j,b3) )
then consider l being Nat such that
A12: l in dom f and
A13: n = (len <*p*>) + l ;
consider i, j being Element of NAT such that
A14: [i,j] in Indices G and
A15: f /. l = G * (i,j) by A1, A12, GOBOARD1:def_9;
take i = i; ::_thesis: ex j being Element of NAT st
( [i,j] in Indices G & (<*p*> ^ f) /. n = G * (i,j) )
take j = j; ::_thesis: ( [i,j] in Indices G & (<*p*> ^ f) /. n = G * (i,j) )
thus [i,j] in Indices G by A14; ::_thesis: (<*p*> ^ f) /. n = G * (i,j)
thus (<*p*> ^ f) /. n = G * (i,j) by A12, A13, A15, FINSEQ_4:69; ::_thesis: verum
end;
end;
end;
A16: now__::_thesis:_for_n_being_Element_of_NAT_st_n_in_dom_<*p*>_&_n_+_1_in_dom_<*p*>_holds_
for_m,_k,_i,_j_being_Element_of_NAT_st_[m,k]_in_Indices_G_&_[i,j]_in_Indices_G_&_<*p*>_/._n_=_G_*_(m,k)_&_<*p*>_/._(n_+_1)_=_G_*_(i,j)_holds_
(abs_(m_-_i))_+_(abs_(k_-_j))_=_1
let n be Element of NAT ; ::_thesis: ( n in dom <*p*> & n + 1 in dom <*p*> implies for m, k, i, j being Element of NAT st [m,k] in Indices G & [i,j] in Indices G & <*p*> /. n = G * (m,k) & <*p*> /. (n + 1) = G * (i,j) holds
(abs (m - i)) + (abs (k - j)) = 1 )
assume that
A17: n in dom <*p*> and
A18: n + 1 in dom <*p*> ; ::_thesis: for m, k, i, j being Element of NAT st [m,k] in Indices G & [i,j] in Indices G & <*p*> /. n = G * (m,k) & <*p*> /. (n + 1) = G * (i,j) holds
(abs (m - i)) + (abs (k - j)) = 1
n + 1 <= len <*p*> by A18, FINSEQ_3:25;
then A19: n + 1 <= 1 by FINSEQ_1:39;
1 <= n by A17, FINSEQ_3:25;
then 1 + 1 <= n + 1 by XREAL_1:6;
hence for m, k, i, j being Element of NAT st [m,k] in Indices G & [i,j] in Indices G & <*p*> /. n = G * (m,k) & <*p*> /. (n + 1) = G * (i,j) holds
(abs (m - i)) + (abs (k - j)) = 1 by A19, XXREAL_0:2; ::_thesis: verum
end;
for n being Element of NAT st n in dom f & n + 1 in dom f holds
for m, k, i, j being Element of NAT st [m,k] in Indices G & [i,j] in Indices G & f /. n = G * (m,k) & f /. (n + 1) = G * (i,j) holds
(abs (m - i)) + (abs (k - j)) = 1 by A1, GOBOARD1:def_9;
then for n being Element of NAT st n in dom (<*p*> ^ f) & n + 1 in dom (<*p*> ^ f) holds
for m, k, i, j being Element of NAT st [m,k] in Indices G & [i,j] in Indices G & (<*p*> ^ f) /. n = G * (m,k) & (<*p*> ^ f) /. (n + 1) = G * (i,j) holds
(abs (m - i)) + (abs (k - j)) = 1 by A16, A4, GOBOARD1:24;
hence <*p*> ^ f is_sequence_on G by A7, GOBOARD1:def_9; ::_thesis: verum
end;
theorem Th12: :: JORDAN1F:12
for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2)
for n being Element of NAT holds Lower_Seq (C,n) is_sequence_on Gauge (C,n)
proof
let C be connected compact non horizontal non vertical Subset of (TOP-REAL 2); ::_thesis: for n being Element of NAT holds Lower_Seq (C,n) is_sequence_on Gauge (C,n)
let n be Element of NAT ; ::_thesis: Lower_Seq (C,n) is_sequence_on Gauge (C,n)
consider j being Element of NAT such that
A1: ( 1 <= j & j <= width (Gauge (C,n)) ) and
A2: E-max (L~ (Cage (C,n))) = (Gauge (C,n)) * ((len (Gauge (C,n))),j) by JORDAN1D:25;
set E1 = ((Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) /^ ((E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))))) /. 1;
set i = len (Gauge (C,n));
A3: Lower_Seq (C,n) = (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) :- (E-max (L~ (Cage (C,n)))) by JORDAN1E:def_2
.= <*(E-max (L~ (Cage (C,n))))*> ^ ((Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) /^ ((E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))))) by FINSEQ_5:def_2 ;
A4: Cage (C,n) is_sequence_on Gauge (C,n) by JORDAN9:def_1;
then Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n))))) is_sequence_on Gauge (C,n) by REVROT_1:34;
then A5: (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) /^ ((E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n))))))) is_sequence_on Gauge (C,n) by JORDAN8:2;
A6: for i1, j1, i2, j2 being Element of NAT st [i1,j1] in Indices (Gauge (C,n)) & [i2,j2] in Indices (Gauge (C,n)) & E-max (L~ (Cage (C,n))) = (Gauge (C,n)) * (i1,j1) & ((Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) /^ ((E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))))) /. 1 = (Gauge (C,n)) * (i2,j2) holds
(abs (i2 - i1)) + (abs (j2 - j1)) = 1
proof
set en = (E-max (L~ (Cage (C,n)))) .. (Cage (C,n));
let i1, j1, i2, j2 be Element of NAT ; ::_thesis: ( [i1,j1] in Indices (Gauge (C,n)) & [i2,j2] in Indices (Gauge (C,n)) & E-max (L~ (Cage (C,n))) = (Gauge (C,n)) * (i1,j1) & ((Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) /^ ((E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))))) /. 1 = (Gauge (C,n)) * (i2,j2) implies (abs (i2 - i1)) + (abs (j2 - j1)) = 1 )
assume A7: ( [i1,j1] in Indices (Gauge (C,n)) & [i2,j2] in Indices (Gauge (C,n)) & E-max (L~ (Cage (C,n))) = (Gauge (C,n)) * (i1,j1) & ((Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) /^ ((E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))))) /. 1 = (Gauge (C,n)) * (i2,j2) ) ; ::_thesis: (abs (i2 - i1)) + (abs (j2 - j1)) = 1
(E-max (L~ (Cage (C,n)))) .. (Cage (C,n)) < len (Cage (C,n)) by SPRECT_5:16;
then ( 1 <= ((E-max (L~ (Cage (C,n)))) .. (Cage (C,n))) + 1 & ((E-max (L~ (Cage (C,n)))) .. (Cage (C,n))) + 1 <= len (Cage (C,n)) ) by NAT_1:11, NAT_1:13;
then A8: ((E-max (L~ (Cage (C,n)))) .. (Cage (C,n))) + 1 in dom (Cage (C,n)) by FINSEQ_3:25;
A9: W-min (L~ (Cage (C,n))) in rng (Cage (C,n)) by SPRECT_2:43;
A10: (Cage (C,n)) /. 1 = N-min (L~ (Cage (C,n))) by JORDAN9:32;
then (E-max (L~ (Cage (C,n)))) .. (Cage (C,n)) < (E-min (L~ (Cage (C,n)))) .. (Cage (C,n)) by SPRECT_2:71;
then (E-max (L~ (Cage (C,n)))) .. (Cage (C,n)) < (S-max (L~ (Cage (C,n)))) .. (Cage (C,n)) by A10, SPRECT_2:72, XXREAL_0:2;
then (E-max (L~ (Cage (C,n)))) .. (Cage (C,n)) < (S-min (L~ (Cage (C,n)))) .. (Cage (C,n)) by A10, SPRECT_2:73, XXREAL_0:2;
then A11: (E-max (L~ (Cage (C,n)))) .. (Cage (C,n)) < (W-min (L~ (Cage (C,n)))) .. (Cage (C,n)) by A10, SPRECT_2:74, XXREAL_0:2;
then A12: ((E-max (L~ (Cage (C,n)))) .. (Cage (C,n))) + 1 <= (W-min (L~ (Cage (C,n)))) .. (Cage (C,n)) by NAT_1:13;
A13: (len (Cage (C,n))) - ((W-min (L~ (Cage (C,n)))) .. (Cage (C,n))) > 0 by SPRECT_5:20, XREAL_1:50;
then A14: (((E-max (L~ (Cage (C,n)))) .. (Cage (C,n))) + 1) + ((len (Cage (C,n))) - ((W-min (L~ (Cage (C,n)))) .. (Cage (C,n)))) >= 0 + 0 ;
A15: E-max (L~ (Cage (C,n))) in rng (Cage (C,n)) by SPRECT_2:46;
then 1 <= (E-max (L~ (Cage (C,n)))) .. (Cage (C,n)) by FINSEQ_4:21;
then A16: 1 < ((E-max (L~ (Cage (C,n)))) .. (Cage (C,n))) + 1 by NAT_1:13;
E-max (L~ (Cage (C,n))) in rng (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) by A15, FINSEQ_6:90, SPRECT_2:43;
then A17: (E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) <= len (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) by FINSEQ_4:21;
now__::_thesis:_not_(E-max_(L~_(Cage_(C,n))))_.._(Rotate_((Cage_(C,n)),(W-min_(L~_(Cage_(C,n))))))_=_len_(Rotate_((Cage_(C,n)),(W-min_(L~_(Cage_(C,n))))))
assume (E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) = len (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) ; ::_thesis: contradiction
then (E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) = len (Cage (C,n)) by REVROT_1:14;
then len (Upper_Seq (C,n)) = len (Cage (C,n)) by JORDAN1E:8;
then (len (Cage (C,n))) + (len (Lower_Seq (C,n))) = (len (Cage (C,n))) + 1 by JORDAN1E:10;
hence contradiction by JORDAN1E:15; ::_thesis: verum
end;
then (E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) < len (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) by A17, XXREAL_0:1;
then ((E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n))))))) + 1 <= len (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) by NAT_1:13;
then (1 + ((E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))))) - ((E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n))))))) <= (len (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n))))))) - ((E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n))))))) by XREAL_1:9;
then 1 <= len ((Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) /^ ((E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))))) by A17, RFINSEQ:def_1;
then 1 in dom ((Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) /^ ((E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))))) by FINSEQ_3:25;
then ((Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) /^ ((E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))))) /. 1 = (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) /. (((E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n))))))) + 1) by FINSEQ_5:27
.= (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) /. ((((len (Cage (C,n))) + ((E-max (L~ (Cage (C,n)))) .. (Cage (C,n)))) - ((W-min (L~ (Cage (C,n)))) .. (Cage (C,n)))) + 1) by A15, A9, A11, SPRECT_5:9
.= (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) /. ((((E-max (L~ (Cage (C,n)))) .. (Cage (C,n))) + ((len (Cage (C,n))) - ((W-min (L~ (Cage (C,n)))) .. (Cage (C,n))))) + 1)
.= (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) /. ((((E-max (L~ (Cage (C,n)))) .. (Cage (C,n))) + ((len (Cage (C,n))) -' ((W-min (L~ (Cage (C,n)))) .. (Cage (C,n))))) + 1) by A13, XREAL_0:def_2
.= (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) /. ((((E-max (L~ (Cage (C,n)))) .. (Cage (C,n))) + 1) + ((len (Cage (C,n))) -' ((W-min (L~ (Cage (C,n)))) .. (Cage (C,n)))))
.= (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) /. ((((E-max (L~ (Cage (C,n)))) .. (Cage (C,n))) + 1) + ((len (Cage (C,n))) - ((W-min (L~ (Cage (C,n)))) .. (Cage (C,n))))) by A13, XREAL_0:def_2
.= (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) /. (((((E-max (L~ (Cage (C,n)))) .. (Cage (C,n))) + 1) + (len (Cage (C,n)))) - ((W-min (L~ (Cage (C,n)))) .. (Cage (C,n))))
.= (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) /. (((((E-max (L~ (Cage (C,n)))) .. (Cage (C,n))) + 1) + (len (Cage (C,n)))) -' ((W-min (L~ (Cage (C,n)))) .. (Cage (C,n)))) by A14, XREAL_0:def_2 ;
then A18: ((Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) /^ ((E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))))) /. 1 = (Cage (C,n)) /. (((E-max (L~ (Cage (C,n)))) .. (Cage (C,n))) + 1) by A9, A16, A12, REVROT_1:13;
( E-max (L~ (Cage (C,n))) = (Cage (C,n)) /. ((E-max (L~ (Cage (C,n)))) .. (Cage (C,n))) & (E-max (L~ (Cage (C,n)))) .. (Cage (C,n)) in dom (Cage (C,n)) ) by A15, FINSEQ_4:20, FINSEQ_5:38;
then (abs (i1 - i2)) + (abs (j1 - j2)) = 1 by A4, A7, A8, A18, GOBOARD1:def_9;
then (abs (i1 - i2)) + (abs (j2 - j1)) = 1 by UNIFORM1:11;
hence (abs (i2 - i1)) + (abs (j2 - j1)) = 1 by UNIFORM1:11; ::_thesis: verum
end;
len (Gauge (C,n)) >= 4 by JORDAN8:10;
then 1 <= len (Gauge (C,n)) by XXREAL_0:2;
then [(len (Gauge (C,n))),j] in Indices (Gauge (C,n)) by A1, MATRIX_1:36;
hence Lower_Seq (C,n) is_sequence_on Gauge (C,n) by A5, A2, A6, A3, Th11; ::_thesis: verum
end;
theorem :: JORDAN1F:13
for i being Element of NAT
for C being non empty being_simple_closed_curve compact non horizontal non vertical Subset of (TOP-REAL 2)
for p being Point of (TOP-REAL 2) st p `1 = ((W-bound C) + (E-bound C)) / 2 & p `2 = lower_bound (proj2 .: ((LSeg (((Gauge (C,1)) * ((Center (Gauge (C,1))),1)),((Gauge (C,1)) * ((Center (Gauge (C,1))),(width (Gauge (C,1))))))) /\ (Upper_Arc (L~ (Cage (C,(i + 1))))))) holds
ex j being Element of NAT st
( 1 <= j & j <= width (Gauge (C,(i + 1))) & p = (Gauge (C,(i + 1))) * ((Center (Gauge (C,(i + 1)))),j) )
proof
let i be Element of NAT ; ::_thesis: for C being non empty being_simple_closed_curve compact non horizontal non vertical Subset of (TOP-REAL 2)
for p being Point of (TOP-REAL 2) st p `1 = ((W-bound C) + (E-bound C)) / 2 & p `2 = lower_bound (proj2 .: ((LSeg (((Gauge (C,1)) * ((Center (Gauge (C,1))),1)),((Gauge (C,1)) * ((Center (Gauge (C,1))),(width (Gauge (C,1))))))) /\ (Upper_Arc (L~ (Cage (C,(i + 1))))))) holds
ex j being Element of NAT st
( 1 <= j & j <= width (Gauge (C,(i + 1))) & p = (Gauge (C,(i + 1))) * ((Center (Gauge (C,(i + 1)))),j) )
let C be non empty being_simple_closed_curve compact non horizontal non vertical Subset of (TOP-REAL 2); ::_thesis: for p being Point of (TOP-REAL 2) st p `1 = ((W-bound C) + (E-bound C)) / 2 & p `2 = lower_bound (proj2 .: ((LSeg (((Gauge (C,1)) * ((Center (Gauge (C,1))),1)),((Gauge (C,1)) * ((Center (Gauge (C,1))),(width (Gauge (C,1))))))) /\ (Upper_Arc (L~ (Cage (C,(i + 1))))))) holds
ex j being Element of NAT st
( 1 <= j & j <= width (Gauge (C,(i + 1))) & p = (Gauge (C,(i + 1))) * ((Center (Gauge (C,(i + 1)))),j) )
let p be Point of (TOP-REAL 2); ::_thesis: ( p `1 = ((W-bound C) + (E-bound C)) / 2 & p `2 = lower_bound (proj2 .: ((LSeg (((Gauge (C,1)) * ((Center (Gauge (C,1))),1)),((Gauge (C,1)) * ((Center (Gauge (C,1))),(width (Gauge (C,1))))))) /\ (Upper_Arc (L~ (Cage (C,(i + 1))))))) implies ex j being Element of NAT st
( 1 <= j & j <= width (Gauge (C,(i + 1))) & p = (Gauge (C,(i + 1))) * ((Center (Gauge (C,(i + 1)))),j) ) )
assume that
A1: p `1 = ((W-bound C) + (E-bound C)) / 2 and
A2: p `2 = lower_bound (proj2 .: ((LSeg (((Gauge (C,1)) * ((Center (Gauge (C,1))),1)),((Gauge (C,1)) * ((Center (Gauge (C,1))),(width (Gauge (C,1))))))) /\ (Upper_Arc (L~ (Cage (C,(i + 1))))))) ; ::_thesis: ex j being Element of NAT st
( 1 <= j & j <= width (Gauge (C,(i + 1))) & p = (Gauge (C,(i + 1))) * ((Center (Gauge (C,(i + 1)))),j) )
percases ( ( L~ (Upper_Seq (C,(i + 1))) = Upper_Arc (L~ (Cage (C,(i + 1)))) & L~ (Lower_Seq (C,(i + 1))) = Lower_Arc (L~ (Cage (C,(i + 1)))) ) or ( L~ (Upper_Seq (C,(i + 1))) = Lower_Arc (L~ (Cage (C,(i + 1)))) & L~ (Lower_Seq (C,(i + 1))) = Upper_Arc (L~ (Cage (C,(i + 1)))) ) ) by Th9;
supposeA3: ( L~ (Upper_Seq (C,(i + 1))) = Upper_Arc (L~ (Cage (C,(i + 1)))) & L~ (Lower_Seq (C,(i + 1))) = Lower_Arc (L~ (Cage (C,(i + 1)))) ) ; ::_thesis: ex j being Element of NAT st
( 1 <= j & j <= width (Gauge (C,(i + 1))) & p = (Gauge (C,(i + 1))) * ((Center (Gauge (C,(i + 1)))),j) )
A4: 1 <= Center (Gauge (C,1)) by JORDAN1B:11;
set k = width (Gauge (C,(i + 1)));
set l = Center (Gauge (C,(i + 1)));
set G = Gauge (C,(i + 1));
set f = Upper_Seq (C,(i + 1));
A5: 1 <= Center (Gauge (C,(i + 1))) by JORDAN1B:11;
A6: width (Gauge (C,(i + 1))) = len (Gauge (C,(i + 1))) by JORDAN8:def_1;
then width (Gauge (C,(i + 1))) >= 4 by JORDAN8:10;
then A7: 1 <= width (Gauge (C,(i + 1))) by XXREAL_0:2;
then A8: Center (Gauge (C,(i + 1))) <= len (Gauge (C,(i + 1))) by A6, JORDAN1B:12;
then A9: ( [(Center (Gauge (C,(i + 1)))),1] in Indices (Gauge (C,(i + 1))) & [(Center (Gauge (C,(i + 1)))),(width (Gauge (C,(i + 1))))] in Indices (Gauge (C,(i + 1))) ) by A7, A5, MATRIX_1:36;
A10: width (Gauge (C,1)) = len (Gauge (C,1)) by JORDAN8:def_1;
then width (Gauge (C,1)) >= 4 by JORDAN8:10;
then A11: 1 <= width (Gauge (C,1)) by XXREAL_0:2;
then A12: Center (Gauge (C,1)) <= len (Gauge (C,1)) by A10, JORDAN1B:12;
A13: (LSeg (((Gauge (C,1)) * ((Center (Gauge (C,1))),1)),((Gauge (C,1)) * ((Center (Gauge (C,1))),(width (Gauge (C,1))))))) /\ (L~ (Upper_Seq (C,(i + 1)))) c= (LSeg (((Gauge (C,(i + 1))) * ((Center (Gauge (C,(i + 1)))),1)),((Gauge (C,(i + 1))) * ((Center (Gauge (C,(i + 1)))),(width (Gauge (C,(i + 1)))))))) /\ (L~ (Upper_Seq (C,(i + 1))))
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in (LSeg (((Gauge (C,1)) * ((Center (Gauge (C,1))),1)),((Gauge (C,1)) * ((Center (Gauge (C,1))),(width (Gauge (C,1))))))) /\ (L~ (Upper_Seq (C,(i + 1)))) or a in (LSeg (((Gauge (C,(i + 1))) * ((Center (Gauge (C,(i + 1)))),1)),((Gauge (C,(i + 1))) * ((Center (Gauge (C,(i + 1)))),(width (Gauge (C,(i + 1)))))))) /\ (L~ (Upper_Seq (C,(i + 1)))) )
A14: Upper_Arc (L~ (Cage (C,(i + 1)))) c= L~ (Cage (C,(i + 1))) by JORDAN6:61;
assume A15: a in (LSeg (((Gauge (C,1)) * ((Center (Gauge (C,1))),1)),((Gauge (C,1)) * ((Center (Gauge (C,1))),(width (Gauge (C,1))))))) /\ (L~ (Upper_Seq (C,(i + 1)))) ; ::_thesis: a in (LSeg (((Gauge (C,(i + 1))) * ((Center (Gauge (C,(i + 1)))),1)),((Gauge (C,(i + 1))) * ((Center (Gauge (C,(i + 1)))),(width (Gauge (C,(i + 1)))))))) /\ (L~ (Upper_Seq (C,(i + 1))))
then reconsider a1 = a as Point of (TOP-REAL 2) ;
A16: a1 in LSeg (((Gauge (C,1)) * ((Center (Gauge (C,1))),1)),((Gauge (C,1)) * ((Center (Gauge (C,1))),(width (Gauge (C,1)))))) by A15, XBOOLE_0:def_4;
a1 in Upper_Arc (L~ (Cage (C,(i + 1)))) by A3, A15, XBOOLE_0:def_4;
then A17: a1 `2 <= N-bound (L~ (Cage (C,(i + 1)))) by A14, PSCOMP_1:24;
Cage (C,(i + 1)) is_sequence_on Gauge (C,(i + 1)) by JORDAN9:def_1;
then ((Gauge (C,(i + 1))) * ((Center (Gauge (C,(i + 1)))),(width (Gauge (C,(i + 1)))))) `2 >= N-bound (L~ (Cage (C,(i + 1)))) by A6, A7, A5, JORDAN1A:20, JORDAN1B:12;
then A18: a1 `2 <= ((Gauge (C,(i + 1))) * ((Center (Gauge (C,(i + 1)))),(width (Gauge (C,(i + 1)))))) `2 by A17, XXREAL_0:2;
a1 in Upper_Arc (L~ (Cage (C,(i + 1)))) by A3, A15, XBOOLE_0:def_4;
then A19: a1 `2 >= S-bound (L~ (Cage (C,(i + 1)))) by A14, PSCOMP_1:24;
Cage (C,(i + 1)) is_sequence_on Gauge (C,(i + 1)) by JORDAN9:def_1;
then ((Gauge (C,(i + 1))) * ((Center (Gauge (C,(i + 1)))),1)) `2 <= S-bound (L~ (Cage (C,(i + 1)))) by A6, A7, A5, JORDAN1A:22, JORDAN1B:12;
then A20: a1 `2 >= ((Gauge (C,(i + 1))) * ((Center (Gauge (C,(i + 1)))),1)) `2 by A19, XXREAL_0:2;
A21: a1 in L~ (Upper_Seq (C,(i + 1))) by A15, XBOOLE_0:def_4;
((Gauge (C,1)) * ((Center (Gauge (C,1))),1)) `1 = ((Gauge (C,1)) * ((Center (Gauge (C,1))),(width (Gauge (C,1))))) `1 by A11, A12, A4, GOBOARD5:2;
then A22: a1 `1 = ((Gauge (C,1)) * ((Center (Gauge (C,1))),1)) `1 by A16, GOBOARD7:5
.= ((Gauge (C,(i + 1))) * ((Center (Gauge (C,(i + 1)))),1)) `1 by A6, A10, A7, A11, JORDAN1A:36 ;
then a1 `1 = ((Gauge (C,(i + 1))) * ((Center (Gauge (C,(i + 1)))),(width (Gauge (C,(i + 1)))))) `1 by A7, A8, A5, GOBOARD5:2;
then a1 in LSeg (((Gauge (C,(i + 1))) * ((Center (Gauge (C,(i + 1)))),1)),((Gauge (C,(i + 1))) * ((Center (Gauge (C,(i + 1)))),(width (Gauge (C,(i + 1))))))) by A22, A20, A18, GOBOARD7:7;
hence a in (LSeg (((Gauge (C,(i + 1))) * ((Center (Gauge (C,(i + 1)))),1)),((Gauge (C,(i + 1))) * ((Center (Gauge (C,(i + 1)))),(width (Gauge (C,(i + 1)))))))) /\ (L~ (Upper_Seq (C,(i + 1)))) by A21, XBOOLE_0:def_4; ::_thesis: verum
end;
1 <= i + 1 by NAT_1:11;
then (LSeg (((Gauge (C,(i + 1))) * ((Center (Gauge (C,(i + 1)))),1)),((Gauge (C,(i + 1))) * ((Center (Gauge (C,(i + 1)))),(width (Gauge (C,(i + 1)))))))) /\ (L~ (Upper_Seq (C,(i + 1)))) c= (LSeg (((Gauge (C,1)) * ((Center (Gauge (C,1))),1)),((Gauge (C,1)) * ((Center (Gauge (C,1))),(width (Gauge (C,1))))))) /\ (L~ (Upper_Seq (C,(i + 1)))) by A6, A10, JORDAN1A:44, XBOOLE_1:26;
then A23: (LSeg (((Gauge (C,1)) * ((Center (Gauge (C,1))),1)),((Gauge (C,1)) * ((Center (Gauge (C,1))),(width (Gauge (C,1))))))) /\ (L~ (Upper_Seq (C,(i + 1)))) = (LSeg (((Gauge (C,(i + 1))) * ((Center (Gauge (C,(i + 1)))),1)),((Gauge (C,(i + 1))) * ((Center (Gauge (C,(i + 1)))),(width (Gauge (C,(i + 1)))))))) /\ (L~ (Upper_Seq (C,(i + 1)))) by A13, XBOOLE_0:def_10;
LSeg (((Gauge (C,(i + 1))) * ((Center (Gauge (C,(i + 1)))),1)),((Gauge (C,(i + 1))) * ((Center (Gauge (C,(i + 1)))),(width (Gauge (C,(i + 1))))))) meets L~ (Upper_Seq (C,(i + 1))) by A3, A6, A7, A5, JORDAN1B:12, JORDAN1B:29;
then consider n being Element of NAT such that
A24: ( 1 <= n & n <= width (Gauge (C,(i + 1))) ) and
A25: ((Gauge (C,(i + 1))) * ((Center (Gauge (C,(i + 1)))),n)) `2 = lower_bound (proj2 .: ((LSeg (((Gauge (C,(i + 1))) * ((Center (Gauge (C,(i + 1)))),1)),((Gauge (C,(i + 1))) * ((Center (Gauge (C,(i + 1)))),(width (Gauge (C,(i + 1)))))))) /\ (L~ (Upper_Seq (C,(i + 1)))))) by A7, A9, Th1, Th10;
take n ; ::_thesis: ( 1 <= n & n <= width (Gauge (C,(i + 1))) & p = (Gauge (C,(i + 1))) * ((Center (Gauge (C,(i + 1)))),n) )
thus ( 1 <= n & n <= width (Gauge (C,(i + 1))) ) by A24; ::_thesis: p = (Gauge (C,(i + 1))) * ((Center (Gauge (C,(i + 1)))),n)
len (Gauge (C,1)) >= 4 by JORDAN8:10;
then A26: 1 <= len (Gauge (C,1)) by XXREAL_0:2;
then p `1 = ((Gauge (C,1)) * ((Center (Gauge (C,1))),1)) `1 by A1, JORDAN1A:38
.= ((Gauge (C,(i + 1))) * ((Center (Gauge (C,(i + 1)))),n)) `1 by A6, A24, A26, JORDAN1A:36 ;
hence p = (Gauge (C,(i + 1))) * ((Center (Gauge (C,(i + 1)))),n) by A2, A3, A25, A23, TOPREAL3:6; ::_thesis: verum
end;
supposeA27: ( L~ (Upper_Seq (C,(i + 1))) = Lower_Arc (L~ (Cage (C,(i + 1)))) & L~ (Lower_Seq (C,(i + 1))) = Upper_Arc (L~ (Cage (C,(i + 1)))) ) ; ::_thesis: ex j being Element of NAT st
( 1 <= j & j <= width (Gauge (C,(i + 1))) & p = (Gauge (C,(i + 1))) * ((Center (Gauge (C,(i + 1)))),j) )
A28: 1 <= Center (Gauge (C,1)) by JORDAN1B:11;
set k = width (Gauge (C,(i + 1)));
set l = Center (Gauge (C,(i + 1)));
set G = Gauge (C,(i + 1));
set f = Lower_Seq (C,(i + 1));
A29: 1 <= Center (Gauge (C,(i + 1))) by JORDAN1B:11;
A30: width (Gauge (C,(i + 1))) = len (Gauge (C,(i + 1))) by JORDAN8:def_1;
then width (Gauge (C,(i + 1))) >= 4 by JORDAN8:10;
then A31: 1 <= width (Gauge (C,(i + 1))) by XXREAL_0:2;
then A32: Center (Gauge (C,(i + 1))) <= len (Gauge (C,(i + 1))) by A30, JORDAN1B:12;
then A33: ( [(Center (Gauge (C,(i + 1)))),1] in Indices (Gauge (C,(i + 1))) & [(Center (Gauge (C,(i + 1)))),(width (Gauge (C,(i + 1))))] in Indices (Gauge (C,(i + 1))) ) by A31, A29, MATRIX_1:36;
A34: width (Gauge (C,1)) = len (Gauge (C,1)) by JORDAN8:def_1;
then width (Gauge (C,1)) >= 4 by JORDAN8:10;
then A35: 1 <= width (Gauge (C,1)) by XXREAL_0:2;
then A36: Center (Gauge (C,1)) <= len (Gauge (C,1)) by A34, JORDAN1B:12;
A37: (LSeg (((Gauge (C,1)) * ((Center (Gauge (C,1))),1)),((Gauge (C,1)) * ((Center (Gauge (C,1))),(width (Gauge (C,1))))))) /\ (L~ (Lower_Seq (C,(i + 1)))) c= (LSeg (((Gauge (C,(i + 1))) * ((Center (Gauge (C,(i + 1)))),1)),((Gauge (C,(i + 1))) * ((Center (Gauge (C,(i + 1)))),(width (Gauge (C,(i + 1)))))))) /\ (L~ (Lower_Seq (C,(i + 1))))
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in (LSeg (((Gauge (C,1)) * ((Center (Gauge (C,1))),1)),((Gauge (C,1)) * ((Center (Gauge (C,1))),(width (Gauge (C,1))))))) /\ (L~ (Lower_Seq (C,(i + 1)))) or a in (LSeg (((Gauge (C,(i + 1))) * ((Center (Gauge (C,(i + 1)))),1)),((Gauge (C,(i + 1))) * ((Center (Gauge (C,(i + 1)))),(width (Gauge (C,(i + 1)))))))) /\ (L~ (Lower_Seq (C,(i + 1)))) )
A38: Upper_Arc (L~ (Cage (C,(i + 1)))) c= L~ (Cage (C,(i + 1))) by JORDAN6:61;
assume A39: a in (LSeg (((Gauge (C,1)) * ((Center (Gauge (C,1))),1)),((Gauge (C,1)) * ((Center (Gauge (C,1))),(width (Gauge (C,1))))))) /\ (L~ (Lower_Seq (C,(i + 1)))) ; ::_thesis: a in (LSeg (((Gauge (C,(i + 1))) * ((Center (Gauge (C,(i + 1)))),1)),((Gauge (C,(i + 1))) * ((Center (Gauge (C,(i + 1)))),(width (Gauge (C,(i + 1)))))))) /\ (L~ (Lower_Seq (C,(i + 1))))
then reconsider a1 = a as Point of (TOP-REAL 2) ;
A40: a1 in LSeg (((Gauge (C,1)) * ((Center (Gauge (C,1))),1)),((Gauge (C,1)) * ((Center (Gauge (C,1))),(width (Gauge (C,1)))))) by A39, XBOOLE_0:def_4;
a1 in Upper_Arc (L~ (Cage (C,(i + 1)))) by A27, A39, XBOOLE_0:def_4;
then A41: a1 `2 <= N-bound (L~ (Cage (C,(i + 1)))) by A38, PSCOMP_1:24;
Cage (C,(i + 1)) is_sequence_on Gauge (C,(i + 1)) by JORDAN9:def_1;
then ((Gauge (C,(i + 1))) * ((Center (Gauge (C,(i + 1)))),(width (Gauge (C,(i + 1)))))) `2 >= N-bound (L~ (Cage (C,(i + 1)))) by A30, A31, A29, JORDAN1A:20, JORDAN1B:12;
then A42: a1 `2 <= ((Gauge (C,(i + 1))) * ((Center (Gauge (C,(i + 1)))),(width (Gauge (C,(i + 1)))))) `2 by A41, XXREAL_0:2;
a1 in Upper_Arc (L~ (Cage (C,(i + 1)))) by A27, A39, XBOOLE_0:def_4;
then A43: a1 `2 >= S-bound (L~ (Cage (C,(i + 1)))) by A38, PSCOMP_1:24;
Cage (C,(i + 1)) is_sequence_on Gauge (C,(i + 1)) by JORDAN9:def_1;
then ((Gauge (C,(i + 1))) * ((Center (Gauge (C,(i + 1)))),1)) `2 <= S-bound (L~ (Cage (C,(i + 1)))) by A30, A31, A29, JORDAN1A:22, JORDAN1B:12;
then A44: a1 `2 >= ((Gauge (C,(i + 1))) * ((Center (Gauge (C,(i + 1)))),1)) `2 by A43, XXREAL_0:2;
A45: a1 in L~ (Lower_Seq (C,(i + 1))) by A39, XBOOLE_0:def_4;
((Gauge (C,1)) * ((Center (Gauge (C,1))),1)) `1 = ((Gauge (C,1)) * ((Center (Gauge (C,1))),(width (Gauge (C,1))))) `1 by A35, A36, A28, GOBOARD5:2;
then A46: a1 `1 = ((Gauge (C,1)) * ((Center (Gauge (C,1))),1)) `1 by A40, GOBOARD7:5
.= ((Gauge (C,(i + 1))) * ((Center (Gauge (C,(i + 1)))),1)) `1 by A30, A34, A31, A35, JORDAN1A:36 ;
then a1 `1 = ((Gauge (C,(i + 1))) * ((Center (Gauge (C,(i + 1)))),(width (Gauge (C,(i + 1)))))) `1 by A31, A32, A29, GOBOARD5:2;
then a1 in LSeg (((Gauge (C,(i + 1))) * ((Center (Gauge (C,(i + 1)))),1)),((Gauge (C,(i + 1))) * ((Center (Gauge (C,(i + 1)))),(width (Gauge (C,(i + 1))))))) by A46, A44, A42, GOBOARD7:7;
hence a in (LSeg (((Gauge (C,(i + 1))) * ((Center (Gauge (C,(i + 1)))),1)),((Gauge (C,(i + 1))) * ((Center (Gauge (C,(i + 1)))),(width (Gauge (C,(i + 1)))))))) /\ (L~ (Lower_Seq (C,(i + 1)))) by A45, XBOOLE_0:def_4; ::_thesis: verum
end;
1 <= i + 1 by NAT_1:11;
then (LSeg (((Gauge (C,(i + 1))) * ((Center (Gauge (C,(i + 1)))),1)),((Gauge (C,(i + 1))) * ((Center (Gauge (C,(i + 1)))),(width (Gauge (C,(i + 1)))))))) /\ (L~ (Lower_Seq (C,(i + 1)))) c= (LSeg (((Gauge (C,1)) * ((Center (Gauge (C,1))),1)),((Gauge (C,1)) * ((Center (Gauge (C,1))),(width (Gauge (C,1))))))) /\ (L~ (Lower_Seq (C,(i + 1)))) by A30, A34, JORDAN1A:44, XBOOLE_1:26;
then A47: (LSeg (((Gauge (C,1)) * ((Center (Gauge (C,1))),1)),((Gauge (C,1)) * ((Center (Gauge (C,1))),(width (Gauge (C,1))))))) /\ (L~ (Lower_Seq (C,(i + 1)))) = (LSeg (((Gauge (C,(i + 1))) * ((Center (Gauge (C,(i + 1)))),1)),((Gauge (C,(i + 1))) * ((Center (Gauge (C,(i + 1)))),(width (Gauge (C,(i + 1)))))))) /\ (L~ (Lower_Seq (C,(i + 1)))) by A37, XBOOLE_0:def_10;
LSeg (((Gauge (C,(i + 1))) * ((Center (Gauge (C,(i + 1)))),1)),((Gauge (C,(i + 1))) * ((Center (Gauge (C,(i + 1)))),(width (Gauge (C,(i + 1))))))) meets L~ (Lower_Seq (C,(i + 1))) by A27, A30, A31, A29, JORDAN1B:12, JORDAN1B:29;
then consider n being Element of NAT such that
A48: ( 1 <= n & n <= width (Gauge (C,(i + 1))) ) and
A49: ((Gauge (C,(i + 1))) * ((Center (Gauge (C,(i + 1)))),n)) `2 = lower_bound (proj2 .: ((LSeg (((Gauge (C,(i + 1))) * ((Center (Gauge (C,(i + 1)))),1)),((Gauge (C,(i + 1))) * ((Center (Gauge (C,(i + 1)))),(width (Gauge (C,(i + 1)))))))) /\ (L~ (Lower_Seq (C,(i + 1)))))) by A31, A33, Th1, Th12;
take n ; ::_thesis: ( 1 <= n & n <= width (Gauge (C,(i + 1))) & p = (Gauge (C,(i + 1))) * ((Center (Gauge (C,(i + 1)))),n) )
thus ( 1 <= n & n <= width (Gauge (C,(i + 1))) ) by A48; ::_thesis: p = (Gauge (C,(i + 1))) * ((Center (Gauge (C,(i + 1)))),n)
len (Gauge (C,1)) >= 4 by JORDAN8:10;
then A50: 1 <= len (Gauge (C,1)) by XXREAL_0:2;
then p `1 = ((Gauge (C,1)) * ((Center (Gauge (C,1))),1)) `1 by A1, JORDAN1A:38
.= ((Gauge (C,(i + 1))) * ((Center (Gauge (C,(i + 1)))),n)) `1 by A30, A48, A50, JORDAN1A:36 ;
hence p = (Gauge (C,(i + 1))) * ((Center (Gauge (C,(i + 1)))),n) by A2, A27, A49, A47, TOPREAL3:6; ::_thesis: verum
end;
end;
end;