let i, j be Nat; :: thesis: for G being Go-board st i <= len G & j <= width G holds

Int (cell (G,i,j)) <> {}

let G be Go-board; :: thesis: ( i <= len G & j <= width G implies Int (cell (G,i,j)) <> {} )

assume that

A1: i <= len G and

A2: j <= width G ; :: thesis: Int (cell (G,i,j)) <> {}

A3: ( j = width G or j < width G ) by A2, XXREAL_0:1;

A4: ( i = len G or i < len G ) by A1, XXREAL_0:1;

set p = the Point of (TOP-REAL 2);

Int (cell (G,i,j)) <> {}

let G be Go-board; :: thesis: ( i <= len G & j <= width G implies Int (cell (G,i,j)) <> {} )

assume that

A1: i <= len G and

A2: j <= width G ; :: thesis: Int (cell (G,i,j)) <> {}

A3: ( j = width G or j < width G ) by A2, XXREAL_0:1;

A4: ( i = len G or i < len G ) by A1, XXREAL_0:1;

set p = the Point of (TOP-REAL 2);

per cases
( ( 1 <= i & i + 1 <= len G & 1 <= j & j + 1 <= width G ) or ( 1 <= i & i + 1 <= len G & j = width G ) or ( 1 <= i & i + 1 <= len G & j = 0 ) or ( 1 <= j & j + 1 <= width G & i = 0 ) or ( 1 <= j & j + 1 <= width G & i = len G ) or ( i = 0 & j = 0 ) or ( i = len G & j = width G ) or ( i = 0 & j = width G ) or ( i = len G & j = 0 ) )
by A3, A4, NAT_1:13, NAT_1:14;

end;

suppose
( 1 <= i & i + 1 <= len G & 1 <= j & j + 1 <= width G )
; :: thesis: Int (cell (G,i,j)) <> {}

then
LSeg (((1 / 2) * ((G * (i,j)) + (G * ((i + 1),(j + 1))))), the Point of (TOP-REAL 2)) meets Int (cell (G,i,j))
by GOBOARD6:82;

hence Int (cell (G,i,j)) <> {} ; :: thesis: verum

end;hence Int (cell (G,i,j)) <> {} ; :: thesis: verum

suppose
( 1 <= i & i + 1 <= len G & j = width G )
; :: thesis: Int (cell (G,i,j)) <> {}

then
LSeg ( the Point of (TOP-REAL 2),(((1 / 2) * ((G * (i,j)) + (G * ((i + 1),j)))) + |[0,1]|)) meets Int (cell (G,i,j))
by GOBOARD6:83;

hence Int (cell (G,i,j)) <> {} ; :: thesis: verum

end;hence Int (cell (G,i,j)) <> {} ; :: thesis: verum

suppose
( 1 <= i & i + 1 <= len G & j = 0 )
; :: thesis: Int (cell (G,i,j)) <> {}

then
LSeg ((((1 / 2) * ((G * (i,(j + 1))) + (G * ((i + 1),(j + 1))))) - |[0,1]|), the Point of (TOP-REAL 2)) meets Int (cell (G,i,j))
by GOBOARD6:84;

hence Int (cell (G,i,j)) <> {} ; :: thesis: verum

end;hence Int (cell (G,i,j)) <> {} ; :: thesis: verum

suppose
( 1 <= j & j + 1 <= width G & i = 0 )
; :: thesis: Int (cell (G,i,j)) <> {}

then
LSeg ((((1 / 2) * ((G * ((i + 1),j)) + (G * ((i + 1),(j + 1))))) - |[1,0]|), the Point of (TOP-REAL 2)) meets Int (cell (G,i,j))
by GOBOARD6:85;

hence Int (cell (G,i,j)) <> {} ; :: thesis: verum

end;hence Int (cell (G,i,j)) <> {} ; :: thesis: verum

suppose
( 1 <= j & j + 1 <= width G & i = len G )
; :: thesis: Int (cell (G,i,j)) <> {}

then
LSeg ( the Point of (TOP-REAL 2),(((1 / 2) * ((G * (i,j)) + (G * (i,(j + 1))))) + |[1,0]|)) meets Int (cell (G,i,j))
by GOBOARD6:86;

hence Int (cell (G,i,j)) <> {} ; :: thesis: verum

end;hence Int (cell (G,i,j)) <> {} ; :: thesis: verum

suppose
( i = 0 & j = 0 )
; :: thesis: Int (cell (G,i,j)) <> {}

then
LSeg ( the Point of (TOP-REAL 2),((G * ((i + 1),(j + 1))) - |[1,1]|)) meets Int (cell (G,i,j))
by GOBOARD6:87;

hence Int (cell (G,i,j)) <> {} ; :: thesis: verum

end;hence Int (cell (G,i,j)) <> {} ; :: thesis: verum

suppose
( i = len G & j = width G )
; :: thesis: Int (cell (G,i,j)) <> {}

then
LSeg ( the Point of (TOP-REAL 2),((G * (i,j)) + |[1,1]|)) meets Int (cell (G,i,j))
by GOBOARD6:88;

hence Int (cell (G,i,j)) <> {} ; :: thesis: verum

end;hence Int (cell (G,i,j)) <> {} ; :: thesis: verum