let G be Go-board; 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; 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); ( 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
; 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; verum