let G be Go-board; :: thesis: for j, m, n being 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 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 and
A2: j < width 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,(len G),j) and
A8: p `1 = (G * (m,n)) `1 ; :: thesis: len G = m
A9: (G * (m,1)) `1 = (G * (m,n)) `1 by A3, A4, A5, A6, GOBOARD5:2;
A10: 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, A2, GOBRD11:29;
A11: 1 <= width G by A1, A2, XXREAL_0:2;
consider r, s being Real such that
A12: p = |[r,s]| and
A13: (G * ((len G),1)) `1 <= r and
(G * (1,j)) `2 <= s and
s <= (G * (1,(j + 1))) `2 by A7, A10;
p `1 = r by A12, EUCLID:52;
then len G <= m by A3, A8, A11, A9, A13, GOBOARD5:3;
hence len G = m by A4, XXREAL_0:1; :: thesis: verum