let G be Go-board; :: thesis: for i, m, n being Element of 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 Element of 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:2;
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:56;
then width G <= n by A5, A8, A11, A9, A13, GOBOARD5:5;
hence width G = n by A6, XXREAL_0:1; :: thesis: verum