let j be Nat; :: thesis: for G being Go-board st 1 <= j & j < width G holds
Int (h_strip (G,j)) = { |[r,s]| where r, s is Real : ( (G * (1,j)) `2 < s & s < (G * (1,(j + 1))) `2 ) }
let G be Go-board; :: thesis: ( 1 <= j & j < width G implies Int (h_strip (G,j)) = { |[r,s]| where r, s is Real : ( (G * (1,j)) `2 < s & s < (G * (1,(j + 1))) `2 ) } )
0 <> len G by MATRIX_0:def 10;
then A1: 1 <= len G by NAT_1:14;
assume ( 1 <= j & j < width G ) ; :: thesis: Int (h_strip (G,j)) = { |[r,s]| where r, s is Real : ( (G * (1,j)) `2 < s & s < (G * (1,(j + 1))) `2 ) }
then A2: h_strip (G,j) = { |[r,s]| where r, s is Real : ( (G * (1,j)) `2 <= s & s <= (G * (1,(j + 1))) `2 ) } by A1, GOBOARD5:5;
thus Int (h_strip (G,j)) c= { |[r,s]| where r, s is Real : ( (G * (1,j)) `2 < s & s < (G * (1,(j + 1))) `2 ) } :: according to XBOOLE_0:def 10 :: thesis: { |[r,s]| where r, s is Real : ( (G * (1,j)) `2 < s & s < (G * (1,(j + 1))) `2 ) } c= Int (h_strip (G,j))

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Int (h_strip (G,j)) or x in { |[r,s]| where r, s is Real : ( (G * (1,j)) `2 < s & s < (G * (1,(j + 1))) `2 ) } )
assume A3: x in Int (h_strip (G,j)) ; :: thesis: x in { |[r,s]| where r, s is Real : ( (G * (1,j)) `2 < s & s < (G * (1,(j + 1))) `2 ) }
then reconsider u = x as Point of (Euclid 2) by Lm6;
consider s1 being Real such that
A4: s1 > 0 and
A5: Ball (u,s1) c= h_strip (G,j) by A3, Th5;
reconsider p = u as Point of (TOP-REAL 2) by Lm6;
A6: p = |[(p `1),(p `2)]| by EUCLID:53;
set q2 = |[((p `1) + 0),((p `2) - (s1 / 2))]|;
A7: s1 / 2 < s1 by A4, XREAL_1:216;
then |[((p `1) + 0),((p `2) - (s1 / 2))]| in Ball (u,s1) by A4, A6, Th10;
then |[((p `1) + 0),((p `2) - (s1 / 2))]| in h_strip (G,j) by A5;
then ex r2, s2 being Real st
( |[((p `1) + 0),((p `2) - (s1 / 2))]| = |[r2,s2]| & (G * (1,j)) `2 <= s2 & s2 <= (G * (1,(j + 1))) `2 ) by A2;
then (G * (1,j)) `2 <= (p `2) - (s1 / 2) by SPPOL_2:1;
then A8: ((G * (1,j)) `2) + (s1 / 2) <= p `2 by XREAL_1:19;
set q1 = |[((p `1) + 0),((p `2) + (s1 / 2))]|;
|[((p `1) + 0),((p `2) + (s1 / 2))]| in Ball (u,s1) by A4, A6, A7, Th8;
then |[((p `1) + 0),((p `2) + (s1 / 2))]| in h_strip (G,j) by A5;
then ex r2, s2 being Real st
( |[((p `1) + 0),((p `2) + (s1 / 2))]| = |[r2,s2]| & (G * (1,j)) `2 <= s2 & s2 <= (G * (1,(j + 1))) `2 ) by A2;
then A9: (p `2) + (s1 / 2) <= (G * (1,(j + 1))) `2 by SPPOL_2:1;
(G * (1,j)) `2 < ((G * (1,j)) `2) + (s1 / 2) by A4, XREAL_1:29, XREAL_1:215;
then A10: (G * (1,j)) `2 < p `2 by A8, XXREAL_0:2;
p `2 < (p `2) + (s1 / 2) by A4, XREAL_1:29, XREAL_1:215;
then p `2 < (G * (1,(j + 1))) `2 by A9, XXREAL_0:2;
hence x in { |[r,s]| where r, s is Real : ( (G * (1,j)) `2 < s & s < (G * (1,(j + 1))) `2 ) } by A6, A10; :: thesis: verum

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { |[r,s]| where r, s is Real : ( (G * (1,j)) `2 < s & s < (G * (1,(j + 1))) `2 ) } or x in Int (h_strip (G,j)) )
assume x in { |[r,s]| where r, s is Real : ( (G * (1,j)) `2 < s & s < (G * (1,(j + 1))) `2 ) } ; :: thesis: x in Int (h_strip (G,j))
then consider r, s being Real such that
A11: x = |[r,s]| and
A12: (G * (1,j)) `2 < s and
A13: s < (G * (1,(j + 1))) `2 ;
reconsider u = |[r,s]| as Point of (Euclid 2) by TOPREAL3:8;
( ((G * (1,(j + 1))) `2) - s > 0 & s - ((G * (1,j)) `2) > 0 ) by A12, A13, XREAL_1:50;
then min ((s - ((G * (1,j)) `2)),(((G * (1,(j + 1))) `2) - s)) > 0 by XXREAL_0:15;
then A14: u in Ball (u,(min ((s - ((G * (1,j)) `2)),(((G * (1,(j + 1))) `2) - s)))) by Th1;
A15: Ball (u,(min ((s - ((G * (1,j)) `2)),(((G * (1,(j + 1))) `2) - s)))) c= h_strip (G,j)

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in Ball (u,(min ((s - ((G * (1,j)) `2)),(((G * (1,(j + 1))) `2) - s)))) or y in h_strip (G,j) )
A16: Ball (u,(min ((s - ((G * (1,j)) `2)),(((G * (1,(j + 1))) `2) - s)))) = { v where v is Point of (Euclid 2) : dist (u,v) < min ((s - ((G * (1,j)) `2)),(((G * (1,(j + 1))) `2) - s)) } by METRIC_1:17;
assume y in Ball (u,(min ((s - ((G * (1,j)) `2)),(((G * (1,(j + 1))) `2) - s)))) ; :: thesis: y in h_strip (G,j)
then consider v being Point of (Euclid 2) such that
A17: v = y and
A18: dist (u,v) < min ((s - ((G * (1,j)) `2)),(((G * (1,(j + 1))) `2) - s)) by A16;
reconsider q = v as Point of (TOP-REAL 2) by TOPREAL3:8;
( (s - (q `2)) ^2 >= 0 & ((s - (q `2)) ^2) + 0 <= ((r - (q `1)) ^2) + ((s - (q `2)) ^2) ) by XREAL_1:6, XREAL_1:63;
then A19: sqrt ((s - (q `2)) ^2) <= sqrt (((r - (q `1)) ^2) + ((s - (q `2)) ^2)) by SQUARE_1:26;
A20: q = |[(q `1),(q `2)]| by EUCLID:53;
then sqrt (((r - (q `1)) ^2) + ((s - (q `2)) ^2)) < min ((s - ((G * (1,j)) `2)),(((G * (1,(j + 1))) `2) - s)) by A18, Th6;
then sqrt ((s - (q `2)) ^2) <= min ((s - ((G * (1,j)) `2)),(((G * (1,(j + 1))) `2) - s)) by A19, XXREAL_0:2;
then A21: |.(s - (q `2)).| <= min ((s - ((G * (1,j)) `2)),(((G * (1,(j + 1))) `2) - s)) by COMPLEX1:72;
then A22: |.(s - (q `2)).| <= s - ((G * (1,j)) `2) by XXREAL_0:22;
A23: |.(s - (q `2)).| <= ((G * (1,(j + 1))) `2) - s by A21, XXREAL_0:22;

per cases ( s <= q `2 or s >= q `2 ) ;

suppose A24: s <= q `2 ; :: thesis: y in h_strip (G,j)

then A25: (q `2) - s >= 0 by XREAL_1:48;
|.(s - (q `2)).| = |.(- (s - (q `2))).| by COMPLEX1:52
.= (q `2) - s by A25, ABSVALUE:def 1 ;
then A26: q `2 <= (G * (1,(j + 1))) `2 by A23, XREAL_1:9;
(G * (1,j)) `2 <= q `2 by A12, A24, XXREAL_0:2;
hence y in h_strip (G,j) by A2, A17, A20, A26; :: thesis: verum

end;

suppose A27: s >= q `2 ; :: thesis: y in h_strip (G,j)

then s - (q `2) >= 0 by XREAL_1:48;
then |.(s - (q `2)).| = s - (q `2) by ABSVALUE:def 1;
then A28: (G * (1,j)) `2 <= q `2 by A22, XREAL_1:10;
q `2 <= (G * (1,(j + 1))) `2 by A13, A27, XXREAL_0:2;
hence y in h_strip (G,j) by A2, A17, A20, A28; :: thesis: verum

end;

end;

end;

reconsider B = Ball (u,(min ((s - ((G * (1,j)) `2)),(((G * (1,(j + 1))) `2) - s)))) as Subset of (TOP-REAL 2) by TOPREAL3:8;
B is open by Th3;
hence x in Int (h_strip (G,j)) by A11, A14, A15, TOPS_1:22; :: thesis: verum