let G be Go-board; :: thesis: for i, m, n being Nat

for p being Point of (TOP-REAL 2) st 1 <= i & i < len G & 1 <= m & m <= len G & 1 <= n & n <= width G & p in cell (G,i,(width G)) & p `2 = (G * (m,n)) `2 holds

width G = n

let i, m, n be Nat; :: thesis: for p being Point of (TOP-REAL 2) st 1 <= i & i < len G & 1 <= m & m <= len G & 1 <= n & n <= width G & p in cell (G,i,(width G)) & p `2 = (G * (m,n)) `2 holds

width G = n

let p be Point of (TOP-REAL 2); :: thesis: ( 1 <= i & i < len G & 1 <= m & m <= len G & 1 <= n & n <= width G & p in cell (G,i,(width G)) & p `2 = (G * (m,n)) `2 implies width G = n )

assume that

A1: 1 <= i and

A2: i < len G and

A3: 1 <= m and

A4: m <= len G and

A5: 1 <= n and

A6: n <= width G and

A7: p in cell (G,i,(width G)) and

A8: p `2 = (G * (m,n)) `2 ; :: thesis: width G = n

A9: (G * (1,n)) `2 = (G * (m,n)) `2 by A3, A4, A5, A6, GOBOARD5:1;

A10: cell (G,i,(width G)) = { |[r,s]| where r, s is Real : ( (G * (i,1)) `1 <= r & r <= (G * ((i + 1),1)) `1 & (G * (1,(width G))) `2 <= s ) } by A1, A2, GOBRD11:31;

A11: 1 <= len G by A1, A2, XXREAL_0:2;

consider r, s being Real such that

A12: p = |[r,s]| and

(G * (i,1)) `1 <= r and

r <= (G * ((i + 1),1)) `1 and

A13: (G * (1,(width G))) `2 <= s by A7, A10;

p `2 = s by A12, EUCLID:52;

then width G <= n by A5, A8, A11, A9, A13, GOBOARD5:4;

hence width G = n by A6, XXREAL_0:1; :: thesis: verum

for p being Point of (TOP-REAL 2) st 1 <= i & i < len G & 1 <= m & m <= len G & 1 <= n & n <= width G & p in cell (G,i,(width G)) & p `2 = (G * (m,n)) `2 holds

width G = n

let i, m, n be Nat; :: thesis: for p being Point of (TOP-REAL 2) st 1 <= i & i < len G & 1 <= m & m <= len G & 1 <= n & n <= width G & p in cell (G,i,(width G)) & p `2 = (G * (m,n)) `2 holds

width G = n

let p be Point of (TOP-REAL 2); :: thesis: ( 1 <= i & i < len G & 1 <= m & m <= len G & 1 <= n & n <= width G & p in cell (G,i,(width G)) & p `2 = (G * (m,n)) `2 implies width G = n )

assume that

A1: 1 <= i and

A2: i < len G and

A3: 1 <= m and

A4: m <= len G and

A5: 1 <= n and

A6: n <= width G and

A7: p in cell (G,i,(width G)) and

A8: p `2 = (G * (m,n)) `2 ; :: thesis: width G = n

A9: (G * (1,n)) `2 = (G * (m,n)) `2 by A3, A4, A5, A6, GOBOARD5:1;

A10: cell (G,i,(width G)) = { |[r,s]| where r, s is Real : ( (G * (i,1)) `1 <= r & r <= (G * ((i + 1),1)) `1 & (G * (1,(width G))) `2 <= s ) } by A1, A2, GOBRD11:31;

A11: 1 <= len G by A1, A2, XXREAL_0:2;

consider r, s being Real such that

A12: p = |[r,s]| and

(G * (i,1)) `1 <= r and

r <= (G * ((i + 1),1)) `1 and

A13: (G * (1,(width G))) `2 <= s by A7, A10;

p `2 = s by A12, EUCLID:52;

then width G <= n by A5, A8, A11, A9, A13, GOBOARD5:4;

hence width G = n by A6, XXREAL_0:1; :: thesis: verum