let j be Element of 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 GOBOARD1:def 5;
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:6;
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 set ; :: 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 number such that
A4: s1 > 0 and
A5: Ball u,s1 c= h_strip G,j by A3, Th8;
reconsider p = u as Point of (TOP-REAL 2) by Lm6;
A6: p = |[(p `1 ),(p `2 )]| by EUCLID:57;
reconsider s1 = s1 as Real by XREAL_0:def 1;
set q2 = |[((p `1 ) + 0 ),((p `2 ) - (s1 / 2))]|;
A7: s1 / 2 < s1 by A4, XREAL_1:218;
then |[((p `1 ) + 0 ),((p `2 ) - (s1 / 2))]| in Ball u,s1 by A4, A6, Th13;
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:21;
set q1 = |[((p `1 ) + 0 ),((p `2 ) + (s1 / 2))]|;
|[((p `1 ) + 0 ),((p `2 ) + (s1 / 2))]| in Ball u,s1 by A4, A6, A7, Th11;
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:31, XREAL_1:217;
then A10: (G * 1,j) `2 < p `2 by A8, XXREAL_0:2;
p `2 < (p `2 ) + (s1 / 2) by A4, XREAL_1:31, XREAL_1:217;
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 set ; :: 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:13;
( ((G * 1,(j + 1)) `2 ) - s > 0 & s - ((G * 1,j) `2 ) > 0 ) by A12, A13, XREAL_1:52;
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 Th4;
A15: Ball u,(min (s - ((G * 1,j) `2 )),(((G * 1,(j + 1)) `2 ) - s)) c= h_strip G,j

proof

let y be set ; :: 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:18;
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:13;
0 <= (r - (q `1 )) ^2 by XREAL_1:65;
then ( (s - (q `2 )) ^2 >= 0 & ((s - (q `2 )) ^2 ) + 0 <= ((r - (q `1 )) ^2 ) + ((s - (q `2 )) ^2 ) ) by XREAL_1:8, XREAL_1:65;
then A19: sqrt ((s - (q `2 )) ^2 ) <= sqrt (((r - (q `1 )) ^2 ) + ((s - (q `2 )) ^2 )) by SQUARE_1:94;
A20: q = |[(q `1 ),(q `2 )]| by EUCLID:57;
then sqrt (((r - (q `1 )) ^2 ) + ((s - (q `2 )) ^2 )) < min (s - ((G * 1,j) `2 )),(((G * 1,(j + 1)) `2 ) - s) by A18, Th9;
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: abs (s - (q `2 )) <= min (s - ((G * 1,j) `2 )),(((G * 1,(j + 1)) `2 ) - s) by COMPLEX1:158;
then A22: abs (s - (q `2 )) <= s - ((G * 1,j) `2 ) by XXREAL_0:22;
A23: abs (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:50;
abs (s - (q `2 )) = abs (- (s - (q `2 ))) by COMPLEX1:138
.= (q `2 ) - s by A25, ABSVALUE:def 1 ;
then A26: q `2 <= (G * 1,(j + 1)) `2 by A23, XREAL_1:11;
(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:50;
then abs (s - (q `2 )) = s - (q `2 ) by ABSVALUE:def 1;
then A28: (G * 1,j) `2 <= q `2 by A22, XREAL_1:12;
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:13;
B is open by Th6;
hence x in Int (h_strip G,j) by A11, A14, A15, TOPS_1:54; :: thesis: verum