let G be Go-board; for f being FinSequence of (TOP-REAL 2) st f is_sequence_on G & f is special holds
for i, j being Nat st i <= len G & j <= width G holds
Int (cell (G,i,j)) misses L~ f
let f be FinSequence of (TOP-REAL 2); ( f is_sequence_on G & f is special implies for i, j being Nat st i <= len G & j <= width G holds
Int (cell (G,i,j)) misses L~ f )
assume that
A1:
f is_sequence_on G
and
A2:
f is special
; for i, j being Nat st i <= len G & j <= width G holds
Int (cell (G,i,j)) misses L~ f
let i, j be Nat; ( i <= len G & j <= width G implies Int (cell (G,i,j)) misses L~ f )
assume that
A3:
i <= len G
and
A4:
j <= width G
; Int (cell (G,i,j)) misses L~ f
A5:
Int (cell (G,i,j)) = (Int (v_strip (G,i))) /\ (Int (h_strip (G,j)))
by TOPS_1:17;
assume
Int (cell (G,i,j)) meets L~ f
; contradiction
then consider x being object such that
A6:
x in Int (cell (G,i,j))
and
A7:
x in L~ f
by XBOOLE_0:3;
L~ f = union { (LSeg (f,k)) where k is Nat : ( 1 <= k & k + 1 <= len f ) }
by TOPREAL1:def 4;
then consider X being set such that
A8:
x in X
and
A9:
X in { (LSeg (f,k)) where k is Nat : ( 1 <= k & k + 1 <= len f ) }
by A7, TARSKI:def 4;
consider k being Nat such that
A10:
X = LSeg (f,k)
and
1 <= k
and
k + 1 <= len f
by A9;
reconsider p = x as Point of (TOP-REAL 2) by A8, A10;
per cases
( LSeg (f,k) is horizontal or LSeg (f,k) is vertical )
by A2, SPPOL_1:19;
suppose
LSeg (
f,
k) is
horizontal
;
contradictionthen consider j0 being
Nat such that A11:
1
<= j0
and A12:
j0 <= width G
and A13:
for
p being
Point of
(TOP-REAL 2) st
p in LSeg (
f,
k) holds
p `2 = (G * (1,j0)) `2
by A1, Th12;
now not p in Int (h_strip (G,j))A14:
(
j0 > j implies
j0 >= j + 1 )
by NAT_1:13;
assume A15:
p in Int (h_strip (G,j))
;
contradictionper cases
( j0 < j or j0 = j or j0 > j + 1 or j0 = j + 1 )
by A14, XXREAL_0:1;
suppose A16:
j0 < j
;
contradiction
0 <> len G
by MATRIX_0:def 10;
then
1
<= len G
by NAT_1:14;
then A17:
(G * (1,j)) `2 > (G * (1,j0)) `2
by A4, A11, A16, GOBOARD5:4;
j >= 1
by A11, A16, XXREAL_0:2;
then
p `2 > (G * (1,j)) `2
by A4, A15, GOBOARD6:27;
hence
contradiction
by A8, A10, A13, A17;
verum end; suppose A18:
j0 > j + 1
;
contradictionthen
j + 1
<= width G
by A12, XXREAL_0:2;
then
j < width G
by NAT_1:13;
then A19:
p `2 < (G * (1,(j + 1))) `2
by A15, GOBOARD6:28;
0 <> len G
by MATRIX_0:def 10;
then A20:
1
<= len G
by NAT_1:14;
j + 1
>= 1
by NAT_1:14;
then
(G * (1,(j + 1))) `2 < (G * (1,j0)) `2
by A12, A18, A20, GOBOARD5:4;
hence
contradiction
by A8, A10, A13, A19;
verum end; end; end; hence
contradiction
by A6, A5, XBOOLE_0:def 4;
verum end; suppose
LSeg (
f,
k) is
vertical
;
contradictionthen consider i0 being
Nat such that A22:
1
<= i0
and A23:
i0 <= len G
and A24:
for
p being
Point of
(TOP-REAL 2) st
p in LSeg (
f,
k) holds
p `1 = (G * (i0,1)) `1
by A1, Th13;
now not p in Int (v_strip (G,i))A25:
(
i0 > i implies
i0 >= i + 1 )
by NAT_1:13;
assume A26:
p in Int (v_strip (G,i))
;
contradictionper cases
( i0 < i or i0 = i or i0 > i + 1 or i0 = i + 1 )
by A25, XXREAL_0:1;
suppose A27:
i0 < i
;
contradiction
0 <> width G
by MATRIX_0:def 10;
then
1
<= width G
by NAT_1:14;
then A28:
(G * (i,1)) `1 > (G * (i0,1)) `1
by A3, A22, A27, GOBOARD5:3;
i >= 1
by A22, A27, XXREAL_0:2;
then
p `1 > (G * (i,1)) `1
by A3, A26, GOBOARD6:29;
hence
contradiction
by A8, A10, A24, A28;
verum end; suppose A29:
i0 > i + 1
;
contradictionthen
i + 1
<= len G
by A23, XXREAL_0:2;
then
i < len G
by NAT_1:13;
then A30:
p `1 < (G * ((i + 1),1)) `1
by A26, GOBOARD6:30;
0 <> width G
by MATRIX_0:def 10;
then A31:
1
<= width G
by NAT_1:14;
i + 1
>= 1
by NAT_1:14;
then
(G * ((i + 1),1)) `1 < (G * (i0,1)) `1
by A23, A29, A31, GOBOARD5:3;
hence
contradiction
by A8, A10, A24, A30;
verum end; end; end; hence
contradiction
by A6, A5, XBOOLE_0:def 4;
verum end; end;