let j be Nat; for p being Point of (TOP-REAL 2)
for G being Go-board st 1 <= j & j <= width G & p in Int (h_strip (G,j)) holds
p `2 > (G * (1,j)) `2
let p be Point of (TOP-REAL 2); for G being Go-board st 1 <= j & j <= width G & p in Int (h_strip (G,j)) holds
p `2 > (G * (1,j)) `2
let G be Go-board; ( 1 <= j & j <= width G & p in Int (h_strip (G,j)) implies p `2 > (G * (1,j)) `2 )
assume that
A1:
1 <= j
and
A2:
j <= width G
and
A3:
p in Int (h_strip (G,j))
; p `2 > (G * (1,j)) `2
per cases
( j = width G or j < width G )
by A2, XXREAL_0:1;
suppose
j < width G
;
p `2 > (G * (1,j)) `2 then
Int (h_strip (G,j)) = { |[r,s]| where r, s is Real : ( (G * (1,j)) `2 < s & s < (G * (1,(j + 1))) `2 ) }
by A1, Th17;
then
ex
r,
s being
Real st
(
p = |[r,s]| &
(G * (1,j)) `2 < s &
s < (G * (1,(j + 1))) `2 )
by A3;
hence
p `2 > (G * (1,j)) `2
by EUCLID:52;
verum end; end;