let G be Go-board; :: thesis: Int (h_strip G,(width G)) = { |[r,s]| where r, s is Real : (G * 1,(width G)) `2 < s }
0 <> len G
by GOBOARD1:def 5;
then
1 <= len G
by NAT_1:14;
then A1:
h_strip G,(width G) = { |[r,s]| where r, s is Real : (G * 1,(width G)) `2 <= s }
by GOBOARD5:7;
thus
Int (h_strip G,(width G)) c= { |[r,s]| where r, s is Real : (G * 1,(width G)) `2 < s }
:: according to XBOOLE_0:def 10 :: thesis: { |[r,s]| where r, s is Real : (G * 1,(width G)) `2 < s } c= Int (h_strip G,(width G))proof
let x be
set ;
:: according to TARSKI:def 3 :: thesis: ( not x in Int (h_strip G,(width G)) or x in { |[r,s]| where r, s is Real : (G * 1,(width G)) `2 < s } )
assume A2:
x in Int (h_strip G,(width G))
;
:: thesis: x in { |[r,s]| where r, s is Real : (G * 1,(width G)) `2 < s }
then reconsider u =
x as
Point of
(Euclid 2) by Lm5;
consider s1 being
real number such that A3:
s1 > 0
and A4:
Ball u,
s1 c= h_strip G,
(width G)
by A2, Th8;
reconsider s1 =
s1 as
Real by XREAL_0:def 1;
reconsider p =
u as
Point of
(TOP-REAL 2) by Lm5;
set q =
|[((p `1 ) + 0 ),((p `2 ) - (s1 / 2))]|;
A5:
p = |[(p `1 ),(p `2 )]|
by EUCLID:57;
A6:
(
s1 / 2
> 0 &
s1 / 2
< s1 )
by A3, XREAL_1:217, XREAL_1:218;
then
|[((p `1 ) + 0 ),((p `2 ) - (s1 / 2))]| in Ball u,
s1
by A5, Th13;
then
|[((p `1 ) + 0 ),((p `2 ) - (s1 / 2))]| in h_strip G,
(width G)
by A4;
then
ex
r2,
s2 being
Real st
(
|[((p `1 ) + 0 ),((p `2 ) - (s1 / 2))]| = |[r2,s2]| &
(G * 1,(width G)) `2 <= s2 )
by A1;
then
(G * 1,(width G)) `2 <= (p `2 ) - (s1 / 2)
by SPPOL_2:1;
then A7:
((G * 1,(width G)) `2 ) + (s1 / 2) <= p `2
by XREAL_1:21;
(G * 1,(width G)) `2 < ((G * 1,(width G)) `2 ) + (s1 / 2)
by A6, XREAL_1:31;
then
(G * 1,(width G)) `2 < p `2
by A7, XXREAL_0:2;
hence
x in { |[r,s]| where r, s is Real : (G * 1,(width G)) `2 < s }
by A5;
:: 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,(width G)) `2 < s } or x in Int (h_strip G,(width G)) )
assume
x in { |[r,s]| where r, s is Real : (G * 1,(width G)) `2 < s }
; :: thesis: x in Int (h_strip G,(width G))
then consider r, s being Real such that
A8:
x = |[r,s]|
and
A9:
(G * 1,(width G)) `2 < s
;
reconsider u = |[r,s]| as Point of (Euclid 2) by TOPREAL3:13;
A10:
u in Ball u,(s - ((G * 1,(width G)) `2 ))
by A9, Th4, XREAL_1:52;
A11:
Ball u,(s - ((G * 1,(width G)) `2 )) c= h_strip G,(width G)
proof
let y be
set ;
:: according to TARSKI:def 3 :: thesis: ( not y in Ball u,(s - ((G * 1,(width G)) `2 )) or y in h_strip G,(width G) )
A12:
Ball u,
(s - ((G * 1,(width G)) `2 )) = { v where v is Point of (Euclid 2) : dist u,v < s - ((G * 1,(width G)) `2 ) }
by METRIC_1:18;
assume
y in Ball u,
(s - ((G * 1,(width G)) `2 ))
;
:: thesis: y in h_strip G,(width G)
then consider v being
Point of
(Euclid 2) such that A13:
v = y
and A14:
dist u,
v < s - ((G * 1,(width G)) `2 )
by A12;
reconsider q =
v as
Point of
(TOP-REAL 2) by TOPREAL3:13;
A15:
q = |[(q `1 ),(q `2 )]|
by EUCLID:57;
then A16:
sqrt (((r - (q `1 )) ^2 ) + ((s - (q `2 )) ^2 )) < s - ((G * 1,(width G)) `2 )
by A14, Th9;
A17:
(s - (q `2 )) ^2 >= 0
by XREAL_1:65;
0 <= (r - (q `1 )) ^2
by XREAL_1:65;
then
((s - (q `2 )) ^2 ) + 0 <= ((r - (q `1 )) ^2 ) + ((s - (q `2 )) ^2 )
by XREAL_1:8;
then
sqrt ((s - (q `2 )) ^2 ) <= sqrt (((r - (q `1 )) ^2 ) + ((s - (q `2 )) ^2 ))
by A17, SQUARE_1:94;
then
sqrt ((s - (q `2 )) ^2 ) <= s - ((G * 1,(width G)) `2 )
by A16, XXREAL_0:2;
then A18:
abs (s - (q `2 )) <= s - ((G * 1,(width G)) `2 )
by COMPLEX1:158;
end;
reconsider B = Ball u,(s - ((G * 1,(width G)) `2 )) as Subset of (TOP-REAL 2) by TOPREAL3:13;
B is open
by Th6;
hence
x in Int (h_strip G,(width G))
by A8, A10, A11, TOPS_1:54; :: thesis: verum