:: GOBRD11 semantic presentation

REAL is V110() V111() V112() V116() set
NAT is V110() V111() V112() V113() V114() V115() V116() Element of bool REAL
bool REAL is non empty set
COMPLEX is V110() V116() set
omega is V110() V111() V112() V113() V114() V115() V116() set
bool omega is non empty set
1 is non empty natural V14() real ext-real positive non negative V108() V109() V110() V111() V112() V113() V114() V115() Element of NAT
[:1,1:] is non empty set
bool [:1,1:] is non empty set
[:[:1,1:],1:] is non empty set
bool [:[:1,1:],1:] is non empty set
[:[:1,1:],REAL:] is set
bool [:[:1,1:],REAL:] is non empty set
[:REAL,REAL:] is set
[:[:REAL,REAL:],REAL:] is set
bool [:[:REAL,REAL:],REAL:] is non empty set
2 is non empty natural V14() real ext-real positive non negative V108() V109() V110() V111() V112() V113() V114() V115() Element of NAT
[:2,2:] is non empty set
[:[:2,2:],REAL:] is set
bool [:[:2,2:],REAL:] is non empty set
RAT is V110() V111() V112() V113() V116() set
INT is V110() V111() V112() V113() V114() V116() set
bool NAT is non empty set
bool [:REAL,REAL:] is non empty set
TOP-REAL 2 is non empty TopSpace-like V136() V161() V162() V163() V164() V165() V166() V167() strict RLTopStruct
the carrier of (TOP-REAL 2) is non empty set
K295( the carrier of (TOP-REAL 2)) is M12( the carrier of (TOP-REAL 2))
bool the carrier of (TOP-REAL 2) is non empty set
{} is empty V110() V111() V112() V113() V114() V115() V116() set
the empty V110() V111() V112() V113() V114() V115() V116() set is empty V110() V111() V112() V113() V114() V115() V116() set
0 is empty natural V14() real ext-real non positive non negative V108() V109() V110() V111() V112() V113() V114() V115() V116() Element of NAT
K396(1,2) is V14() real ext-real non negative Element of COMPLEX
|[1,0]| is V43(2) V100() FinSequence-like Element of the carrier of (TOP-REAL 2)
K47(1) is V14() real ext-real non positive set
|[K47(1),1]| is V43(2) V100() FinSequence-like Element of the carrier of (TOP-REAL 2)
sqrt 2 is V14() real ext-real Element of REAL
Euclid 2 is non empty strict Reflexive discerning symmetric triangle MetrStruct
REAL 2 is non empty FinSequence-membered M12( REAL )
K296(2,REAL) is FinSequence-membered M12( REAL )
Pitag_dist 2 is V19() V22([:(REAL 2),(REAL 2):]) V23( REAL ) V24() V33([:(REAL 2),(REAL 2):], REAL ) Element of bool [:[:(REAL 2),(REAL 2):],REAL:]
[:(REAL 2),(REAL 2):] is non empty set
[:[:(REAL 2),(REAL 2):],REAL:] is set
bool [:[:(REAL 2),(REAL 2):],REAL:] is non empty set
MetrStruct(# (REAL 2),(Pitag_dist 2) #) is strict MetrStruct
the carrier of (Euclid 2) is non empty set
i is non empty TopSpace-like TopStruct
the carrier of i is non empty set
bool the carrier of i is non empty set
j is Element of bool the carrier of i
G is Element of the carrier of i
Component_of G is Element of bool the carrier of i
bool (bool the carrier of i) is non empty set
Y is Element of bool (bool the carrier of i)
union Y is set
x is set
i is non empty TopSpace-like TopStruct
the carrier of i is non empty set
bool the carrier of i is non empty set
Y is Element of bool the carrier of i
j is Element of bool the carrier of i
G is Element of bool the carrier of i
Cl j is Element of bool the carrier of i
Cl G is Element of bool the carrier of i
(Cl j) /\ (Cl G) is Element of bool the carrier of i
x is Element of the carrier of i
p is Element of bool the carrier of i
Cl Y is Element of bool the carrier of i
Component_of x is Element of bool the carrier of i
i is non empty TopSpace-like TopStruct
the carrier of i is non empty set
bool the carrier of i is non empty set
j is Element of bool the carrier of i
G is Element of bool the carrier of i
j \/ G is Element of bool the carrier of i
{j,G} is non empty set
Y is set
bool (bool the carrier of i) is non empty set
Y is Element of bool (bool the carrier of i)
x is Element of bool (bool the carrier of i)
p is Element of bool the carrier of i
union x is set
i is non empty TopSpace-like TopStruct
the carrier of i is non empty set
bool the carrier of i is non empty set
j is Element of bool the carrier of i
G is Element of bool the carrier of i
j \/ G is Element of bool the carrier of i
Y is Element of bool the carrier of i
Down ((j \/ G),Y) is Element of bool the carrier of (i | Y)
i | Y is strict TopSpace-like SubSpace of i
the carrier of (i | Y) is set
bool the carrier of (i | Y) is non empty set
Down (j,Y) is Element of bool the carrier of (i | Y)
Down (G,Y) is Element of bool the carrier of (i | Y)
(Down (j,Y)) \/ (Down (G,Y)) is Element of bool the carrier of (i | Y)
G /\ Y is Element of bool the carrier of i
(j \/ G) /\ Y is Element of bool the carrier of i
j /\ Y is Element of bool the carrier of i
i is non empty TopSpace-like TopStruct
the carrier of i is non empty set
bool the carrier of i is non empty set
j is Element of bool the carrier of i
G is Element of bool the carrier of i
j /\ G is Element of bool the carrier of i
Y is Element of bool the carrier of i
Down ((j /\ G),Y) is Element of bool the carrier of (i | Y)
i | Y is strict TopSpace-like SubSpace of i
the carrier of (i | Y) is set
bool the carrier of (i | Y) is non empty set
Down (j,Y) is Element of bool the carrier of (i | Y)
Down (G,Y) is Element of bool the carrier of (i | Y)
(Down (j,Y)) /\ (Down (G,Y)) is Element of bool the carrier of (i | Y)
(j /\ G) /\ Y is Element of bool the carrier of i
Y /\ Y is Element of bool the carrier of i
G /\ (Y /\ Y) is Element of bool the carrier of i
j /\ (G /\ (Y /\ Y)) is Element of bool the carrier of i
G /\ Y is Element of bool the carrier of i
(G /\ Y) /\ Y is Element of bool the carrier of i
j /\ ((G /\ Y) /\ Y) is Element of bool the carrier of i
j /\ Y is Element of bool the carrier of i
(j /\ Y) /\ (G /\ Y) is Element of bool the carrier of i
i is non empty V19() V22( NAT ) V23( the carrier of (TOP-REAL 2)) V24() non constant FinSequence-like V180( the carrier of (TOP-REAL 2)) special unfolded s.c.c. standard FinSequence of the carrier of (TOP-REAL 2)
L~ i is Element of bool the carrier of (TOP-REAL 2)
(L~ i) ` is Element of bool the carrier of (TOP-REAL 2)
GoB i is V19() V21() V22( NAT ) V23(K295( the carrier of (TOP-REAL 2))) V24() FinSequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of K295( the carrier of (TOP-REAL 2))
width (GoB i) is natural V14() real ext-real V108() V109() V110() V111() V112() V113() V114() V115() Element of NAT
(width (GoB i)) -' 1 is natural V14() real ext-real non negative V108() V109() V110() V111() V112() V113() V114() V115() Element of NAT
(GoB i) * (1,((width (GoB i)) -' 1)) is V43(2) V100() FinSequence-like Element of the carrier of (TOP-REAL 2)
(GoB i) * (1,(width (GoB i))) is V43(2) V100() FinSequence-like Element of the carrier of (TOP-REAL 2)
((GoB i) * (1,((width (GoB i)) -' 1))) + ((GoB i) * (1,(width (GoB i)))) is V43(2) V100() FinSequence-like Element of the carrier of (TOP-REAL 2)
1 / 2 is V14() real ext-real non negative Element of REAL
(1 / 2) * (((GoB i) * (1,((width (GoB i)) -' 1))) + ((GoB i) * (1,(width (GoB i))))) is V43(2) V100() FinSequence-like Element of the carrier of (TOP-REAL 2)
((1 / 2) * (((GoB i) * (1,((width (GoB i)) -' 1))) + ((GoB i) * (1,(width (GoB i)))))) - |[1,0]| is V43(2) V100() FinSequence-like Element of the carrier of (TOP-REAL 2)
- 1 is V14() real ext-real non positive Element of REAL
|[(- 1),1]| is V43(2) V100() FinSequence-like Element of the carrier of (TOP-REAL 2)
((GoB i) * (1,(width (GoB i)))) + |[(- 1),1]| is V43(2) V100() FinSequence-like Element of the carrier of (TOP-REAL 2)
LSeg ((((1 / 2) * (((GoB i) * (1,((width (GoB i)) -' 1))) + ((GoB i) * (1,(width (GoB i)))))) - |[1,0]|),(((GoB i) * (1,(width (GoB i)))) + |[(- 1),1]|)) is non empty V220( TOP-REAL 2) Element of bool the carrier of (TOP-REAL 2)
i is non empty V19() V22( NAT ) V23( the carrier of (TOP-REAL 2)) V24() non constant FinSequence-like V180( the carrier of (TOP-REAL 2)) special unfolded s.c.c. standard FinSequence of the carrier of (TOP-REAL 2)
L~ i is Element of bool the carrier of (TOP-REAL 2)
(L~ i) ` is Element of bool the carrier of (TOP-REAL 2)
i is non empty V19() V22( NAT ) V23( the carrier of (TOP-REAL 2)) V24() non constant FinSequence-like V180( the carrier of (TOP-REAL 2)) special unfolded s.c.c. standard FinSequence of the carrier of (TOP-REAL 2)
GoB i is V19() V21() V22( NAT ) V23(K295( the carrier of (TOP-REAL 2))) V24() FinSequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of K295( the carrier of (TOP-REAL 2))
len (GoB i) is natural V14() real ext-real V108() V109() V110() V111() V112() V113() V114() V115() Element of NAT
width (GoB i) is natural V14() real ext-real V108() V109() V110() V111() V112() V113() V114() V115() Element of NAT
{ (cell ((GoB i),b<sub>1</sub>,b<sub>2</sub>)) where b<sub>1</sub>, b<sub>2</sub> is natural V14() real ext-real V108() V109() V110() V111() V112() V113() V114() V115() Element of NAT : ( b<sub>1</sub> <= len (GoB i) & b<sub>2</sub> <= width (GoB i) ) } is set
union { (cell ((GoB i),b<sub>1</sub>,b<sub>2</sub>)) where b<sub>1</sub>, b<sub>2</sub> is natural V14() real ext-real V108() V109() V110() V111() V112() V113() V114() V115() Element of NAT : ( b<sub>1</sub> <= len (GoB i) & b<sub>2</sub> <= width (GoB i) ) } is set
Y is set
x is V43(2) V100() FinSequence-like Element of the carrier of (TOP-REAL 2)
x `1 is V14() real ext-real Element of REAL
(GoB i) * (1,1) is V43(2) V100() FinSequence-like Element of the carrier of (TOP-REAL 2)
((GoB i) * (1,1)) `1 is V14() real ext-real Element of REAL
(GoB i) * ((len (GoB i)),1) is V43(2) V100() FinSequence-like Element of the carrier of (TOP-REAL 2)
((GoB i) * ((len (GoB i)),1)) `1 is V14() real ext-real Element of REAL
1 + 1 is non empty natural V14() real ext-real positive non negative V108() V109() V110() V111() V112() V113() V114() V115() Element of NAT
(1 + 1) - 1 is V14() real ext-real Element of REAL
G0 is natural V14() real ext-real V108() V109() V110() V111() V112() V113() V114() V115() Element of NAT
G0 - 1 is V14() real ext-real Element of REAL
u is natural V14() real ext-real V108() V109() V110() V111() V112() V113() V114() V115() Element of NAT
u + 1 is natural V14() real ext-real V108() V109() V110() V111() V112() V113() V114() V115() Element of NAT
(GoB i) * ((u + 1),1) is V43(2) V100() FinSequence-like Element of the carrier of (TOP-REAL 2)
((GoB i) * ((u + 1),1)) `1 is V14() real ext-real Element of REAL
(u + 1) + 1 is natural V14() real ext-real V108() V109() V110() V111() V112() V113() V114() V115() Element of NAT
(GoB i) * (((u + 1) + 1),1) is V43(2) V100() FinSequence-like Element of the carrier of (TOP-REAL 2)
((GoB i) * (((u + 1) + 1),1)) `1 is V14() real ext-real Element of REAL
0 + 1 is non empty natural V14() real ext-real positive non negative V108() V109() V110() V111() V112() V113() V114() V115() Element of NAT
0 + 1 is non empty natural V14() real ext-real positive non negative V108() V109() V110() V111() V112() V113() V114() V115() Element of NAT
(GoB i) * ((0 + 1),1) is V43(2) V100() FinSequence-like Element of the carrier of (TOP-REAL 2)
((GoB i) * ((0 + 1),1)) `1 is V14() real ext-real Element of REAL
(G0 - 1) + 1 is V14() real ext-real Element of REAL
u is natural V14() real ext-real V108() V109() V110() V111() V112() V113() V114() V115() Element of NAT
G0 is natural V14() real ext-real V108() V109() V110() V111() V112() V113() V114() V115() Element of NAT
(GoB i) * (G0,1) is V43(2) V100() FinSequence-like Element of the carrier of (TOP-REAL 2)
((GoB i) * (G0,1)) `1 is V14() real ext-real Element of REAL
G0 + 1 is natural V14() real ext-real V108() V109() V110() V111() V112() V113() V114() V115() Element of NAT
(GoB i) * ((G0 + 1),1) is V43(2) V100() FinSequence-like Element of the carrier of (TOP-REAL 2)
((GoB i) * ((G0 + 1),1)) `1 is V14() real ext-real Element of REAL
G0 is V19() V21() V22( NAT ) V23(K295( the carrier of (TOP-REAL 2))) V24() FinSequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of K295( the carrier of (TOP-REAL 2))
width G0 is natural V14() real ext-real V108() V109() V110() V111() V112() V113() V114() V115() Element of NAT
v_strip (G0,0) is Element of bool the carrier of (TOP-REAL 2)
G0 * (1,1) is V43(2) V100() FinSequence-like Element of the carrier of (TOP-REAL 2)
(G0 * (1,1)) `1 is V14() real ext-real Element of REAL
{ |[b₁,b₂]| where b₁, b₂ is V14() real ext-real Element of REAL : b₁ <= (G0 * (1,1)) `1 } is set
x `2 is V14() real ext-real Element of REAL
|[(x `1),(x `2)]| is V43(2) V100() FinSequence-like Element of the carrier of (TOP-REAL 2)
{ |[b₁,b₂]| where b₁, b₂ is V14() real ext-real Element of REAL : b₁ <= ((GoB i) * (1,1)) `1 } is set
v_strip ((GoB i),0) is Element of bool the carrier of (TOP-REAL 2)
G0 is V19() V21() V22( NAT ) V23(K295( the carrier of (TOP-REAL 2))) V24() FinSequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of K295( the carrier of (TOP-REAL 2))
width G0 is natural V14() real ext-real V108() V109() V110() V111() V112() V113() V114() V115() Element of NAT
len G0 is natural V14() real ext-real V108() V109() V110() V111() V112() V113() V114() V115() Element of NAT
v_strip (G0,(len G0)) is Element of bool the carrier of (TOP-REAL 2)
G0 * ((len G0),1) is V43(2) V100() FinSequence-like Element of the carrier of (TOP-REAL 2)
(G0 * ((len G0),1)) `1 is V14() real ext-real Element of REAL
{ |[b₁,b₂]| where b₁, b₂ is V14() real ext-real Element of REAL : (G0 * ((len G0),1)) `1 <= b<sub>1</sub> } is set
x `2 is V14() real ext-real Element of REAL
|[(x `1),(x `2)]| is V43(2) V100() FinSequence-like Element of the carrier of (TOP-REAL 2)
(GoB i) * ((len G0),1) is V43(2) V100() FinSequence-like Element of the carrier of (TOP-REAL 2)
((GoB i) * ((len G0),1)) `1 is V14() real ext-real Element of REAL
{ |[b<sub>1</sub>,b<sub>2</sub>]| where b<sub>1</sub>, b<sub>2</sub> is V14() real ext-real Element of REAL : ((GoB i) * ((len G0),1)) `1 <= b₁ } is set
v_strip ((GoB i),(len (GoB i))) is Element of bool the carrier of (TOP-REAL 2)
u is natural V14() real ext-real V108() V109() V110() V111() V112() V113() V114() V115() Element of NAT
(GoB i) * (u,1) is V43(2) V100() FinSequence-like Element of the carrier of (TOP-REAL 2)
((GoB i) * (u,1)) `1 is V14() real ext-real Element of REAL
u + 1 is natural V14() real ext-real V108() V109() V110() V111() V112() V113() V114() V115() Element of NAT
(GoB i) * ((u + 1),1) is V43(2) V100() FinSequence-like Element of the carrier of (TOP-REAL 2)
((GoB i) * ((u + 1),1)) `1 is V14() real ext-real Element of REAL
u is natural V14() real ext-real V108() V109() V110() V111() V112() V113() V114() V115() Element of NAT
(GoB i) * (u,1) is V43(2) V100() FinSequence-like Element of the carrier of (TOP-REAL 2)
((GoB i) * (u,1)) `1 is V14() real ext-real Element of REAL
u + 1 is natural V14() real ext-real V108() V109() V110() V111() V112() V113() V114() V115() Element of NAT
(GoB i) * ((u + 1),1) is V43(2) V100() FinSequence-like Element of the carrier of (TOP-REAL 2)
((GoB i) * ((u + 1),1)) `1 is V14() real ext-real Element of REAL
x `2 is V14() real ext-real Element of REAL
|[(x `1),(x `2)]| is V43(2) V100() FinSequence-like Element of the carrier of (TOP-REAL 2)
G0 is V19() V21() V22( NAT ) V23(K295( the carrier of (TOP-REAL 2))) V24() FinSequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of K295( the carrier of (TOP-REAL 2))
G0 * (u,1) is V43(2) V100() FinSequence-like Element of the carrier of (TOP-REAL 2)
(G0 * (u,1)) `1 is V14() real ext-real Element of REAL
G0 * ((u + 1),1) is V43(2) V100() FinSequence-like Element of the carrier of (TOP-REAL 2)
(G0 * ((u + 1),1)) `1 is V14() real ext-real Element of REAL
{ |[b<sub>1</sub>,b<sub>2</sub>]| where b<sub>1</sub>, b<sub>2</sub> is V14() real ext-real Element of REAL : ( (G0 * (u,1)) `1 <= b₁ & b₁ <= (G0 * ((u + 1),1)) `1 ) } is set
width G0 is natural V14() real ext-real V108() V109() V110() V111() V112() V113() V114() V115() Element of NAT
v_strip (G0,u) is Element of bool the carrier of (TOP-REAL 2)
v_strip ((GoB i),u) is Element of bool the carrier of (TOP-REAL 2)
G0 is natural V14() real ext-real V108() V109() V110() V111() V112() V113() V114() V115() Element of NAT
(GoB i) * (G0,1) is V43(2) V100() FinSequence-like Element of the carrier of (TOP-REAL 2)
((GoB i) * (G0,1)) `1 is V14() real ext-real Element of REAL
G0 + 1 is natural V14() real ext-real V108() V109() V110() V111() V112() V113() V114() V115() Element of NAT
(GoB i) * ((G0 + 1),1) is V43(2) V100() FinSequence-like Element of the carrier of (TOP-REAL 2)
((GoB i) * ((G0 + 1),1)) `1 is V14() real ext-real Element of REAL
G0 is natural V14() real ext-real V108() V109() V110() V111() V112() V113() V114() V115() Element of NAT
v_strip ((GoB i),G0) is Element of bool the carrier of (TOP-REAL 2)
u is natural V14() real ext-real V108() V109() V110() V111() V112() V113() V114() V115() Element of NAT
v_strip ((GoB i),u) is Element of bool the carrier of (TOP-REAL 2)
v is natural V14() real ext-real V108() V109() V110() V111() V112() V113() V114() V115() Element of NAT
(GoB i) * (v,1) is V43(2) V100() FinSequence-like Element of the carrier of (TOP-REAL 2)
((GoB i) * (v,1)) `1 is V14() real ext-real Element of REAL
v + 1 is natural V14() real ext-real V108() V109() V110() V111() V112() V113() V114() V115() Element of NAT
(GoB i) * ((v + 1),1) is V43(2) V100() FinSequence-like Element of the carrier of (TOP-REAL 2)
((GoB i) * ((v + 1),1)) `1 is V14() real ext-real Element of REAL
G00 is natural V14() real ext-real V108() V109() V110() V111() V112() V113() V114() V115() Element of NAT
v_strip ((GoB i),G00) is Element of bool the carrier of (TOP-REAL 2)
G0 is natural V14() real ext-real V108() V109() V110() V111() V112() V113() V114() V115() Element of NAT
v_strip ((GoB i),G0) is Element of bool the carrier of (TOP-REAL 2)
x `2 is V14() real ext-real Element of REAL
((GoB i) * (1,1)) `2 is V14() real ext-real Element of REAL
(GoB i) * (1,(width (GoB i))) is V43(2) V100() FinSequence-like Element of the carrier of (TOP-REAL 2)
((GoB i) * (1,(width (GoB i)))) `2 is V14() real ext-real Element of REAL
v is natural V14() real ext-real V108() V109() V110() V111() V112() V113() V114() V115() Element of NAT
v - 1 is V14() real ext-real Element of REAL
G00 is natural V14() real ext-real V108() V109() V110() V111() V112() V113() V114() V115() Element of NAT
G00 + 1 is natural V14() real ext-real V108() V109() V110() V111() V112() V113() V114() V115() Element of NAT
(GoB i) * (1,(G00 + 1)) is V43(2) V100() FinSequence-like Element of the carrier of (TOP-REAL 2)
((GoB i) * (1,(G00 + 1))) `2 is V14() real ext-real Element of REAL
(G00 + 1) + 1 is natural V14() real ext-real V108() V109() V110() V111() V112() V113() V114() V115() Element of NAT
(GoB i) * (1,((G00 + 1) + 1)) is V43(2) V100() FinSequence-like Element of the carrier of (TOP-REAL 2)
((GoB i) * (1,((G00 + 1) + 1))) `2 is V14() real ext-real Element of REAL
(GoB i) * (1,(0 + 1)) is V43(2) V100() FinSequence-like Element of the carrier of (TOP-REAL 2)
((GoB i) * (1,(0 + 1))) `2 is V14() real ext-real Element of REAL
(v - 1) + 1 is V14() real ext-real Element of REAL
G00 is natural V14() real ext-real V108() V109() V110() V111() V112() V113() V114() V115() Element of NAT
v is natural V14() real ext-real V108() V109() V110() V111() V112() V113() V114() V115() Element of NAT
(GoB i) * (1,v) is V43(2) V100() FinSequence-like Element of the carrier of (TOP-REAL 2)
((GoB i) * (1,v)) `2 is V14() real ext-real Element of REAL
v + 1 is natural V14() real ext-real V108() V109() V110() V111() V112() V113() V114() V115() Element of NAT
(GoB i) * (1,(v + 1)) is V43(2) V100() FinSequence-like Element of the carrier of (TOP-REAL 2)
((GoB i) * (1,(v + 1))) `2 is V14() real ext-real Element of REAL
v is V19() V21() V22( NAT ) V23(K295( the carrier of (TOP-REAL 2))) V24() FinSequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of K295( the carrier of (TOP-REAL 2))
len v is natural V14() real ext-real V108() V109() V110() V111() V112() V113() V114() V115() Element of NAT
h_strip (v,0) is Element of bool the carrier of (TOP-REAL 2)
v * (1,1) is V43(2) V100() FinSequence-like Element of the carrier of (TOP-REAL 2)
(v * (1,1)) `2 is V14() real ext-real Element of REAL
{ |[b₁,b₂]| where b₁, b₂ is V14() real ext-real Element of REAL : b₂ <= (v * (1,1)) `2 } is set
|[(x `1),(x `2)]| is V43(2) V100() FinSequence-like Element of the carrier of (TOP-REAL 2)
{ |[b<sub>1</sub>,b<sub>2</sub>]| where b<sub>1</sub>, b<sub>2</sub> is V14() real ext-real Element of REAL : b<sub>2</sub> <= ((GoB i) * (1,1)) `2 } is set
h_strip ((GoB i),0) is Element of bool the carrier of (TOP-REAL 2)
v is V19() V21() V22( NAT ) V23(K295( the carrier of (TOP-REAL 2))) V24() FinSequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of K295( the carrier of (TOP-REAL 2))
len v is natural V14() real ext-real V108() V109() V110() V111() V112() V113() V114() V115() Element of NAT
width v is natural V14() real ext-real V108() V109() V110() V111() V112() V113() V114() V115() Element of NAT
h_strip (v,(width v)) is Element of bool the carrier of (TOP-REAL 2)
v * (1,(width v)) is V43(2) V100() FinSequence-like Element of the carrier of (TOP-REAL 2)
(v * (1,(width v))) `2 is V14() real ext-real Element of REAL
{ |[b<sub>1</sub>,b<sub>2</sub>]| where b<sub>1</sub>, b<sub>2</sub> is V14() real ext-real Element of REAL : (v * (1,(width v))) `2 <= b₂ } is set
|[(x `1),(x `2)]| is V43(2) V100() FinSequence-like Element of the carrier of (TOP-REAL 2)
(GoB i) * (1,(width v)) is V43(2) V100() FinSequence-like Element of the carrier of (TOP-REAL 2)
((GoB i) * (1,(width v))) `2 is V14() real ext-real Element of REAL
{ |[b<sub>1</sub>,b<sub>2</sub>]| where b<sub>1</sub>, b<sub>2</sub> is V14() real ext-real Element of REAL : ((GoB i) * (1,(width v))) `2 <= b₂ } is set
h_strip ((GoB i),(width (GoB i))) is Element of bool the carrier of (TOP-REAL 2)
G00 is natural V14() real ext-real V108() V109() V110() V111() V112() V113() V114() V115() Element of NAT
(GoB i) * (1,G00) is V43(2) V100() FinSequence-like Element of the carrier of (TOP-REAL 2)
((GoB i) * (1,G00)) `2 is V14() real ext-real Element of REAL
G00 + 1 is natural V14() real ext-real V108() V109() V110() V111() V112() V113() V114() V115() Element of NAT
(GoB i) * (1,(G00 + 1)) is V43(2) V100() FinSequence-like Element of the carrier of (TOP-REAL 2)
((GoB i) * (1,(G00 + 1))) `2 is V14() real ext-real Element of REAL
G00 is natural V14() real ext-real V108() V109() V110() V111() V112() V113() V114() V115() Element of NAT
(GoB i) * (1,G00) is V43(2) V100() FinSequence-like Element of the carrier of (TOP-REAL 2)
((GoB i) * (1,G00)) `2 is V14() real ext-real Element of REAL
G00 + 1 is natural V14() real ext-real V108() V109() V110() V111() V112() V113() V114() V115() Element of NAT
(GoB i) * (1,(G00 + 1)) is V43(2) V100() FinSequence-like Element of the carrier of (TOP-REAL 2)
((GoB i) * (1,(G00 + 1))) `2 is V14() real ext-real Element of REAL
|[(x `1),(x `2)]| is V43(2) V100() FinSequence-like Element of the carrier of (TOP-REAL 2)
v is V19() V21() V22( NAT ) V23(K295( the carrier of (TOP-REAL 2))) V24() FinSequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of K295( the carrier of (TOP-REAL 2))
v * (1,G00) is V43(2) V100() FinSequence-like Element of the carrier of (TOP-REAL 2)
(v * (1,G00)) `2 is V14() real ext-real Element of REAL
v * (1,(G00 + 1)) is V43(2) V100() FinSequence-like Element of the carrier of (TOP-REAL 2)
(v * (1,(G00 + 1))) `2 is V14() real ext-real Element of REAL
{ |[b₁,b₂]| where b₁, b₂ is V14() real ext-real Element of REAL : ( (v * (1,G00)) `2 <= b<sub>2</sub> & b<sub>2</sub> <= (v * (1,(G00 + 1))) `2 ) } is set
len v is natural V14() real ext-real V108() V109() V110() V111() V112() V113() V114() V115() Element of NAT
h_strip (v,G00) is Element of bool the carrier of (TOP-REAL 2)
h_strip ((GoB i),G00) is Element of bool the carrier of (TOP-REAL 2)
v is natural V14() real ext-real V108() V109() V110() V111() V112() V113() V114() V115() Element of NAT
(GoB i) * (1,v) is V43(2) V100() FinSequence-like Element of the carrier of (TOP-REAL 2)
((GoB i) * (1,v)) `2 is V14() real ext-real Element of REAL
v + 1 is natural V14() real ext-real V108() V109() V110() V111() V112() V113() V114() V115() Element of NAT
(GoB i) * (1,(v + 1)) is V43(2) V100() FinSequence-like Element of the carrier of (TOP-REAL 2)
((GoB i) * (1,(v + 1))) `2 is V14() real ext-real Element of REAL
v is natural V14() real ext-real V108() V109() V110() V111() V112() V113() V114() V115() Element of NAT
h_strip ((GoB i),v) is Element of bool the carrier of (TOP-REAL 2)
G00 is natural V14() real ext-real V108() V109() V110() V111() V112() V113() V114() V115() Element of NAT
h_strip ((GoB i),G00) is Element of bool the carrier of (TOP-REAL 2)
r is natural V14() real ext-real V108() V109() V110() V111() V112() V113() V114() V115() Element of NAT
(GoB i) * (1,r) is V43(2) V100() FinSequence-like Element of the carrier of (TOP-REAL 2)
((GoB i) * (1,r)) `2 is V14() real ext-real Element of REAL
r + 1 is natural V14() real ext-real V108() V109() V110() V111() V112() V113() V114() V115() Element of NAT
(GoB i) * (1,(r + 1)) is V43(2) V100() FinSequence-like Element of the carrier of (TOP-REAL 2)
((GoB i) * (1,(r + 1))) `2 is V14() real ext-real Element of REAL
r is natural V14() real ext-real V108() V109() V110() V111() V112() V113() V114() V115() Element of NAT
h_strip ((GoB i),r) is Element of bool the carrier of (TOP-REAL 2)
v is natural V14() real ext-real V108() V109() V110() V111() V112() V113() V114() V115() Element of NAT
h_strip ((GoB i),v) is Element of bool the carrier of (TOP-REAL 2)
cell ((GoB i),G0,v) is Element of bool the carrier of (TOP-REAL 2)
(v_strip ((GoB i),G0)) /\ (h_strip ((GoB i),v)) is Element of bool the carrier of (TOP-REAL 2)
G00 is set
Y is set
x is set
p is natural V14() real ext-real V108() V109() V110() V111() V112() V113() V114() V115() Element of NAT
G0 is natural V14() real ext-real V108() V109() V110() V111() V112() V113() V114() V115() Element of NAT
cell ((GoB i),p,G0) is Element of bool the carrier of (TOP-REAL 2)
i is V14() real ext-real Element of REAL
{ |[b₁,b₂]| where b₁, b₂ is V14() real ext-real Element of REAL : i <= b₂ } is set
j is set
G is V14() real ext-real Element of REAL
Y is V14() real ext-real Element of REAL
|[G,Y]| is V43(2) V100() FinSequence-like Element of the carrier of (TOP-REAL 2)
i is V14() real ext-real Element of REAL
{ |[b₁,b₂]| where b₁, b₂ is V14() real ext-real Element of REAL : not b₂ <= i } is set
j is set
G is V14() real ext-real Element of REAL
Y is V14() real ext-real Element of REAL
|[G,Y]| is V43(2) V100() FinSequence-like Element of the carrier of (TOP-REAL 2)
i is V14() real ext-real Element of REAL
{ |[b₁,b₂]| where b₁, b₂ is V14() real ext-real Element of REAL : b₂ <= i } is set
j is set
G is V14() real ext-real Element of REAL
Y is V14() real ext-real Element of REAL
|[G,Y]| is V43(2) V100() FinSequence-like Element of the carrier of (TOP-REAL 2)
i is V14() real ext-real Element of REAL
{ |[b₁,b₂]| where b₁, b₂ is V14() real ext-real Element of REAL : not i <= b₂ } is set
j is set
G is V14() real ext-real Element of REAL
Y is V14() real ext-real Element of REAL
|[G,Y]| is V43(2) V100() FinSequence-like Element of the carrier of (TOP-REAL 2)
i is V14() real ext-real Element of REAL
{ |[b₁,b₂]| where b₁, b₂ is V14() real ext-real Element of REAL : b₁ <= i } is set
j is set
G is V14() real ext-real Element of REAL
Y is V14() real ext-real Element of REAL
|[G,Y]| is V43(2) V100() FinSequence-like Element of the carrier of (TOP-REAL 2)
i is V14() real ext-real Element of REAL
{ |[b₁,b₂]| where b₁, b₂ is V14() real ext-real Element of REAL : not i <= b₁ } is set
j is set
G is V14() real ext-real Element of REAL
Y is V14() real ext-real Element of REAL
|[G,Y]| is V43(2) V100() FinSequence-like Element of the carrier of (TOP-REAL 2)
i is V14() real ext-real Element of REAL
{ |[b₁,b₂]| where b₁, b₂ is V14() real ext-real Element of REAL : i <= b₁ } is set
j is set
G is V14() real ext-real Element of REAL
Y is V14() real ext-real Element of REAL
|[G,Y]| is V43(2) V100() FinSequence-like Element of the carrier of (TOP-REAL 2)
i is V14() real ext-real Element of REAL
{ |[b₁,b₂]| where b₁, b₂ is V14() real ext-real Element of REAL : not b₁ <= i } is set
j is set
G is V14() real ext-real Element of REAL
Y is V14() real ext-real Element of REAL
|[G,Y]| is V43(2) V100() FinSequence-like Element of the carrier of (TOP-REAL 2)
i is V14() real ext-real Element of REAL
{ |[b₁,b₂]| where b₁, b₂ is V14() real ext-real Element of REAL : b₂ <= i } is set
{ |[b₁,b₂]| where b₁, b₂ is V14() real ext-real Element of REAL : not b₂ <= i } is set
j is Element of bool the carrier of (TOP-REAL 2)
G is Element of bool the carrier of (TOP-REAL 2)
G ` is Element of bool the carrier of (TOP-REAL 2)
Y is set
x is V43(2) V100() FinSequence-like Element of the carrier of (TOP-REAL 2)
x `1 is V14() real ext-real Element of REAL
x `2 is V14() real ext-real Element of REAL
|[(x `1),(x `2)]| is V43(2) V100() FinSequence-like Element of the carrier of (TOP-REAL 2)
the carrier of (TOP-REAL 2) \ G is Element of bool the carrier of (TOP-REAL 2)
Y is set
x is V14() real ext-real Element of REAL
p is V14() real ext-real Element of REAL
|[x,p]| is V43(2) V100() FinSequence-like Element of the carrier of (TOP-REAL 2)
G0 is V14() real ext-real Element of REAL
u is V14() real ext-real Element of REAL
|[G0,u]| is V43(2) V100() FinSequence-like Element of the carrier of (TOP-REAL 2)
the carrier of (TOP-REAL 2) \ G is Element of bool the carrier of (TOP-REAL 2)
i is V14() real ext-real Element of REAL
{ |[b<sub>1</sub>,b<sub>2</sub>]| where b<sub>1</sub>, b<sub>2</sub> is V14() real ext-real Element of REAL : i <= b<sub>2</sub> } is set
{ |[b<sub>1</sub>,b<sub>2</sub>]| where b<sub>1</sub>, b<sub>2</sub> is V14() real ext-real Element of REAL : not i <= b<sub>2</sub> } is set
j is Element of bool the carrier of (TOP-REAL 2)
G is Element of bool the carrier of (TOP-REAL 2)
G ` is Element of bool the carrier of (TOP-REAL 2)
Y is set
x is V43(2) V100() FinSequence-like Element of the carrier of (TOP-REAL 2)
x `1 is V14() real ext-real Element of REAL
x `2 is V14() real ext-real Element of REAL
|[(x `1),(x `2)]| is V43(2) V100() FinSequence-like Element of the carrier of (TOP-REAL 2)
the carrier of (TOP-REAL 2) \ G is Element of bool the carrier of (TOP-REAL 2)
Y is set
x is V14() real ext-real Element of REAL
p is V14() real ext-real Element of REAL
|[x,p]| is V43(2) V100() FinSequence-like Element of the carrier of (TOP-REAL 2)
G0 is V14() real ext-real Element of REAL
u is V14() real ext-real Element of REAL
|[G0,u]| is V43(2) V100() FinSequence-like Element of the carrier of (TOP-REAL 2)
the carrier of (TOP-REAL 2) \ G is Element of bool the carrier of (TOP-REAL 2)
i is V14() real ext-real Element of REAL
{ |[b₁,b₂]| where b₁, b₂ is V14() real ext-real Element of REAL : i <= b₁ } is set
{ |[b₁,b₂]| where b₁, b₂ is V14() real ext-real Element of REAL : not i <= b₁ } is set
j is Element of bool the carrier of (TOP-REAL 2)
G is Element of bool the carrier of (TOP-REAL 2)
G ` is Element of bool the carrier of (TOP-REAL 2)
Y is set
x is V43(2) V100() FinSequence-like Element of the carrier of (TOP-REAL 2)
x `1 is V14() real ext-real Element of REAL
x `2 is V14() real ext-real Element of REAL
|[(x `1),(x `2)]| is V43(2) V100() FinSequence-like Element of the carrier of (TOP-REAL 2)
the carrier of (TOP-REAL 2) \ G is Element of bool the carrier of (TOP-REAL 2)
Y is set
x is V14() real ext-real Element of REAL
p is V14() real ext-real Element of REAL
|[x,p]| is V43(2) V100() FinSequence-like Element of the carrier of (TOP-REAL 2)
G0 is V14() real ext-real Element of REAL
u is V14() real ext-real Element of REAL
|[G0,u]| is V43(2) V100() FinSequence-like Element of the carrier of (TOP-REAL 2)
the carrier of (TOP-REAL 2) \ G is Element of bool the carrier of (TOP-REAL 2)
i is V14() real ext-real Element of REAL
{ |[b<sub>1</sub>,b<sub>2</sub>]| where b<sub>1</sub>, b<sub>2</sub> is V14() real ext-real Element of REAL : b<sub>1</sub> <= i } is set
{ |[b<sub>1</sub>,b<sub>2</sub>]| where b<sub>1</sub>, b<sub>2</sub> is V14() real ext-real Element of REAL : not b<sub>1</sub> <= i } is set
j is Element of bool the carrier of (TOP-REAL 2)
G is Element of bool the carrier of (TOP-REAL 2)
G ` is Element of bool the carrier of (TOP-REAL 2)
Y is set
x is V43(2) V100() FinSequence-like Element of the carrier of (TOP-REAL 2)
x `1 is V14() real ext-real Element of REAL
x `2 is V14() real ext-real Element of REAL
|[(x `1),(x `2)]| is V43(2) V100() FinSequence-like Element of the carrier of (TOP-REAL 2)
the carrier of (TOP-REAL 2) \ G is Element of bool the carrier of (TOP-REAL 2)
Y is set
x is V14() real ext-real Element of REAL
p is V14() real ext-real Element of REAL
|[x,p]| is V43(2) V100() FinSequence-like Element of the carrier of (TOP-REAL 2)
G0 is V14() real ext-real Element of REAL
u is V14() real ext-real Element of REAL
|[G0,u]| is V43(2) V100() FinSequence-like Element of the carrier of (TOP-REAL 2)
the carrier of (TOP-REAL 2) \ G is Element of bool the carrier of (TOP-REAL 2)
i is Element of bool the carrier of (TOP-REAL 2)
j is V14() real ext-real Element of REAL
{ |[b₁,b₂]| where b₁, b₂ is V14() real ext-real Element of REAL : b₂ <= j } is set
{ |[b₁,b₂]| where b₁, b₂ is V14() real ext-real Element of REAL : not b₂ <= j } is set
G is Element of bool the carrier of (TOP-REAL 2)
G ` is Element of bool the carrier of (TOP-REAL 2)
i is Element of bool the carrier of (TOP-REAL 2)
j is V14() real ext-real Element of REAL
{ |[b<sub>1</sub>,b<sub>2</sub>]| where b<sub>1</sub>, b<sub>2</sub> is V14() real ext-real Element of REAL : j <= b<sub>2</sub> } is set
{ |[b<sub>1</sub>,b<sub>2</sub>]| where b<sub>1</sub>, b<sub>2</sub> is V14() real ext-real Element of REAL : not j <= b<sub>2</sub> } is set
G is Element of bool the carrier of (TOP-REAL 2)
G ` is Element of bool the carrier of (TOP-REAL 2)
i is Element of bool the carrier of (TOP-REAL 2)
j is V14() real ext-real Element of REAL
{ |[b₁,b₂]| where b₁, b₂ is V14() real ext-real Element of REAL : b₁ <= j } is set
{ |[b₁,b₂]| where b₁, b₂ is V14() real ext-real Element of REAL : not b₁ <= j } is set
G is Element of bool the carrier of (TOP-REAL 2)
G ` is Element of bool the carrier of (TOP-REAL 2)
i is Element of bool the carrier of (TOP-REAL 2)
j is V14() real ext-real Element of REAL
{ |[b<sub>1</sub>,b<sub>2</sub>]| where b<sub>1</sub>, b<sub>2</sub> is V14() real ext-real Element of REAL : j <= b<sub>1</sub> } is set
{ |[b<sub>1</sub>,b<sub>2</sub>]| where b<sub>1</sub>, b<sub>2</sub> is V14() real ext-real Element of REAL : not j <= b<sub>1</sub> } is set
G is Element of bool the carrier of (TOP-REAL 2)
G ` is Element of bool the carrier of (TOP-REAL 2)
i is natural V14() real ext-real V108() V109() V110() V111() V112() V113() V114() V115() Element of NAT
j is V19() V22( NAT ) V23(K295( the carrier of (TOP-REAL 2))) V24() FinSequence-like tabular FinSequence of K295( the carrier of (TOP-REAL 2))
h_strip (j,i) is Element of bool the carrier of (TOP-REAL 2)
width j is natural V14() real ext-real V108() V109() V110() V111() V112() V113() V114() V115() Element of NAT
j * (1,i) is V43(2) V100() FinSequence-like Element of the carrier of (TOP-REAL 2)
(j * (1,i)) `2 is V14() real ext-real Element of REAL
{ |[b<sub>1</sub>,b<sub>2</sub>]| where b<sub>1</sub>, b<sub>2</sub> is V14() real ext-real Element of REAL : (j * (1,i)) `2 <= b₂ } is set
i + 1 is natural V14() real ext-real V108() V109() V110() V111() V112() V113() V114() V115() Element of NAT
j * (1,(i + 1)) is V43(2) V100() FinSequence-like Element of the carrier of (TOP-REAL 2)
(j * (1,(i + 1))) `2 is V14() real ext-real Element of REAL
{ |[b<sub>1</sub>,b<sub>2</sub>]| where b<sub>1</sub>, b<sub>2</sub> is V14() real ext-real Element of REAL : b<sub>2</sub> <= (j * (1,(i + 1))) `2 } is set
width j is natural V14() real ext-real V108() V109() V110() V111() V112() V113() V114() V115() Element of NAT
j * (1,i) is V43(2) V100() FinSequence-like Element of the carrier of (TOP-REAL 2)
(j * (1,i)) `2 is V14() real ext-real Element of REAL
i + 1 is natural V14() real ext-real V108() V109() V110() V111() V112() V113() V114() V115() Element of NAT
j * (1,(i + 1)) is V43(2) V100() FinSequence-like Element of the carrier of (TOP-REAL 2)
(j * (1,(i + 1))) `2 is V14() real ext-real Element of REAL
{ |[b₁,b₂]| where b₁, b₂ is V14() real ext-real Element of REAL : ( (j * (1,i)) `2 <= b<sub>2</sub> & b<sub>2</sub> <= (j * (1,(i + 1))) `2 ) } is set
{ |[b₁,b₂]| where b₁, b₂ is V14() real ext-real Element of REAL : b₂ <= (j * (1,(i + 1))) `2 } is set
{ |[b<sub>1</sub>,b<sub>2</sub>]| where b<sub>1</sub>, b<sub>2</sub> is V14() real ext-real Element of REAL : (j * (1,i)) `2 <= b₂ } is set
{ |[b₁,b₂]| where b₁, b₂ is V14() real ext-real Element of REAL : (j * (1,i)) `2 <= b<sub>2</sub> } /\ { |[b<sub>1</sub>,b<sub>2</sub>]| where b<sub>1</sub>, b<sub>2</sub> is V14() real ext-real Element of REAL : b<sub>2</sub> <= (j * (1,(i + 1))) `2 } is set
x is set
p is V14() real ext-real Element of REAL
G0 is V14() real ext-real Element of REAL
|[p,G0]| is V43(2) V100() FinSequence-like Element of the carrier of (TOP-REAL 2)
u is V14() real ext-real Element of REAL
v is V14() real ext-real Element of REAL
|[u,v]| is V43(2) V100() FinSequence-like Element of the carrier of (TOP-REAL 2)
x is set
p is V14() real ext-real Element of REAL
G0 is V14() real ext-real Element of REAL
|[p,G0]| is V43(2) V100() FinSequence-like Element of the carrier of (TOP-REAL 2)
x is set
p is V14() real ext-real Element of REAL
G0 is V14() real ext-real Element of REAL
|[p,G0]| is V43(2) V100() FinSequence-like Element of the carrier of (TOP-REAL 2)
Y is Element of bool the carrier of (TOP-REAL 2)
G is Element of bool the carrier of (TOP-REAL 2)
width j is natural V14() real ext-real V108() V109() V110() V111() V112() V113() V114() V115() Element of NAT
j * (1,i) is V43(2) V100() FinSequence-like Element of the carrier of (TOP-REAL 2)
(j * (1,i)) `2 is V14() real ext-real Element of REAL
{ |[b<sub>1</sub>,b<sub>2</sub>]| where b<sub>1</sub>, b<sub>2</sub> is V14() real ext-real Element of REAL : (j * (1,i)) `2 <= b₂ } is set
width j is natural V14() real ext-real V108() V109() V110() V111() V112() V113() V114() V115() Element of NAT
width j is natural V14() real ext-real V108() V109() V110() V111() V112() V113() V114() V115() Element of NAT
i is natural V14() real ext-real V108() V109() V110() V111() V112() V113() V114() V115() Element of NAT
j is V19() V22( NAT ) V23(K295( the carrier of (TOP-REAL 2))) V24() FinSequence-like tabular FinSequence of K295( the carrier of (TOP-REAL 2))
v_strip (j,i) is Element of bool the carrier of (TOP-REAL 2)
len j is natural V14() real ext-real V108() V109() V110() V111() V112() V113() V114() V115() Element of NAT
j * (i,1) is V43(2) V100() FinSequence-like Element of the carrier of (TOP-REAL 2)
(j * (i,1)) `1 is V14() real ext-real Element of REAL
{ |[b<sub>1</sub>,b<sub>2</sub>]| where b<sub>1</sub>, b<sub>2</sub> is V14() real ext-real Element of REAL : (j * (i,1)) `1 <= b₁ } is set
i + 1 is natural V14() real ext-real V108() V109() V110() V111() V112() V113() V114() V115() Element of NAT
j * ((i + 1),1) is V43(2) V100() FinSequence-like Element of the carrier of (TOP-REAL 2)
(j * ((i + 1),1)) `1 is V14() real ext-real Element of REAL
{ |[b<sub>1</sub>,b<sub>2</sub>]| where b<sub>1</sub>, b<sub>2</sub> is V14() real ext-real Element of REAL : b<sub>1</sub> <= (j * ((i + 1),1)) `1 } is set
len j is natural V14() real ext-real V108() V109() V110() V111() V112() V113() V114() V115() Element of NAT
j * (i,1) is V43(2) V100() FinSequence-like Element of the carrier of (TOP-REAL 2)
(j * (i,1)) `1 is V14() real ext-real Element of REAL
i + 1 is natural V14() real ext-real V108() V109() V110() V111() V112() V113() V114() V115() Element of NAT
j * ((i + 1),1) is V43(2) V100() FinSequence-like Element of the carrier of (TOP-REAL 2)
(j * ((i + 1),1)) `1 is V14() real ext-real Element of REAL
{ |[b₁,b₂]| where b₁, b₂ is V14() real ext-real Element of REAL : ( (j * (i,1)) `1 <= b<sub>1</sub> & b<sub>1</sub> <= (j * ((i + 1),1)) `1 ) } is set
{ |[b₁,b₂]| where b₁, b₂ is V14() real ext-real Element of REAL : b₁ <= (j * ((i + 1),1)) `1 } is set
{ |[b<sub>1</sub>,b<sub>2</sub>]| where b<sub>1</sub>, b<sub>2</sub> is V14() real ext-real Element of REAL : (j * (i,1)) `1 <= b₁ } is set
{ |[b₁,b₂]| where b₁, b₂ is V14() real ext-real Element of REAL : (j * (i,1)) `1 <= b<sub>1</sub> } /\ { |[b<sub>1</sub>,b<sub>2</sub>]| where b<sub>1</sub>, b<sub>2</sub> is V14() real ext-real Element of REAL : b<sub>1</sub> <= (j * ((i + 1),1)) `1 } is set
x is set
p is V14() real ext-real Element of REAL
G0 is V14() real ext-real Element of REAL
|[p,G0]| is V43(2) V100() FinSequence-like Element of the carrier of (TOP-REAL 2)
G0 is V14() real ext-real Element of REAL
p is V14() real ext-real Element of REAL
|[G0,p]| is V43(2) V100() FinSequence-like Element of the carrier of (TOP-REAL 2)
u is V14() real ext-real Element of REAL
v is V14() real ext-real Element of REAL
|[u,v]| is V43(2) V100() FinSequence-like Element of the carrier of (TOP-REAL 2)
x is set
p is V14() real ext-real Element of REAL
G0 is V14() real ext-real Element of REAL
|[p,G0]| is V43(2) V100() FinSequence-like Element of the carrier of (TOP-REAL 2)
x is set
p is V14() real ext-real Element of REAL
G0 is V14() real ext-real Element of REAL
|[p,G0]| is V43(2) V100() FinSequence-like Element of the carrier of (TOP-REAL 2)
Y is Element of bool the carrier of (TOP-REAL 2)
G is Element of bool the carrier of (TOP-REAL 2)
len j is natural V14() real ext-real V108() V109() V110() V111() V112() V113() V114() V115() Element of NAT
j * (i,1) is V43(2) V100() FinSequence-like Element of the carrier of (TOP-REAL 2)
(j * (i,1)) `1 is V14() real ext-real Element of REAL
{ |[b<sub>1</sub>,b<sub>2</sub>]| where b<sub>1</sub>, b<sub>2</sub> is V14() real ext-real Element of REAL : (j * (i,1)) `1 <= b₁ } is set
len j is natural V14() real ext-real V108() V109() V110() V111() V112() V113() V114() V115() Element of NAT
len j is natural V14() real ext-real V108() V109() V110() V111() V112() V113() V114() V115() Element of NAT
i is V19() V21() V22( NAT ) V23(K295( the carrier of (TOP-REAL 2))) V24() FinSequence-like tabular FinSequence of K295( the carrier of (TOP-REAL 2))
v_strip (i,0) is Element of bool the carrier of (TOP-REAL 2)
i * (1,1) is V43(2) V100() FinSequence-like Element of the carrier of (TOP-REAL 2)
(i * (1,1)) `1 is V14() real ext-real Element of REAL
{ |[b<sub>1</sub>,b<sub>2</sub>]| where b<sub>1</sub>, b<sub>2</sub> is V14() real ext-real Element of REAL : b<sub>1</sub> <= (i * (1,1)) `1 } is set
width i is natural V14() real ext-real V108() V109() V110() V111() V112() V113() V114() V115() Element of NAT
i is V19() V21() V22( NAT ) V23(K295( the carrier of (TOP-REAL 2))) V24() FinSequence-like tabular FinSequence of K295( the carrier of (TOP-REAL 2))
len i is natural V14() real ext-real V108() V109() V110() V111() V112() V113() V114() V115() Element of NAT
v_strip (i,(len i)) is Element of bool the carrier of (TOP-REAL 2)
i * ((len i),1) is V43(2) V100() FinSequence-like Element of the carrier of (TOP-REAL 2)
(i * ((len i),1)) `1 is V14() real ext-real Element of REAL
{ |[b<sub>1</sub>,b<sub>2</sub>]| where b<sub>1</sub>, b<sub>2</sub> is V14() real ext-real Element of REAL : (i * ((len i),1)) `1 <= b₁ } is set
width i is natural V14() real ext-real V108() V109() V110() V111() V112() V113() V114() V115() Element of NAT
i is natural V14() real ext-real V108() V109() V110() V111() V112() V113() V114() V115() Element of NAT
i + 1 is natural V14() real ext-real V108() V109() V110() V111() V112() V113() V114() V115() Element of NAT
j is V19() V21() V22( NAT ) V23(K295( the carrier of (TOP-REAL 2))) V24() FinSequence-like tabular FinSequence of K295( the carrier of (TOP-REAL 2))
len j is natural V14() real ext-real V108() V109() V110() V111() V112() V113() V114() V115() Element of NAT
v_strip (j,i) is Element of bool the carrier of (TOP-REAL 2)
j * (i,1) is V43(2) V100() FinSequence-like Element of the carrier of (TOP-REAL 2)
(j * (i,1)) `1 is V14() real ext-real Element of REAL
j * ((i + 1),1) is V43(2) V100() FinSequence-like Element of the carrier of (TOP-REAL 2)
(j * ((i + 1),1)) `1 is V14() real ext-real Element of REAL
{ |[b₁,b₂]| where b₁, b₂ is V14() real ext-real Element of REAL : ( (j * (i,1)) `1 <= b<sub>1</sub> & b<sub>1</sub> <= (j * ((i + 1),1)) `1 ) } is set
width j is natural V14() real ext-real V108() V109() V110() V111() V112() V113() V114() V115() Element of NAT
i is V19() V21() V22( NAT ) V23(K295( the carrier of (TOP-REAL 2))) V24() FinSequence-like tabular FinSequence of K295( the carrier of (TOP-REAL 2))
h_strip (i,0) is Element of bool the carrier of (TOP-REAL 2)
i * (1,1) is V43(2) V100() FinSequence-like Element of the carrier of (TOP-REAL 2)
(i * (1,1)) `2 is V14() real ext-real Element of REAL
{ |[b<sub>1</sub>,b<sub>2</sub>]| where b<sub>1</sub>, b<sub>2</sub> is V14() real ext-real Element of REAL : b<sub>2</sub> <= (i * (1,1)) `2 } is set
len i is natural V14() real ext-real V108() V109() V110() V111() V112() V113() V114() V115() Element of NAT
i is V19() V21() V22( NAT ) V23(K295( the carrier of (TOP-REAL 2))) V24() FinSequence-like tabular FinSequence of K295( the carrier of (TOP-REAL 2))
width i is natural V14() real ext-real V108() V109() V110() V111() V112() V113() V114() V115() Element of NAT
h_strip (i,(width i)) is Element of bool the carrier of (TOP-REAL 2)
i * (1,(width i)) is V43(2) V100() FinSequence-like Element of the carrier of (TOP-REAL 2)
(i * (1,(width i))) `2 is V14() real ext-real Element of REAL
{ |[b<sub>1</sub>,b<sub>2</sub>]| where b<sub>1</sub>, b<sub>2</sub> is V14() real ext-real Element of REAL : (i * (1,(width i))) `2 <= b₂ } is set
len i is natural V14() real ext-real V108() V109() V110() V111() V112() V113() V114() V115() Element of NAT
i is natural V14() real ext-real V108() V109() V110() V111() V112() V113() V114() V115() Element of NAT
i + 1 is natural V14() real ext-real V108() V109() V110() V111() V112() V113() V114() V115() Element of NAT
j is V19() V21() V22( NAT ) V23(K295( the carrier of (TOP-REAL 2))) V24() FinSequence-like tabular FinSequence of K295( the carrier of (TOP-REAL 2))
width j is natural V14() real ext-real V108() V109() V110() V111() V112() V113() V114() V115() Element of NAT
h_strip (j,i) is Element of bool the carrier of (TOP-REAL 2)
j * (1,i) is V43(2) V100() FinSequence-like Element of the carrier of (TOP-REAL 2)
(j * (1,i)) `2 is V14() real ext-real Element of REAL
j * (1,(i + 1)) is V43(2) V100() FinSequence-like Element of the carrier of (TOP-REAL 2)
(j * (1,(i + 1))) `2 is V14() real ext-real Element of REAL
{ |[b₁,b₂]| where b₁, b₂ is V14() real ext-real Element of REAL : ( (j * (1,i)) `2 <= b<sub>2</sub> & b<sub>2</sub> <= (j * (1,(i + 1))) `2 ) } is set
len j is natural V14() real ext-real V108() V109() V110() V111() V112() V113() V114() V115() Element of NAT
i is V19() V21() V22( NAT ) V23(K295( the carrier of (TOP-REAL 2))) V24() FinSequence-like tabular X_equal-in-line Y_equal-in-column FinSequence of K295( the carrier of (TOP-REAL 2))
cell (i,0,0) is Element of bool the carrier of (TOP-REAL 2)
i * (1,1) is V43(2) V100() FinSequence-like Element of the carrier of (TOP-REAL 2)
(i * (1,1)) `1 is V14() real ext-real Element of REAL
(i * (1,1)) `2 is V14() real ext-real Element of REAL
{ |[b₁,b₂]| where b₁, b₂ is V14() real ext-real Element of REAL : ( b₁ <= (i * (1,1)) `1 & b<sub>2</sub> <= (i * (1,1)) `2 ) } is set
v_strip (i,0) is Element of bool the carrier of (TOP-REAL 2)
h_strip (i,0) is Element of bool the carrier of (TOP-REAL 2)
(v_strip (i,0)) /\ (h_strip (i,0)) is Element of bool the carrier of (TOP-REAL 2)
{ |[b₁,b₂]| where b₁, b₂ is V14() real ext-real Element of REAL : b₂ <= (i * (1,1)) `2 } is set
{ |[b<sub>1</sub>,b<sub>2</sub>]| where b<sub>1</sub>, b<sub>2</sub> is V14() real ext-real Element of REAL : b<sub>1</sub> <= (i * (1,1)) `1 } is set
j is set
G is V14() real ext-real Element of REAL
Y is V14() real ext-real Element of REAL
|[G,Y]| is V43(2) V100() FinSequence-like Element of the carrier of (TOP-REAL 2)
x is V14() real ext-real Element of REAL
p is V14() real ext-real Element of REAL
|[x,p]| is V43(2) V100() FinSequence-like Element of the carrier of (TOP-REAL 2)
j is set
G is V14() real ext-real Element of REAL
Y is V14() real ext-real Element of REAL
|[G,Y]| is V43(2) V100() FinSequence-like Element of the carrier of (TOP-REAL 2)
G is V14() real ext-real Element of REAL
Y is V14() real ext-real Element of REAL
|[G,Y]| is V43(2) V100() FinSequence-like Element of the carrier of (TOP-REAL 2)
i is V19() V21() V22( NAT ) V23(K295( the carrier of (TOP-REAL 2))) V24() FinSequence-like tabular X_equal-in-line Y_equal-in-column FinSequence of K295( the carrier of (TOP-REAL 2))
width i is natural V14() real ext-real V108() V109() V110() V111() V112() V113() V114() V115() Element of NAT
cell (i,0,(width i)) is Element of bool the carrier of (TOP-REAL 2)
i * (1,1) is V43(2) V100() FinSequence-like Element of the carrier of (TOP-REAL 2)
(i * (1,1)) `1 is V14() real ext-real Element of REAL
i * (1,(width i)) is V43(2) V100() FinSequence-like Element of the carrier of (TOP-REAL 2)
(i * (1,(width i))) `2 is V14() real ext-real Element of REAL
{ |[b₁,b₂]| where b₁, b₂ is V14() real ext-real Element of REAL : ( b₁ <= (i * (1,1)) `1 & (i * (1,(width i))) `2 <= b₂ ) } is set
v_strip (i,0) is Element of bool the carrier of (TOP-REAL 2)
h_strip (i,(width i)) is Element of bool the carrier of (TOP-REAL 2)
(v_strip (i,0)) /\ (h_strip (i,(width i))) is Element of bool the carrier of (TOP-REAL 2)
{ |[b₁,b₂]| where b₁, b₂ is V14() real ext-real Element of REAL : (i * (1,(width i))) `2 <= b<sub>2</sub> } is set
{ |[b<sub>1</sub>,b<sub>2</sub>]| where b<sub>1</sub>, b<sub>2</sub> is V14() real ext-real Element of REAL : b<sub>1</sub> <= (i * (1,1)) `1 } is set
j is set
G is V14() real ext-real Element of REAL
Y is V14() real ext-real Element of REAL
|[G,Y]| is V43(2) V100() FinSequence-like Element of the carrier of (TOP-REAL 2)
x is V14() real ext-real Element of REAL
p is V14() real ext-real Element of REAL
|[x,p]| is V43(2) V100() FinSequence-like Element of the carrier of (TOP-REAL 2)
j is set
G is V14() real ext-real Element of REAL
Y is V14() real ext-real Element of REAL
|[G,Y]| is V43(2) V100() FinSequence-like Element of the carrier of (TOP-REAL 2)
G is V14() real ext-real Element of REAL
Y is V14() real ext-real Element of REAL
|[G,Y]| is V43(2) V100() FinSequence-like Element of the carrier of (TOP-REAL 2)
i is natural V14() real ext-real V108() V109() V110() V111() V112() V113() V114() V115() Element of NAT
i + 1 is natural V14() real ext-real V108() V109() V110() V111() V112() V113() V114() V115() Element of NAT
j is V19() V21() V22( NAT ) V23(K295( the carrier of (TOP-REAL 2))) V24() FinSequence-like tabular X_equal-in-line Y_equal-in-column FinSequence of K295( the carrier of (TOP-REAL 2))
width j is natural V14() real ext-real V108() V109() V110() V111() V112() V113() V114() V115() Element of NAT
cell (j,0,i) is Element of bool the carrier of (TOP-REAL 2)
j * (1,1) is V43(2) V100() FinSequence-like Element of the carrier of (TOP-REAL 2)
(j * (1,1)) `1 is V14() real ext-real Element of REAL
j * (1,i) is V43(2) V100() FinSequence-like Element of the carrier of (TOP-REAL 2)
(j * (1,i)) `2 is V14() real ext-real Element of REAL
j * (1,(i + 1)) is V43(2) V100() FinSequence-like Element of the carrier of (TOP-REAL 2)
(j * (1,(i + 1))) `2 is V14() real ext-real Element of REAL
{ |[b<sub>1</sub>,b<sub>2</sub>]| where b<sub>1</sub>, b<sub>2</sub> is V14() real ext-real Element of REAL : ( b<sub>1</sub> <= (j * (1,1)) `1 & (j * (1,i)) `2 <= b<sub>2</sub> & b<sub>2</sub> <= (j * (1,(i + 1))) `2 ) } is set
v_strip (j,0) is Element of bool the carrier of (TOP-REAL 2)
h_strip (j,i) is Element of bool the carrier of (TOP-REAL 2)
(v_strip (j,0)) /\ (h_strip (j,i)) is Element of bool the carrier of (TOP-REAL 2)
{ |[b₁,b₂]| where b₁, b₂ is V14() real ext-real Element of REAL : ( (j * (1,i)) `2 <= b<sub>2</sub> & b<sub>2</sub> <= (j * (1,(i + 1))) `2 ) } is set
{ |[b₁,b₂]| where b₁, b₂ is V14() real ext-real Element of REAL : b₁ <= (j * (1,1)) `1 } is set
G is set
Y is V14() real ext-real Element of REAL
x is V14() real ext-real Element of REAL
|[Y,x]| is V43(2) V100() FinSequence-like Element of the carrier of (TOP-REAL 2)
p is V14() real ext-real Element of REAL
G0 is V14() real ext-real Element of REAL
|[p,G0]| is V43(2) V100() FinSequence-like Element of the carrier of (TOP-REAL 2)
G is set
Y is V14() real ext-real Element of REAL
x is V14() real ext-real Element of REAL
|[Y,x]| is V43(2) V100() FinSequence-like Element of the carrier of (TOP-REAL 2)
Y is V14() real ext-real Element of REAL
x is V14() real ext-real Element of REAL
|[Y,x]| is V43(2) V100() FinSequence-like Element of the carrier of (TOP-REAL 2)
i is V19() V21() V22( NAT ) V23(K295( the carrier of (TOP-REAL 2))) V24() FinSequence-like tabular X_equal-in-line Y_equal-in-column FinSequence of K295( the carrier of (TOP-REAL 2))
len i is natural V14() real ext-real V108() V109() V110() V111() V112() V113() V114() V115() Element of NAT
cell (i,(len i),0) is Element of bool the carrier of (TOP-REAL 2)
i * ((len i),1) is V43(2) V100() FinSequence-like Element of the carrier of (TOP-REAL 2)
(i * ((len i),1)) `1 is V14() real ext-real Element of REAL
i * (1,1) is V43(2) V100() FinSequence-like Element of the carrier of (TOP-REAL 2)
(i * (1,1)) `2 is V14() real ext-real Element of REAL
{ |[b<sub>1</sub>,b<sub>2</sub>]| where b<sub>1</sub>, b<sub>2</sub> is V14() real ext-real Element of REAL : ( (i * ((len i),1)) `1 <= b₁ & b₂ <= (i * (1,1)) `2 ) } is set
v_strip (i,(len i)) is Element of bool the carrier of (TOP-REAL 2)
h_strip (i,0) is Element of bool the carrier of (TOP-REAL 2)
(v_strip (i,(len i))) /\ (h_strip (i,0)) is Element of bool the carrier of (TOP-REAL 2)
{ |[b<sub>1</sub>,b<sub>2</sub>]| where b<sub>1</sub>, b<sub>2</sub> is V14() real ext-real Element of REAL : b<sub>2</sub> <= (i * (1,1)) `2 } is set
{ |[b₁,b₂]| where b₁, b₂ is V14() real ext-real Element of REAL : (i * ((len i),1)) `1 <= b<sub>1</sub> } is set
j is set
G is V14() real ext-real Element of REAL
Y is V14() real ext-real Element of REAL
|[G,Y]| is V43(2) V100() FinSequence-like Element of the carrier of (TOP-REAL 2)
x is V14() real ext-real Element of REAL
p is V14() real ext-real Element of REAL
|[x,p]| is V43(2) V100() FinSequence-like Element of the carrier of (TOP-REAL 2)
j is set
G is V14() real ext-real Element of REAL
Y is V14() real ext-real Element of REAL
|[G,Y]| is V43(2) V100() FinSequence-like Element of the carrier of (TOP-REAL 2)
G is V14() real ext-real Element of REAL
Y is V14() real ext-real Element of REAL
|[G,Y]| is V43(2) V100() FinSequence-like Element of the carrier of (TOP-REAL 2)
i is V19() V21() V22( NAT ) V23(K295( the carrier of (TOP-REAL 2))) V24() FinSequence-like tabular X_equal-in-line Y_equal-in-column FinSequence of K295( the carrier of (TOP-REAL 2))
len i is natural V14() real ext-real V108() V109() V110() V111() V112() V113() V114() V115() Element of NAT
width i is natural V14() real ext-real V108() V109() V110() V111() V112() V113() V114() V115() Element of NAT
cell (i,(len i),(width i)) is Element of bool the carrier of (TOP-REAL 2)
i * ((len i),1) is V43(2) V100() FinSequence-like Element of the carrier of (TOP-REAL 2)
(i * ((len i),1)) `1 is V14() real ext-real Element of REAL
i * (1,(width i)) is V43(2) V100() FinSequence-like Element of the carrier of (TOP-REAL 2)
(i * (1,(width i))) `2 is V14() real ext-real Element of REAL
{ |[b<sub>1</sub>,b<sub>2</sub>]| where b<sub>1</sub>, b<sub>2</sub> is V14() real ext-real Element of REAL : ( (i * ((len i),1)) `1 <= b₁ & (i * (1,(width i))) `2 <= b<sub>2</sub> ) } is set
v_strip (i,(len i)) is Element of bool the carrier of (TOP-REAL 2)
h_strip (i,(width i)) is Element of bool the carrier of (TOP-REAL 2)
(v_strip (i,(len i))) /\ (h_strip (i,(width i))) is Element of bool the carrier of (TOP-REAL 2)
{ |[b<sub>1</sub>,b<sub>2</sub>]| where b<sub>1</sub>, b<sub>2</sub> is V14() real ext-real Element of REAL : (i * (1,(width i))) `2 <= b₂ } is set
{ |[b₁,b₂]| where b₁, b₂ is V14() real ext-real Element of REAL : (i * ((len i),1)) `1 <= b<sub>1</sub> } is set
j is set
G is V14() real ext-real Element of REAL
Y is V14() real ext-real Element of REAL
|[G,Y]| is V43(2) V100() FinSequence-like Element of the carrier of (TOP-REAL 2)
x is V14() real ext-real Element of REAL
p is V14() real ext-real Element of REAL
|[x,p]| is V43(2) V100() FinSequence-like Element of the carrier of (TOP-REAL 2)
j is set
G is V14() real ext-real Element of REAL
Y is V14() real ext-real Element of REAL
|[G,Y]| is V43(2) V100() FinSequence-like Element of the carrier of (TOP-REAL 2)
G is V14() real ext-real Element of REAL
Y is V14() real ext-real Element of REAL
|[G,Y]| is V43(2) V100() FinSequence-like Element of the carrier of (TOP-REAL 2)
i is natural V14() real ext-real V108() V109() V110() V111() V112() V113() V114() V115() Element of NAT
i + 1 is natural V14() real ext-real V108() V109() V110() V111() V112() V113() V114() V115() Element of NAT
j is V19() V21() V22( NAT ) V23(K295( the carrier of (TOP-REAL 2))) V24() FinSequence-like tabular X_equal-in-line Y_equal-in-column FinSequence of K295( the carrier of (TOP-REAL 2))
width j is natural V14() real ext-real V108() V109() V110() V111() V112() V113() V114() V115() Element of NAT
len j is natural V14() real ext-real V108() V109() V110() V111() V112() V113() V114() V115() Element of NAT
cell (j,(len j),i) is Element of bool the carrier of (TOP-REAL 2)
j * ((len j),1) is V43(2) V100() FinSequence-like Element of the carrier of (TOP-REAL 2)
(j * ((len j),1)) `1 is V14() real ext-real Element of REAL
j * (1,i) is V43(2) V100() FinSequence-like Element of the carrier of (TOP-REAL 2)
(j * (1,i)) `2 is V14() real ext-real Element of REAL
j * (1,(i + 1)) is V43(2) V100() FinSequence-like Element of the carrier of (TOP-REAL 2)
(j * (1,(i + 1))) `2 is V14() real ext-real Element of REAL
{ |[b₁,b₂]| where b₁, b₂ is V14() real ext-real Element of REAL : ( (j * ((len j),1)) `1 <= b<sub>1</sub> & (j * (1,i)) `2 <= b₂ & b₂ <= (j * (1,(i + 1))) `2 ) } is set
v_strip (j,(len j)) is Element of bool the carrier of (TOP-REAL 2)
h_strip (j,i) is Element of bool the carrier of (TOP-REAL 2)
(v_strip (j,(len j))) /\ (h_strip (j,i)) is Element of bool the carrier of (TOP-REAL 2)
{ |[b<sub>1</sub>,b<sub>2</sub>]| where b<sub>1</sub>, b<sub>2</sub> is V14() real ext-real Element of REAL : ( (j * (1,i)) `2 <= b₂ & b₂ <= (j * (1,(i + 1))) `2 ) } is set
{ |[b<sub>1</sub>,b<sub>2</sub>]| where b<sub>1</sub>, b<sub>2</sub> is V14() real ext-real Element of REAL : (j * ((len j),1)) `1 <= b₁ } is set
G is set
Y is V14() real ext-real Element of REAL
x is V14() real ext-real Element of REAL
|[Y,x]| is V43(2) V100() FinSequence-like Element of the carrier of (TOP-REAL 2)
p is V14() real ext-real Element of REAL
G0 is V14() real ext-real Element of REAL
|[p,G0]| is V43(2) V100() FinSequence-like Element of the carrier of (TOP-REAL 2)
G is set
Y is V14() real ext-real Element of REAL
x is V14() real ext-real Element of REAL
|[Y,x]| is V43(2) V100() FinSequence-like Element of the carrier of (TOP-REAL 2)
Y is V14() real ext-real Element of REAL
x is V14() real ext-real Element of REAL
|[Y,x]| is V43(2) V100() FinSequence-like Element of the carrier of (TOP-REAL 2)
i is natural V14() real ext-real V108() V109() V110() V111() V112() V113() V114() V115() Element of NAT
i + 1 is natural V14() real ext-real V108() V109() V110() V111() V112() V113() V114() V115() Element of NAT
j is V19() V21() V22( NAT ) V23(K295( the carrier of (TOP-REAL 2))) V24() FinSequence-like tabular X_equal-in-line Y_equal-in-column FinSequence of K295( the carrier of (TOP-REAL 2))
len j is natural V14() real ext-real V108() V109() V110() V111() V112() V113() V114() V115() Element of NAT
cell (j,i,0) is Element of bool the carrier of (TOP-REAL 2)
j * (i,1) is V43(2) V100() FinSequence-like Element of the carrier of (TOP-REAL 2)
(j * (i,1)) `1 is V14() real ext-real Element of REAL
j * ((i + 1),1) is V43(2) V100() FinSequence-like Element of the carrier of (TOP-REAL 2)
(j * ((i + 1),1)) `1 is V14() real ext-real Element of REAL
j * (1,1) is V43(2) V100() FinSequence-like Element of the carrier of (TOP-REAL 2)
(j * (1,1)) `2 is V14() real ext-real Element of REAL
{ |[b<sub>1</sub>,b<sub>2</sub>]| where b<sub>1</sub>, b<sub>2</sub> is V14() real ext-real Element of REAL : ( (j * (i,1)) `1 <= b₁ & b₁ <= (j * ((i + 1),1)) `1 & b<sub>2</sub> <= (j * (1,1)) `2 ) } is set
v_strip (j,i) is Element of bool the carrier of (TOP-REAL 2)
h_strip (j,0) is Element of bool the carrier of (TOP-REAL 2)
(v_strip (j,i)) /\ (h_strip (j,0)) is Element of bool the carrier of (TOP-REAL 2)
{ |[b₁,b₂]| where b₁, b₂ is V14() real ext-real Element of REAL : ( (j * (i,1)) `1 <= b<sub>1</sub> & b<sub>1</sub> <= (j * ((i + 1),1)) `1 ) } is set
{ |[b₁,b₂]| where b₁, b₂ is V14() real ext-real Element of REAL : b₂ <= (j * (1,1)) `2 } is set
G is set
Y is V14() real ext-real Element of REAL
x is V14() real ext-real Element of REAL
|[Y,x]| is V43(2) V100() FinSequence-like Element of the carrier of (TOP-REAL 2)
p is V14() real ext-real Element of REAL
G0 is V14() real ext-real Element of REAL
|[p,G0]| is V43(2) V100() FinSequence-like Element of the carrier of (TOP-REAL 2)
G is set
Y is V14() real ext-real Element of REAL
x is V14() real ext-real Element of REAL
|[Y,x]| is V43(2) V100() FinSequence-like Element of the carrier of (TOP-REAL 2)
Y is V14() real ext-real Element of REAL
x is V14() real ext-real Element of REAL
|[Y,x]| is V43(2) V100() FinSequence-like Element of the carrier of (TOP-REAL 2)
i is natural V14() real ext-real V108() V109() V110() V111() V112() V113() V114() V115() Element of NAT
i + 1 is natural V14() real ext-real V108() V109() V110() V111() V112() V113() V114() V115() Element of NAT
j is V19() V21() V22( NAT ) V23(K295( the carrier of (TOP-REAL 2))) V24() FinSequence-like tabular X_equal-in-line Y_equal-in-column FinSequence of K295( the carrier of (TOP-REAL 2))
len j is natural V14() real ext-real V108() V109() V110() V111() V112() V113() V114() V115() Element of NAT
width j is natural V14() real ext-real V108() V109() V110() V111() V112() V113() V114() V115() Element of NAT
cell (j,i,(width j)) is Element of bool the carrier of (TOP-REAL 2)
j * (i,1) is V43(2) V100() FinSequence-like Element of the carrier of (TOP-REAL 2)
(j * (i,1)) `1 is V14() real ext-real Element of REAL
j * ((i + 1),1) is V43(2) V100() FinSequence-like Element of the carrier of (TOP-REAL 2)
(j * ((i + 1),1)) `1 is V14() real ext-real Element of REAL
j * (1,(width j)) is V43(2) V100() FinSequence-like Element of the carrier of (TOP-REAL 2)
(j * (1,(width j))) `2 is V14() real ext-real Element of REAL
{ |[b₁,b₂]| where b₁, b₂ is V14() real ext-real Element of REAL : ( (j * (i,1)) `1 <= b<sub>1</sub> & b<sub>1</sub> <= (j * ((i + 1),1)) `1 & (j * (1,(width j))) `2 <= b<sub>2</sub> ) } is set
v_strip (j,i) is Element of bool the carrier of (TOP-REAL 2)
h_strip (j,(width j)) is Element of bool the carrier of (TOP-REAL 2)
(v_strip (j,i)) /\ (h_strip (j,(width j))) is Element of bool the carrier of (TOP-REAL 2)
{ |[b<sub>1</sub>,b<sub>2</sub>]| where b<sub>1</sub>, b<sub>2</sub> is V14() real ext-real Element of REAL : ( (j * (i,1)) `1 <= b₁ & b₁ <= (j * ((i + 1),1)) `1 ) } is set
{ |[b<sub>1</sub>,b<sub>2</sub>]| where b<sub>1</sub>, b<sub>2</sub> is V14() real ext-real Element of REAL : (j * (1,(width j))) `2 <= b₂ } is set
G is set
Y is V14() real ext-real Element of REAL
x is V14() real ext-real Element of REAL
|[Y,x]| is V43(2) V100() FinSequence-like Element of the carrier of (TOP-REAL 2)
p is V14() real ext-real Element of REAL
G0 is V14() real ext-real Element of REAL
|[p,G0]| is V43(2) V100() FinSequence-like Element of the carrier of (TOP-REAL 2)
G is set
Y is V14() real ext-real Element of REAL
x is V14() real ext-real Element of REAL
|[Y,x]| is V43(2) V100() FinSequence-like Element of the carrier of (TOP-REAL 2)
Y is V14() real ext-real Element of REAL
x is V14() real ext-real Element of REAL
|[Y,x]| is V43(2) V100() FinSequence-like Element of the carrier of (TOP-REAL 2)
i is natural V14() real ext-real V108() V109() V110() V111() V112() V113() V114() V115() Element of NAT
i + 1 is natural V14() real ext-real V108() V109() V110() V111() V112() V113() V114() V115() Element of NAT
j is natural V14() real ext-real V108() V109() V110() V111() V112() V113() V114() V115() Element of NAT
j + 1 is natural V14() real ext-real V108() V109() V110() V111() V112() V113() V114() V115() Element of NAT
G is V19() V21() V22( NAT ) V23(K295( the carrier of (TOP-REAL 2))) V24() FinSequence-like tabular X_equal-in-line Y_equal-in-column FinSequence of K295( the carrier of (TOP-REAL 2))
len G is natural V14() real ext-real V108() V109() V110() V111() V112() V113() V114() V115() Element of NAT
width G is natural V14() real ext-real V108() V109() V110() V111() V112() V113() V114() V115() Element of NAT
cell (G,i,j) is Element of bool the carrier of (TOP-REAL 2)
G * (i,1) is V43(2) V100() FinSequence-like Element of the carrier of (TOP-REAL 2)
(G * (i,1)) `1 is V14() real ext-real Element of REAL
G * ((i + 1),1) is V43(2) V100() FinSequence-like Element of the carrier of (TOP-REAL 2)
(G * ((i + 1),1)) `1 is V14() real ext-real Element of REAL
G * (1,j) is V43(2) V100() FinSequence-like Element of the carrier of (TOP-REAL 2)
(G * (1,j)) `2 is V14() real ext-real Element of REAL
G * (1,(j + 1)) is V43(2) V100() FinSequence-like Element of the carrier of (TOP-REAL 2)
(G * (1,(j + 1))) `2 is V14() real ext-real Element of REAL
{ |[b₁,b₂]| where b₁, b₂ is V14() real ext-real Element of REAL : ( (G * (i,1)) `1 <= b<sub>1</sub> & b<sub>1</sub> <= (G * ((i + 1),1)) `1 & (G * (1,j)) `2 <= b<sub>2</sub> & b<sub>2</sub> <= (G * (1,(j + 1))) `2 ) } is set
h_strip (G,j) is Element of bool the carrier of (TOP-REAL 2)
{ |[b₁,b₂]| where b₁, b₂ is V14() real ext-real Element of REAL : ( (G * (1,j)) `2 <= b<sub>2</sub> & b<sub>2</sub> <= (G * (1,(j + 1))) `2 ) } is set
v_strip (G,i) is Element of bool the carrier of (TOP-REAL 2)
(v_strip (G,i)) /\ (h_strip (G,j)) is Element of bool the carrier of (TOP-REAL 2)
{ |[b₁,b₂]| where b₁, b₂ is V14() real ext-real Element of REAL : ( (G * (i,1)) `1 <= b<sub>1</sub> & b<sub>1</sub> <= (G * ((i + 1),1)) `1 ) } is set
Y is set
x is V14() real ext-real Element of REAL
p is V14() real ext-real Element of REAL
|[x,p]| is V43(2) V100() FinSequence-like Element of the carrier of (TOP-REAL 2)
G0 is V14() real ext-real Element of REAL
u is V14() real ext-real Element of REAL
|[G0,u]| is V43(2) V100() FinSequence-like Element of the carrier of (TOP-REAL 2)
Y is set
x is V14() real ext-real Element of REAL
p is V14() real ext-real Element of REAL
|[x,p]| is V43(2) V100() FinSequence-like Element of the carrier of (TOP-REAL 2)
x is V14() real ext-real Element of REAL
p is V14() real ext-real Element of REAL
|[x,p]| is V43(2) V100() FinSequence-like Element of the carrier of (TOP-REAL 2)
i is natural V14() real ext-real V108() V109() V110() V111() V112() V113() V114() V115() Element of NAT
j is natural V14() real ext-real V108() V109() V110() V111() V112() V113() V114() V115() Element of NAT
G is V19() V22( NAT ) V23(K295( the carrier of (TOP-REAL 2))) V24() FinSequence-like tabular FinSequence of K295( the carrier of (TOP-REAL 2))
cell (G,i,j) is Element of bool the carrier of (TOP-REAL 2)
v_strip (G,i) is Element of bool the carrier of (TOP-REAL 2)
h_strip (G,j) is Element of bool the carrier of (TOP-REAL 2)
(h_strip (G,j)) /\ (v_strip (G,i)) is Element of bool the carrier of (TOP-REAL 2)
i is V19() V21() V22( NAT ) V23(K295( the carrier of (TOP-REAL 2))) V24() FinSequence-like tabular FinSequence of K295( the carrier of (TOP-REAL 2))
len i is natural V14() real ext-real V108() V109() V110() V111() V112() V113() V114() V115() Element of NAT
width i is natural V14() real ext-real V108() V109() V110() V111() V112() V113() V114() V115() Element of NAT
i is natural V14() real ext-real V108() V109() V110() V111() V112() V113() V114() V115() Element of NAT
j is natural V14() real ext-real V108() V109() V110() V111() V112() V113() V114() V115() Element of NAT
G is V19() V21() V22( NAT ) V23(K295( the carrier of (TOP-REAL 2))) V24() FinSequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of K295( the carrier of (TOP-REAL 2))
len G is natural V14() real ext-real V108() V109() V110() V111() V112() V113() V114() V115() Element of NAT
width G is natural V14() real ext-real V108() V109() V110() V111() V112() V113() V114() V115() Element of NAT
cell (G,i,j) is Element of bool the carrier of (TOP-REAL 2)
Int (cell (G,i,j)) is Element of bool the carrier of (TOP-REAL 2)
Cl (Int (cell (G,i,j))) is Element of bool the carrier of (TOP-REAL 2)
x is set
p is V43(2) V100() FinSequence-like Element of the carrier of (TOP-REAL 2)
G0 is Element of bool the carrier of (TOP-REAL 2)
0 + 1 is non empty natural V14() real ext-real positive non negative V108() V109() V110() V111() V112() V113() V114() V115() Element of NAT
u is Element of the carrier of (Euclid 2)
TopSpaceMetr (Euclid 2) is TopStruct
the topology of (TOP-REAL 2) is non empty Element of bool (bool the carrier of (TOP-REAL 2))
bool (bool the carrier of (TOP-REAL 2)) is non empty set
TopStruct(# the carrier of (TOP-REAL 2), the topology of (TOP-REAL 2) #) is non empty strict TopSpace-like TopStruct
the carrier of (TopSpaceMetr (Euclid 2)) is set
bool the carrier of (TopSpaceMetr (Euclid 2)) is non empty set
G00 is Element of bool the carrier of (TopSpaceMetr (Euclid 2))
r is V14() real ext-real set
Ball (u,r) is Element of bool the carrier of (Euclid 2)
bool the carrier of (Euclid 2) is non empty set
G * (1,1) is V43(2) V100() FinSequence-like Element of the carrier of (TOP-REAL 2)
(G * (1,1)) `1 is V14() real ext-real Element of REAL
(G * (1,1)) `2 is V14() real ext-real Element of REAL
{ |[b₁,b₂]| where b₁, b₂ is V14() real ext-real Element of REAL : ( b₁ <= (G * (1,1)) `1 & b<sub>2</sub> <= (G * (1,1)) `2 ) } is set
r2 is V14() real ext-real Element of REAL
s2 is V14() real ext-real Element of REAL
|[r2,s2]| is V43(2) V100() FinSequence-like Element of the carrier of (TOP-REAL 2)
r is V14() real ext-real Element of REAL
r / 2 is V14() real ext-real Element of REAL
r2 - (r / 2) is V14() real ext-real Element of REAL
s2 - (r / 2) is V14() real ext-real Element of REAL
2 " is non empty V14() real ext-real positive non negative Element of REAL
r * (2 ") is V14() real ext-real Element of REAL
(s2 - (r / 2)) + (r / 2) is V14() real ext-real Element of REAL
|[(r2 - (r / 2)),(s2 - (r / 2))]| is V43(2) V100() FinSequence-like Element of the carrier of (TOP-REAL 2)
rm is V43(2) V100() FinSequence-like Element of the carrier of (TOP-REAL 2)
(r2 - (r / 2)) + (r / 2) is V14() real ext-real Element of REAL
rm1 is Element of the carrier of (Euclid 2)
{ |[b₁,b₂]| where b₁, b₂ is V14() real ext-real Element of REAL : ( not (G * (1,1)) `1 <= b<sub>1</sub> & not (G * (1,1)) `2 <= b₂ ) } is set
rm `1 is V14() real ext-real Element of REAL
rm `2 is V14() real ext-real Element of REAL
(sqrt 2) / 2 is V14() real ext-real Element of REAL
r * 1 is V14() real ext-real Element of REAL
r * ((sqrt 2) / 2) is V14() real ext-real Element of REAL
(r / 2) ^2 is V14() real ext-real Element of REAL
K46((r / 2),(r / 2)) is V14() real ext-real set
((r / 2) ^2) + ((r / 2) ^2) is V14() real ext-real Element of REAL
2 * ((r / 2) ^2) is V14() real ext-real Element of REAL
(sqrt 2) ^2 is V14() real ext-real Element of REAL
K46((sqrt 2),(sqrt 2)) is V14() real ext-real set
((sqrt 2) ^2) * ((r / 2) ^2) is V14() real ext-real Element of REAL
(r / 2) * (sqrt 2) is V14() real ext-real Element of REAL
((r / 2) * (sqrt 2)) ^2 is V14() real ext-real Element of REAL
K46(((r / 2) * (sqrt 2)),((r / 2) * (sqrt 2))) is V14() real ext-real set
sqrt (((r / 2) ^2) + ((r / 2) ^2)) is V14() real ext-real Element of REAL
r2 - (r2 - (r / 2)) is V14() real ext-real Element of REAL
s2 - (s2 - (r / 2)) is V14() real ext-real Element of REAL
p `1 is V14() real ext-real Element of REAL
p `2 is V14() real ext-real Element of REAL
dist (u,rm1) is V14() real ext-real Element of REAL
v is V43(2) Element of REAL 2
r3 is V43(2) Element of REAL 2
(Pitag_dist 2) . (v,r3) is V14() real ext-real Element of REAL
Ball (u,r) is Element of bool the carrier of (Euclid 2)
(Int (cell (G,i,j))) /\ G0 is Element of bool the carrier of (TOP-REAL 2)
{} (TOP-REAL 2) is empty proper closed V110() V111() V112() V113() V114() V115() V116() symmetric circled Element of bool the carrier of (TOP-REAL 2)
G * (1,1) is V43(2) V100() FinSequence-like Element of the carrier of (TOP-REAL 2)
(G * (1,1)) `1 is V14() real ext-real Element of REAL
G * (1,(width G)) is V43(2) V100() FinSequence-like Element of the carrier of (TOP-REAL 2)
(G * (1,(width G))) `2 is V14() real ext-real Element of REAL
{ |[b₁,b₂]| where b₁, b₂ is V14() real ext-real Element of REAL : ( b₁ <= (G * (1,1)) `1 & (G * (1,(width G))) `2 <= b₂ ) } is set
r2 is V14() real ext-real Element of REAL
s2 is V14() real ext-real Element of REAL
|[r2,s2]| is V43(2) V100() FinSequence-like Element of the carrier of (TOP-REAL 2)
r is V14() real ext-real Element of REAL
r / 2 is V14() real ext-real Element of REAL
r2 - (r / 2) is V14() real ext-real Element of REAL
s2 + (r / 2) is V14() real ext-real Element of REAL
2 " is non empty V14() real ext-real positive non negative Element of REAL
r * (2 ") is V14() real ext-real Element of REAL
|[(r2 - (r / 2)),(s2 + (r / 2))]| is V43(2) V100() FinSequence-like Element of the carrier of (TOP-REAL 2)
rm is V43(2) V100() FinSequence-like Element of the carrier of (TOP-REAL 2)
(r2 - (r / 2)) + (r / 2) is V14() real ext-real Element of REAL
rm1 is Element of the carrier of (Euclid 2)
{ |[b₁,b₂]| where b₁, b₂ is V14() real ext-real Element of REAL : ( not (G * (1,1)) `1 <= b<sub>1</sub> & not b<sub>2</sub> <= (G * (1,(width G))) `2 ) } is set
rm `1 is V14() real ext-real Element of REAL
rm `2 is V14() real ext-real Element of REAL
(sqrt 2) / 2 is V14() real ext-real Element of REAL
r * 1 is V14() real ext-real Element of REAL
r * ((sqrt 2) / 2) is V14() real ext-real Element of REAL
(r / 2) ^2 is V14() real ext-real Element of REAL
K46((r / 2),(r / 2)) is V14() real ext-real set
((r / 2) ^2) + ((r / 2) ^2) is V14() real ext-real Element of REAL
2 * ((r / 2) ^2) is V14() real ext-real Element of REAL
(sqrt 2) ^2 is V14() real ext-real Element of REAL
K46((sqrt 2),(sqrt 2)) is V14() real ext-real set
((sqrt 2) ^2) * ((r / 2) ^2) is V14() real ext-real Element of REAL
(r / 2) * (sqrt 2) is V14() real ext-real Element of REAL
((r / 2) * (sqrt 2)) ^2 is V14() real ext-real Element of REAL
K46(((r / 2) * (sqrt 2)),((r / 2) * (sqrt 2))) is V14() real ext-real set
dist (u,rm1) is V14() real ext-real Element of REAL
v is V43(2) Element of REAL 2
r3 is V43(2) Element of REAL 2
(Pitag_dist 2) . (v,r3) is V14() real ext-real Element of REAL
r2 - (r2 - (r / 2)) is V14() real ext-real Element of REAL
(r2 - (r2 - (r / 2))) ^2 is V14() real ext-real Element of REAL
K46((r2 - (r2 - (r / 2))),(r2 - (r2 - (r / 2)))) is V14() real ext-real set
s2 - (s2 + (r / 2)) is V14() real ext-real Element of REAL
(s2 - (s2 + (r / 2))) ^2 is V14() real ext-real Element of REAL
K46((s2 - (s2 + (r / 2))),(s2 - (s2 + (r / 2)))) is V14() real ext-real set
((r2 - (r2 - (r / 2))) ^2) + ((s2 - (s2 + (r / 2))) ^2) is V14() real ext-real Element of REAL
sqrt (((r2 - (r2 - (r / 2))) ^2) + ((s2 - (s2 + (r / 2))) ^2)) is V14() real ext-real Element of REAL
p `1 is V14() real ext-real Element of REAL
p `2 is V14() real ext-real Element of REAL
Ball (u,r) is Element of bool the carrier of (Euclid 2)
(Int (cell (G,i,j))) /\ G0 is Element of bool the carrier of (TOP-REAL 2)
{} (TOP-REAL 2) is empty proper closed V110() V111() V112() V113() V114() V115() V116() symmetric circled Element of bool the carrier of (TOP-REAL 2)
G * (1,1) is V43(2) V100() FinSequence-like Element of the carrier of (TOP-REAL 2)
(G * (1,1)) `1 is V14() real ext-real Element of REAL
G * (1,j) is V43(2) V100() FinSequence-like Element of the carrier of (TOP-REAL 2)
(G * (1,j)) `2 is V14() real ext-real Element of REAL
j + 1 is natural V14() real ext-real V108() V109() V110() V111() V112() V113() V114() V115() Element of NAT
G * (1,(j + 1)) is V43(2) V100() FinSequence-like Element of the carrier of (TOP-REAL 2)
(G * (1,(j + 1))) `2 is V14() real ext-real Element of REAL
{ |[b<sub>1</sub>,b<sub>2</sub>]| where b<sub>1</sub>, b<sub>2</sub> is V14() real ext-real Element of REAL : ( b<sub>1</sub> <= (G * (1,1)) `1 & (G * (1,j)) `2 <= b<sub>2</sub> & b<sub>2</sub> <= (G * (1,(j + 1))) `2 ) } is set
r2 is V14() real ext-real Element of REAL
s2 is V14() real ext-real Element of REAL
|[r2,s2]| is V43(2) V100() FinSequence-like Element of the carrier of (TOP-REAL 2)
p `1 is V14() real ext-real Element of REAL
p `2 is V14() real ext-real Element of REAL
(sqrt 2) / 2 is V14() real ext-real Element of REAL
r is V14() real ext-real Element of REAL
r * 1 is V14() real ext-real Element of REAL
r * ((sqrt 2) / 2) is V14() real ext-real Element of REAL
r / 2 is V14() real ext-real Element of REAL
(r / 2) ^2 is V14() real ext-real Element of REAL
K46((r / 2),(r / 2)) is V14() real ext-real set
((r / 2) ^2) + ((r / 2) ^2) is V14() real ext-real Element of REAL
2 * ((r / 2) ^2) is V14() real ext-real Element of REAL
(sqrt 2) ^2 is V14() real ext-real Element of REAL
K46((sqrt 2),(sqrt 2)) is V14() real ext-real set
((sqrt 2) ^2) * ((r / 2) ^2) is V14() real ext-real Element of REAL
(r / 2) * (sqrt 2) is V14() real ext-real Element of REAL
((r / 2) * (sqrt 2)) ^2 is V14() real ext-real Element of REAL
K46(((r / 2) * (sqrt 2)),((r / 2) * (sqrt 2))) is V14() real ext-real set
sqrt (((r / 2) ^2) + ((r / 2) ^2)) is V14() real ext-real Element of REAL
((G * (1,(j + 1))) `2) - ((G * (1,j)) `2) is V14() real ext-real Element of REAL
min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2))) is V14() real ext-real Element of REAL
r2 - (r / 2) is V14() real ext-real Element of REAL
(min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2 is V14() real ext-real Element of REAL
s2 + ((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2) is V14() real ext-real Element of REAL
|[(r2 - (r / 2)),(s2 + ((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2))]| is V43(2) V100() FinSequence-like Element of the carrier of (TOP-REAL 2)
|[(r2 - (r / 2)),(s2 + ((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2))]| `1 is V14() real ext-real Element of REAL
|[(r2 - (r / 2)),(s2 + ((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2))]| `2 is V14() real ext-real Element of REAL
s3 is Element of the carrier of (Euclid 2)
((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2) ^2 is V14() real ext-real Element of REAL
K46(((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2),((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2)) is V14() real ext-real set
((r / 2) ^2) + (((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2) ^2) is V14() real ext-real Element of REAL
sqrt (((r / 2) ^2) + (((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2) ^2)) is V14() real ext-real Element of REAL
dist (u,s3) is V14() real ext-real Element of REAL
v is V43(2) Element of REAL 2
q0 is V43(2) Element of REAL 2
(Pitag_dist 2) . (v,q0) is V14() real ext-real Element of REAL
r2 - (r2 - (r / 2)) is V14() real ext-real Element of REAL
(r2 - (r2 - (r / 2))) ^2 is V14() real ext-real Element of REAL
K46((r2 - (r2 - (r / 2))),(r2 - (r2 - (r / 2)))) is V14() real ext-real set
s2 - (s2 + ((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2)) is V14() real ext-real Element of REAL
(s2 - (s2 + ((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2))) ^2 is V14() real ext-real Element of REAL
K46((s2 - (s2 + ((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2))),(s2 - (s2 + ((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2)))) is V14() real ext-real set
((r2 - (r2 - (r / 2))) ^2) + ((s2 - (s2 + ((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2))) ^2) is V14() real ext-real Element of REAL
sqrt (((r2 - (r2 - (r / 2))) ^2) + ((s2 - (s2 + ((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2))) ^2)) is V14() real ext-real Element of REAL
Ball (u,r) is Element of bool the carrier of (Euclid 2)
(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)) / 2 is V14() real ext-real Element of REAL
((G * (1,j)) `2) + ((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2) is V14() real ext-real Element of REAL
((G * (1,j)) `2) + ((((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)) / 2) is V14() real ext-real Element of REAL
2 " is non empty V14() real ext-real positive non negative Element of REAL
r * (2 ") is V14() real ext-real Element of REAL
(r2 - (r / 2)) + (r / 2) is V14() real ext-real Element of REAL
(((G * (1,j)) `2) + ((((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)) / 2)) + ((((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)) / 2) is V14() real ext-real Element of REAL
{ |[b<sub>1</sub>,b<sub>2</sub>]| where b<sub>1</sub>, b<sub>2</sub> is V14() real ext-real Element of REAL : ( not (G * (1,1)) `1 <= b₁ & not b₂ <= (G * (1,j)) `2 & not (G * (1,(j + 1))) `2 <= b₂ ) } is set
(Int (cell (G,i,j))) /\ G0 is Element of bool the carrier of (TOP-REAL 2)
{} (TOP-REAL 2) is empty proper closed V110() V111() V112() V113() V114() V115() V116() symmetric circled Element of bool the carrier of (TOP-REAL 2)
r is V14() real ext-real Element of REAL
r / 2 is V14() real ext-real Element of REAL
r2 - (r / 2) is V14() real ext-real Element of REAL
|[(r2 - (r / 2)),s2]| is V43(2) V100() FinSequence-like Element of the carrier of (TOP-REAL 2)
rm is V43(2) V100() FinSequence-like Element of the carrier of (TOP-REAL 2)
2 " is non empty V14() real ext-real positive non negative Element of REAL
r * (2 ") is V14() real ext-real Element of REAL
(r2 - (r / 2)) + (r / 2) is V14() real ext-real Element of REAL
rm1 is Element of the carrier of (Euclid 2)
{ |[b₁,b₂]| where b₁, b₂ is V14() real ext-real Element of REAL : ( not (G * (1,1)) `1 <= b<sub>1</sub> & not b<sub>2</sub> <= (G * (1,j)) `2 & not (G * (1,(j + 1))) `2 <= b<sub>2</sub> ) } is set
rm `1 is V14() real ext-real Element of REAL
rm `2 is V14() real ext-real Element of REAL
(sqrt 2) / 2 is V14() real ext-real Element of REAL
r * 1 is V14() real ext-real Element of REAL
r * ((sqrt 2) / 2) is V14() real ext-real Element of REAL
(r / 2) ^2 is V14() real ext-real Element of REAL
K46((r / 2),(r / 2)) is V14() real ext-real set
((r / 2) ^2) + 0 is V14() real ext-real Element of REAL
((r / 2) ^2) + ((r / 2) ^2) is V14() real ext-real Element of REAL
0 ^2 is V14() real ext-real Element of REAL
K46(0,0) is empty V14() real ext-real non positive non negative V110() V111() V112() V113() V114() V115() V116() set
((r / 2) ^2) + (0 ^2) is V14() real ext-real Element of REAL
sqrt (((r / 2) ^2) + (0 ^2)) is V14() real ext-real Element of REAL
sqrt (((r / 2) ^2) + ((r / 2) ^2)) is V14() real ext-real Element of REAL
p `1 is V14() real ext-real Element of REAL
p `2 is V14() real ext-real Element of REAL
2 * ((r / 2) ^2) is V14() real ext-real Element of REAL
(sqrt 2) ^2 is V14() real ext-real Element of REAL
K46((sqrt 2),(sqrt 2)) is V14() real ext-real set
((sqrt 2) ^2) * ((r / 2) ^2) is V14() real ext-real Element of REAL
(r / 2) * (sqrt 2) is V14() real ext-real Element of REAL
((r / 2) * (sqrt 2)) ^2 is V14() real ext-real Element of REAL
K46(((r / 2) * (sqrt 2)),((r / 2) * (sqrt 2))) is V14() real ext-real set
dist (u,rm1) is V14() real ext-real Element of REAL
v is V43(2) Element of REAL 2
r3 is V43(2) Element of REAL 2
(Pitag_dist 2) . (v,r3) is V14() real ext-real Element of REAL
r2 - (r2 - (r / 2)) is V14() real ext-real Element of REAL
(r2 - (r2 - (r / 2))) ^2 is V14() real ext-real Element of REAL
K46((r2 - (r2 - (r / 2))),(r2 - (r2 - (r / 2)))) is V14() real ext-real set
s2 - s2 is V14() real ext-real Element of REAL
(s2 - s2) ^2 is V14() real ext-real Element of REAL
K46((s2 - s2),(s2 - s2)) is V14() real ext-real set
((r2 - (r2 - (r / 2))) ^2) + ((s2 - s2) ^2) is V14() real ext-real Element of REAL
sqrt (((r2 - (r2 - (r / 2))) ^2) + ((s2 - s2) ^2)) is V14() real ext-real Element of REAL
Ball (u,r) is Element of bool the carrier of (Euclid 2)
(Int (cell (G,i,j))) /\ G0 is Element of bool the carrier of (TOP-REAL 2)
p `1 is V14() real ext-real Element of REAL
p `2 is V14() real ext-real Element of REAL
(sqrt 2) / 2 is V14() real ext-real Element of REAL
r is V14() real ext-real Element of REAL
r * 1 is V14() real ext-real Element of REAL
r * ((sqrt 2) / 2) is V14() real ext-real Element of REAL
r / 2 is V14() real ext-real Element of REAL
(r / 2) ^2 is V14() real ext-real Element of REAL
K46((r / 2),(r / 2)) is V14() real ext-real set
((r / 2) ^2) + ((r / 2) ^2) is V14() real ext-real Element of REAL
2 * ((r / 2) ^2) is V14() real ext-real Element of REAL
(sqrt 2) ^2 is V14() real ext-real Element of REAL
K46((sqrt 2),(sqrt 2)) is V14() real ext-real set
((sqrt 2) ^2) * ((r / 2) ^2) is V14() real ext-real Element of REAL
(r / 2) * (sqrt 2) is V14() real ext-real Element of REAL
((r / 2) * (sqrt 2)) ^2 is V14() real ext-real Element of REAL
K46(((r / 2) * (sqrt 2)),((r / 2) * (sqrt 2))) is V14() real ext-real set
sqrt (((r / 2) ^2) + ((r / 2) ^2)) is V14() real ext-real Element of REAL
((G * (1,(j + 1))) `2) - ((G * (1,j)) `2) is V14() real ext-real Element of REAL
min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2))) is V14() real ext-real Element of REAL
r2 - (r / 2) is V14() real ext-real Element of REAL
(min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2 is V14() real ext-real Element of REAL
s2 - ((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2) is V14() real ext-real Element of REAL
|[(r2 - (r / 2)),(s2 - ((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2))]| is V43(2) V100() FinSequence-like Element of the carrier of (TOP-REAL 2)
r3 is V43(2) V100() FinSequence-like Element of the carrier of (TOP-REAL 2)
r3 `1 is V14() real ext-real Element of REAL
r3 `2 is V14() real ext-real Element of REAL
s3 is Element of the carrier of (Euclid 2)
(s2 - ((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2)) + ((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2) is V14() real ext-real Element of REAL
((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2) ^2 is V14() real ext-real Element of REAL
K46(((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2),((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2)) is V14() real ext-real set
((r / 2) ^2) + (((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2) ^2) is V14() real ext-real Element of REAL
sqrt (((r / 2) ^2) + (((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2) ^2)) is V14() real ext-real Element of REAL
dist (u,s3) is V14() real ext-real Element of REAL
v is V43(2) Element of REAL 2
q0 is V43(2) Element of REAL 2
(Pitag_dist 2) . (v,q0) is V14() real ext-real Element of REAL
r2 - (r2 - (r / 2)) is V14() real ext-real Element of REAL
(r2 - (r2 - (r / 2))) ^2 is V14() real ext-real Element of REAL
K46((r2 - (r2 - (r / 2))),(r2 - (r2 - (r / 2)))) is V14() real ext-real set
s2 - (s2 - ((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2)) is V14() real ext-real Element of REAL
(s2 - (s2 - ((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2))) ^2 is V14() real ext-real Element of REAL
K46((s2 - (s2 - ((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2))),(s2 - (s2 - ((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2)))) is V14() real ext-real set
((r2 - (r2 - (r / 2))) ^2) + ((s2 - (s2 - ((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2))) ^2) is V14() real ext-real Element of REAL
sqrt (((r2 - (r2 - (r / 2))) ^2) + ((s2 - (s2 - ((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2))) ^2)) is V14() real ext-real Element of REAL
Ball (u,r) is Element of bool the carrier of (Euclid 2)
(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)) / 2 is V14() real ext-real Element of REAL
((G * (1,(j + 1))) `2) - ((((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)) / 2) is V14() real ext-real Element of REAL
((G * (1,(j + 1))) `2) - ((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2) is V14() real ext-real Element of REAL
2 " is non empty V14() real ext-real positive non negative Element of REAL
r * (2 ") is V14() real ext-real Element of REAL
(r2 - (r / 2)) + (r / 2) is V14() real ext-real Element of REAL
(((G * (1,(j + 1))) `2) - ((((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)) / 2)) - ((((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)) / 2) is V14() real ext-real Element of REAL
{ |[b₁,b₂]| where b₁, b₂ is V14() real ext-real Element of REAL : ( not (G * (1,1)) `1 <= b<sub>1</sub> & not b<sub>2</sub> <= (G * (1,j)) `2 & not (G * (1,(j + 1))) `2 <= b<sub>2</sub> ) } is set
(Int (cell (G,i,j))) /\ G0 is Element of bool the carrier of (TOP-REAL 2)
(Int (cell (G,i,j))) /\ G0 is Element of bool the carrier of (TOP-REAL 2)
{} (TOP-REAL 2) is empty proper closed V110() V111() V112() V113() V114() V115() V116() symmetric circled Element of bool the carrier of (TOP-REAL 2)
(Int (cell (G,i,j))) /\ G0 is Element of bool the carrier of (TOP-REAL 2)
{} (TOP-REAL 2) is empty proper closed V110() V111() V112() V113() V114() V115() V116() symmetric circled Element of bool the carrier of (TOP-REAL 2)
G * ((len G),1) is V43(2) V100() FinSequence-like Element of the carrier of (TOP-REAL 2)
(G * ((len G),1)) `1 is V14() real ext-real Element of REAL
G * (1,1) is V43(2) V100() FinSequence-like Element of the carrier of (TOP-REAL 2)
(G * (1,1)) `2 is V14() real ext-real Element of REAL
{ |[b<sub>1</sub>,b<sub>2</sub>]| where b<sub>1</sub>, b<sub>2</sub> is V14() real ext-real Element of REAL : ( (G * ((len G),1)) `1 <= b₁ & b₂ <= (G * (1,1)) `2 ) } is set
r2 is V14() real ext-real Element of REAL
s2 is V14() real ext-real Element of REAL
|[r2,s2]| is V43(2) V100() FinSequence-like Element of the carrier of (TOP-REAL 2)
r is V14() real ext-real Element of REAL
r / 2 is V14() real ext-real Element of REAL
r2 + (r / 2) is V14() real ext-real Element of REAL
s2 - (r / 2) is V14() real ext-real Element of REAL
2 " is non empty V14() real ext-real positive non negative Element of REAL
r * (2 ") is V14() real ext-real Element of REAL
|[(r2 + (r / 2)),(s2 - (r / 2))]| is V43(2) V100() FinSequence-like Element of the carrier of (TOP-REAL 2)
rm is V43(2) V100() FinSequence-like Element of the carrier of (TOP-REAL 2)
(s2 - (r / 2)) + (r / 2) is V14() real ext-real Element of REAL
rm1 is Element of the carrier of (Euclid 2)
{ |[b<sub>1</sub>,b<sub>2</sub>]| where b<sub>1</sub>, b<sub>2</sub> is V14() real ext-real Element of REAL : ( not b<sub>1</sub> <= (G * ((len G),1)) `1 & not (G * (1,1)) `2 <= b<sub>2</sub> ) } is set
rm `1 is V14() real ext-real Element of REAL
rm `2 is V14() real ext-real Element of REAL
(sqrt 2) / 2 is V14() real ext-real Element of REAL
r * 1 is V14() real ext-real Element of REAL
r * ((sqrt 2) / 2) is V14() real ext-real Element of REAL
(r / 2) ^2 is V14() real ext-real Element of REAL
K46((r / 2),(r / 2)) is V14() real ext-real set
((r / 2) ^2) + ((r / 2) ^2) is V14() real ext-real Element of REAL
2 * ((r / 2) ^2) is V14() real ext-real Element of REAL
(sqrt 2) ^2 is V14() real ext-real Element of REAL
K46((sqrt 2),(sqrt 2)) is V14() real ext-real set
((sqrt 2) ^2) * ((r / 2) ^2) is V14() real ext-real Element of REAL
(r / 2) * (sqrt 2) is V14() real ext-real Element of REAL
((r / 2) * (sqrt 2)) ^2 is V14() real ext-real Element of REAL
K46(((r / 2) * (sqrt 2)),((r / 2) * (sqrt 2))) is V14() real ext-real set
dist (u,rm1) is V14() real ext-real Element of REAL
v is V43(2) Element of REAL 2
r3 is V43(2) Element of REAL 2
(Pitag_dist 2) . (v,r3) is V14() real ext-real Element of REAL
r2 - (r2 + (r / 2)) is V14() real ext-real Element of REAL
(r2 - (r2 + (r / 2))) ^2 is V14() real ext-real Element of REAL
K46((r2 - (r2 + (r / 2))),(r2 - (r2 + (r / 2)))) is V14() real ext-real set
s2 - (s2 - (r / 2)) is V14() real ext-real Element of REAL
(s2 - (s2 - (r / 2))) ^2 is V14() real ext-real Element of REAL
K46((s2 - (s2 - (r / 2))),(s2 - (s2 - (r / 2)))) is V14() real ext-real set
((r2 - (r2 + (r / 2))) ^2) + ((s2 - (s2 - (r / 2))) ^2) is V14() real ext-real Element of REAL
sqrt (((r2 - (r2 + (r / 2))) ^2) + ((s2 - (s2 - (r / 2))) ^2)) is V14() real ext-real Element of REAL
p `1 is V14() real ext-real Element of REAL
p `2 is V14() real ext-real Element of REAL
Ball (u,r) is Element of bool the carrier of (Euclid 2)
(Int (cell (G,i,j))) /\ G0 is Element of bool the carrier of (TOP-REAL 2)
(sqrt 2) / 2 is V14() real ext-real Element of REAL
r is V14() real ext-real Element of REAL
r * 1 is V14() real ext-real Element of REAL
r * ((sqrt 2) / 2) is V14() real ext-real Element of REAL
r / 2 is V14() real ext-real Element of REAL
(r / 2) ^2 is V14() real ext-real Element of REAL
K46((r / 2),(r / 2)) is V14() real ext-real set
((r / 2) ^2) + ((r / 2) ^2) is V14() real ext-real Element of REAL
2 * ((r / 2) ^2) is V14() real ext-real Element of REAL
(sqrt 2) ^2 is V14() real ext-real Element of REAL
K46((sqrt 2),(sqrt 2)) is V14() real ext-real set
((sqrt 2) ^2) * ((r / 2) ^2) is V14() real ext-real Element of REAL
(r / 2) * (sqrt 2) is V14() real ext-real Element of REAL
((r / 2) * (sqrt 2)) ^2 is V14() real ext-real Element of REAL
K46(((r / 2) * (sqrt 2)),((r / 2) * (sqrt 2))) is V14() real ext-real set
sqrt (((r / 2) ^2) + ((r / 2) ^2)) is V14() real ext-real Element of REAL
G * ((len G),1) is V43(2) V100() FinSequence-like Element of the carrier of (TOP-REAL 2)
(G * ((len G),1)) `1 is V14() real ext-real Element of REAL
G * (1,(width G)) is V43(2) V100() FinSequence-like Element of the carrier of (TOP-REAL 2)
(G * (1,(width G))) `2 is V14() real ext-real Element of REAL
{ |[b<sub>1</sub>,b<sub>2</sub>]| where b<sub>1</sub>, b<sub>2</sub> is V14() real ext-real Element of REAL : ( (G * ((len G),1)) `1 <= b₁ & (G * (1,(width G))) `2 <= b<sub>2</sub> ) } is set
r2 is V14() real ext-real Element of REAL
s2 is V14() real ext-real Element of REAL
|[r2,s2]| is V43(2) V100() FinSequence-like Element of the carrier of (TOP-REAL 2)
r2 + (r / 2) is V14() real ext-real Element of REAL
s2 + (r / 2) is V14() real ext-real Element of REAL
2 " is non empty V14() real ext-real positive non negative Element of REAL
r * (2 ") is V14() real ext-real Element of REAL
|[(r2 + (r / 2)),(s2 + (r / 2))]| is V43(2) V100() FinSequence-like Element of the carrier of (TOP-REAL 2)
rm is V43(2) V100() FinSequence-like Element of the carrier of (TOP-REAL 2)
rm1 is Element of the carrier of (Euclid 2)
{ |[b<sub>1</sub>,b<sub>2</sub>]| where b<sub>1</sub>, b<sub>2</sub> is V14() real ext-real Element of REAL : ( not b<sub>1</sub> <= (G * ((len G),1)) `1 & not b₂ <= (G * (1,(width G))) `2 ) } is set
rm `1 is V14() real ext-real Element of REAL
rm `2 is V14() real ext-real Element of REAL
- (r / 2) is V14() real ext-real Element of REAL
(- (r / 2)) ^2 is V14() real ext-real Element of REAL
K46((- (r / 2)),(- (r / 2))) is V14() real ext-real set
dist (u,rm1) is V14() real ext-real Element of REAL
v is V43(2) Element of REAL 2
r3 is V43(2) Element of REAL 2
(Pitag_dist 2) . (v,r3) is V14() real ext-real Element of REAL
r2 - (r2 + (r / 2)) is V14() real ext-real Element of REAL
s2 - (s2 + (r / 2)) is V14() real ext-real Element of REAL
p `1 is V14() real ext-real Element of REAL
p `2 is V14() real ext-real Element of REAL
Ball (u,r) is Element of bool the carrier of (Euclid 2)
(Int (cell (G,i,j))) /\ G0 is Element of bool the carrier of (TOP-REAL 2)
G * ((len G),1) is V43(2) V100() FinSequence-like Element of the carrier of (TOP-REAL 2)
(G * ((len G),1)) `1 is V14() real ext-real Element of REAL
G * (1,j) is V43(2) V100() FinSequence-like Element of the carrier of (TOP-REAL 2)
(G * (1,j)) `2 is V14() real ext-real Element of REAL
j + 1 is natural V14() real ext-real V108() V109() V110() V111() V112() V113() V114() V115() Element of NAT
G * (1,(j + 1)) is V43(2) V100() FinSequence-like Element of the carrier of (TOP-REAL 2)
(G * (1,(j + 1))) `2 is V14() real ext-real Element of REAL
{ |[b<sub>1</sub>,b<sub>2</sub>]| where b<sub>1</sub>, b<sub>2</sub> is V14() real ext-real Element of REAL : ( (G * ((len G),1)) `1 <= b₁ & (G * (1,j)) `2 <= b<sub>2</sub> & b<sub>2</sub> <= (G * (1,(j + 1))) `2 ) } is set
r2 is V14() real ext-real Element of REAL
s2 is V14() real ext-real Element of REAL
|[r2,s2]| is V43(2) V100() FinSequence-like Element of the carrier of (TOP-REAL 2)
p `1 is V14() real ext-real Element of REAL
p `2 is V14() real ext-real Element of REAL
(sqrt 2) / 2 is V14() real ext-real Element of REAL
r is V14() real ext-real Element of REAL
r * 1 is V14() real ext-real Element of REAL
r * ((sqrt 2) / 2) is V14() real ext-real Element of REAL
r / 2 is V14() real ext-real Element of REAL
(r / 2) ^2 is V14() real ext-real Element of REAL
K46((r / 2),(r / 2)) is V14() real ext-real set
((r / 2) ^2) + ((r / 2) ^2) is V14() real ext-real Element of REAL
2 * ((r / 2) ^2) is V14() real ext-real Element of REAL
(sqrt 2) ^2 is V14() real ext-real Element of REAL
K46((sqrt 2),(sqrt 2)) is V14() real ext-real set
((sqrt 2) ^2) * ((r / 2) ^2) is V14() real ext-real Element of REAL
(r / 2) * (sqrt 2) is V14() real ext-real Element of REAL
((r / 2) * (sqrt 2)) ^2 is V14() real ext-real Element of REAL
K46(((r / 2) * (sqrt 2)),((r / 2) * (sqrt 2))) is V14() real ext-real set
sqrt (((r / 2) ^2) + ((r / 2) ^2)) is V14() real ext-real Element of REAL
((G * (1,(j + 1))) `2) - ((G * (1,j)) `2) is V14() real ext-real Element of REAL
min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2))) is V14() real ext-real Element of REAL
r2 + (r / 2) is V14() real ext-real Element of REAL
(min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2 is V14() real ext-real Element of REAL
s2 + ((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2) is V14() real ext-real Element of REAL
|[(r2 + (r / 2)),(s2 + ((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2))]| is V43(2) V100() FinSequence-like Element of the carrier of (TOP-REAL 2)
r3 is V43(2) V100() FinSequence-like Element of the carrier of (TOP-REAL 2)
r3 `1 is V14() real ext-real Element of REAL
r3 `2 is V14() real ext-real Element of REAL
s3 is Element of the carrier of (Euclid 2)
((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2) ^2 is V14() real ext-real Element of REAL
K46(((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2),((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2)) is V14() real ext-real set
((r / 2) ^2) + (((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2) ^2) is V14() real ext-real Element of REAL
sqrt (((r / 2) ^2) + (((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2) ^2)) is V14() real ext-real Element of REAL
dist (u,s3) is V14() real ext-real Element of REAL
v is V43(2) Element of REAL 2
q0 is V43(2) Element of REAL 2
(Pitag_dist 2) . (v,q0) is V14() real ext-real Element of REAL
r2 - (r2 + (r / 2)) is V14() real ext-real Element of REAL
(r2 - (r2 + (r / 2))) ^2 is V14() real ext-real Element of REAL
K46((r2 - (r2 + (r / 2))),(r2 - (r2 + (r / 2)))) is V14() real ext-real set
s2 - (s2 + ((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2)) is V14() real ext-real Element of REAL
(s2 - (s2 + ((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2))) ^2 is V14() real ext-real Element of REAL
K46((s2 - (s2 + ((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2))),(s2 - (s2 + ((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2)))) is V14() real ext-real set
((r2 - (r2 + (r / 2))) ^2) + ((s2 - (s2 + ((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2))) ^2) is V14() real ext-real Element of REAL
sqrt (((r2 - (r2 + (r / 2))) ^2) + ((s2 - (s2 + ((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2))) ^2)) is V14() real ext-real Element of REAL
Ball (u,r) is Element of bool the carrier of (Euclid 2)
(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)) / 2 is V14() real ext-real Element of REAL
((G * (1,j)) `2) + ((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2) is V14() real ext-real Element of REAL
((G * (1,j)) `2) + ((((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)) / 2) is V14() real ext-real Element of REAL
2 " is non empty V14() real ext-real positive non negative Element of REAL
r * (2 ") is V14() real ext-real Element of REAL
(((G * (1,j)) `2) + ((((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)) / 2)) + ((((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)) / 2) is V14() real ext-real Element of REAL
{ |[b<sub>1</sub>,b<sub>2</sub>]| where b<sub>1</sub>, b<sub>2</sub> is V14() real ext-real Element of REAL : ( not b<sub>1</sub> <= (G * ((len G),1)) `1 & not b₂ <= (G * (1,j)) `2 & not (G * (1,(j + 1))) `2 <= b₂ ) } is set
(Int (cell (G,i,j))) /\ G0 is Element of bool the carrier of (TOP-REAL 2)
r is V14() real ext-real Element of REAL
r / 2 is V14() real ext-real Element of REAL
r2 + (r / 2) is V14() real ext-real Element of REAL
|[(r2 + (r / 2)),s2]| is V43(2) V100() FinSequence-like Element of the carrier of (TOP-REAL 2)
rm is V43(2) V100() FinSequence-like Element of the carrier of (TOP-REAL 2)
2 " is non empty V14() real ext-real positive non negative Element of REAL
r * (2 ") is V14() real ext-real Element of REAL
rm1 is Element of the carrier of (Euclid 2)
{ |[b₁,b₂]| where b₁, b₂ is V14() real ext-real Element of REAL : ( not b₁ <= (G * ((len G),1)) `1 & not b<sub>2</sub> <= (G * (1,j)) `2 & not (G * (1,(j + 1))) `2 <= b<sub>2</sub> ) } is set
rm `1 is V14() real ext-real Element of REAL
rm `2 is V14() real ext-real Element of REAL
(sqrt 2) / 2 is V14() real ext-real Element of REAL
r * 1 is V14() real ext-real Element of REAL
r * ((sqrt 2) / 2) is V14() real ext-real Element of REAL
(r / 2) ^2 is V14() real ext-real Element of REAL
K46((r / 2),(r / 2)) is V14() real ext-real set
((r / 2) ^2) + 0 is V14() real ext-real Element of REAL
((r / 2) ^2) + ((r / 2) ^2) is V14() real ext-real Element of REAL
0 ^2 is V14() real ext-real Element of REAL
K46(0,0) is empty V14() real ext-real non positive non negative V110() V111() V112() V113() V114() V115() V116() set
((r / 2) ^2) + (0 ^2) is V14() real ext-real Element of REAL
sqrt (((r / 2) ^2) + (0 ^2)) is V14() real ext-real Element of REAL
sqrt (((r / 2) ^2) + ((r / 2) ^2)) is V14() real ext-real Element of REAL
p `1 is V14() real ext-real Element of REAL
p `2 is V14() real ext-real Element of REAL
2 * ((r / 2) ^2) is V14() real ext-real Element of REAL
(sqrt 2) ^2 is V14() real ext-real Element of REAL
K46((sqrt 2),(sqrt 2)) is V14() real ext-real set
((sqrt 2) ^2) * ((r / 2) ^2) is V14() real ext-real Element of REAL
(r / 2) * (sqrt 2) is V14() real ext-real Element of REAL
((r / 2) * (sqrt 2)) ^2 is V14() real ext-real Element of REAL
K46(((r / 2) * (sqrt 2)),((r / 2) * (sqrt 2))) is V14() real ext-real set
dist (u,rm1) is V14() real ext-real Element of REAL
v is V43(2) Element of REAL 2
r3 is V43(2) Element of REAL 2
(Pitag_dist 2) . (v,r3) is V14() real ext-real Element of REAL
r2 - (r2 + (r / 2)) is V14() real ext-real Element of REAL
(r2 - (r2 + (r / 2))) ^2 is V14() real ext-real Element of REAL
K46((r2 - (r2 + (r / 2))),(r2 - (r2 + (r / 2)))) is V14() real ext-real set
s2 - s2 is V14() real ext-real Element of REAL
(s2 - s2) ^2 is V14() real ext-real Element of REAL
K46((s2 - s2),(s2 - s2)) is V14() real ext-real set
((r2 - (r2 + (r / 2))) ^2) + ((s2 - s2) ^2) is V14() real ext-real Element of REAL
sqrt (((r2 - (r2 + (r / 2))) ^2) + ((s2 - s2) ^2)) is V14() real ext-real Element of REAL
Ball (u,r) is Element of bool the carrier of (Euclid 2)
(Int (cell (G,i,j))) /\ G0 is Element of bool the carrier of (TOP-REAL 2)
p `1 is V14() real ext-real Element of REAL
p `2 is V14() real ext-real Element of REAL
(sqrt 2) / 2 is V14() real ext-real Element of REAL
r is V14() real ext-real Element of REAL
r * 1 is V14() real ext-real Element of REAL
r * ((sqrt 2) / 2) is V14() real ext-real Element of REAL
r / 2 is V14() real ext-real Element of REAL
(r / 2) ^2 is V14() real ext-real Element of REAL
K46((r / 2),(r / 2)) is V14() real ext-real set
((r / 2) ^2) + ((r / 2) ^2) is V14() real ext-real Element of REAL
2 * ((r / 2) ^2) is V14() real ext-real Element of REAL
(sqrt 2) ^2 is V14() real ext-real Element of REAL
K46((sqrt 2),(sqrt 2)) is V14() real ext-real set
((sqrt 2) ^2) * ((r / 2) ^2) is V14() real ext-real Element of REAL
(r / 2) * (sqrt 2) is V14() real ext-real Element of REAL
((r / 2) * (sqrt 2)) ^2 is V14() real ext-real Element of REAL
K46(((r / 2) * (sqrt 2)),((r / 2) * (sqrt 2))) is V14() real ext-real set
sqrt (((r / 2) ^2) + ((r / 2) ^2)) is V14() real ext-real Element of REAL
((G * (1,(j + 1))) `2) - ((G * (1,j)) `2) is V14() real ext-real Element of REAL
min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2))) is V14() real ext-real Element of REAL
r2 + (r / 2) is V14() real ext-real Element of REAL
(min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2 is V14() real ext-real Element of REAL
s2 - ((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2) is V14() real ext-real Element of REAL
|[(r2 + (r / 2)),(s2 - ((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2))]| is V43(2) V100() FinSequence-like Element of the carrier of (TOP-REAL 2)
r3 is V43(2) V100() FinSequence-like Element of the carrier of (TOP-REAL 2)
r3 `1 is V14() real ext-real Element of REAL
r3 `2 is V14() real ext-real Element of REAL
s3 is Element of the carrier of (Euclid 2)
(s2 - ((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2)) + ((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2) is V14() real ext-real Element of REAL
((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2) ^2 is V14() real ext-real Element of REAL
K46(((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2),((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2)) is V14() real ext-real set
((r / 2) ^2) + (((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2) ^2) is V14() real ext-real Element of REAL
sqrt (((r / 2) ^2) + (((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2) ^2)) is V14() real ext-real Element of REAL
dist (u,s3) is V14() real ext-real Element of REAL
v is V43(2) Element of REAL 2
q0 is V43(2) Element of REAL 2
(Pitag_dist 2) . (v,q0) is V14() real ext-real Element of REAL
r2 - (r2 + (r / 2)) is V14() real ext-real Element of REAL
(r2 - (r2 + (r / 2))) ^2 is V14() real ext-real Element of REAL
K46((r2 - (r2 + (r / 2))),(r2 - (r2 + (r / 2)))) is V14() real ext-real set
s2 - (s2 - ((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2)) is V14() real ext-real Element of REAL
(s2 - (s2 - ((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2))) ^2 is V14() real ext-real Element of REAL
K46((s2 - (s2 - ((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2))),(s2 - (s2 - ((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2)))) is V14() real ext-real set
((r2 - (r2 + (r / 2))) ^2) + ((s2 - (s2 - ((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2))) ^2) is V14() real ext-real Element of REAL
sqrt (((r2 - (r2 + (r / 2))) ^2) + ((s2 - (s2 - ((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2))) ^2)) is V14() real ext-real Element of REAL
Ball (u,r) is Element of bool the carrier of (Euclid 2)
(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)) / 2 is V14() real ext-real Element of REAL
((G * (1,(j + 1))) `2) - ((((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)) / 2) is V14() real ext-real Element of REAL
((G * (1,(j + 1))) `2) - ((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2) is V14() real ext-real Element of REAL
2 " is non empty V14() real ext-real positive non negative Element of REAL
r * (2 ") is V14() real ext-real Element of REAL
(((G * (1,(j + 1))) `2) - ((((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)) / 2)) - ((((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)) / 2) is V14() real ext-real Element of REAL
{ |[b₁,b₂]| where b₁, b₂ is V14() real ext-real Element of REAL : ( not b₁ <= (G * ((len G),1)) `1 & not b<sub>2</sub> <= (G * (1,j)) `2 & not (G * (1,(j + 1))) `2 <= b<sub>2</sub> ) } is set
(Int (cell (G,i,j))) /\ G0 is Element of bool the carrier of (TOP-REAL 2)
{} (TOP-REAL 2) is empty proper closed V110() V111() V112() V113() V114() V115() V116() symmetric circled Element of bool the carrier of (TOP-REAL 2)
(Int (cell (G,i,j))) /\ G0 is Element of bool the carrier of (TOP-REAL 2)
{} (TOP-REAL 2) is empty proper closed V110() V111() V112() V113() V114() V115() V116() symmetric circled Element of bool the carrier of (TOP-REAL 2)
(Int (cell (G,i,j))) /\ G0 is Element of bool the carrier of (TOP-REAL 2)
{} (TOP-REAL 2) is empty proper closed V110() V111() V112() V113() V114() V115() V116() symmetric circled Element of bool the carrier of (TOP-REAL 2)
G * (i,1) is V43(2) V100() FinSequence-like Element of the carrier of (TOP-REAL 2)
(G * (i,1)) `1 is V14() real ext-real Element of REAL
i + 1 is natural V14() real ext-real V108() V109() V110() V111() V112() V113() V114() V115() Element of NAT
G * ((i + 1),1) is V43(2) V100() FinSequence-like Element of the carrier of (TOP-REAL 2)
(G * ((i + 1),1)) `1 is V14() real ext-real Element of REAL
G * (1,1) is V43(2) V100() FinSequence-like Element of the carrier of (TOP-REAL 2)
(G * (1,1)) `2 is V14() real ext-real Element of REAL
{ |[b₁,b₂]| where b₁, b₂ is V14() real ext-real Element of REAL : ( (G * (i,1)) `1 <= b<sub>1</sub> & b<sub>1</sub> <= (G * ((i + 1),1)) `1 & b₂ <= (G * (1,1)) `2 ) } is set
r2 is V14() real ext-real Element of REAL
s2 is V14() real ext-real Element of REAL
|[r2,s2]| is V43(2) V100() FinSequence-like Element of the carrier of (TOP-REAL 2)
r is V14() real ext-real Element of REAL
r / 2 is V14() real ext-real Element of REAL
(r / 2) ^2 is V14() real ext-real Element of REAL
K46((r / 2),(r / 2)) is V14() real ext-real set
((r / 2) ^2) + ((r / 2) ^2) is V14() real ext-real Element of REAL
2 * ((r / 2) ^2) is V14() real ext-real Element of REAL
(sqrt 2) ^2 is V14() real ext-real Element of REAL
K46((sqrt 2),(sqrt 2)) is V14() real ext-real set
((sqrt 2) ^2) * ((r / 2) ^2) is V14() real ext-real Element of REAL
(r / 2) * (sqrt 2) is V14() real ext-real Element of REAL
((r / 2) * (sqrt 2)) ^2 is V14() real ext-real Element of REAL
K46(((r / 2) * (sqrt 2)),((r / 2) * (sqrt 2))) is V14() real ext-real set
sqrt (((r / 2) ^2) + ((r / 2) ^2)) is V14() real ext-real Element of REAL
(sqrt 2) / 2 is V14() real ext-real Element of REAL
r * ((sqrt 2) / 2) is V14() real ext-real Element of REAL
((G * ((i + 1),1)) `1) - ((G * (i,1)) `1) is V14() real ext-real Element of REAL
min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1))) is V14() real ext-real Element of REAL
s2 - (r / 2) is V14() real ext-real Element of REAL
(min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2 is V14() real ext-real Element of REAL
r2 + ((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2) is V14() real ext-real Element of REAL
|[(r2 + ((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2)),(s2 - (r / 2))]| is V43(2) V100() FinSequence-like Element of the carrier of (TOP-REAL 2)
r3 is V43(2) V100() FinSequence-like Element of the carrier of (TOP-REAL 2)
r3 `1 is V14() real ext-real Element of REAL
r3 `2 is V14() real ext-real Element of REAL
s3 is Element of the carrier of (Euclid 2)
r * 1 is V14() real ext-real Element of REAL
((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2) ^2 is V14() real ext-real Element of REAL
K46(((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2),((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2)) is V14() real ext-real set
((r / 2) ^2) + (((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2) ^2) is V14() real ext-real Element of REAL
sqrt (((r / 2) ^2) + (((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2) ^2)) is V14() real ext-real Element of REAL
p `1 is V14() real ext-real Element of REAL
p `2 is V14() real ext-real Element of REAL
dist (u,s3) is V14() real ext-real Element of REAL
v is V43(2) Element of REAL 2
q0 is V43(2) Element of REAL 2
(Pitag_dist 2) . (v,q0) is V14() real ext-real Element of REAL
(p `1) - (r3 `1) is V14() real ext-real Element of REAL
((p `1) - (r3 `1)) ^2 is V14() real ext-real Element of REAL
K46(((p `1) - (r3 `1)),((p `1) - (r3 `1))) is V14() real ext-real set
(p `2) - (r3 `2) is V14() real ext-real Element of REAL
((p `2) - (r3 `2)) ^2 is V14() real ext-real Element of REAL
K46(((p `2) - (r3 `2)),((p `2) - (r3 `2))) is V14() real ext-real set
(((p `1) - (r3 `1)) ^2) + (((p `2) - (r3 `2)) ^2) is V14() real ext-real Element of REAL
sqrt ((((p `1) - (r3 `1)) ^2) + (((p `2) - (r3 `2)) ^2)) is V14() real ext-real Element of REAL
Ball (u,r) is Element of bool the carrier of (Euclid 2)
(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)) / 2 is V14() real ext-real Element of REAL
((G * (i,1)) `1) + ((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2) is V14() real ext-real Element of REAL
((G * (i,1)) `1) + ((((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)) / 2) is V14() real ext-real Element of REAL
2 " is non empty V14() real ext-real positive non negative Element of REAL
r * (2 ") is V14() real ext-real Element of REAL
(s2 - (r / 2)) + (r / 2) is V14() real ext-real Element of REAL
(((G * (i,1)) `1) + ((((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)) / 2)) + ((((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)) / 2) is V14() real ext-real Element of REAL
{ |[b₁,b₂]| where b₁, b₂ is V14() real ext-real Element of REAL : ( not b₁ <= (G * (i,1)) `1 & not (G * ((i + 1),1)) `1 <= b₁ & not (G * (1,1)) `2 <= b<sub>2</sub> ) } is set
(Int (cell (G,i,j))) /\ G0 is Element of bool the carrier of (TOP-REAL 2)
{} (TOP-REAL 2) is empty proper closed V110() V111() V112() V113() V114() V115() V116() symmetric circled Element of bool the carrier of (TOP-REAL 2)
r is V14() real ext-real Element of REAL
r / 2 is V14() real ext-real Element of REAL
s2 - (r / 2) is V14() real ext-real Element of REAL
|[r2,(s2 - (r / 2))]| is V43(2) V100() FinSequence-like Element of the carrier of (TOP-REAL 2)
rm is V43(2) V100() FinSequence-like Element of the carrier of (TOP-REAL 2)
2 " is non empty V14() real ext-real positive non negative Element of REAL
r * (2 ") is V14() real ext-real Element of REAL
(s2 - (r / 2)) + (r / 2) is V14() real ext-real Element of REAL
rm1 is Element of the carrier of (Euclid 2)
{ |[b<sub>1</sub>,b<sub>2</sub>]| where b<sub>1</sub>, b<sub>2</sub> is V14() real ext-real Element of REAL : ( not b<sub>1</sub> <= (G * (i,1)) `1 & not (G * ((i + 1),1)) `1 <= b<sub>1</sub> & not (G * (1,1)) `2 <= b₂ ) } is set
rm `1 is V14() real ext-real Element of REAL
rm `2 is V14() real ext-real Element of REAL
(sqrt 2) / 2 is V14() real ext-real Element of REAL
r * 1 is V14() real ext-real Element of REAL
r * ((sqrt 2) / 2) is V14() real ext-real Element of REAL
(r / 2) ^2 is V14() real ext-real Element of REAL
K46((r / 2),(r / 2)) is V14() real ext-real set
0 ^2 is V14() real ext-real Element of REAL
K46(0,0) is empty V14() real ext-real non positive non negative V110() V111() V112() V113() V114() V115() V116() set
(0 ^2) + ((r / 2) ^2) is V14() real ext-real Element of REAL
((r / 2) ^2) + ((r / 2) ^2) is V14() real ext-real Element of REAL
sqrt ((0 ^2) + ((r / 2) ^2)) is V14() real ext-real Element of REAL
sqrt (((r / 2) ^2) + ((r / 2) ^2)) is V14() real ext-real Element of REAL
p `1 is V14() real ext-real Element of REAL
p `2 is V14() real ext-real Element of REAL
2 * ((r / 2) ^2) is V14() real ext-real Element of REAL
(sqrt 2) ^2 is V14() real ext-real Element of REAL
K46((sqrt 2),(sqrt 2)) is V14() real ext-real set
((sqrt 2) ^2) * ((r / 2) ^2) is V14() real ext-real Element of REAL
(r / 2) * (sqrt 2) is V14() real ext-real Element of REAL
((r / 2) * (sqrt 2)) ^2 is V14() real ext-real Element of REAL
K46(((r / 2) * (sqrt 2)),((r / 2) * (sqrt 2))) is V14() real ext-real set
dist (u,rm1) is V14() real ext-real Element of REAL
v is V43(2) Element of REAL 2
r3 is V43(2) Element of REAL 2
(Pitag_dist 2) . (v,r3) is V14() real ext-real Element of REAL
r2 - r2 is V14() real ext-real Element of REAL
(r2 - r2) ^2 is V14() real ext-real Element of REAL
K46((r2 - r2),(r2 - r2)) is V14() real ext-real set
s2 - (s2 - (r / 2)) is V14() real ext-real Element of REAL
(s2 - (s2 - (r / 2))) ^2 is V14() real ext-real Element of REAL
K46((s2 - (s2 - (r / 2))),(s2 - (s2 - (r / 2)))) is V14() real ext-real set
((r2 - r2) ^2) + ((s2 - (s2 - (r / 2))) ^2) is V14() real ext-real Element of REAL
sqrt (((r2 - r2) ^2) + ((s2 - (s2 - (r / 2))) ^2)) is V14() real ext-real Element of REAL
Ball (u,r) is Element of bool the carrier of (Euclid 2)
(Int (cell (G,i,j))) /\ G0 is Element of bool the carrier of (TOP-REAL 2)
{} (TOP-REAL 2) is empty proper closed V110() V111() V112() V113() V114() V115() V116() symmetric circled Element of bool the carrier of (TOP-REAL 2)
r is V14() real ext-real Element of REAL
r / 2 is V14() real ext-real Element of REAL
(r / 2) ^2 is V14() real ext-real Element of REAL
K46((r / 2),(r / 2)) is V14() real ext-real set
((r / 2) ^2) + ((r / 2) ^2) is V14() real ext-real Element of REAL
2 * ((r / 2) ^2) is V14() real ext-real Element of REAL
(sqrt 2) ^2 is V14() real ext-real Element of REAL
K46((sqrt 2),(sqrt 2)) is V14() real ext-real set
((sqrt 2) ^2) * ((r / 2) ^2) is V14() real ext-real Element of REAL
(r / 2) * (sqrt 2) is V14() real ext-real Element of REAL
((r / 2) * (sqrt 2)) ^2 is V14() real ext-real Element of REAL
K46(((r / 2) * (sqrt 2)),((r / 2) * (sqrt 2))) is V14() real ext-real set
sqrt (((r / 2) ^2) + ((r / 2) ^2)) is V14() real ext-real Element of REAL
(sqrt 2) / 2 is V14() real ext-real Element of REAL
r * ((sqrt 2) / 2) is V14() real ext-real Element of REAL
((G * ((i + 1),1)) `1) - ((G * (i,1)) `1) is V14() real ext-real Element of REAL
min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1))) is V14() real ext-real Element of REAL
s2 - (r / 2) is V14() real ext-real Element of REAL
(min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2 is V14() real ext-real Element of REAL
r2 - ((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2) is V14() real ext-real Element of REAL
|[(r2 - ((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2)),(s2 - (r / 2))]| is V43(2) V100() FinSequence-like Element of the carrier of (TOP-REAL 2)
r3 is V43(2) V100() FinSequence-like Element of the carrier of (TOP-REAL 2)
r3 `1 is V14() real ext-real Element of REAL
r3 `2 is V14() real ext-real Element of REAL
s3 is Element of the carrier of (Euclid 2)
(r2 - ((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2)) + ((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2) is V14() real ext-real Element of REAL
r * 1 is V14() real ext-real Element of REAL
((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2) ^2 is V14() real ext-real Element of REAL
K46(((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2),((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2)) is V14() real ext-real set
((r / 2) ^2) + (((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2) ^2) is V14() real ext-real Element of REAL
sqrt (((r / 2) ^2) + (((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2) ^2)) is V14() real ext-real Element of REAL
p `1 is V14() real ext-real Element of REAL
p `2 is V14() real ext-real Element of REAL
dist (u,s3) is V14() real ext-real Element of REAL
v is V43(2) Element of REAL 2
q0 is V43(2) Element of REAL 2
(Pitag_dist 2) . (v,q0) is V14() real ext-real Element of REAL
(p `1) - (r3 `1) is V14() real ext-real Element of REAL
((p `1) - (r3 `1)) ^2 is V14() real ext-real Element of REAL
K46(((p `1) - (r3 `1)),((p `1) - (r3 `1))) is V14() real ext-real set
(p `2) - (r3 `2) is V14() real ext-real Element of REAL
((p `2) - (r3 `2)) ^2 is V14() real ext-real Element of REAL
K46(((p `2) - (r3 `2)),((p `2) - (r3 `2))) is V14() real ext-real set
(((p `1) - (r3 `1)) ^2) + (((p `2) - (r3 `2)) ^2) is V14() real ext-real Element of REAL
sqrt ((((p `1) - (r3 `1)) ^2) + (((p `2) - (r3 `2)) ^2)) is V14() real ext-real Element of REAL
Ball (u,r) is Element of bool the carrier of (Euclid 2)
(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)) / 2 is V14() real ext-real Element of REAL
((G * ((i + 1),1)) `1) - ((((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)) / 2) is V14() real ext-real Element of REAL
((G * ((i + 1),1)) `1) - ((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2) is V14() real ext-real Element of REAL
2 " is non empty V14() real ext-real positive non negative Element of REAL
r * (2 ") is V14() real ext-real Element of REAL
(s2 - (r / 2)) + (r / 2) is V14() real ext-real Element of REAL
(((G * ((i + 1),1)) `1) - ((((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)) / 2)) - ((((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)) / 2) is V14() real ext-real Element of REAL
{ |[b<sub>1</sub>,b<sub>2</sub>]| where b<sub>1</sub>, b<sub>2</sub> is V14() real ext-real Element of REAL : ( not b<sub>1</sub> <= (G * (i,1)) `1 & not (G * ((i + 1),1)) `1 <= b<sub>1</sub> & not (G * (1,1)) `2 <= b₂ ) } is set
(Int (cell (G,i,j))) /\ G0 is Element of bool the carrier of (TOP-REAL 2)
{} (TOP-REAL 2) is empty proper closed V110() V111() V112() V113() V114() V115() V116() symmetric circled Element of bool the carrier of (TOP-REAL 2)
(Int (cell (G,i,j))) /\ G0 is Element of bool the carrier of (TOP-REAL 2)
{} (TOP-REAL 2) is empty proper closed V110() V111() V112() V113() V114() V115() V116() symmetric circled Element of bool the carrier of (TOP-REAL 2)
(Int (cell (G,i,j))) /\ G0 is Element of bool the carrier of (TOP-REAL 2)
{} (TOP-REAL 2) is empty proper closed V110() V111() V112() V113() V114() V115() V116() symmetric circled Element of bool the carrier of (TOP-REAL 2)
G * (i,1) is V43(2) V100() FinSequence-like Element of the carrier of (TOP-REAL 2)
(G * (i,1)) `1 is V14() real ext-real Element of REAL
i + 1 is natural V14() real ext-real V108() V109() V110() V111() V112() V113() V114() V115() Element of NAT
G * ((i + 1),1) is V43(2) V100() FinSequence-like Element of the carrier of (TOP-REAL 2)
(G * ((i + 1),1)) `1 is V14() real ext-real Element of REAL
G * (1,(width G)) is V43(2) V100() FinSequence-like Element of the carrier of (TOP-REAL 2)
(G * (1,(width G))) `2 is V14() real ext-real Element of REAL
{ |[b<sub>1</sub>,b<sub>2</sub>]| where b<sub>1</sub>, b<sub>2</sub> is V14() real ext-real Element of REAL : ( (G * (i,1)) `1 <= b₁ & b₁ <= (G * ((i + 1),1)) `1 & (G * (1,(width G))) `2 <= b₂ ) } is set
r2 is V14() real ext-real Element of REAL
s2 is V14() real ext-real Element of REAL
|[r2,s2]| is V43(2) V100() FinSequence-like Element of the carrier of (TOP-REAL 2)
p `1 is V14() real ext-real Element of REAL
p `2 is V14() real ext-real Element of REAL
(sqrt 2) / 2 is V14() real ext-real Element of REAL
r is V14() real ext-real Element of REAL
r * 1 is V14() real ext-real Element of REAL
r * ((sqrt 2) / 2) is V14() real ext-real Element of REAL
r / 2 is V14() real ext-real Element of REAL
(r / 2) ^2 is V14() real ext-real Element of REAL
K46((r / 2),(r / 2)) is V14() real ext-real set
((r / 2) ^2) + ((r / 2) ^2) is V14() real ext-real Element of REAL
2 * ((r / 2) ^2) is V14() real ext-real Element of REAL
(sqrt 2) ^2 is V14() real ext-real Element of REAL
K46((sqrt 2),(sqrt 2)) is V14() real ext-real set
((sqrt 2) ^2) * ((r / 2) ^2) is V14() real ext-real Element of REAL
(r / 2) * (sqrt 2) is V14() real ext-real Element of REAL
((r / 2) * (sqrt 2)) ^2 is V14() real ext-real Element of REAL
K46(((r / 2) * (sqrt 2)),((r / 2) * (sqrt 2))) is V14() real ext-real set
sqrt (((r / 2) ^2) + ((r / 2) ^2)) is V14() real ext-real Element of REAL
((G * ((i + 1),1)) `1) - ((G * (i,1)) `1) is V14() real ext-real Element of REAL
min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1))) is V14() real ext-real Element of REAL
s2 + (r / 2) is V14() real ext-real Element of REAL
(min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2 is V14() real ext-real Element of REAL
r2 + ((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2) is V14() real ext-real Element of REAL
|[(r2 + ((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2)),(s2 + (r / 2))]| is V43(2) V100() FinSequence-like Element of the carrier of (TOP-REAL 2)
r3 is V43(2) V100() FinSequence-like Element of the carrier of (TOP-REAL 2)
r3 `1 is V14() real ext-real Element of REAL
r3 `2 is V14() real ext-real Element of REAL
s3 is Element of the carrier of (Euclid 2)
((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2) ^2 is V14() real ext-real Element of REAL
K46(((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2),((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2)) is V14() real ext-real set
((r / 2) ^2) + (((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2) ^2) is V14() real ext-real Element of REAL
sqrt (((r / 2) ^2) + (((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2) ^2)) is V14() real ext-real Element of REAL
dist (u,s3) is V14() real ext-real Element of REAL
v is V43(2) Element of REAL 2
q0 is V43(2) Element of REAL 2
(Pitag_dist 2) . (v,q0) is V14() real ext-real Element of REAL
r2 - (r2 + ((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2)) is V14() real ext-real Element of REAL
(r2 - (r2 + ((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2))) ^2 is V14() real ext-real Element of REAL
K46((r2 - (r2 + ((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2))),(r2 - (r2 + ((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2)))) is V14() real ext-real set
s2 - (s2 + (r / 2)) is V14() real ext-real Element of REAL
(s2 - (s2 + (r / 2))) ^2 is V14() real ext-real Element of REAL
K46((s2 - (s2 + (r / 2))),(s2 - (s2 + (r / 2)))) is V14() real ext-real set
((r2 - (r2 + ((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2))) ^2) + ((s2 - (s2 + (r / 2))) ^2) is V14() real ext-real Element of REAL
sqrt (((r2 - (r2 + ((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2))) ^2) + ((s2 - (s2 + (r / 2))) ^2)) is V14() real ext-real Element of REAL
Ball (u,r) is Element of bool the carrier of (Euclid 2)
(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)) / 2 is V14() real ext-real Element of REAL
((G * (i,1)) `1) + ((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2) is V14() real ext-real Element of REAL
((G * (i,1)) `1) + ((((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)) / 2) is V14() real ext-real Element of REAL
2 " is non empty V14() real ext-real positive non negative Element of REAL
r * (2 ") is V14() real ext-real Element of REAL
(((G * (i,1)) `1) + ((((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)) / 2)) + ((((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)) / 2) is V14() real ext-real Element of REAL
{ |[b<sub>1</sub>,b<sub>2</sub>]| where b<sub>1</sub>, b<sub>2</sub> is V14() real ext-real Element of REAL : ( not b<sub>1</sub> <= (G * (i,1)) `1 & not (G * ((i + 1),1)) `1 <= b<sub>1</sub> & not b<sub>2</sub> <= (G * (1,(width G))) `2 ) } is set
(Int (cell (G,i,j))) /\ G0 is Element of bool the carrier of (TOP-REAL 2)
{} (TOP-REAL 2) is empty proper closed V110() V111() V112() V113() V114() V115() V116() symmetric circled Element of bool the carrier of (TOP-REAL 2)
r is V14() real ext-real Element of REAL
r / 2 is V14() real ext-real Element of REAL
s2 + (r / 2) is V14() real ext-real Element of REAL
|[r2,(s2 + (r / 2))]| is V43(2) V100() FinSequence-like Element of the carrier of (TOP-REAL 2)
rm is V43(2) V100() FinSequence-like Element of the carrier of (TOP-REAL 2)
2 " is non empty V14() real ext-real positive non negative Element of REAL
r * (2 ") is V14() real ext-real Element of REAL
rm1 is Element of the carrier of (Euclid 2)
{ |[b₁,b₂]| where b₁, b₂ is V14() real ext-real Element of REAL : ( not b₁ <= (G * (i,1)) `1 & not (G * ((i + 1),1)) `1 <= b₁ & not b₂ <= (G * (1,(width G))) `2 ) } is set
rm `1 is V14() real ext-real Element of REAL
rm `2 is V14() real ext-real Element of REAL
(sqrt 2) / 2 is V14() real ext-real Element of REAL
r * 1 is V14() real ext-real Element of REAL
r * ((sqrt 2) / 2) is V14() real ext-real Element of REAL
(r / 2) ^2 is V14() real ext-real Element of REAL
K46((r / 2),(r / 2)) is V14() real ext-real set
0 ^2 is V14() real ext-real Element of REAL
K46(0,0) is empty V14() real ext-real non positive non negative V110() V111() V112() V113() V114() V115() V116() set
((r / 2) ^2) + (0 ^2) is V14() real ext-real Element of REAL
((r / 2) ^2) + ((r / 2) ^2) is V14() real ext-real Element of REAL
sqrt (((r / 2) ^2) + (0 ^2)) is V14() real ext-real Element of REAL
sqrt (((r / 2) ^2) + ((r / 2) ^2)) is V14() real ext-real Element of REAL
p `1 is V14() real ext-real Element of REAL
p `2 is V14() real ext-real Element of REAL
2 * ((r / 2) ^2) is V14() real ext-real Element of REAL
(sqrt 2) ^2 is V14() real ext-real Element of REAL
K46((sqrt 2),(sqrt 2)) is V14() real ext-real set
((sqrt 2) ^2) * ((r / 2) ^2) is V14() real ext-real Element of REAL
(r / 2) * (sqrt 2) is V14() real ext-real Element of REAL
((r / 2) * (sqrt 2)) ^2 is V14() real ext-real Element of REAL
K46(((r / 2) * (sqrt 2)),((r / 2) * (sqrt 2))) is V14() real ext-real set
dist (u,rm1) is V14() real ext-real Element of REAL
v is V43(2) Element of REAL 2
r3 is V43(2) Element of REAL 2
(Pitag_dist 2) . (v,r3) is V14() real ext-real Element of REAL
r2 - r2 is V14() real ext-real Element of REAL
(r2 - r2) ^2 is V14() real ext-real Element of REAL
K46((r2 - r2),(r2 - r2)) is V14() real ext-real set
s2 - (s2 + (r / 2)) is V14() real ext-real Element of REAL
(s2 - (s2 + (r / 2))) ^2 is V14() real ext-real Element of REAL
K46((s2 - (s2 + (r / 2))),(s2 - (s2 + (r / 2)))) is V14() real ext-real set
((r2 - r2) ^2) + ((s2 - (s2 + (r / 2))) ^2) is V14() real ext-real Element of REAL
sqrt (((r2 - r2) ^2) + ((s2 - (s2 + (r / 2))) ^2)) is V14() real ext-real Element of REAL
Ball (u,r) is Element of bool the carrier of (Euclid 2)
(Int (cell (G,i,j))) /\ G0 is Element of bool the carrier of (TOP-REAL 2)
{} (TOP-REAL 2) is empty proper closed V110() V111() V112() V113() V114() V115() V116() symmetric circled Element of bool the carrier of (TOP-REAL 2)
p `1 is V14() real ext-real Element of REAL
p `2 is V14() real ext-real Element of REAL
(sqrt 2) / 2 is V14() real ext-real Element of REAL
r is V14() real ext-real Element of REAL
r * 1 is V14() real ext-real Element of REAL
r * ((sqrt 2) / 2) is V14() real ext-real Element of REAL
r / 2 is V14() real ext-real Element of REAL
(r / 2) ^2 is V14() real ext-real Element of REAL
K46((r / 2),(r / 2)) is V14() real ext-real set
((r / 2) ^2) + ((r / 2) ^2) is V14() real ext-real Element of REAL
2 * ((r / 2) ^2) is V14() real ext-real Element of REAL
(sqrt 2) ^2 is V14() real ext-real Element of REAL
K46((sqrt 2),(sqrt 2)) is V14() real ext-real set
((sqrt 2) ^2) * ((r / 2) ^2) is V14() real ext-real Element of REAL
(r / 2) * (sqrt 2) is V14() real ext-real Element of REAL
((r / 2) * (sqrt 2)) ^2 is V14() real ext-real Element of REAL
K46(((r / 2) * (sqrt 2)),((r / 2) * (sqrt 2))) is V14() real ext-real set
sqrt (((r / 2) ^2) + ((r / 2) ^2)) is V14() real ext-real Element of REAL
((G * ((i + 1),1)) `1) - ((G * (i,1)) `1) is V14() real ext-real Element of REAL
min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1))) is V14() real ext-real Element of REAL
s2 + (r / 2) is V14() real ext-real Element of REAL
(min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2 is V14() real ext-real Element of REAL
r2 - ((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2) is V14() real ext-real Element of REAL
|[(r2 - ((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2)),(s2 + (r / 2))]| is V43(2) V100() FinSequence-like Element of the carrier of (TOP-REAL 2)
r3 is V43(2) V100() FinSequence-like Element of the carrier of (TOP-REAL 2)
r3 `1 is V14() real ext-real Element of REAL
r3 `2 is V14() real ext-real Element of REAL
s3 is Element of the carrier of (Euclid 2)
(r2 - ((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2)) + ((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2) is V14() real ext-real Element of REAL
((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2) ^2 is V14() real ext-real Element of REAL
K46(((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2),((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2)) is V14() real ext-real set
((r / 2) ^2) + (((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2) ^2) is V14() real ext-real Element of REAL
sqrt (((r / 2) ^2) + (((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2) ^2)) is V14() real ext-real Element of REAL
dist (u,s3) is V14() real ext-real Element of REAL
v is V43(2) Element of REAL 2
q0 is V43(2) Element of REAL 2
(Pitag_dist 2) . (v,q0) is V14() real ext-real Element of REAL
r2 - (r2 - ((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2)) is V14() real ext-real Element of REAL
(r2 - (r2 - ((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2))) ^2 is V14() real ext-real Element of REAL
K46((r2 - (r2 - ((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2))),(r2 - (r2 - ((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2)))) is V14() real ext-real set
s2 - (s2 + (r / 2)) is V14() real ext-real Element of REAL
(s2 - (s2 + (r / 2))) ^2 is V14() real ext-real Element of REAL
K46((s2 - (s2 + (r / 2))),(s2 - (s2 + (r / 2)))) is V14() real ext-real set
((r2 - (r2 - ((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2))) ^2) + ((s2 - (s2 + (r / 2))) ^2) is V14() real ext-real Element of REAL
sqrt (((r2 - (r2 - ((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2))) ^2) + ((s2 - (s2 + (r / 2))) ^2)) is V14() real ext-real Element of REAL
Ball (u,r) is Element of bool the carrier of (Euclid 2)
(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)) / 2 is V14() real ext-real Element of REAL
((G * ((i + 1),1)) `1) - ((((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)) / 2) is V14() real ext-real Element of REAL
((G * ((i + 1),1)) `1) - ((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2) is V14() real ext-real Element of REAL
2 " is non empty V14() real ext-real positive non negative Element of REAL
r * (2 ") is V14() real ext-real Element of REAL
(((G * ((i + 1),1)) `1) - ((((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)) / 2)) - ((((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)) / 2) is V14() real ext-real Element of REAL
{ |[b₁,b₂]| where b₁, b₂ is V14() real ext-real Element of REAL : ( not b₁ <= (G * (i,1)) `1 & not (G * ((i + 1),1)) `1 <= b₁ & not b₂ <= (G * (1,(width G))) `2 ) } is set
(Int (cell (G,i,j))) /\ G0 is Element of bool the carrier of (TOP-REAL 2)
{} (TOP-REAL 2) is empty proper closed V110() V111() V112() V113() V114() V115() V116() symmetric circled Element of bool the carrier of (TOP-REAL 2)
(Int (cell (G,i,j))) /\ G0 is Element of bool the carrier of (TOP-REAL 2)
{} (TOP-REAL 2) is empty proper closed V110() V111() V112() V113() V114() V115() V116() symmetric circled Element of bool the carrier of (TOP-REAL 2)
(Int (cell (G,i,j))) /\ G0 is Element of bool the carrier of (TOP-REAL 2)
{} (TOP-REAL 2) is empty proper closed V110() V111() V112() V113() V114() V115() V116() symmetric circled Element of bool the carrier of (TOP-REAL 2)
G * (i,1) is V43(2) V100() FinSequence-like Element of the carrier of (TOP-REAL 2)
(G * (i,1)) `1 is V14() real ext-real Element of REAL
i + 1 is natural V14() real ext-real V108() V109() V110() V111() V112() V113() V114() V115() Element of NAT
G * ((i + 1),1) is V43(2) V100() FinSequence-like Element of the carrier of (TOP-REAL 2)
(G * ((i + 1),1)) `1 is V14() real ext-real Element of REAL
G * (1,j) is V43(2) V100() FinSequence-like Element of the carrier of (TOP-REAL 2)
(G * (1,j)) `2 is V14() real ext-real Element of REAL
j + 1 is natural V14() real ext-real V108() V109() V110() V111() V112() V113() V114() V115() Element of NAT
G * (1,(j + 1)) is V43(2) V100() FinSequence-like Element of the carrier of (TOP-REAL 2)
(G * (1,(j + 1))) `2 is V14() real ext-real Element of REAL
{ |[b<sub>1</sub>,b<sub>2</sub>]| where b<sub>1</sub>, b<sub>2</sub> is V14() real ext-real Element of REAL : ( (G * (i,1)) `1 <= b₁ & b₁ <= (G * ((i + 1),1)) `1 & (G * (1,j)) `2 <= b₂ & b₂ <= (G * (1,(j + 1))) `2 ) } is set
r2 is V14() real ext-real Element of REAL
s2 is V14() real ext-real Element of REAL
|[r2,s2]| is V43(2) V100() FinSequence-like Element of the carrier of (TOP-REAL 2)
((G * ((i + 1),1)) `1) - ((G * (i,1)) `1) is V14() real ext-real Element of REAL
((G * (1,(j + 1))) `2) - ((G * (1,j)) `2) is V14() real ext-real Element of REAL
r is V14() real ext-real Element of REAL
min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2))) is V14() real ext-real Element of REAL
min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1))) is V14() real ext-real Element of REAL
(min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2 is V14() real ext-real Element of REAL
r2 + ((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2) is V14() real ext-real Element of REAL
(min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2 is V14() real ext-real Element of REAL
s2 + ((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2) is V14() real ext-real Element of REAL
(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)) / 2 is V14() real ext-real Element of REAL
((G * (i,1)) `1) + ((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2) is V14() real ext-real Element of REAL
((G * (i,1)) `1) + ((((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)) / 2) is V14() real ext-real Element of REAL
(((G * (i,1)) `1) + ((((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)) / 2)) + ((((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)) / 2) is V14() real ext-real Element of REAL
(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)) / 2 is V14() real ext-real Element of REAL
((G * (1,j)) `2) + ((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2) is V14() real ext-real Element of REAL
((G * (1,j)) `2) + ((((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)) / 2) is V14() real ext-real Element of REAL
|[(r2 + ((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2)),(s2 + ((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2))]| is V43(2) V100() FinSequence-like Element of the carrier of (TOP-REAL 2)
q0 is V43(2) V100() FinSequence-like Element of the carrier of (TOP-REAL 2)
q0 `1 is V14() real ext-real Element of REAL
q0 `2 is V14() real ext-real Element of REAL
u0 is Element of the carrier of (Euclid 2)
r / 2 is V14() real ext-real Element of REAL
((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2) ^2 is V14() real ext-real Element of REAL
K46(((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2),((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2)) is V14() real ext-real set
(r / 2) ^2 is V14() real ext-real Element of REAL
K46((r / 2),(r / 2)) is V14() real ext-real set
((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2) ^2 is V14() real ext-real Element of REAL
K46(((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2),((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2)) is V14() real ext-real set
(((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2) ^2) + (((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2) ^2) is V14() real ext-real Element of REAL
((r / 2) ^2) + ((r / 2) ^2) is V14() real ext-real Element of REAL
(sqrt 2) / 2 is V14() real ext-real Element of REAL
r * 1 is V14() real ext-real Element of REAL
r * ((sqrt 2) / 2) is V14() real ext-real Element of REAL
2 * ((r / 2) ^2) is V14() real ext-real Element of REAL
(sqrt 2) ^2 is V14() real ext-real Element of REAL
K46((sqrt 2),(sqrt 2)) is V14() real ext-real set
((sqrt 2) ^2) * ((r / 2) ^2) is V14() real ext-real Element of REAL
(r / 2) * (sqrt 2) is V14() real ext-real Element of REAL
((r / 2) * (sqrt 2)) ^2 is V14() real ext-real Element of REAL
K46(((r / 2) * (sqrt 2)),((r / 2) * (sqrt 2))) is V14() real ext-real set
sqrt (((r / 2) ^2) + ((r / 2) ^2)) is V14() real ext-real Element of REAL
p `1 is V14() real ext-real Element of REAL
p `2 is V14() real ext-real Element of REAL
sqrt ((((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2) ^2) + (((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2) ^2)) is V14() real ext-real Element of REAL
dist (u,u0) is V14() real ext-real Element of REAL
v is V43(2) Element of REAL 2
v0 is V43(2) Element of REAL 2
(Pitag_dist 2) . (v,v0) is V14() real ext-real Element of REAL
r2 - (r2 + ((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2)) is V14() real ext-real Element of REAL
(r2 - (r2 + ((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2))) ^2 is V14() real ext-real Element of REAL
K46((r2 - (r2 + ((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2))),(r2 - (r2 + ((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2)))) is V14() real ext-real set
s2 - (s2 + ((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2)) is V14() real ext-real Element of REAL
(s2 - (s2 + ((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2))) ^2 is V14() real ext-real Element of REAL
K46((s2 - (s2 + ((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2))),(s2 - (s2 + ((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2)))) is V14() real ext-real set
((r2 - (r2 + ((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2))) ^2) + ((s2 - (s2 + ((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2))) ^2) is V14() real ext-real Element of REAL
sqrt (((r2 - (r2 + ((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2))) ^2) + ((s2 - (s2 + ((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2))) ^2)) is V14() real ext-real Element of REAL
Ball (u,r) is Element of bool the carrier of (Euclid 2)
(((G * (1,j)) `2) + ((((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)) / 2)) + ((((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)) / 2) is V14() real ext-real Element of REAL
{ |[b<sub>1</sub>,b<sub>2</sub>]| where b<sub>1</sub>, b<sub>2</sub> is V14() real ext-real Element of REAL : ( not b<sub>1</sub> <= (G * (i,1)) `1 & not (G * ((i + 1),1)) `1 <= b<sub>1</sub> & not b<sub>2</sub> <= (G * (1,j)) `2 & not (G * (1,(j + 1))) `2 <= b<sub>2</sub> ) } is set
(Int (cell (G,i,j))) /\ G0 is Element of bool the carrier of (TOP-REAL 2)
{} (TOP-REAL 2) is empty proper closed V110() V111() V112() V113() V114() V115() V116() symmetric circled Element of bool the carrier of (TOP-REAL 2)
((G * ((i + 1),1)) `1) - ((G * (i,1)) `1) is V14() real ext-real Element of REAL
r is V14() real ext-real Element of REAL
min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1))) is V14() real ext-real Element of REAL
(min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2 is V14() real ext-real Element of REAL
r2 + ((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2) is V14() real ext-real Element of REAL
|[(r2 + ((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2)),s2]| is V43(2) V100() FinSequence-like Element of the carrier of (TOP-REAL 2)
r3 is V43(2) V100() FinSequence-like Element of the carrier of (TOP-REAL 2)
(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)) / 2 is V14() real ext-real Element of REAL
((G * (i,1)) `1) + ((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2) is V14() real ext-real Element of REAL
((G * (i,1)) `1) + ((((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)) / 2) is V14() real ext-real Element of REAL
(((G * (i,1)) `1) + ((((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)) / 2)) + ((((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)) / 2) is V14() real ext-real Element of REAL
s3 is Element of the carrier of (Euclid 2)
{ |[b₁,b₂]| where b₁, b₂ is V14() real ext-real Element of REAL : ( not b₁ <= (G * (i,1)) `1 & not (G * ((i + 1),1)) `1 <= b₁ & not b₂ <= (G * (1,j)) `2 & not (G * (1,(j + 1))) `2 <= b₂ ) } is set
(sqrt 2) / 2 is V14() real ext-real Element of REAL
r * 1 is V14() real ext-real Element of REAL
r * ((sqrt 2) / 2) is V14() real ext-real Element of REAL
((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2) ^2 is V14() real ext-real Element of REAL
K46(((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2),((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2)) is V14() real ext-real set
r / 2 is V14() real ext-real Element of REAL
0 ^2 is V14() real ext-real Element of REAL
K46(0,0) is empty V14() real ext-real non positive non negative V110() V111() V112() V113() V114() V115() V116() set
(((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2) ^2) + (0 ^2) is V14() real ext-real Element of REAL
(r / 2) ^2 is V14() real ext-real Element of REAL
K46((r / 2),(r / 2)) is V14() real ext-real set
((r / 2) ^2) + (0 ^2) is V14() real ext-real Element of REAL
sqrt ((((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2) ^2) + (0 ^2)) is V14() real ext-real Element of REAL
sqrt (((r / 2) ^2) + (0 ^2)) is V14() real ext-real Element of REAL
r3 `1 is V14() real ext-real Element of REAL
r3 `2 is V14() real ext-real Element of REAL
((r / 2) ^2) + ((r / 2) ^2) is V14() real ext-real Element of REAL
sqrt (((r / 2) ^2) + ((r / 2) ^2)) is V14() real ext-real Element of REAL
2 * ((r / 2) ^2) is V14() real ext-real Element of REAL
(sqrt 2) ^2 is V14() real ext-real Element of REAL
K46((sqrt 2),(sqrt 2)) is V14() real ext-real set
((sqrt 2) ^2) * ((r / 2) ^2) is V14() real ext-real Element of REAL
(r / 2) * (sqrt 2) is V14() real ext-real Element of REAL
((r / 2) * (sqrt 2)) ^2 is V14() real ext-real Element of REAL
K46(((r / 2) * (sqrt 2)),((r / 2) * (sqrt 2))) is V14() real ext-real set
dist (u,s3) is V14() real ext-real Element of REAL
v is V43(2) Element of REAL 2
q0 is V43(2) Element of REAL 2
(Pitag_dist 2) . (v,q0) is V14() real ext-real Element of REAL
r2 - (r2 + ((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2)) is V14() real ext-real Element of REAL
(r2 - (r2 + ((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2))) ^2 is V14() real ext-real Element of REAL
K46((r2 - (r2 + ((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2))),(r2 - (r2 + ((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2)))) is V14() real ext-real set
s2 - s2 is V14() real ext-real Element of REAL
(s2 - s2) ^2 is V14() real ext-real Element of REAL
K46((s2 - s2),(s2 - s2)) is V14() real ext-real set
((r2 - (r2 + ((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2))) ^2) + ((s2 - s2) ^2) is V14() real ext-real Element of REAL
sqrt (((r2 - (r2 + ((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2))) ^2) + ((s2 - s2) ^2)) is V14() real ext-real Element of REAL
p `1 is V14() real ext-real Element of REAL
p `2 is V14() real ext-real Element of REAL
Ball (u,r) is Element of bool the carrier of (Euclid 2)
(Int (cell (G,i,j))) /\ G0 is Element of bool the carrier of (TOP-REAL 2)
{} (TOP-REAL 2) is empty proper closed V110() V111() V112() V113() V114() V115() V116() symmetric circled Element of bool the carrier of (TOP-REAL 2)
((G * ((i + 1),1)) `1) - ((G * (i,1)) `1) is V14() real ext-real Element of REAL
((G * (1,(j + 1))) `2) - ((G * (1,j)) `2) is V14() real ext-real Element of REAL
r is V14() real ext-real Element of REAL
min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2))) is V14() real ext-real Element of REAL
min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1))) is V14() real ext-real Element of REAL
(min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2 is V14() real ext-real Element of REAL
r2 + ((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2) is V14() real ext-real Element of REAL
(min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2 is V14() real ext-real Element of REAL
s2 - ((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2) is V14() real ext-real Element of REAL
(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)) / 2 is V14() real ext-real Element of REAL
((G * (i,1)) `1) + ((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2) is V14() real ext-real Element of REAL
((G * (i,1)) `1) + ((((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)) / 2) is V14() real ext-real Element of REAL
(((G * (i,1)) `1) + ((((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)) / 2)) + ((((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)) / 2) is V14() real ext-real Element of REAL
(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)) / 2 is V14() real ext-real Element of REAL
((G * (1,(j + 1))) `2) - ((((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)) / 2) is V14() real ext-real Element of REAL
((G * (1,(j + 1))) `2) - ((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2) is V14() real ext-real Element of REAL
|[(r2 + ((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2)),(s2 - ((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2))]| is V43(2) V100() FinSequence-like Element of the carrier of (TOP-REAL 2)
q0 is V43(2) V100() FinSequence-like Element of the carrier of (TOP-REAL 2)
q0 `1 is V14() real ext-real Element of REAL
q0 `2 is V14() real ext-real Element of REAL
u0 is Element of the carrier of (Euclid 2)
r / 2 is V14() real ext-real Element of REAL
((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2) ^2 is V14() real ext-real Element of REAL
K46(((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2),((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2)) is V14() real ext-real set
(r / 2) ^2 is V14() real ext-real Element of REAL
K46((r / 2),(r / 2)) is V14() real ext-real set
((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2) ^2 is V14() real ext-real Element of REAL
K46(((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2),((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2)) is V14() real ext-real set
(((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2) ^2) + (((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2) ^2) is V14() real ext-real Element of REAL
((r / 2) ^2) + ((r / 2) ^2) is V14() real ext-real Element of REAL
(sqrt 2) / 2 is V14() real ext-real Element of REAL
r * 1 is V14() real ext-real Element of REAL
r * ((sqrt 2) / 2) is V14() real ext-real Element of REAL
2 * ((r / 2) ^2) is V14() real ext-real Element of REAL
(sqrt 2) ^2 is V14() real ext-real Element of REAL
K46((sqrt 2),(sqrt 2)) is V14() real ext-real set
((sqrt 2) ^2) * ((r / 2) ^2) is V14() real ext-real Element of REAL
(r / 2) * (sqrt 2) is V14() real ext-real Element of REAL
((r / 2) * (sqrt 2)) ^2 is V14() real ext-real Element of REAL
K46(((r / 2) * (sqrt 2)),((r / 2) * (sqrt 2))) is V14() real ext-real set
sqrt (((r / 2) ^2) + ((r / 2) ^2)) is V14() real ext-real Element of REAL
p `1 is V14() real ext-real Element of REAL
p `2 is V14() real ext-real Element of REAL
sqrt ((((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2) ^2) + (((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2) ^2)) is V14() real ext-real Element of REAL
dist (u,u0) is V14() real ext-real Element of REAL
v is V43(2) Element of REAL 2
v0 is V43(2) Element of REAL 2
(Pitag_dist 2) . (v,v0) is V14() real ext-real Element of REAL
r2 - (r2 + ((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2)) is V14() real ext-real Element of REAL
(r2 - (r2 + ((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2))) ^2 is V14() real ext-real Element of REAL
K46((r2 - (r2 + ((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2))),(r2 - (r2 + ((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2)))) is V14() real ext-real set
s2 - (s2 - ((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2)) is V14() real ext-real Element of REAL
(s2 - (s2 - ((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2))) ^2 is V14() real ext-real Element of REAL
K46((s2 - (s2 - ((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2))),(s2 - (s2 - ((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2)))) is V14() real ext-real set
((r2 - (r2 + ((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2))) ^2) + ((s2 - (s2 - ((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2))) ^2) is V14() real ext-real Element of REAL
sqrt (((r2 - (r2 + ((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2))) ^2) + ((s2 - (s2 - ((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2))) ^2)) is V14() real ext-real Element of REAL
Ball (u,r) is Element of bool the carrier of (Euclid 2)
(((G * (1,(j + 1))) `2) - ((((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)) / 2)) - ((((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)) / 2) is V14() real ext-real Element of REAL
{ |[b₁,b₂]| where b₁, b₂ is V14() real ext-real Element of REAL : ( not b₁ <= (G * (i,1)) `1 & not (G * ((i + 1),1)) `1 <= b₁ & not b₂ <= (G * (1,j)) `2 & not (G * (1,(j + 1))) `2 <= b₂ ) } is set
(Int (cell (G,i,j))) /\ G0 is Element of bool the carrier of (TOP-REAL 2)
{} (TOP-REAL 2) is empty proper closed V110() V111() V112() V113() V114() V115() V116() symmetric circled Element of bool the carrier of (TOP-REAL 2)
((G * (1,(j + 1))) `2) - ((G * (1,j)) `2) is V14() real ext-real Element of REAL
r is V14() real ext-real Element of REAL
min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2))) is V14() real ext-real Element of REAL
(min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2 is V14() real ext-real Element of REAL
s2 + ((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2) is V14() real ext-real Element of REAL
|[r2,(s2 + ((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2))]| is V43(2) V100() FinSequence-like Element of the carrier of (TOP-REAL 2)
r3 is V43(2) V100() FinSequence-like Element of the carrier of (TOP-REAL 2)
(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)) / 2 is V14() real ext-real Element of REAL
((G * (1,j)) `2) + ((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2) is V14() real ext-real Element of REAL
((G * (1,j)) `2) + ((((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)) / 2) is V14() real ext-real Element of REAL
(((G * (1,j)) `2) + ((((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)) / 2)) + ((((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)) / 2) is V14() real ext-real Element of REAL
s3 is Element of the carrier of (Euclid 2)
{ |[b<sub>1</sub>,b<sub>2</sub>]| where b<sub>1</sub>, b<sub>2</sub> is V14() real ext-real Element of REAL : ( not b<sub>1</sub> <= (G * (i,1)) `1 & not (G * ((i + 1),1)) `1 <= b<sub>1</sub> & not b<sub>2</sub> <= (G * (1,j)) `2 & not (G * (1,(j + 1))) `2 <= b<sub>2</sub> ) } is set
(sqrt 2) / 2 is V14() real ext-real Element of REAL
r * 1 is V14() real ext-real Element of REAL
r * ((sqrt 2) / 2) is V14() real ext-real Element of REAL
((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2) ^2 is V14() real ext-real Element of REAL
K46(((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2),((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2)) is V14() real ext-real set
r / 2 is V14() real ext-real Element of REAL
0 ^2 is V14() real ext-real Element of REAL
K46(0,0) is empty V14() real ext-real non positive non negative V110() V111() V112() V113() V114() V115() V116() set
(((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2) ^2) + (0 ^2) is V14() real ext-real Element of REAL
(r / 2) ^2 is V14() real ext-real Element of REAL
K46((r / 2),(r / 2)) is V14() real ext-real set
((r / 2) ^2) + (0 ^2) is V14() real ext-real Element of REAL
(0 ^2) + (((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2) ^2) is V14() real ext-real Element of REAL
sqrt ((0 ^2) + (((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2) ^2)) is V14() real ext-real Element of REAL
(0 ^2) + ((r / 2) ^2) is V14() real ext-real Element of REAL
sqrt ((0 ^2) + ((r / 2) ^2)) is V14() real ext-real Element of REAL
r3 `1 is V14() real ext-real Element of REAL
r3 `2 is V14() real ext-real Element of REAL
((r / 2) ^2) + ((r / 2) ^2) is V14() real ext-real Element of REAL
sqrt (((r / 2) ^2) + ((r / 2) ^2)) is V14() real ext-real Element of REAL
2 * ((r / 2) ^2) is V14() real ext-real Element of REAL
(sqrt 2) ^2 is V14() real ext-real Element of REAL
K46((sqrt 2),(sqrt 2)) is V14() real ext-real set
((sqrt 2) ^2) * ((r / 2) ^2) is V14() real ext-real Element of REAL
(r / 2) * (sqrt 2) is V14() real ext-real Element of REAL
((r / 2) * (sqrt 2)) ^2 is V14() real ext-real Element of REAL
K46(((r / 2) * (sqrt 2)),((r / 2) * (sqrt 2))) is V14() real ext-real set
dist (u,s3) is V14() real ext-real Element of REAL
v is V43(2) Element of REAL 2
q0 is V43(2) Element of REAL 2
(Pitag_dist 2) . (v,q0) is V14() real ext-real Element of REAL
r2 - r2 is V14() real ext-real Element of REAL
(r2 - r2) ^2 is V14() real ext-real Element of REAL
K46((r2 - r2),(r2 - r2)) is V14() real ext-real set
s2 - (s2 + ((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2)) is V14() real ext-real Element of REAL
(s2 - (s2 + ((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2))) ^2 is V14() real ext-real Element of REAL
K46((s2 - (s2 + ((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2))),(s2 - (s2 + ((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2)))) is V14() real ext-real set
((r2 - r2) ^2) + ((s2 - (s2 + ((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2))) ^2) is V14() real ext-real Element of REAL
sqrt (((r2 - r2) ^2) + ((s2 - (s2 + ((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2))) ^2)) is V14() real ext-real Element of REAL
p `1 is V14() real ext-real Element of REAL
p `2 is V14() real ext-real Element of REAL
Ball (u,r) is Element of bool the carrier of (Euclid 2)
(Int (cell (G,i,j))) /\ G0 is Element of bool the carrier of (TOP-REAL 2)
{} (TOP-REAL 2) is empty proper closed V110() V111() V112() V113() V114() V115() V116() symmetric circled Element of bool the carrier of (TOP-REAL 2)
rm is V43(2) V100() FinSequence-like Element of the carrier of (TOP-REAL 2)
rm `1 is V14() real ext-real Element of REAL
rm `2 is V14() real ext-real Element of REAL
rm1 is Element of the carrier of (Euclid 2)
dist (u,rm1) is V14() real ext-real Element of REAL
v is V43(2) Element of REAL 2
r3 is V43(2) Element of REAL 2
(Pitag_dist 2) . (v,r3) is V14() real ext-real Element of REAL
r is V14() real ext-real Element of REAL
r2 - r2 is V14() real ext-real Element of REAL
(r2 - r2) ^2 is V14() real ext-real Element of REAL
K46((r2 - r2),(r2 - r2)) is V14() real ext-real set
s2 - s2 is V14() real ext-real Element of REAL
(s2 - s2) ^2 is V14() real ext-real Element of REAL
K46((s2 - s2),(s2 - s2)) is V14() real ext-real set
((r2 - r2) ^2) + ((s2 - s2) ^2) is V14() real ext-real Element of REAL
sqrt (((r2 - r2) ^2) + ((s2 - s2) ^2)) is V14() real ext-real Element of REAL
Ball (u,r) is Element of bool the carrier of (Euclid 2)
{ |[b<sub>1</sub>,b<sub>2</sub>]| where b<sub>1</sub>, b<sub>2</sub> is V14() real ext-real Element of REAL : ( not b<sub>1</sub> <= (G * (i,1)) `1 & not (G * ((i + 1),1)) `1 <= b<sub>1</sub> & not b<sub>2</sub> <= (G * (1,j)) `2 & not (G * (1,(j + 1))) `2 <= b<sub>2</sub> ) } is set
(Int (cell (G,i,j))) /\ G0 is Element of bool the carrier of (TOP-REAL 2)
{} (TOP-REAL 2) is empty proper closed V110() V111() V112() V113() V114() V115() V116() symmetric circled Element of bool the carrier of (TOP-REAL 2)
((G * (1,(j + 1))) `2) - ((G * (1,j)) `2) is V14() real ext-real Element of REAL
r is V14() real ext-real Element of REAL
min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2))) is V14() real ext-real Element of REAL
(min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2 is V14() real ext-real Element of REAL
s2 - ((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2) is V14() real ext-real Element of REAL
|[r2,(s2 - ((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2))]| is V43(2) V100() FinSequence-like Element of the carrier of (TOP-REAL 2)
r3 is V43(2) V100() FinSequence-like Element of the carrier of (TOP-REAL 2)
(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)) / 2 is V14() real ext-real Element of REAL
((G * (1,(j + 1))) `2) - ((((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)) / 2) is V14() real ext-real Element of REAL
((G * (1,(j + 1))) `2) - ((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2) is V14() real ext-real Element of REAL
(((G * (1,(j + 1))) `2) - ((((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)) / 2)) - ((((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)) / 2) is V14() real ext-real Element of REAL
s3 is Element of the carrier of (Euclid 2)
{ |[b₁,b₂]| where b₁, b₂ is V14() real ext-real Element of REAL : ( not b₁ <= (G * (i,1)) `1 & not (G * ((i + 1),1)) `1 <= b₁ & not b₂ <= (G * (1,j)) `2 & not (G * (1,(j + 1))) `2 <= b₂ ) } is set
(sqrt 2) / 2 is V14() real ext-real Element of REAL
r * 1 is V14() real ext-real Element of REAL
r * ((sqrt 2) / 2) is V14() real ext-real Element of REAL
((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2) ^2 is V14() real ext-real Element of REAL
K46(((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2),((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2)) is V14() real ext-real set
r / 2 is V14() real ext-real Element of REAL
0 ^2 is V14() real ext-real Element of REAL
K46(0,0) is empty V14() real ext-real non positive non negative V110() V111() V112() V113() V114() V115() V116() set
(((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2) ^2) + (0 ^2) is V14() real ext-real Element of REAL
(r / 2) ^2 is V14() real ext-real Element of REAL
K46((r / 2),(r / 2)) is V14() real ext-real set
((r / 2) ^2) + (0 ^2) is V14() real ext-real Element of REAL
(0 ^2) + (((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2) ^2) is V14() real ext-real Element of REAL
sqrt ((0 ^2) + (((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2) ^2)) is V14() real ext-real Element of REAL
(0 ^2) + ((r / 2) ^2) is V14() real ext-real Element of REAL
sqrt ((0 ^2) + ((r / 2) ^2)) is V14() real ext-real Element of REAL
r3 `1 is V14() real ext-real Element of REAL
r3 `2 is V14() real ext-real Element of REAL
0 + ((r / 2) ^2) is V14() real ext-real Element of REAL
((r / 2) ^2) + ((r / 2) ^2) is V14() real ext-real Element of REAL
sqrt (((r / 2) ^2) + ((r / 2) ^2)) is V14() real ext-real Element of REAL
2 * ((r / 2) ^2) is V14() real ext-real Element of REAL
(sqrt 2) ^2 is V14() real ext-real Element of REAL
K46((sqrt 2),(sqrt 2)) is V14() real ext-real set
((sqrt 2) ^2) * ((r / 2) ^2) is V14() real ext-real Element of REAL
(r / 2) * (sqrt 2) is V14() real ext-real Element of REAL
((r / 2) * (sqrt 2)) ^2 is V14() real ext-real Element of REAL
K46(((r / 2) * (sqrt 2)),((r / 2) * (sqrt 2))) is V14() real ext-real set
dist (u,s3) is V14() real ext-real Element of REAL
v is V43(2) Element of REAL 2
q0 is V43(2) Element of REAL 2
(Pitag_dist 2) . (v,q0) is V14() real ext-real Element of REAL
r2 - r2 is V14() real ext-real Element of REAL
(r2 - r2) ^2 is V14() real ext-real Element of REAL
K46((r2 - r2),(r2 - r2)) is V14() real ext-real set
s2 - (s2 - ((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2)) is V14() real ext-real Element of REAL
(s2 - (s2 - ((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2))) ^2 is V14() real ext-real Element of REAL
K46((s2 - (s2 - ((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2))),(s2 - (s2 - ((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2)))) is V14() real ext-real set
((r2 - r2) ^2) + ((s2 - (s2 - ((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2))) ^2) is V14() real ext-real Element of REAL
sqrt (((r2 - r2) ^2) + ((s2 - (s2 - ((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2))) ^2)) is V14() real ext-real Element of REAL
p `1 is V14() real ext-real Element of REAL
p `2 is V14() real ext-real Element of REAL
Ball (u,r) is Element of bool the carrier of (Euclid 2)
(Int (cell (G,i,j))) /\ G0 is Element of bool the carrier of (TOP-REAL 2)
{} (TOP-REAL 2) is empty proper closed V110() V111() V112() V113() V114() V115() V116() symmetric circled Element of bool the carrier of (TOP-REAL 2)
((G * ((i + 1),1)) `1) - ((G * (i,1)) `1) is V14() real ext-real Element of REAL
((G * (1,(j + 1))) `2) - ((G * (1,j)) `2) is V14() real ext-real Element of REAL
r is V14() real ext-real Element of REAL
min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2))) is V14() real ext-real Element of REAL
min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1))) is V14() real ext-real Element of REAL
(min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2 is V14() real ext-real Element of REAL
r2 - ((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2) is V14() real ext-real Element of REAL
(min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2 is V14() real ext-real Element of REAL
s2 + ((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2) is V14() real ext-real Element of REAL
(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)) / 2 is V14() real ext-real Element of REAL
((G * ((i + 1),1)) `1) - ((((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)) / 2) is V14() real ext-real Element of REAL
((G * ((i + 1),1)) `1) - ((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2) is V14() real ext-real Element of REAL
(((G * ((i + 1),1)) `1) - ((((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)) / 2)) - ((((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)) / 2) is V14() real ext-real Element of REAL
(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)) / 2 is V14() real ext-real Element of REAL
((G * (1,j)) `2) + ((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2) is V14() real ext-real Element of REAL
((G * (1,j)) `2) + ((((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)) / 2) is V14() real ext-real Element of REAL
|[(r2 - ((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2)),(s2 + ((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2))]| is V43(2) V100() FinSequence-like Element of the carrier of (TOP-REAL 2)
q0 is V43(2) V100() FinSequence-like Element of the carrier of (TOP-REAL 2)
q0 `1 is V14() real ext-real Element of REAL
q0 `2 is V14() real ext-real Element of REAL
u0 is Element of the carrier of (Euclid 2)
r / 2 is V14() real ext-real Element of REAL
((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2) ^2 is V14() real ext-real Element of REAL
K46(((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2),((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2)) is V14() real ext-real set
(r / 2) ^2 is V14() real ext-real Element of REAL
K46((r / 2),(r / 2)) is V14() real ext-real set
((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2) ^2 is V14() real ext-real Element of REAL
K46(((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2),((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2)) is V14() real ext-real set
(((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2) ^2) + (((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2) ^2) is V14() real ext-real Element of REAL
((r / 2) ^2) + ((r / 2) ^2) is V14() real ext-real Element of REAL
(sqrt 2) / 2 is V14() real ext-real Element of REAL
r * 1 is V14() real ext-real Element of REAL
r * ((sqrt 2) / 2) is V14() real ext-real Element of REAL
2 * ((r / 2) ^2) is V14() real ext-real Element of REAL
(sqrt 2) ^2 is V14() real ext-real Element of REAL
K46((sqrt 2),(sqrt 2)) is V14() real ext-real set
((sqrt 2) ^2) * ((r / 2) ^2) is V14() real ext-real Element of REAL
(r / 2) * (sqrt 2) is V14() real ext-real Element of REAL
((r / 2) * (sqrt 2)) ^2 is V14() real ext-real Element of REAL
K46(((r / 2) * (sqrt 2)),((r / 2) * (sqrt 2))) is V14() real ext-real set
sqrt (((r / 2) ^2) + ((r / 2) ^2)) is V14() real ext-real Element of REAL
p `1 is V14() real ext-real Element of REAL
p `2 is V14() real ext-real Element of REAL
sqrt ((((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2) ^2) + (((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2) ^2)) is V14() real ext-real Element of REAL
dist (u,u0) is V14() real ext-real Element of REAL
v is V43(2) Element of REAL 2
v0 is V43(2) Element of REAL 2
(Pitag_dist 2) . (v,v0) is V14() real ext-real Element of REAL
r2 - (r2 - ((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2)) is V14() real ext-real Element of REAL
(r2 - (r2 - ((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2))) ^2 is V14() real ext-real Element of REAL
K46((r2 - (r2 - ((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2))),(r2 - (r2 - ((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2)))) is V14() real ext-real set
s2 - (s2 + ((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2)) is V14() real ext-real Element of REAL
(s2 - (s2 + ((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2))) ^2 is V14() real ext-real Element of REAL
K46((s2 - (s2 + ((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2))),(s2 - (s2 + ((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2)))) is V14() real ext-real set
((r2 - (r2 - ((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2))) ^2) + ((s2 - (s2 + ((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2))) ^2) is V14() real ext-real Element of REAL
sqrt (((r2 - (r2 - ((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2))) ^2) + ((s2 - (s2 + ((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2))) ^2)) is V14() real ext-real Element of REAL
Ball (u,r) is Element of bool the carrier of (Euclid 2)
(((G * (1,j)) `2) + ((((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)) / 2)) + ((((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)) / 2) is V14() real ext-real Element of REAL
{ |[b₁,b₂]| where b₁, b₂ is V14() real ext-real Element of REAL : ( not b₁ <= (G * (i,1)) `1 & not (G * ((i + 1),1)) `1 <= b₁ & not b₂ <= (G * (1,j)) `2 & not (G * (1,(j + 1))) `2 <= b₂ ) } is set
(Int (cell (G,i,j))) /\ G0 is Element of bool the carrier of (TOP-REAL 2)
{} (TOP-REAL 2) is empty proper closed V110() V111() V112() V113() V114() V115() V116() symmetric circled Element of bool the carrier of (TOP-REAL 2)
((G * ((i + 1),1)) `1) - ((G * (i,1)) `1) is V14() real ext-real Element of REAL
r is V14() real ext-real Element of REAL
min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1))) is V14() real ext-real Element of REAL
(min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2 is V14() real ext-real Element of REAL
r2 - ((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2) is V14() real ext-real Element of REAL
|[(r2 - ((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2)),s2]| is V43(2) V100() FinSequence-like Element of the carrier of (TOP-REAL 2)
r3 is V43(2) V100() FinSequence-like Element of the carrier of (TOP-REAL 2)
(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)) / 2 is V14() real ext-real Element of REAL
((G * ((i + 1),1)) `1) - ((((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)) / 2) is V14() real ext-real Element of REAL
((G * ((i + 1),1)) `1) - ((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2) is V14() real ext-real Element of REAL
(((G * ((i + 1),1)) `1) - ((((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)) / 2)) - ((((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)) / 2) is V14() real ext-real Element of REAL
s3 is Element of the carrier of (Euclid 2)
{ |[b<sub>1</sub>,b<sub>2</sub>]| where b<sub>1</sub>, b<sub>2</sub> is V14() real ext-real Element of REAL : ( not b<sub>1</sub> <= (G * (i,1)) `1 & not (G * ((i + 1),1)) `1 <= b<sub>1</sub> & not b<sub>2</sub> <= (G * (1,j)) `2 & not (G * (1,(j + 1))) `2 <= b<sub>2</sub> ) } is set
(sqrt 2) / 2 is V14() real ext-real Element of REAL
r * 1 is V14() real ext-real Element of REAL
r * ((sqrt 2) / 2) is V14() real ext-real Element of REAL
((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2) ^2 is V14() real ext-real Element of REAL
K46(((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2),((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2)) is V14() real ext-real set
r / 2 is V14() real ext-real Element of REAL
0 ^2 is V14() real ext-real Element of REAL
K46(0,0) is empty V14() real ext-real non positive non negative V110() V111() V112() V113() V114() V115() V116() set
(0 ^2) + (((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2) ^2) is V14() real ext-real Element of REAL
(r / 2) ^2 is V14() real ext-real Element of REAL
K46((r / 2),(r / 2)) is V14() real ext-real set
(0 ^2) + ((r / 2) ^2) is V14() real ext-real Element of REAL
(((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2) ^2) + (0 ^2) is V14() real ext-real Element of REAL
sqrt ((((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2) ^2) + (0 ^2)) is V14() real ext-real Element of REAL
((r / 2) ^2) + (0 ^2) is V14() real ext-real Element of REAL
sqrt (((r / 2) ^2) + (0 ^2)) is V14() real ext-real Element of REAL
r3 `1 is V14() real ext-real Element of REAL
r3 `2 is V14() real ext-real Element of REAL
((r / 2) ^2) + 0 is V14() real ext-real Element of REAL
((r / 2) ^2) + ((r / 2) ^2) is V14() real ext-real Element of REAL
sqrt (((r / 2) ^2) + ((r / 2) ^2)) is V14() real ext-real Element of REAL
2 * ((r / 2) ^2) is V14() real ext-real Element of REAL
(sqrt 2) ^2 is V14() real ext-real Element of REAL
K46((sqrt 2),(sqrt 2)) is V14() real ext-real set
((sqrt 2) ^2) * ((r / 2) ^2) is V14() real ext-real Element of REAL
(r / 2) * (sqrt 2) is V14() real ext-real Element of REAL
((r / 2) * (sqrt 2)) ^2 is V14() real ext-real Element of REAL
K46(((r / 2) * (sqrt 2)),((r / 2) * (sqrt 2))) is V14() real ext-real set
dist (u,s3) is V14() real ext-real Element of REAL
v is V43(2) Element of REAL 2
q0 is V43(2) Element of REAL 2
(Pitag_dist 2) . (v,q0) is V14() real ext-real Element of REAL
r2 - (r2 - ((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2)) is V14() real ext-real Element of REAL
(r2 - (r2 - ((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2))) ^2 is V14() real ext-real Element of REAL
K46((r2 - (r2 - ((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2))),(r2 - (r2 - ((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2)))) is V14() real ext-real set
s2 - s2 is V14() real ext-real Element of REAL
(s2 - s2) ^2 is V14() real ext-real Element of REAL
K46((s2 - s2),(s2 - s2)) is V14() real ext-real set
((r2 - (r2 - ((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2))) ^2) + ((s2 - s2) ^2) is V14() real ext-real Element of REAL
sqrt (((r2 - (r2 - ((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2))) ^2) + ((s2 - s2) ^2)) is V14() real ext-real Element of REAL
p `1 is V14() real ext-real Element of REAL
p `2 is V14() real ext-real Element of REAL
Ball (u,r) is Element of bool the carrier of (Euclid 2)
(Int (cell (G,i,j))) /\ G0 is Element of bool the carrier of (TOP-REAL 2)
{} (TOP-REAL 2) is empty proper closed V110() V111() V112() V113() V114() V115() V116() symmetric circled Element of bool the carrier of (TOP-REAL 2)
((G * ((i + 1),1)) `1) - ((G * (i,1)) `1) is V14() real ext-real Element of REAL
((G * (1,(j + 1))) `2) - ((G * (1,j)) `2) is V14() real ext-real Element of REAL
r is V14() real ext-real Element of REAL
min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2))) is V14() real ext-real Element of REAL
min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1))) is V14() real ext-real Element of REAL
(min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2 is V14() real ext-real Element of REAL
r2 - ((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2) is V14() real ext-real Element of REAL
(min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2 is V14() real ext-real Element of REAL
s2 - ((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2) is V14() real ext-real Element of REAL
(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)) / 2 is V14() real ext-real Element of REAL
((G * ((i + 1),1)) `1) - ((((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)) / 2) is V14() real ext-real Element of REAL
((G * ((i + 1),1)) `1) - ((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2) is V14() real ext-real Element of REAL
(((G * ((i + 1),1)) `1) - ((((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)) / 2)) - ((((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)) / 2) is V14() real ext-real Element of REAL
(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)) / 2 is V14() real ext-real Element of REAL
((G * (1,(j + 1))) `2) - ((((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)) / 2) is V14() real ext-real Element of REAL
((G * (1,(j + 1))) `2) - ((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2) is V14() real ext-real Element of REAL
(sqrt 2) / 2 is V14() real ext-real Element of REAL
r * 1 is V14() real ext-real Element of REAL
r * ((sqrt 2) / 2) is V14() real ext-real Element of REAL
p `1 is V14() real ext-real Element of REAL
p `2 is V14() real ext-real Element of REAL
r / 2 is V14() real ext-real Element of REAL
(r / 2) ^2 is V14() real ext-real Element of REAL
K46((r / 2),(r / 2)) is V14() real ext-real set
((r / 2) ^2) + ((r / 2) ^2) is V14() real ext-real Element of REAL
2 * ((r / 2) ^2) is V14() real ext-real Element of REAL
(sqrt 2) ^2 is V14() real ext-real Element of REAL
K46((sqrt 2),(sqrt 2)) is V14() real ext-real set
((sqrt 2) ^2) * ((r / 2) ^2) is V14() real ext-real Element of REAL
(r / 2) * (sqrt 2) is V14() real ext-real Element of REAL
((r / 2) * (sqrt 2)) ^2 is V14() real ext-real Element of REAL
K46(((r / 2) * (sqrt 2)),((r / 2) * (sqrt 2))) is V14() real ext-real set
sqrt (((r / 2) ^2) + ((r / 2) ^2)) is V14() real ext-real Element of REAL
((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2) ^2 is V14() real ext-real Element of REAL
K46(((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2),((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2)) is V14() real ext-real set
|[(r2 - ((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2)),(s2 - ((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2))]| is V43(2) V100() FinSequence-like Element of the carrier of (TOP-REAL 2)
q0 is V43(2) V100() FinSequence-like Element of the carrier of (TOP-REAL 2)
q0 `1 is V14() real ext-real Element of REAL
q0 `2 is V14() real ext-real Element of REAL
u0 is Element of the carrier of (Euclid 2)
r2 - (r2 - ((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2)) is V14() real ext-real Element of REAL
s2 - (s2 - ((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2)) is V14() real ext-real Element of REAL
((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2) ^2 is V14() real ext-real Element of REAL
K46(((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2),((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2)) is V14() real ext-real set
(((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2) ^2) + (((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2) ^2) is V14() real ext-real Element of REAL
sqrt ((((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2) ^2) + (((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2) ^2)) is V14() real ext-real Element of REAL
dist (u,u0) is V14() real ext-real Element of REAL
v is V43(2) Element of REAL 2
v0 is V43(2) Element of REAL 2
(Pitag_dist 2) . (v,v0) is V14() real ext-real Element of REAL
Ball (u,r) is Element of bool the carrier of (Euclid 2)
(((G * (1,(j + 1))) `2) - ((((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)) / 2)) - ((((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)) / 2) is V14() real ext-real Element of REAL
{ |[b<sub>1</sub>,b<sub>2</sub>]| where b<sub>1</sub>, b<sub>2</sub> is V14() real ext-real Element of REAL : ( not b<sub>1</sub> <= (G * (i,1)) `1 & not (G * ((i + 1),1)) `1 <= b<sub>1</sub> & not b<sub>2</sub> <= (G * (1,j)) `2 & not (G * (1,(j + 1))) `2 <= b₂ ) } is set
(Int (cell (G,i,j))) /\ G0 is Element of bool the carrier of (TOP-REAL 2)
{} (TOP-REAL 2) is empty proper closed V110() V111() V112() V113() V114() V115() V116() symmetric circled Element of bool the carrier of (TOP-REAL 2)
(Int (cell (G,i,j))) /\ G0 is Element of bool the carrier of (TOP-REAL 2)
{} (TOP-REAL 2) is empty proper closed V110() V111() V112() V113() V114() V115() V116() symmetric circled Element of bool the carrier of (TOP-REAL 2)
(Int (cell (G,i,j))) /\ G0 is Element of bool the carrier of (TOP-REAL 2)
{} (TOP-REAL 2) is empty proper closed V110() V111() V112() V113() V114() V115() V116() symmetric circled Element of bool the carrier of (TOP-REAL 2)
(Int (cell (G,i,j))) /\ G0 is Element of bool the carrier of (TOP-REAL 2)
{} (TOP-REAL 2) is empty proper closed V110() V111() V112() V113() V114() V115() V116() symmetric circled Element of bool the carrier of (TOP-REAL 2)
(Int (cell (G,i,j))) /\ G0 is Element of bool the carrier of (TOP-REAL 2)
{} (TOP-REAL 2) is empty proper closed V110() V111() V112() V113() V114() V115() V116() symmetric circled Element of bool the carrier of (TOP-REAL 2)
Cl (cell (G,i,j)) is Element of bool the carrier of (TOP-REAL 2)