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 & i < len G ) and
A2: ( 1 <= m & m <= len G ) and
A3: ( 1 <= n & n <= width G ) and
A4: p in cell G,i,(width G) and
A5: p `2 = (G * m,n) `2 ; :: thesis: width G = n
A6: 1 <= len G by A1, XXREAL_0:2;
A7: (G * 1,n) `2 = (G * m,n) `2 by A2, A3, GOBOARD5:2;
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, GOBRD11:31;
then consider r, s being Real such that
A8: p = |[r,s]| and
(G * i,1) `1 <= r and
A9: ( r <= (G * (i + 1),1) `1 & (G * 1,(width G)) `2 <= s ) by A4;
p `2 = s by A8, EUCLID:56;
then width G <= n by A3, A5, A6, A7, A9, GOBOARD5:5;
hence width G = n by A3, XXREAL_0:1; :: thesis: verum