let G be Go-board; :: thesis: for j, m, n being Element of NAT
for p being Point of (TOP-REAL 2) st 1 <= j & j < width G & 1 <= m & m <= len G & 1 <= n & n <= width G & p in cell G,(len G),j & p `1 = (G * m,n) `1 holds
len G = m
let j, m, n be Element of NAT ; :: thesis: for p being Point of (TOP-REAL 2) st 1 <= j & j < width G & 1 <= m & m <= len G & 1 <= n & n <= width G & p in cell G,(len G),j & p `1 = (G * m,n) `1 holds
len G = m
let p be Point of (TOP-REAL 2); :: thesis: ( 1 <= j & j < width G & 1 <= m & m <= len G & 1 <= n & n <= width G & p in cell G,(len G),j & p `1 = (G * m,n) `1 implies len G = m )
assume that
A1: ( 1 <= j & j < width G ) and
A2: ( 1 <= m & m <= len G ) and
A3: ( 1 <= n & n <= width G ) and
A4: p in cell G,(len G),j and
A5: p `1 = (G * m,n) `1 ; :: thesis: len G = m
A6: 1 <= width G by A1, XXREAL_0:2;
A7: (G * m,1) `1 = (G * m,n) `1 by A2, A3, GOBOARD5:3;
cell G,(len G),j = { |[r,s]| where r, s is Real : ( (G * (len G),1) `1 <= r & (G * 1,j) `2 <= s & s <= (G * 1,(j + 1)) `2 ) } by A1, GOBRD11:29;
then consider r, s being Real such that
A8: p = |[r,s]| and
A9: (G * (len G),1) `1 <= r and
( (G * 1,j) `2 <= s & s <= (G * 1,(j + 1)) `2 ) by A4;
p `1 = r by A8, EUCLID:56;
then len G <= m by A2, A5, A6, A7, A9, GOBOARD5:4;
hence len G = m by A2, XXREAL_0:1; :: thesis: verum