REAL is non empty V38() V174() V175() V176() V180() set
NAT is V174() V175() V176() V177() V178() V179() V180() Element of K19(REAL)
K19(REAL) is non empty set
COMPLEX is non empty V38() V174() V180() set
omega is V174() V175() V176() V177() V178() V179() V180() set
K19(omega) is non empty set
K19(NAT) is non empty set
1 is non empty ordinal natural V28() real ext-real positive non negative integer V108() V174() V175() V176() V177() V178() V179() Element of NAT
K20(1,1) is non empty set
K19(K20(1,1)) is non empty set
K20(K20(1,1),1) is non empty set
K19(K20(K20(1,1),1)) is non empty set
K20(K20(1,1),REAL) is non empty set
K19(K20(K20(1,1),REAL)) is non empty set
K20(REAL,REAL) is non empty set
K20(K20(REAL,REAL),REAL) is non empty set
K19(K20(K20(REAL,REAL),REAL)) is non empty set
2 is non empty ordinal natural V28() real ext-real positive non negative integer V108() V174() V175() V176() V177() V178() V179() Element of NAT
K20(2,2) is non empty set
K20(K20(2,2),REAL) is non empty set
K19(K20(K20(2,2),REAL)) is non empty set
RAT is non empty V38() V174() V175() V176() V177() V180() set
INT is non empty V38() V174() V175() V176() V177() V178() V180() set
K19(K20(REAL,REAL)) is non empty set
K404() is non empty V123() L10()
the carrier of K404() is non empty set
K409() is non empty V123() V145() V146() V147() V149() V196() V197() V198() V199() V200() V201() L10()
K410() is non empty V123() V147() V149() V199() V200() V201() M15(K409())
K411() is non empty V123() V145() V147() V149() V199() V200() V201() V202() M18(K409(),K410())
K413() is non empty V123() V145() V147() V149() L10()
K414() is non empty V123() V145() V147() V149() V202() M15(K413())
TOP-REAL 2 is non empty V55() TopSpace-like V121() V186() V187() V204() V205() V206() V207() V208() V209() V210() strict add-continuous Mult-continuous RLTopStruct
the carrier of (TOP-REAL 2) is non empty V12() set
the carrier of (TOP-REAL 2) * is functional non empty FinSequence-membered FinSequenceSet of the carrier of (TOP-REAL 2)
K20( the carrier of (TOP-REAL 2),REAL) is non empty set
K19(K20( the carrier of (TOP-REAL 2),REAL)) is non empty set
K19( the carrier of (TOP-REAL 2)) is non empty set
K20(COMPLEX,COMPLEX) is non empty set
K19(K20(COMPLEX,COMPLEX)) is non empty set
K20(COMPLEX,REAL) is non empty set
K19(K20(COMPLEX,REAL)) is non empty set
K20(K20(COMPLEX,COMPLEX),COMPLEX) is non empty set
K19(K20(K20(COMPLEX,COMPLEX),COMPLEX)) is non empty set
K20(RAT,RAT) is non empty set
K19(K20(RAT,RAT)) is non empty set
K20(K20(RAT,RAT),RAT) is non empty set
K19(K20(K20(RAT,RAT),RAT)) is non empty set
K20(INT,INT) is non empty set
K19(K20(INT,INT)) is non empty set
K20(K20(INT,INT),INT) is non empty set
K19(K20(K20(INT,INT),INT)) is non empty set
K20(NAT,NAT) is set
K20(K20(NAT,NAT),NAT) is set
K19(K20(K20(NAT,NAT),NAT)) is non empty set
{} is Function-like functional empty V12() FinSequence-membered V174() V175() V176() V177() V178() V179() V180() set
the Function-like functional empty V12() FinSequence-membered V174() V175() V176() V177() V178() V179() V180() set is Function-like functional empty V12() FinSequence-membered V174() V175() V176() V177() V178() V179() V180() set
3 is non empty ordinal natural V28() real ext-real positive non negative integer V108() V174() V175() V176() V177() V178() V179() Element of NAT
0 is Function-like functional empty V12() ordinal natural V28() real ext-real non positive non negative integer FinSequence-membered V108() V174() V175() V176() V177() V178() V179() V180() Element of NAT
Seg 1 is non empty V38() V45(1) V174() V175() V176() V177() V178() V179() Element of K19(NAT)
{1} is non empty V12() V174() V175() V176() V177() V178() V179() set
Seg 2 is non empty V38() V45(2) V174() V175() V176() V177() V178() V179() Element of K19(NAT)
{1,2} is non empty V174() V175() V176() V177() V178() V179() set
4 is non empty ordinal natural V28() real ext-real positive non negative integer V108() V174() V175() V176() V177() V178() V179() Element of NAT
proj1 is Relation-like the carrier of (TOP-REAL 2) -defined REAL -valued Function-like V18( the carrier of (TOP-REAL 2), REAL ) V229( TOP-REAL 2) Element of K19(K20( the carrier of (TOP-REAL 2),REAL))
proj2 is Relation-like the carrier of (TOP-REAL 2) -defined REAL -valued Function-like V18( the carrier of (TOP-REAL 2), REAL ) V229( TOP-REAL 2) Element of K19(K20( the carrier of (TOP-REAL 2),REAL))
Euclid 2 is non empty strict Reflexive discerning symmetric triangle MetrStruct
REAL 2 is functional non empty FinSequence-membered FinSequenceSet of REAL
2 -tuples_on REAL is functional FinSequence-membered FinSequenceSet of REAL
Pitag_dist 2 is Relation-like K20((REAL 2),(REAL 2)) -defined REAL -valued Function-like V18(K20((REAL 2),(REAL 2)), REAL ) Element of K19(K20(K20((REAL 2),(REAL 2)),REAL))
K20((REAL 2),(REAL 2)) is non empty set
K20(K20((REAL 2),(REAL 2)),REAL) is non empty set
K19(K20(K20((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
0.REAL 2 is Relation-like NAT -defined Function-like V38() V45(2) FinSequence-like FinSubsequence-like V166() Element of the carrier of (TOP-REAL 2)
2 |-> 0 is Relation-like NAT -defined REAL -valued Function-like V38() FinSequence-like FinSubsequence-like Element of 2 -tuples_on REAL
g is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like non constant non empty V12() V38() FinSequence-like FinSubsequence-like circular special unfolded s.c.c. standard FinSequence of the carrier of (TOP-REAL 2)
L~ g is non empty boundary compact bounded non horizontal non vertical Element of K19( the carrier of (TOP-REAL 2))
A is Element of K19( the carrier of (TOP-REAL 2))
A is Element of the carrier of (Euclid 2)
K19( the carrier of (Euclid 2)) is non empty set
x is bounded Element of K19( the carrier of (Euclid 2))
x is V28() real ext-real Element of REAL
b is Element of the carrier of (Euclid 2)
dist (A,b) is V28() real ext-real Element of REAL
(dist (A,b)) + x is V28() real ext-real Element of REAL
((dist (A,b)) + x) + 1 is V28() real ext-real Element of REAL
Ball (A,(((dist (A,b)) + x) + 1)) is Element of K19( the carrier of (Euclid 2))
(Ball (A,(((dist (A,b)) + x) + 1))) ` is Element of K19( the carrier of (Euclid 2))
the carrier of (Euclid 2) \ (Ball (A,(((dist (A,b)) + x) + 1))) is set
{ b1 where b1 is Relation-like NAT -defined Function-like V38() V45(2) FinSequence-like FinSubsequence-like V166() Element of the carrier of (TOP-REAL 2) : not ((dist (A,b)) + x) + 1 <= |.b1.| } is set
(REAL 2) \ { b1 where b1 is Relation-like NAT -defined Function-like V38() V45(2) FinSequence-like FinSubsequence-like V166() Element of the carrier of (TOP-REAL 2) : not ((dist (A,b)) + x) + 1 <= |.b1.| } is functional FinSequence-membered Element of K19((REAL 2))
K19((REAL 2)) is non empty set
((dist (A,b)) + x) + 0 is V28() real ext-real Element of REAL
abs (((dist (A,b)) + x) + 1) is V28() real ext-real Element of REAL
|[0,(((dist (A,b)) + x) + 1)]| is Relation-like NAT -defined Function-like non empty V38() V45(2) FinSequence-like FinSubsequence-like V166() Element of the carrier of (TOP-REAL 2)
O is Relation-like NAT -defined Function-like V38() V45(2) FinSequence-like FinSubsequence-like V166() Element of the carrier of (TOP-REAL 2)
|.O.| is V28() real ext-real non negative Element of REAL
K391(O) is Relation-like NAT -defined REAL -valued Function-like V38() FinSequence-like FinSubsequence-like FinSequence of REAL
K397(K391(O)) is V28() real ext-real Element of REAL
sqrt K397(K391(O)) is V28() real ext-real Element of REAL
i is set
p2 is Element of the carrier of (Euclid 2)
dist (A,p2) is V28() real ext-real Element of REAL
x is Relation-like NAT -defined Function-like V38() V45(2) FinSequence-like FinSubsequence-like V166() Element of the carrier of (TOP-REAL 2)
|.x.| is V28() real ext-real non negative Element of REAL
K391(x) is Relation-like NAT -defined REAL -valued Function-like V38() FinSequence-like FinSubsequence-like FinSequence of REAL
K397(K391(x)) is V28() real ext-real Element of REAL
sqrt K397(K391(x)) is V28() real ext-real Element of REAL
p is set
q is Element of the carrier of (Euclid 2)
dist (b,q) is V28() real ext-real Element of REAL
(dist (A,b)) + (dist (b,q)) is V28() real ext-real Element of REAL
dist (A,q) is V28() real ext-real Element of REAL
O is non empty Element of K19( the carrier of (TOP-REAL 2))
(L~ g) ` is non empty Element of K19( the carrier of (TOP-REAL 2))
the carrier of (TOP-REAL 2) \ (L~ g) is set
p is set
q is Relation-like NAT -defined Function-like V38() V45(2) FinSequence-like FinSubsequence-like V166() Element of the carrier of (TOP-REAL 2)
|.q.| is V28() real ext-real non negative Element of REAL
K391(q) is Relation-like NAT -defined REAL -valued Function-like V38() FinSequence-like FinSubsequence-like FinSequence of REAL
K397(K391(q)) is V28() real ext-real Element of REAL
sqrt K397(K391(q)) is V28() real ext-real Element of REAL
t is Element of the carrier of (Euclid 2)
dist (t,A) is V28() real ext-real Element of REAL
p is Element of K19( the carrier of (TOP-REAL 2))
q is Element of K19( the carrier of (Euclid 2))
{ b1 where b1 is Element of K19( the carrier of (TOP-REAL 2)) : b1 is_outside_component_of L~ g } is set
q is Relation-like NAT -defined Function-like V38() V45(2) FinSequence-like FinSubsequence-like V166() Element of the carrier of (TOP-REAL 2)
|.q.| is V28() real ext-real non negative Element of REAL
K391(q) is Relation-like NAT -defined REAL -valued Function-like V38() FinSequence-like FinSubsequence-like FinSequence of REAL
K397(K391(q)) is V28() real ext-real Element of REAL
sqrt K397(K391(q)) is V28() real ext-real Element of REAL
UBD (L~ g) is non empty connected Element of K19( the carrier of (TOP-REAL 2))
union { b1 where b1 is Element of K19( the carrier of (TOP-REAL 2)) : b1 is_outside_component_of L~ g } is set
g is ordinal natural V28() real ext-real non negative integer V108() V174() V175() V176() V177() V178() V179() Element of NAT
TOP-REAL g is non empty TopSpace-like V121() V186() V187() V204() V205() V206() V207() V208() V209() V210() strict add-continuous Mult-continuous RLTopStruct
the carrier of (TOP-REAL g) is non empty set
A is Relation-like NAT -defined the carrier of (TOP-REAL g) -valued Function-like V38() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL g)
L~ A is Element of K19( the carrier of (TOP-REAL g))
K19( the carrier of (TOP-REAL g)) is non empty set
len A is ordinal natural V28() real ext-real non negative integer V108() V174() V175() V176() V177() V178() V179() Element of NAT
1 + 1 is non empty ordinal natural V28() real ext-real positive non negative integer V108() V174() V175() V176() V177() V178() V179() Element of NAT
g is ordinal natural V28() real ext-real non negative integer V108() V174() V175() V176() V177() V178() V179() Element of NAT
g + 1 is non empty ordinal natural V28() real ext-real positive non negative integer V108() V174() V175() V176() V177() V178() V179() Element of NAT
A is ordinal natural V28() real ext-real non negative integer V108() V174() V175() V176() V177() V178() V179() Element of NAT
A + 1 is non empty ordinal natural V28() real ext-real positive non negative integer V108() V174() V175() V176() V177() V178() V179() Element of NAT
A is Relation-like non empty-yielding NAT -defined the carrier of (TOP-REAL 2) * -valued Function-like V38() FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of the carrier of (TOP-REAL 2) *
len A is ordinal natural V28() real ext-real non negative integer V108() V174() V175() V176() V177() V178() V179() Element of NAT
width A is ordinal natural V28() real ext-real non negative integer V108() V174() V175() V176() V177() V178() V179() Element of NAT
cell (A,g,A) is Element of K19( the carrier of (TOP-REAL 2))
A * (g,1) is Relation-like NAT -defined Function-like V38() V45(2) FinSequence-like FinSubsequence-like V166() Element of the carrier of (TOP-REAL 2)
(A * (g,1)) `1 is V28() real ext-real Element of REAL
K526((A * (g,1)),1) is V28() real ext-real Element of REAL
A * ((g + 1),1) is Relation-like NAT -defined Function-like V38() V45(2) FinSequence-like FinSubsequence-like V166() Element of the carrier of (TOP-REAL 2)
(A * ((g + 1),1)) `1 is V28() real ext-real Element of REAL
K526((A * ((g + 1),1)),1) is V28() real ext-real Element of REAL
[.((A * (g,1)) `1),((A * ((g + 1),1)) `1).] is compact V174() V175() V176() real-bounded Element of K19(REAL)
A * (1,A) is Relation-like NAT -defined Function-like V38() V45(2) FinSequence-like FinSubsequence-like V166() Element of the carrier of (TOP-REAL 2)
(A * (1,A)) `2 is V28() real ext-real Element of REAL
K526((A * (1,A)),2) is V28() real ext-real Element of REAL
A * (1,(A + 1)) is Relation-like NAT -defined Function-like V38() V45(2) FinSequence-like FinSubsequence-like V166() Element of the carrier of (TOP-REAL 2)
(A * (1,(A + 1))) `2 is V28() real ext-real Element of REAL
K526((A * (1,(A + 1))),2) is V28() real ext-real Element of REAL
[.((A * (1,A)) `2),((A * (1,(A + 1))) `2).] is compact V174() V175() V176() real-bounded Element of K19(REAL)
(1,2) --> ([.((A * (g,1)) `1),((A * ((g + 1),1)) `1).],[.((A * (1,A)) `2),((A * (1,(A + 1))) `2).]) is Relation-like {1,2} -defined K19(REAL) -valued Function-like V18({1,2},K19(REAL)) Element of K19(K20({1,2},K19(REAL)))
K20({1,2},K19(REAL)) is non empty set
K19(K20({1,2},K19(REAL))) is non empty set
product ((1,2) --> ([.((A * (g,1)) `1),((A * ((g + 1),1)) `1).],[.((A * (1,A)) `2),((A * (1,(A + 1))) `2).])) is set
{ b1 where b1 is V28() real ext-real Element of REAL : ( (A * (1,A)) `2 <= b1 & b1 <= (A * (1,(A + 1))) `2 ) } is set
dom ((1,2) --> ([.((A * (g,1)) `1),((A * ((g + 1),1)) `1).],[.((A * (1,A)) `2),((A * (1,(A + 1))) `2).])) is V174() V175() V176() V177() V178() V179() Element of K19({1,2})
K19({1,2}) is non empty set
{ |[b1,b2]| where b1, b2 is V28() real ext-real Element of REAL : ( (A * (g,1)) `1 <= b1 & b1 <= (A * ((g + 1),1)) `1 & (A * (1,A)) `2 <= b2 & b2 <= (A * (1,(A + 1))) `2 ) } is set
{ b1 where b1 is V28() real ext-real Element of REAL : ( (A * (g,1)) `1 <= b1 & b1 <= (A * ((g + 1),1)) `1 ) } is set
x is set
b is V28() real ext-real Element of REAL
c is V28() real ext-real Element of REAL
|[b,c]| is Relation-like NAT -defined Function-like non empty V38() V45(2) FinSequence-like FinSubsequence-like V166() Element of the carrier of (TOP-REAL 2)
<*b,c*> is Relation-like NAT -defined Function-like non empty V38() V45(2) FinSequence-like FinSubsequence-like set
c is set
<*b,c*> . c is set
((1,2) --> ([.((A * (g,1)) `1),((A * ((g + 1),1)) `1).],[.((A * (1,A)) `2),((A * (1,(A + 1))) `2).])) . c is set
|[b,c]| `2 is V28() real ext-real Element of REAL
K526(|[b,c]|,2) is V28() real ext-real Element of REAL
<*b,c*> . 2 is set
|[b,c]| `1 is V28() real ext-real Element of REAL
K526(|[b,c]|,1) is V28() real ext-real Element of REAL
<*b,c*> . 1 is set
dom <*b,c*> is V174() V175() V176() V177() V178() V179() Element of K19(NAT)
x is set
b is Relation-like Function-like set
dom b is set
b . 2 is set
((1,2) --> ([.((A * (g,1)) `1),((A * ((g + 1),1)) `1).],[.((A * (1,A)) `2),((A * (1,(A + 1))) `2).])) . 2 is set
c is V28() real ext-real Element of REAL
b . 1 is set
((1,2) --> ([.((A * (g,1)) `1),((A * ((g + 1),1)) `1).],[.((A * (1,A)) `2),((A * (1,(A + 1))) `2).])) . 1 is set
c is V28() real ext-real Element of REAL
<*c,c*> is Relation-like NAT -defined Function-like non empty V38() V45(2) FinSequence-like FinSubsequence-like set
O is set
b . O is set
<*c,c*> . O is set
dom <*c,c*> is V174() V175() V176() V177() V178() V179() Element of K19(NAT)
|[c,c]| is Relation-like NAT -defined Function-like non empty V38() V45(2) FinSequence-like FinSubsequence-like V166() Element of the carrier of (TOP-REAL 2)
g is ordinal natural V28() real ext-real non negative integer V108() V174() V175() V176() V177() V178() V179() Element of NAT
A is ordinal natural V28() real ext-real non negative integer V108() V174() V175() V176() V177() V178() V179() Element of NAT
A is Relation-like non empty-yielding NAT -defined the carrier of (TOP-REAL 2) * -valued Function-like V38() FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of the carrier of (TOP-REAL 2) *
len A is ordinal natural V28() real ext-real non negative integer V108() V174() V175() V176() V177() V178() V179() Element of NAT
width A is ordinal natural V28() real ext-real non negative integer V108() V174() V175() V176() V177() V178() V179() Element of NAT
cell (A,g,A) is Element of K19( the carrier of (TOP-REAL 2))
A * (g,1) is Relation-like NAT -defined Function-like V38() V45(2) FinSequence-like FinSubsequence-like V166() Element of the carrier of (TOP-REAL 2)
(A * (g,1)) `1 is V28() real ext-real Element of REAL
K526((A * (g,1)),1) is V28() real ext-real Element of REAL
g + 1 is non empty ordinal natural V28() real ext-real positive non negative integer V108() V174() V175() V176() V177() V178() V179() Element of NAT
A * ((g + 1),1) is Relation-like NAT -defined Function-like V38() V45(2) FinSequence-like FinSubsequence-like V166() Element of the carrier of (TOP-REAL 2)
(A * ((g + 1),1)) `1 is V28() real ext-real Element of REAL
K526((A * ((g + 1),1)),1) is V28() real ext-real Element of REAL
[.((A * (g,1)) `1),((A * ((g + 1),1)) `1).] is compact V174() V175() V176() real-bounded Element of K19(REAL)
A * (1,A) is Relation-like NAT -defined Function-like V38() V45(2) FinSequence-like FinSubsequence-like V166() Element of the carrier of (TOP-REAL 2)
(A * (1,A)) `2 is V28() real ext-real Element of REAL
K526((A * (1,A)),2) is V28() real ext-real Element of REAL
A + 1 is non empty ordinal natural V28() real ext-real positive non negative integer V108() V174() V175() V176() V177() V178() V179() Element of NAT
A * (1,(A + 1)) is Relation-like NAT -defined Function-like V38() V45(2) FinSequence-like FinSubsequence-like V166() Element of the carrier of (TOP-REAL 2)
(A * (1,(A + 1))) `2 is V28() real ext-real Element of REAL
K526((A * (1,(A + 1))),2) is V28() real ext-real Element of REAL
[.((A * (1,A)) `2),((A * (1,(A + 1))) `2).] is compact V174() V175() V176() real-bounded Element of K19(REAL)
(1,2) --> ([.((A * (g,1)) `1),((A * ((g + 1),1)) `1).],[.((A * (1,A)) `2),((A * (1,(A + 1))) `2).]) is Relation-like {1,2} -defined K19(REAL) -valued Function-like V18({1,2},K19(REAL)) Element of K19(K20({1,2},K19(REAL)))
K20({1,2},K19(REAL)) is non empty set
K19(K20({1,2},K19(REAL))) is non empty set
product ((1,2) --> ([.((A * (g,1)) `1),((A * ((g + 1),1)) `1).],[.((A * (1,A)) `2),((A * (1,(A + 1))) `2).])) is set
g is ordinal natural V28() real ext-real non negative integer V108() V174() V175() V176() V177() V178() V179() Element of NAT
A is ordinal natural V28() real ext-real non negative integer V108() V174() V175() V176() V177() V178() V179() Element of NAT
[g,A] is non empty set
{g,A} is non empty V174() V175() V176() V177() V178() V179() set
{g} is non empty V12() V174() V175() V176() V177() V178() V179() set
{{g,A},{g}} is non empty set
A is ordinal natural V28() real ext-real non negative integer V108() V174() V175() V176() V177() V178() V179() Element of NAT
g + A is ordinal natural V28() real ext-real non negative integer V108() V174() V175() V176() V177() V178() V179() Element of NAT
[(g + A),A] is non empty set
{(g + A),A} is non empty V174() V175() V176() V177() V178() V179() set
{(g + A)} is non empty V12() V174() V175() V176() V177() V178() V179() set
{{(g + A),A},{(g + A)}} is non empty set
x is Relation-like non empty-yielding NAT -defined the carrier of (TOP-REAL 2) * -valued Function-like V38() FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of the carrier of (TOP-REAL 2) *
Indices x is set
x * (g,A) is Relation-like NAT -defined Function-like V38() V45(2) FinSequence-like FinSubsequence-like V166() Element of the carrier of (TOP-REAL 2)
x * ((g + A),A) is Relation-like NAT -defined Function-like V38() V45(2) FinSequence-like FinSubsequence-like V166() Element of the carrier of (TOP-REAL 2)
dist ((x * (g,A)),(x * ((g + A),A))) is V28() real ext-real Element of REAL
(x * ((g + A),A)) `1 is V28() real ext-real Element of REAL
K526((x * ((g + A),A)),1) is V28() real ext-real Element of REAL
(x * (g,A)) `1 is V28() real ext-real Element of REAL
K526((x * (g,A)),1) is V28() real ext-real Element of REAL
((x * ((g + A),A)) `1) - ((x * (g,A)) `1) is V28() real ext-real Element of REAL
len x is ordinal natural V28() real ext-real non negative integer V108() V174() V175() V176() V177() V178() V179() Element of NAT
width x is ordinal natural V28() real ext-real non negative integer V108() V174() V175() V176() V177() V178() V179() Element of NAT
((x * (g,A)) `1) - ((x * (g,A)) `1) is V28() real ext-real Element of REAL
(x * (g,A)) `2 is V28() real ext-real Element of REAL
K526((x * (g,A)),2) is V28() real ext-real Element of REAL
x * (1,A) is Relation-like NAT -defined Function-like V38() V45(2) FinSequence-like FinSubsequence-like V166() Element of the carrier of (TOP-REAL 2)
(x * (1,A)) `2 is V28() real ext-real Element of REAL
K526((x * (1,A)),2) is V28() real ext-real Element of REAL
(x * ((g + A),A)) `2 is V28() real ext-real Element of REAL
K526((x * ((g + A),A)),2) is V28() real ext-real Element of REAL
((x * (g,A)) `1) - ((x * ((g + A),A)) `1) is V28() real ext-real Element of REAL
(((x * (g,A)) `1) - ((x * ((g + A),A)) `1)) ^2 is V28() real ext-real Element of REAL
K104((((x * (g,A)) `1) - ((x * ((g + A),A)) `1)),(((x * (g,A)) `1) - ((x * ((g + A),A)) `1))) is V28() real ext-real set
((x * (g,A)) `2) - ((x * ((g + A),A)) `2) is V28() real ext-real Element of REAL
(((x * (g,A)) `2) - ((x * ((g + A),A)) `2)) ^2 is V28() real ext-real Element of REAL
K104((((x * (g,A)) `2) - ((x * ((g + A),A)) `2)),(((x * (g,A)) `2) - ((x * ((g + A),A)) `2))) is V28() real ext-real set
((((x * (g,A)) `1) - ((x * ((g + A),A)) `1)) ^2) + ((((x * (g,A)) `2) - ((x * ((g + A),A)) `2)) ^2) is V28() real ext-real Element of REAL
sqrt (((((x * (g,A)) `1) - ((x * ((g + A),A)) `1)) ^2) + ((((x * (g,A)) `2) - ((x * ((g + A),A)) `2)) ^2)) is V28() real ext-real Element of REAL
abs (((x * (g,A)) `1) - ((x * ((g + A),A)) `1)) is V28() real ext-real Element of REAL
- (((x * (g,A)) `1) - ((x * ((g + A),A)) `1)) is V28() real ext-real Element of REAL
abs (- (((x * (g,A)) `1) - ((x * ((g + A),A)) `1))) is V28() real ext-real Element of REAL
g is ordinal natural V28() real ext-real non negative integer V108() V174() V175() V176() V177() V178() V179() Element of NAT
A is ordinal natural V28() real ext-real non negative integer V108() V174() V175() V176() V177() V178() V179() Element of NAT
[g,A] is non empty set
{g,A} is non empty V174() V175() V176() V177() V178() V179() set
{g} is non empty V12() V174() V175() V176() V177() V178() V179() set
{{g,A},{g}} is non empty set
A is ordinal natural V28() real ext-real non negative integer V108() V174() V175() V176() V177() V178() V179() Element of NAT
A + A is ordinal natural V28() real ext-real non negative integer V108() V174() V175() V176() V177() V178() V179() Element of NAT
[g,(A + A)] is non empty set
{g,(A + A)} is non empty V174() V175() V176() V177() V178() V179() set
{{g,(A + A)},{g}} is non empty set
x is Relation-like non empty-yielding NAT -defined the carrier of (TOP-REAL 2) * -valued Function-like V38() FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of the carrier of (TOP-REAL 2) *
Indices x is set
x * (g,A) is Relation-like NAT -defined Function-like V38() V45(2) FinSequence-like FinSubsequence-like V166() Element of the carrier of (TOP-REAL 2)
x * (g,(A + A)) is Relation-like NAT -defined Function-like V38() V45(2) FinSequence-like FinSubsequence-like V166() Element of the carrier of (TOP-REAL 2)
dist ((x * (g,A)),(x * (g,(A + A)))) is V28() real ext-real Element of REAL
(x * (g,(A + A))) `2 is V28() real ext-real Element of REAL
K526((x * (g,(A + A))),2) is V28() real ext-real Element of REAL
(x * (g,A)) `2 is V28() real ext-real Element of REAL
K526((x * (g,A)),2) is V28() real ext-real Element of REAL
((x * (g,(A + A))) `2) - ((x * (g,A)) `2) is V28() real ext-real Element of REAL
width x is ordinal natural V28() real ext-real non negative integer V108() V174() V175() V176() V177() V178() V179() Element of NAT
len x is ordinal natural V28() real ext-real non negative integer V108() V174() V175() V176() V177() V178() V179() Element of NAT
((x * (g,A)) `2) - ((x * (g,A)) `2) is V28() real ext-real Element of REAL
(x * (g,A)) `1 is V28() real ext-real Element of REAL
K526((x * (g,A)),1) is V28() real ext-real Element of REAL
x * (g,1) is Relation-like NAT -defined Function-like V38() V45(2) FinSequence-like FinSubsequence-like V166() Element of the carrier of (TOP-REAL 2)
(x * (g,1)) `1 is V28() real ext-real Element of REAL
K526((x * (g,1)),1) is V28() real ext-real Element of REAL
(x * (g,(A + A))) `1 is V28() real ext-real Element of REAL
K526((x * (g,(A + A))),1) is V28() real ext-real Element of REAL
((x * (g,A)) `1) - ((x * (g,(A + A))) `1) is V28() real ext-real Element of REAL
(((x * (g,A)) `1) - ((x * (g,(A + A))) `1)) ^2 is V28() real ext-real Element of REAL
K104((((x * (g,A)) `1) - ((x * (g,(A + A))) `1)),(((x * (g,A)) `1) - ((x * (g,(A + A))) `1))) is V28() real ext-real set
((x * (g,A)) `2) - ((x * (g,(A + A))) `2) is V28() real ext-real Element of REAL
(((x * (g,A)) `2) - ((x * (g,(A + A))) `2)) ^2 is V28() real ext-real Element of REAL
K104((((x * (g,A)) `2) - ((x * (g,(A + A))) `2)),(((x * (g,A)) `2) - ((x * (g,(A + A))) `2))) is V28() real ext-real set
((((x * (g,A)) `1) - ((x * (g,(A + A))) `1)) ^2) + ((((x * (g,A)) `2) - ((x * (g,(A + A))) `2)) ^2) is V28() real ext-real Element of REAL
sqrt (((((x * (g,A)) `1) - ((x * (g,(A + A))) `1)) ^2) + ((((x * (g,A)) `2) - ((x * (g,(A + A))) `2)) ^2)) is V28() real ext-real Element of REAL
abs (((x * (g,A)) `2) - ((x * (g,(A + A))) `2)) is V28() real ext-real Element of REAL
- (((x * (g,A)) `2) - ((x * (g,(A + A))) `2)) is V28() real ext-real Element of REAL
abs (- (((x * (g,A)) `2) - ((x * (g,(A + A))) `2))) is V28() real ext-real Element of REAL
g is ordinal natural V28() real ext-real non negative integer V108() V174() V175() V176() V177() V178() V179() Element of NAT
A is non empty compact bounded non horizontal non vertical Element of K19( the carrier of (TOP-REAL 2))
Gauge (A,g) is Relation-like NAT -defined the carrier of (TOP-REAL 2) * -valued Function-like V38() FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of (TOP-REAL 2) *
len (Gauge (A,g)) is ordinal natural V28() real ext-real non negative integer V108() V174() V175() V176() V177() V178() V179() Element of NAT
(len (Gauge (A,g))) -' 1 is ordinal natural V28() real ext-real non negative integer V108() V174() V175() V176() V177() V178() V179() Element of NAT
4 - 1 is V28() real ext-real integer Element of REAL
(len (Gauge (A,g))) - 1 is V28() real ext-real integer Element of REAL
g is ordinal natural V28() real ext-real non negative integer V108() V174() V175() V176() V177() V178() V179() Element of NAT
A is ordinal natural V28() real ext-real non negative integer V108() V174() V175() V176() V177() V178() V179() Element of NAT
A -' g is ordinal natural V28() real ext-real non negative integer V108() V174() V175() V176() V177() V178() V179() Element of NAT
2 |^ (A -' g) is ordinal natural V28() real ext-real non negative integer V108() V174() V175() V176() V177() V178() V179() Element of NAT
A is non empty compact bounded non horizontal non vertical Element of K19( the carrier of (TOP-REAL 2))
Gauge (A,g) is Relation-like NAT -defined the carrier of (TOP-REAL 2) * -valued Function-like V38() FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of (TOP-REAL 2) *
len (Gauge (A,g)) is ordinal natural V28() real ext-real non negative integer V108() V174() V175() V176() V177() V178() V179() Element of NAT
(len (Gauge (A,g))) - 1 is V28() real ext-real integer Element of REAL
Gauge (A,A) is Relation-like NAT -defined the carrier of (TOP-REAL 2) * -valued Function-like V38() FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of (TOP-REAL 2) *
len (Gauge (A,A)) is ordinal natural V28() real ext-real non negative integer V108() V174() V175() V176() V177() V178() V179() Element of NAT
(len (Gauge (A,A))) - 1 is V28() real ext-real integer Element of REAL
Indices (Gauge (A,A)) is set
2 |^ g is ordinal natural V28() real ext-real non negative integer V108() V174() V175() V176() V177() V178() V179() Element of NAT
(2 |^ (A -' g)) * (2 |^ g) is ordinal natural V28() real ext-real non negative integer V108() V174() V175() V176() V177() V178() V179() Element of NAT
2 |^ A is ordinal natural V28() real ext-real non negative integer V108() V174() V175() V176() V177() V178() V179() Element of NAT
(2 |^ A) / (2 |^ g) is V28() real ext-real non negative Element of REAL
((2 |^ A) / (2 |^ g)) * (2 |^ g) is V28() real ext-real non negative Element of REAL
x is ordinal natural V28() real ext-real non negative integer V108() V174() V175() V176() V177() V178() V179() Element of NAT
x is ordinal natural V28() real ext-real non negative integer V108() V174() V175() V176() V177() V178() V179() Element of NAT
(Gauge (A,g)) * (x,x) is Relation-like NAT -defined Function-like V38() V45(2) FinSequence-like FinSubsequence-like V166() Element of the carrier of (TOP-REAL 2)
x -' 2 is ordinal natural V28() real ext-real non negative integer V108() V174() V175() V176() V177() V178() V179() Element of NAT
(2 |^ (A -' g)) * (x -' 2) is ordinal natural V28() real ext-real non negative integer V108() V174() V175() V176() V177() V178() V179() Element of NAT
2 + ((2 |^ (A -' g)) * (x -' 2)) is non empty ordinal natural V28() real ext-real positive non negative integer V108() V174() V175() V176() V177() V178() V179() Element of NAT
x -' 2 is ordinal natural V28() real ext-real non negative integer V108() V174() V175() V176() V177() V178() V179() Element of NAT
(2 |^ (A -' g)) * (x -' 2) is ordinal natural V28() real ext-real non negative integer V108() V174() V175() V176() V177() V178() V179() Element of NAT
2 + ((2 |^ (A -' g)) * (x -' 2)) is non empty ordinal natural V28() real ext-real positive non negative integer V108() V174() V175() V176() V177() V178() V179() Element of NAT
x - 2 is V28() real ext-real integer Element of REAL
N-bound A is V28() real ext-real Element of REAL
E-bound A is V28() real ext-real Element of REAL
S-bound A is V28() real ext-real Element of REAL
W-bound A is V28() real ext-real Element of REAL
(N-bound A) - (S-bound A) is V28() real ext-real Element of REAL
((N-bound A) - (S-bound A)) / (2 |^ A) is V28() real ext-real Element of REAL
(2 + ((2 |^ (A -' g)) * (x -' 2))) - 2 is V28() real ext-real integer Element of REAL
(((N-bound A) - (S-bound A)) / (2 |^ A)) * ((2 + ((2 |^ (A -' g)) * (x -' 2))) - 2) is V28() real ext-real Element of REAL
((2 |^ A) / (2 |^ g)) * (x -' 2) is V28() real ext-real non negative Element of REAL
(((N-bound A) - (S-bound A)) / (2 |^ A)) * (((2 |^ A) / (2 |^ g)) * (x -' 2)) is V28() real ext-real Element of REAL
(((N-bound A) - (S-bound A)) / (2 |^ A)) * ((2 |^ A) / (2 |^ g)) is V28() real ext-real Element of REAL
((((N-bound A) - (S-bound A)) / (2 |^ A)) * ((2 |^ A) / (2 |^ g))) * (x -' 2) is V28() real ext-real Element of REAL
(2 |^ A) / ((2 |^ A) / (2 |^ g)) is V28() real ext-real non negative Element of REAL
((N-bound A) - (S-bound A)) / ((2 |^ A) / ((2 |^ A) / (2 |^ g))) is V28() real ext-real Element of REAL
(((N-bound A) - (S-bound A)) / ((2 |^ A) / ((2 |^ A) / (2 |^ g)))) * (x -' 2) is V28() real ext-real Element of REAL
((N-bound A) - (S-bound A)) / (2 |^ g) is V28() real ext-real Element of REAL
(((N-bound A) - (S-bound A)) / (2 |^ g)) * (x -' 2) is V28() real ext-real Element of REAL
(((N-bound A) - (S-bound A)) / (2 |^ g)) * (x - 2) is V28() real ext-real Element of REAL
[(2 + ((2 |^ (A -' g)) * (x -' 2))),(2 + ((2 |^ (A -' g)) * (x -' 2)))] is non empty set
{(2 + ((2 |^ (A -' g)) * (x -' 2))),(2 + ((2 |^ (A -' g)) * (x -' 2)))} is non empty V174() V175() V176() V177() V178() V179() set
{(2 + ((2 |^ (A -' g)) * (x -' 2)))} is non empty V12() V174() V175() V176() V177() V178() V179() set
{{(2 + ((2 |^ (A -' g)) * (x -' 2))),(2 + ((2 |^ (A -' g)) * (x -' 2)))},{(2 + ((2 |^ (A -' g)) * (x -' 2)))}} is non empty set
(Gauge (A,A)) * ((2 + ((2 |^ (A -' g)) * (x -' 2))),(2 + ((2 |^ (A -' g)) * (x -' 2)))) is Relation-like NAT -defined Function-like V38() V45(2) FinSequence-like FinSubsequence-like V166() Element of the carrier of (TOP-REAL 2)
2 + 0 is non empty ordinal natural V28() real ext-real positive non negative integer V108() V174() V175() V176() V177() V178() V179() Element of NAT
(2 |^ g) + 2 is non empty ordinal natural V28() real ext-real positive non negative integer V108() V174() V175() V176() V177() V178() V179() Element of NAT
((2 |^ g) + 2) - 2 is V28() real ext-real integer Element of REAL
((2 |^ g) + 2) -' 2 is ordinal natural V28() real ext-real non negative integer V108() V174() V175() V176() V177() V178() V179() Element of NAT
(2 |^ g) + 0 is ordinal natural V28() real ext-real non negative integer V108() V174() V175() V176() V177() V178() V179() Element of NAT
x - 2 is V28() real ext-real integer Element of REAL
(E-bound A) - (W-bound A) is V28() real ext-real Element of REAL
((E-bound A) - (W-bound A)) / (2 |^ A) is V28() real ext-real Element of REAL
(2 + ((2 |^ (A -' g)) * (x -' 2))) - 2 is V28() real ext-real integer Element of REAL
(((E-bound A) - (W-bound A)) / (2 |^ A)) * ((2 + ((2 |^ (A -' g)) * (x -' 2))) - 2) is V28() real ext-real Element of REAL
((2 |^ A) / (2 |^ g)) * (x -' 2) is V28() real ext-real non negative Element of REAL
(((E-bound A) - (W-bound A)) / (2 |^ A)) * (((2 |^ A) / (2 |^ g)) * (x -' 2)) is V28() real ext-real Element of REAL
(((E-bound A) - (W-bound A)) / (2 |^ A)) * ((2 |^ A) / (2 |^ g)) is V28() real ext-real Element of REAL
((((E-bound A) - (W-bound A)) / (2 |^ A)) * ((2 |^ A) / (2 |^ g))) * (x -' 2) is V28() real ext-real Element of REAL
((E-bound A) - (W-bound A)) / ((2 |^ A) / ((2 |^ A) / (2 |^ g))) is V28() real ext-real Element of REAL
(((E-bound A) - (W-bound A)) / ((2 |^ A) / ((2 |^ A) / (2 |^ g)))) * (x -' 2) is V28() real ext-real Element of REAL
((E-bound A) - (W-bound A)) / (2 |^ g) is V28() real ext-real Element of REAL
(((E-bound A) - (W-bound A)) / (2 |^ g)) * (x -' 2) is V28() real ext-real Element of REAL
(((E-bound A) - (W-bound A)) / (2 |^ g)) * (x - 2) is V28() real ext-real Element of REAL
(len (Gauge (A,A))) - 0 is V28() real ext-real non negative integer Element of REAL
(2 |^ g) + 3 is non empty ordinal natural V28() real ext-real positive non negative integer V108() V174() V175() V176() V177() V178() V179() Element of NAT
((2 |^ g) + 3) - 1 is V28() real ext-real integer Element of REAL
(len (Gauge (A,g))) - 0 is V28() real ext-real non negative integer Element of REAL
(2 |^ A) + 3 is non empty ordinal natural V28() real ext-real positive non negative integer V108() V174() V175() V176() V177() V178() V179() Element of NAT
((2 |^ A) + 3) - 1 is V28() real ext-real integer Element of REAL
(2 |^ A) + 2 is non empty ordinal natural V28() real ext-real positive non negative integer V108() V174() V175() V176() V177() V178() V179() Element of NAT
width (Gauge (A,A)) is ordinal natural V28() real ext-real non negative integer V108() V174() V175() V176() V177() V178() V179() Element of NAT
(W-bound A) + ((((E-bound A) - (W-bound A)) / (2 |^ A)) * ((2 + ((2 |^ (A -' g)) * (x -' 2))) - 2)) is V28() real ext-real Element of REAL
(S-bound A) + ((((N-bound A) - (S-bound A)) / (2 |^ A)) * ((2 + ((2 |^ (A -' g)) * (x -' 2))) - 2)) is V28() real ext-real Element of REAL
|[((W-bound A) + ((((E-bound A) - (W-bound A)) / (2 |^ A)) * ((2 + ((2 |^ (A -' g)) * (x -' 2))) - 2))),((S-bound A) + ((((N-bound A) - (S-bound A)) / (2 |^ A)) * ((2 + ((2 |^ (A -' g)) * (x -' 2))) - 2)))]| is Relation-like NAT -defined Function-like non empty V38() V45(2) FinSequence-like FinSubsequence-like V166() Element of the carrier of (TOP-REAL 2)
width (Gauge (A,g)) is ordinal natural V28() real ext-real non negative integer V108() V174() V175() V176() V177() V178() V179() Element of NAT
[x,x] is non empty set
{x,x} is non empty V174() V175() V176() V177() V178() V179() set
{x} is non empty V12() V174() V175() V176() V177() V178() V179() set
{{x,x},{x}} is non empty set
Indices (Gauge (A,g)) is set
(W-bound A) + ((((E-bound A) - (W-bound A)) / (2 |^ g)) * (x - 2)) is V28() real ext-real Element of REAL
(S-bound A) + ((((N-bound A) - (S-bound A)) / (2 |^ g)) * (x - 2)) is V28() real ext-real Element of REAL
|[((W-bound A) + ((((E-bound A) - (W-bound A)) / (2 |^ g)) * (x - 2))),((S-bound A) + ((((N-bound A) - (S-bound A)) / (2 |^ g)) * (x - 2)))]| is Relation-like NAT -defined Function-like non empty V38() V45(2) FinSequence-like FinSubsequence-like V166() Element of the carrier of (TOP-REAL 2)
((Gauge (A,g)) * (x,x)) `2 is V28() real ext-real Element of REAL
K526(((Gauge (A,g)) * (x,x)),2) is V28() real ext-real Element of REAL
((Gauge (A,A)) * ((2 + ((2 |^ (A -' g)) * (x -' 2))),(2 + ((2 |^ (A -' g)) * (x -' 2))))) `2 is V28() real ext-real Element of REAL
K526(((Gauge (A,A)) * ((2 + ((2 |^ (A -' g)) * (x -' 2))),(2 + ((2 |^ (A -' g)) * (x -' 2))))),2) is V28() real ext-real Element of REAL
((Gauge (A,g)) * (x,x)) `1 is V28() real ext-real Element of REAL
K526(((Gauge (A,g)) * (x,x)),1) is V28() real ext-real Element of REAL
((Gauge (A,A)) * ((2 + ((2 |^ (A -' g)) * (x -' 2))),(2 + ((2 |^ (A -' g)) * (x -' 2))))) `1 is V28() real ext-real Element of REAL
K526(((Gauge (A,A)) * ((2 + ((2 |^ (A -' g)) * (x -' 2))),(2 + ((2 |^ (A -' g)) * (x -' 2))))),1) is V28() real ext-real Element of REAL
g is ordinal natural V28() real ext-real non negative integer V108() V174() V175() V176() V177() V178() V179() Element of NAT
A is ordinal natural V28() real ext-real non negative integer V108() V174() V175() V176() V177() V178() V179() Element of NAT
[g,A] is non empty set
{g,A} is non empty V174() V175() V176() V177() V178() V179() set
{g} is non empty V12() V174() V175() V176() V177() V178() V179() set
{{g,A},{g}} is non empty set
A + 1 is non empty ordinal natural V28() real ext-real positive non negative integer V108() V174() V175() V176() V177() V178() V179() Element of NAT
[g,(A + 1)] is non empty set
{g,(A + 1)} is non empty V174() V175() V176() V177() V178() V179() set
{{g,(A + 1)},{g}} is non empty set
A is ordinal natural V28() real ext-real non negative integer V108() V174() V175() V176() V177() V178() V179() Element of NAT
2 |^ A is ordinal natural V28() real ext-real non negative integer V108() V174() V175() V176() V177() V178() V179() Element of NAT
x is non empty compact bounded non horizontal non vertical Element of K19( the carrier of (TOP-REAL 2))
Gauge (x,A) is Relation-like NAT -defined the carrier of (TOP-REAL 2) * -valued Function-like V38() FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of (TOP-REAL 2) *
Indices (Gauge (x,A)) is set
(Gauge (x,A)) * (g,A) is Relation-like NAT -defined Function-like V38() V45(2) FinSequence-like FinSubsequence-like V166() Element of the carrier of (TOP-REAL 2)
(Gauge (x,A)) * (g,(A + 1)) is Relation-like NAT -defined Function-like V38() V45(2) FinSequence-like FinSubsequence-like V166() Element of the carrier of (TOP-REAL 2)
dist (((Gauge (x,A)) * (g,A)),((Gauge (x,A)) * (g,(A + 1)))) is V28() real ext-real Element of REAL
N-bound x is V28() real ext-real Element of REAL
S-bound x is V28() real ext-real Element of REAL
(N-bound x) - (S-bound x) is V28() real ext-real Element of REAL
((N-bound x) - (S-bound x)) / (2 |^ A) is V28() real ext-real Element of REAL
E-bound x is V28() real ext-real Element of REAL
W-bound x is V28() real ext-real Element of REAL
(E-bound x) - (W-bound x) is V28() real ext-real Element of REAL
((E-bound x) - (W-bound x)) / (2 |^ A) is V28() real ext-real Element of REAL
g - 2 is V28() real ext-real integer Element of REAL
(((E-bound x) - (W-bound x)) / (2 |^ A)) * (g - 2) is V28() real ext-real Element of REAL
(W-bound x) + ((((E-bound x) - (W-bound x)) / (2 |^ A)) * (g - 2)) is V28() real ext-real Element of REAL
(A + 1) - 2 is V28() real ext-real integer Element of REAL
(((N-bound x) - (S-bound x)) / (2 |^ A)) * ((A + 1) - 2) is V28() real ext-real Element of REAL
(S-bound x) + ((((N-bound x) - (S-bound x)) / (2 |^ A)) * ((A + 1) - 2)) is V28() real ext-real Element of REAL
|[((W-bound x) + ((((E-bound x) - (W-bound x)) / (2 |^ A)) * (g - 2))),((S-bound x) + ((((N-bound x) - (S-bound x)) / (2 |^ A)) * ((A + 1) - 2)))]| is Relation-like NAT -defined Function-like non empty V38() V45(2) FinSequence-like FinSubsequence-like V166() Element of the carrier of (TOP-REAL 2)
(S-bound x) - (S-bound x) is V28() real ext-real Element of REAL
p is Element of the carrier of (Euclid 2)
q is Element of the carrier of (Euclid 2)
dist (p,q) is V28() real ext-real Element of REAL
A - 2 is V28() real ext-real integer Element of REAL
(((N-bound x) - (S-bound x)) / (2 |^ A)) * (A - 2) is V28() real ext-real Element of REAL
(S-bound x) + ((((N-bound x) - (S-bound x)) / (2 |^ A)) * (A - 2)) is V28() real ext-real Element of REAL
|[((W-bound x) + ((((E-bound x) - (W-bound x)) / (2 |^ A)) * (g - 2))),((S-bound x) + ((((N-bound x) - (S-bound x)) / (2 |^ A)) * (A - 2)))]| is Relation-like NAT -defined Function-like non empty V38() V45(2) FinSequence-like FinSubsequence-like V166() Element of the carrier of (TOP-REAL 2)
(Pitag_dist 2) . (p,q) is set
((Gauge (x,A)) * (g,A)) `1 is V28() real ext-real Element of REAL
K526(((Gauge (x,A)) * (g,A)),1) is V28() real ext-real Element of REAL
((Gauge (x,A)) * (g,(A + 1))) `1 is V28() real ext-real Element of REAL
K526(((Gauge (x,A)) * (g,(A + 1))),1) is V28() real ext-real Element of REAL
(((Gauge (x,A)) * (g,A)) `1) - (((Gauge (x,A)) * (g,(A + 1))) `1) is V28() real ext-real Element of REAL
((((Gauge (x,A)) * (g,A)) `1) - (((Gauge (x,A)) * (g,(A + 1))) `1)) ^2 is V28() real ext-real Element of REAL
K104(((((Gauge (x,A)) * (g,A)) `1) - (((Gauge (x,A)) * (g,(A + 1))) `1)),((((Gauge (x,A)) * (g,A)) `1) - (((Gauge (x,A)) * (g,(A + 1))) `1))) is V28() real ext-real set
((Gauge (x,A)) * (g,A)) `2 is V28() real ext-real Element of REAL
K526(((Gauge (x,A)) * (g,A)),2) is V28() real ext-real Element of REAL
((Gauge (x,A)) * (g,(A + 1))) `2 is V28() real ext-real Element of REAL
K526(((Gauge (x,A)) * (g,(A + 1))),2) is V28() real ext-real Element of REAL
(((Gauge (x,A)) * (g,A)) `2) - (((Gauge (x,A)) * (g,(A + 1))) `2) is V28() real ext-real Element of REAL
((((Gauge (x,A)) * (g,A)) `2) - (((Gauge (x,A)) * (g,(A + 1))) `2)) ^2 is V28() real ext-real Element of REAL
K104(((((Gauge (x,A)) * (g,A)) `2) - (((Gauge (x,A)) * (g,(A + 1))) `2)),((((Gauge (x,A)) * (g,A)) `2) - (((Gauge (x,A)) * (g,(A + 1))) `2))) is V28() real ext-real set
(((((Gauge (x,A)) * (g,A)) `1) - (((Gauge (x,A)) * (g,(A + 1))) `1)) ^2) + (((((Gauge (x,A)) * (g,A)) `2) - (((Gauge (x,A)) * (g,(A + 1))) `2)) ^2) is V28() real ext-real Element of REAL
sqrt ((((((Gauge (x,A)) * (g,A)) `1) - (((Gauge (x,A)) * (g,(A + 1))) `1)) ^2) + (((((Gauge (x,A)) * (g,A)) `2) - (((Gauge (x,A)) * (g,(A + 1))) `2)) ^2)) is V28() real ext-real Element of REAL
((W-bound x) + ((((E-bound x) - (W-bound x)) / (2 |^ A)) * (g - 2))) - (((Gauge (x,A)) * (g,(A + 1))) `1) is V28() real ext-real Element of REAL
(((W-bound x) + ((((E-bound x) - (W-bound x)) / (2 |^ A)) * (g - 2))) - (((Gauge (x,A)) * (g,(A + 1))) `1)) ^2 is V28() real ext-real Element of REAL
K104((((W-bound x) + ((((E-bound x) - (W-bound x)) / (2 |^ A)) * (g - 2))) - (((Gauge (x,A)) * (g,(A + 1))) `1)),(((W-bound x) + ((((E-bound x) - (W-bound x)) / (2 |^ A)) * (g - 2))) - (((Gauge (x,A)) * (g,(A + 1))) `1))) is V28() real ext-real set
((((W-bound x) + ((((E-bound x) - (W-bound x)) / (2 |^ A)) * (g - 2))) - (((Gauge (x,A)) * (g,(A + 1))) `1)) ^2) + (((((Gauge (x,A)) * (g,A)) `2) - (((Gauge (x,A)) * (g,(A + 1))) `2)) ^2) is V28() real ext-real Element of REAL
sqrt (((((W-bound x) + ((((E-bound x) - (W-bound x)) / (2 |^ A)) * (g - 2))) - (((Gauge (x,A)) * (g,(A + 1))) `1)) ^2) + (((((Gauge (x,A)) * (g,A)) `2) - (((Gauge (x,A)) * (g,(A + 1))) `2)) ^2)) is V28() real ext-real Element of REAL
((W-bound x) + ((((E-bound x) - (W-bound x)) / (2 |^ A)) * (g - 2))) - ((W-bound x) + ((((E-bound x) - (W-bound x)) / (2 |^ A)) * (g - 2))) is V28() real ext-real Element of REAL
(((W-bound x) + ((((E-bound x) - (W-bound x)) / (2 |^ A)) * (g - 2))) - ((W-bound x) + ((((E-bound x) - (W-bound x)) / (2 |^ A)) * (g - 2)))) ^2 is V28() real ext-real Element of REAL
K104((((W-bound x) + ((((E-bound x) - (W-bound x)) / (2 |^ A)) * (g - 2))) - ((W-bound x) + ((((E-bound x) - (W-bound x)) / (2 |^ A)) * (g - 2)))),(((W-bound x) + ((((E-bound x) - (W-bound x)) / (2 |^ A)) * (g - 2))) - ((W-bound x) + ((((E-bound x) - (W-bound x)) / (2 |^ A)) * (g - 2))))) is V28() real ext-real set
((((W-bound x) + ((((E-bound x) - (W-bound x)) / (2 |^ A)) * (g - 2))) - ((W-bound x) + ((((E-bound x) - (W-bound x)) / (2 |^ A)) * (g - 2)))) ^2) + (((((Gauge (x,A)) * (g,A)) `2) - (((Gauge (x,A)) * (g,(A + 1))) `2)) ^2) is V28() real ext-real Element of REAL
sqrt (((((W-bound x) + ((((E-bound x) - (W-bound x)) / (2 |^ A)) * (g - 2))) - ((W-bound x) + ((((E-bound x) - (W-bound x)) / (2 |^ A)) * (g - 2)))) ^2) + (((((Gauge (x,A)) * (g,A)) `2) - (((Gauge (x,A)) * (g,(A + 1))) `2)) ^2)) is V28() real ext-real Element of REAL
abs ((((Gauge (x,A)) * (g,A)) `2) - (((Gauge (x,A)) * (g,(A + 1))) `2)) is V28() real ext-real Element of REAL
((S-bound x) + ((((N-bound x) - (S-bound x)) / (2 |^ A)) * (A - 2))) - (((Gauge (x,A)) * (g,(A + 1))) `2) is V28() real ext-real Element of REAL
abs (((S-bound x) + ((((N-bound x) - (S-bound x)) / (2 |^ A)) * (A - 2))) - (((Gauge (x,A)) * (g,(A + 1))) `2)) is V28() real ext-real Element of REAL
((S-bound x) + ((((N-bound x) - (S-bound x)) / (2 |^ A)) * (A - 2))) - ((S-bound x) + ((((N-bound x) - (S-bound x)) / (2 |^ A)) * ((A + 1) - 2))) is V28() real ext-real Element of REAL
abs (((S-bound x) + ((((N-bound x) - (S-bound x)) / (2 |^ A)) * (A - 2))) - ((S-bound x) + ((((N-bound x) - (S-bound x)) / (2 |^ A)) * ((A + 1) - 2)))) is V28() real ext-real Element of REAL
- (((N-bound x) - (S-bound x)) / (2 |^ A)) is V28() real ext-real Element of REAL
abs (- (((N-bound x) - (S-bound x)) / (2 |^ A))) is V28() real ext-real Element of REAL
abs (((N-bound x) - (S-bound x)) / (2 |^ A)) is V28() real ext-real Element of REAL
abs ((N-bound x) - (S-bound x)) is V28() real ext-real Element of REAL
abs (2 |^ A) is ordinal natural V28() real ext-real non negative integer V108() V174() V175() V176() V177() V178() V179() Element of NAT
(abs ((N-bound x) - (S-bound x))) / (abs (2 |^ A)) is V28() real ext-real Element of REAL
((N-bound x) - (S-bound x)) / (abs (2 |^ A)) is V28() real ext-real Element of REAL
g is ordinal natural V28() real ext-real non negative integer V108() V174() V175() V176() V177() V178() V179() Element of NAT
g + 1 is non empty ordinal natural V28() real ext-real positive non negative integer V108() V174() V175() V176() V177() V178() V179() Element of NAT
A is ordinal natural V28() real ext-real non negative integer V108() V174() V175() V176() V177() V178() V179() Element of NAT
[g,A] is non empty set
{g,A} is non empty V174() V175() V176() V177() V178() V179() set
{g} is non empty V12() V174() V175() V176() V177() V178() V179() set
{{g,A},{g}} is non empty set
[(g + 1),A] is non empty set
{(g + 1),A} is non empty V174() V175() V176() V177() V178() V179() set
{(g + 1)} is non empty V12() V174() V175() V176() V177() V178() V179() set
{{(g + 1),A},{(g + 1)}} is non empty set
A is ordinal natural V28() real ext-real non negative integer V108() V174() V175() V176() V177() V178() V179() Element of NAT
2 |^ A is ordinal natural V28() real ext-real non negative integer V108() V174() V175() V176() V177() V178() V179() Element of NAT
x is non empty compact bounded non horizontal non vertical Element of K19( the carrier of (TOP-REAL 2))
Gauge (x,A) is Relation-like NAT -defined the carrier of (TOP-REAL 2) * -valued Function-like V38() FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of (TOP-REAL 2) *
Indices (Gauge (x,A)) is set
(Gauge (x,A)) * (g,A) is Relation-like NAT -defined Function-like V38() V45(2) FinSequence-like FinSubsequence-like V166() Element of the carrier of (TOP-REAL 2)
(Gauge (x,A)) * ((g + 1),A) is Relation-like NAT -defined Function-like V38() V45(2) FinSequence-like FinSubsequence-like V166() Element of the carrier of (TOP-REAL 2)
dist (((Gauge (x,A)) * (g,A)),((Gauge (x,A)) * ((g + 1),A))) is V28() real ext-real Element of REAL
E-bound x is V28() real ext-real Element of REAL
W-bound x is V28() real ext-real Element of REAL
(E-bound x) - (W-bound x) is V28() real ext-real Element of REAL
((E-bound x) - (W-bound x)) / (2 |^ A) is V28() real ext-real Element of REAL
N-bound x is V28() real ext-real Element of REAL
S-bound x is V28() real ext-real Element of REAL
(g + 1) - 2 is V28() real ext-real integer Element of REAL
(((E-bound x) - (W-bound x)) / (2 |^ A)) * ((g + 1) - 2) is V28() real ext-real Element of REAL
(W-bound x) + ((((E-bound x) - (W-bound x)) / (2 |^ A)) * ((g + 1) - 2)) is V28() real ext-real Element of REAL
(N-bound x) - (S-bound x) is V28() real ext-real Element of REAL
((N-bound x) - (S-bound x)) / (2 |^ A) is V28() real ext-real Element of REAL
A - 2 is V28() real ext-real integer Element of REAL
(((N-bound x) - (S-bound x)) / (2 |^ A)) * (A - 2) is V28() real ext-real Element of REAL
(S-bound x) + ((((N-bound x) - (S-bound x)) / (2 |^ A)) * (A - 2)) is V28() real ext-real Element of REAL
|[((W-bound x) + ((((E-bound x) - (W-bound x)) / (2 |^ A)) * ((g + 1) - 2))),((S-bound x) + ((((N-bound x) - (S-bound x)) / (2 |^ A)) * (A - 2)))]| is Relation-like NAT -defined Function-like non empty V38() V45(2) FinSequence-like FinSubsequence-like V166() Element of the carrier of (TOP-REAL 2)
(W-bound x) - (W-bound x) is V28() real ext-real Element of REAL
p is Element of the carrier of (Euclid 2)
q is Element of the carrier of (Euclid 2)
dist (p,q) is V28() real ext-real Element of REAL
g - 2 is V28() real ext-real integer Element of REAL
(((E-bound x) - (W-bound x)) / (2 |^ A)) * (g - 2) is V28() real ext-real Element of REAL
(W-bound x) + ((((E-bound x) - (W-bound x)) / (2 |^ A)) * (g - 2)) is V28() real ext-real Element of REAL
|[((W-bound x) + ((((E-bound x) - (W-bound x)) / (2 |^ A)) * (g - 2))),((S-bound x) + ((((N-bound x) - (S-bound x)) / (2 |^ A)) * (A - 2)))]| is Relation-like NAT -defined Function-like non empty V38() V45(2) FinSequence-like FinSubsequence-like V166() Element of the carrier of (TOP-REAL 2)
(Pitag_dist 2) . (p,q) is set
((Gauge (x,A)) * (g,A)) `1 is V28() real ext-real Element of REAL
K526(((Gauge (x,A)) * (g,A)),1) is V28() real ext-real Element of REAL
((Gauge (x,A)) * ((g + 1),A)) `1 is V28() real ext-real Element of REAL
K526(((Gauge (x,A)) * ((g + 1),A)),1) is V28() real ext-real Element of REAL
(((Gauge (x,A)) * (g,A)) `1) - (((Gauge (x,A)) * ((g + 1),A)) `1) is V28() real ext-real Element of REAL
((((Gauge (x,A)) * (g,A)) `1) - (((Gauge (x,A)) * ((g + 1),A)) `1)) ^2 is V28() real ext-real Element of REAL
K104(((((Gauge (x,A)) * (g,A)) `1) - (((Gauge (x,A)) * ((g + 1),A)) `1)),((((Gauge (x,A)) * (g,A)) `1) - (((Gauge (x,A)) * ((g + 1),A)) `1))) is V28() real ext-real set
((Gauge (x,A)) * (g,A)) `2 is V28() real ext-real Element of REAL
K526(((Gauge (x,A)) * (g,A)),2) is V28() real ext-real Element of REAL
((Gauge (x,A)) * ((g + 1),A)) `2 is V28() real ext-real Element of REAL
K526(((Gauge (x,A)) * ((g + 1),A)),2) is V28() real ext-real Element of REAL
(((Gauge (x,A)) * (g,A)) `2) - (((Gauge (x,A)) * ((g + 1),A)) `2) is V28() real ext-real Element of REAL
((((Gauge (x,A)) * (g,A)) `2) - (((Gauge (x,A)) * ((g + 1),A)) `2)) ^2 is V28() real ext-real Element of REAL
K104(((((Gauge (x,A)) * (g,A)) `2) - (((Gauge (x,A)) * ((g + 1),A)) `2)),((((Gauge (x,A)) * (g,A)) `2) - (((Gauge (x,A)) * ((g + 1),A)) `2))) is V28() real ext-real set
(((((Gauge (x,A)) * (g,A)) `1) - (((Gauge (x,A)) * ((g + 1),A)) `1)) ^2) + (((((Gauge (x,A)) * (g,A)) `2) - (((Gauge (x,A)) * ((g + 1),A)) `2)) ^2) is V28() real ext-real Element of REAL
sqrt ((((((Gauge (x,A)) * (g,A)) `1) - (((Gauge (x,A)) * ((g + 1),A)) `1)) ^2) + (((((Gauge (x,A)) * (g,A)) `2) - (((Gauge (x,A)) * ((g + 1),A)) `2)) ^2)) is V28() real ext-real Element of REAL
((S-bound x) + ((((N-bound x) - (S-bound x)) / (2 |^ A)) * (A - 2))) - (((Gauge (x,A)) * ((g + 1),A)) `2) is V28() real ext-real Element of REAL
(((S-bound x) + ((((N-bound x) - (S-bound x)) / (2 |^ A)) * (A - 2))) - (((Gauge (x,A)) * ((g + 1),A)) `2)) ^2 is V28() real ext-real Element of REAL
K104((((S-bound x) + ((((N-bound x) - (S-bound x)) / (2 |^ A)) * (A - 2))) - (((Gauge (x,A)) * ((g + 1),A)) `2)),(((S-bound x) + ((((N-bound x) - (S-bound x)) / (2 |^ A)) * (A - 2))) - (((Gauge (x,A)) * ((g + 1),A)) `2))) is V28() real ext-real set
(((((Gauge (x,A)) * (g,A)) `1) - (((Gauge (x,A)) * ((g + 1),A)) `1)) ^2) + ((((S-bound x) + ((((N-bound x) - (S-bound x)) / (2 |^ A)) * (A - 2))) - (((Gauge (x,A)) * ((g + 1),A)) `2)) ^2) is V28() real ext-real Element of REAL
sqrt ((((((Gauge (x,A)) * (g,A)) `1) - (((Gauge (x,A)) * ((g + 1),A)) `1)) ^2) + ((((S-bound x) + ((((N-bound x) - (S-bound x)) / (2 |^ A)) * (A - 2))) - (((Gauge (x,A)) * ((g + 1),A)) `2)) ^2)) is V28() real ext-real Element of REAL
((S-bound x) + ((((N-bound x) - (S-bound x)) / (2 |^ A)) * (A - 2))) - ((S-bound x) + ((((N-bound x) - (S-bound x)) / (2 |^ A)) * (A - 2))) is V28() real ext-real Element of REAL
(((S-bound x) + ((((N-bound x) - (S-bound x)) / (2 |^ A)) * (A - 2))) - ((S-bound x) + ((((N-bound x) - (S-bound x)) / (2 |^ A)) * (A - 2)))) ^2 is V28() real ext-real Element of REAL
K104((((S-bound x) + ((((N-bound x) - (S-bound x)) / (2 |^ A)) * (A - 2))) - ((S-bound x) + ((((N-bound x) - (S-bound x)) / (2 |^ A)) * (A - 2)))),(((S-bound x) + ((((N-bound x) - (S-bound x)) / (2 |^ A)) * (A - 2))) - ((S-bound x) + ((((N-bound x) - (S-bound x)) / (2 |^ A)) * (A - 2))))) is V28() real ext-real set
(((((Gauge (x,A)) * (g,A)) `1) - (((Gauge (x,A)) * ((g + 1),A)) `1)) ^2) + ((((S-bound x) + ((((N-bound x) - (S-bound x)) / (2 |^ A)) * (A - 2))) - ((S-bound x) + ((((N-bound x) - (S-bound x)) / (2 |^ A)) * (A - 2)))) ^2) is V28() real ext-real Element of REAL
sqrt ((((((Gauge (x,A)) * (g,A)) `1) - (((Gauge (x,A)) * ((g + 1),A)) `1)) ^2) + ((((S-bound x) + ((((N-bound x) - (S-bound x)) / (2 |^ A)) * (A - 2))) - ((S-bound x) + ((((N-bound x) - (S-bound x)) / (2 |^ A)) * (A - 2)))) ^2)) is V28() real ext-real Element of REAL
abs ((((Gauge (x,A)) * (g,A)) `1) - (((Gauge (x,A)) * ((g + 1),A)) `1)) is V28() real ext-real Element of REAL
((W-bound x) + ((((E-bound x) - (W-bound x)) / (2 |^ A)) * (g - 2))) - (((Gauge (x,A)) * ((g + 1),A)) `1) is V28() real ext-real Element of REAL
abs (((W-bound x) + ((((E-bound x) - (W-bound x)) / (2 |^ A)) * (g - 2))) - (((Gauge (x,A)) * ((g + 1),A)) `1)) is V28() real ext-real Element of REAL
((W-bound x) + ((((E-bound x) - (W-bound x)) / (2 |^ A)) * (g - 2))) - ((W-bound x) + ((((E-bound x) - (W-bound x)) / (2 |^ A)) * ((g + 1) - 2))) is V28() real ext-real Element of REAL
abs (((W-bound x) + ((((E-bound x) - (W-bound x)) / (2 |^ A)) * (g - 2))) - ((W-bound x) + ((((E-bound x) - (W-bound x)) / (2 |^ A)) * ((g + 1) - 2)))) is V28() real ext-real Element of REAL
- (((E-bound x) - (W-bound x)) / (2 |^ A)) is V28() real ext-real Element of REAL
abs (- (((E-bound x) - (W-bound x)) / (2 |^ A))) is V28() real ext-real Element of REAL
abs (((E-bound x) - (W-bound x)) / (2 |^ A)) is V28() real ext-real Element of REAL
abs ((E-bound x) - (W-bound x)) is V28() real ext-real Element of REAL
abs (2 |^ A) is ordinal natural V28() real ext-real non negative integer V108() V174() V175() V176() V177() V178() V179() Element of NAT
(abs ((E-bound x) - (W-bound x))) / (abs (2 |^ A)) is V28() real ext-real Element of REAL
((E-bound x) - (W-bound x)) / (abs (2 |^ A)) is V28() real ext-real Element of REAL
g is non empty compact bounded non horizontal non vertical Element of K19( the carrier of (TOP-REAL 2))
A is V28() real ext-real set
A is V28() real ext-real set
N-bound g is V28() real ext-real Element of REAL
E-bound g is V28() real ext-real Element of REAL
S-bound g is V28() real ext-real Element of REAL
W-bound g is V28() real ext-real Element of REAL
(N-bound g) - (S-bound g) is V28() real ext-real Element of REAL
((N-bound g) - (S-bound g)) / A is V28() real ext-real Element of REAL
log (2,(((N-bound g) - (S-bound g)) / A)) is V28() real ext-real Element of REAL
[\(log (2,(((N-bound g) - (S-bound g)) / A)))/] is V28() real ext-real integer set
abs [\(log (2,(((N-bound g) - (S-bound g)) / A)))/] is ordinal natural V28() real ext-real non negative integer V108() V174() V175() V176() V177() V178() V179() Element of NAT
(abs [\(log (2,(((N-bound g) - (S-bound g)) / A)))/]) + 1 is non empty ordinal natural V28() real ext-real positive non negative integer V108() V174() V175() V176() V177() V178() V179() Element of NAT
(E-bound g) - (W-bound g) is V28() real ext-real Element of REAL
((E-bound g) - (W-bound g)) / A is V28() real ext-real Element of REAL
log (2,(((E-bound g) - (W-bound g)) / A)) is V28() real ext-real Element of REAL
[\(log (2,(((E-bound g) - (W-bound g)) / A)))/] is V28() real ext-real integer set
abs [\(log (2,(((E-bound g) - (W-bound g)) / A)))/] is ordinal natural V28() real ext-real non negative integer V108() V174() V175() V176() V177() V178() V179() Element of NAT
(abs [\(log (2,(((E-bound g) - (W-bound g)) / A)))/]) + 1 is non empty ordinal natural V28() real ext-real positive non negative integer V108() V174() V175() V176() V177() V178() V179() Element of NAT
max (((abs [\(log (2,(((N-bound g) - (S-bound g)) / A)))/]) + 1),((abs [\(log (2,(((E-bound g) - (W-bound g)) / A)))/]) + 1)) is ordinal natural V28() real ext-real non negative integer V108() V174() V175() V176() V177() V178() V179() Element of NAT
(max (((abs [\(log (2,(((N-bound g) - (S-bound g)) / A)))/]) + 1),((abs [\(log (2,(((E-bound g) - (W-bound g)) / A)))/]) + 1))) + 1 is non empty ordinal natural V28() real ext-real positive non negative integer V108() V174() V175() V176() V177() V178() V179() Element of NAT
i is non empty ordinal natural V28() real ext-real positive non negative integer V108() V174() V175() V176() V177() V178() V179() Element of NAT
Gauge (g,i) is Relation-like NAT -defined the carrier of (TOP-REAL 2) * -valued Function-like V38() FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of (TOP-REAL 2) *
(Gauge (g,i)) * (1,1) is Relation-like NAT -defined Function-like V38() V45(2) FinSequence-like FinSubsequence-like V166() Element of the carrier of (TOP-REAL 2)
(Gauge (g,i)) * (1,2) is Relation-like NAT -defined Function-like V38() V45(2) FinSequence-like FinSubsequence-like V166() Element of the carrier of (TOP-REAL 2)
dist (((Gauge (g,i)) * (1,1)),((Gauge (g,i)) * (1,2))) is V28() real ext-real Element of REAL
(Gauge (g,i)) * (2,1) is Relation-like NAT -defined Function-like V38() V45(2) FinSequence-like FinSubsequence-like V166() Element of the carrier of (TOP-REAL 2)
dist (((Gauge (g,i)) * (1,1)),((Gauge (g,i)) * (2,1))) is V28() real ext-real Element of REAL
2 to_power i is V28() real ext-real Element of REAL
2 |^ i is ordinal natural V28() real ext-real non negative integer V108() V174() V175() V176() V177() V178() V179() Element of NAT
[\(log (2,(((N-bound g) - (S-bound g)) / A)))/] + 1 is V28() real ext-real integer Element of REAL
(log (2,(((N-bound g) - (S-bound g)) / A))) - 1 is V28() real ext-real Element of REAL
((log (2,(((N-bound g) - (S-bound g)) / A))) - 1) + 1 is V28() real ext-real Element of REAL
((abs [\(log (2,(((N-bound g) - (S-bound g)) / A)))/]) + 1) + 1 is non empty ordinal natural V28() real ext-real positive non negative integer V108() V174() V175() V176() V177() V178() V179() Element of NAT
log (2,(2 to_power i)) is V28() real ext-real Element of REAL
(2 |^ i) * A is V28() real ext-real Element of REAL
(((N-bound g) - (S-bound g)) / A) * A is V28() real ext-real Element of REAL
((2 |^ i) * A) / (2 |^ i) is V28() real ext-real Element of REAL
((N-bound g) - (S-bound g)) / (2 |^ i) is V28() real ext-real Element of REAL
0 + 1 is non empty ordinal natural V28() real ext-real positive non negative integer V108() V174() V175() V176() V177() V178() V179() Element of NAT
1 + 1 is non empty ordinal natural V28() real ext-real positive non negative integer V108() V174() V175() V176() V177() V178() V179() Element of NAT
len (Gauge (g,i)) is ordinal natural V28() real ext-real non negative integer V108() V174() V175() V176() V177() V178() V179() Element of NAT
[\(log (2,(((E-bound g) - (W-bound g)) / A)))/] + 1 is V28() real ext-real integer Element of REAL
(log (2,(((E-bound g) - (W-bound g)) / A))) - 1 is V28() real ext-real Element of REAL
((log (2,(((E-bound g) - (W-bound g)) / A))) - 1) + 1 is V28() real ext-real Element of REAL
((abs [\(log (2,(((E-bound g) - (W-bound g)) / A)))/]) + 1) + 1 is non empty ordinal natural V28() real ext-real positive non negative integer V108() V174() V175() V176() V177() V178() V179() Element of NAT
(2 |^ i) * A is V28() real ext-real Element of REAL
(((E-bound g) - (W-bound g)) / A) * A is V28() real ext-real Element of REAL
((2 |^ i) * A) / (2 |^ i) is V28() real ext-real Element of REAL
((E-bound g) - (W-bound g)) / (2 |^ i) is V28() real ext-real Element of REAL
width (Gauge (g,i)) is ordinal natural V28() real ext-real non negative integer V108() V174() V175() V176() V177() V178() V179() Element of NAT
[1,1] is non empty set
{1,1} is non empty V174() V175() V176() V177() V178() V179() set
{{1,1},{1}} is non empty set
Indices (Gauge (g,i)) is set
[1,(1 + 1)] is non empty set
{1,(1 + 1)} is non empty V174() V175() V176() V177() V178() V179() set
{{1,(1 + 1)},{1}} is non empty set
[(1 + 1),1] is non empty set
{(1 + 1),1} is non empty V174() V175() V176() V177() V178() V179() set
{(1 + 1)} is non empty V12() V174() V175() V176() V177() V178() V179() set
{{(1 + 1),1},{(1 + 1)}} is non empty set
g is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like non constant non empty V12() V38() FinSequence-like FinSubsequence-like circular special unfolded s.c.c. standard FinSequence of the carrier of (TOP-REAL 2)
L~ g is non empty boundary compact bounded non horizontal non vertical Element of K19( the carrier of (TOP-REAL 2))
(L~ g) ` is non empty Element of K19( the carrier of (TOP-REAL 2))
the carrier of (TOP-REAL 2) \ (L~ g) is set
(TOP-REAL 2) | ((L~ g) `) is non empty strict TopSpace-like SubSpace of TOP-REAL 2
the carrier of ((TOP-REAL 2) | ((L~ g) `)) is non empty set
K19( the carrier of ((TOP-REAL 2) | ((L~ g) `))) is non empty set
RightComp g is non empty open connected V222( TOP-REAL 2) Element of K19( the carrier of (TOP-REAL 2))
LeftComp g is non empty open connected V222( TOP-REAL 2) Element of K19( the carrier of (TOP-REAL 2))
A is Element of K19( the carrier of ((TOP-REAL 2) | ((L~ g) `)))
{} ((TOP-REAL 2) | ((L~ g) `)) is Function-like functional empty V12() proper FinSequence-membered open closed boundary nowhere_dense connected V174() V175() V176() V177() V178() V179() V180() Element of K19( the carrier of ((TOP-REAL 2) | ((L~ g) `)))
A is Element of the carrier of ((TOP-REAL 2) | ((L~ g) `))
(LeftComp g) \/ (RightComp g) is non empty open Element of K19( the carrier of (TOP-REAL 2))
x is Element of K19( the carrier of ((TOP-REAL 2) | ((L~ g) `)))
x is Element of K19( the carrier of ((TOP-REAL 2) | ((L~ g) `)))
g is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like non constant non empty V12() V38() FinSequence-like FinSubsequence-like circular special unfolded s.c.c. standard FinSequence of the carrier of (TOP-REAL 2)
L~ g is non empty boundary compact bounded non horizontal non vertical Element of K19( the carrier of (TOP-REAL 2))
(L~ g) ` is non empty Element of K19( the carrier of (TOP-REAL 2))
the carrier of (TOP-REAL 2) \ (L~ g) is set
(TOP-REAL 2) | ((L~ g) `) is non empty strict TopSpace-like SubSpace of TOP-REAL 2
the carrier of ((TOP-REAL 2) | ((L~ g) `)) is non empty set
K19( the carrier of ((TOP-REAL 2) | ((L~ g) `))) is non empty set
RightComp g is non empty open connected V222( TOP-REAL 2) Element of K19( the carrier of (TOP-REAL 2))
LeftComp g is non empty open connected V222( TOP-REAL 2) Element of K19( the carrier of (TOP-REAL 2))
A is Element of K19( the carrier of (TOP-REAL 2))
A is Element of K19( the carrier of (TOP-REAL 2))
A \/ A is Element of K19( the carrier of (TOP-REAL 2))
A /\ A is Element of K19( the carrier of (TOP-REAL 2))
x is Element of K19( the carrier of ((TOP-REAL 2) | ((L~ g) `)))
x is Element of K19( the carrier of ((TOP-REAL 2) | ((L~ g) `)))
g is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like non constant non empty V12() V38() FinSequence-like FinSubsequence-like circular special unfolded s.c.c. standard FinSequence of the carrier of (TOP-REAL 2)
LeftComp g is non empty open connected V222( TOP-REAL 2) Element of K19( the carrier of (TOP-REAL 2))
RightComp g is non empty open connected V222( TOP-REAL 2) Element of K19( the carrier of (TOP-REAL 2))
(LeftComp g) /\ (RightComp g) is open Element of K19( the carrier of (TOP-REAL 2))
A is set
A is set
A is set
L~ g is non empty boundary compact bounded non horizontal non vertical Element of K19( the carrier of (TOP-REAL 2))
(L~ g) ` is non empty Element of K19( the carrier of (TOP-REAL 2))
the carrier of (TOP-REAL 2) \ (L~ g) is set
g is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like non constant non empty V12() V38() FinSequence-like FinSubsequence-like circular special unfolded s.c.c. standard FinSequence of the carrier of (TOP-REAL 2)
L~ g is non empty boundary compact bounded non horizontal non vertical Element of K19( the carrier of (TOP-REAL 2))
RightComp g is non empty open connected V222( TOP-REAL 2) Element of K19( the carrier of (TOP-REAL 2))
(L~ g) \/ (RightComp g) is non empty Element of K19( the carrier of (TOP-REAL 2))
LeftComp g is non empty open connected V222( TOP-REAL 2) Element of K19( the carrier of (TOP-REAL 2))
((L~ g) \/ (RightComp g)) \/ (LeftComp g) is non empty Element of K19( the carrier of (TOP-REAL 2))
(L~ g) ` is non empty Element of K19( the carrier of (TOP-REAL 2))
the carrier of (TOP-REAL 2) \ (L~ g) is set
((L~ g) `) \/ (L~ g) is non empty Element of K19( the carrier of (TOP-REAL 2))
[#] the carrier of (TOP-REAL 2) is non empty non proper Element of K19( the carrier of (TOP-REAL 2))
(RightComp g) \/ (LeftComp g) is non empty open Element of K19( the carrier of (TOP-REAL 2))
g is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like non constant non empty V12() V38() FinSequence-like FinSubsequence-like circular special unfolded s.c.c. standard FinSequence of the carrier of (TOP-REAL 2)
L~ g is non empty boundary compact bounded non horizontal non vertical Element of K19( the carrier of (TOP-REAL 2))
LeftComp g is non empty open connected V222( TOP-REAL 2) Element of K19( the carrier of (TOP-REAL 2))
RightComp g is non empty open connected V222( TOP-REAL 2) Element of K19( the carrier of (TOP-REAL 2))
A is Relation-like NAT -defined Function-like V38() V45(2) FinSequence-like FinSubsequence-like V166() Element of the carrier of (TOP-REAL 2)
(L~ g) ` is non empty Element of K19( the carrier of (TOP-REAL 2))
the carrier of (TOP-REAL 2) \ (L~ g) is set
(LeftComp g) \/ (RightComp g) is non empty open Element of K19( the carrier of (TOP-REAL 2))
g is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like non constant non empty V12() V38() FinSequence-like FinSubsequence-like circular special unfolded s.c.c. standard FinSequence of the carrier of (TOP-REAL 2)
LeftComp g is non empty open connected V222( TOP-REAL 2) Element of K19( the carrier of (TOP-REAL 2))
L~ g is non empty boundary compact bounded non horizontal non vertical Element of K19( the carrier of (TOP-REAL 2))
RightComp g is non empty open connected V222( TOP-REAL 2) Element of K19( the carrier of (TOP-REAL 2))
A is Relation-like NAT -defined Function-like V38() V45(2) FinSequence-like FinSubsequence-like V166() Element of the carrier of (TOP-REAL 2)
(L~ g) ` is non empty Element of K19( the carrier of (TOP-REAL 2))
the carrier of (TOP-REAL 2) \ (L~ g) is set
(LeftComp g) \/ (RightComp g) is non empty open Element of K19( the carrier of (TOP-REAL 2))
(LeftComp g) /\ (RightComp g) is open Element of K19( the carrier of (TOP-REAL 2))
A is Relation-like NAT -defined Function-like V38() V45(2) FinSequence-like FinSubsequence-like V166() Element of the carrier of (TOP-REAL 2)
g is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like non constant non empty V12() V38() FinSequence-like FinSubsequence-like circular special unfolded s.c.c. standard FinSequence of the carrier of (TOP-REAL 2)
RightComp g is non empty open connected V222( TOP-REAL 2) Element of K19( the carrier of (TOP-REAL 2))
L~ g is non empty boundary compact bounded non horizontal non vertical Element of K19( the carrier of (TOP-REAL 2))
LeftComp g is non empty open connected V222( TOP-REAL 2) Element of K19( the carrier of (TOP-REAL 2))
x is Relation-like NAT -defined Function-like V38() V45(2) FinSequence-like FinSubsequence-like V166() Element of the carrier of (TOP-REAL 2)
A is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like non constant non empty V12() V38() FinSequence-like FinSubsequence-like circular special unfolded s.c.c. standard FinSequence of the carrier of (TOP-REAL 2)
L~ A is non empty boundary compact bounded non horizontal non vertical Element of K19( the carrier of (TOP-REAL 2))
LeftComp A is non empty open connected V222( TOP-REAL 2) Element of K19( the carrier of (TOP-REAL 2))
RightComp A is non empty open connected V222( TOP-REAL 2) Element of K19( the carrier of (TOP-REAL 2))
g is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like non constant non empty V12() V38() FinSequence-like FinSubsequence-like circular special unfolded s.c.c. standard FinSequence of the carrier of (TOP-REAL 2)
L~ g is non empty boundary compact bounded non horizontal non vertical Element of K19( the carrier of (TOP-REAL 2))
RightComp g is non empty open connected V222( TOP-REAL 2) Element of K19( the carrier of (TOP-REAL 2))
Cl (RightComp g) is closed Element of K19( the carrier of (TOP-REAL 2))
(Cl (RightComp g)) \ (RightComp g) is Element of K19( the carrier of (TOP-REAL 2))
A is set
len g is ordinal natural V28() real ext-real non negative integer V108() V174() V175() V176() V177() V178() V179() Element of NAT
A is Relation-like NAT -defined Function-like V38() V45(2) FinSequence-like FinSubsequence-like V166() Element of the carrier of (TOP-REAL 2)
x is ordinal natural V28() real ext-real non negative integer V108() V174() V175() V176() V177() V178() V179() Element of NAT
x + 1 is non empty ordinal natural V28() real ext-real positive non negative integer V108() V174() V175() V176() V177() V178() V179() Element of NAT
LSeg (g,x) is Element of K19( the carrier of (TOP-REAL 2))
left_cell (g,x) is Element of K19( the carrier of (TOP-REAL 2))
right_cell (g,x) is Element of K19( the carrier of (TOP-REAL 2))
(left_cell (g,x)) /\ (right_cell (g,x)) is Element of K19( the carrier of (TOP-REAL 2))
GoB g is Relation-like non empty-yielding NAT -defined the carrier of (TOP-REAL 2) * -valued Function-like V38() FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of the carrier of (TOP-REAL 2) *
Indices (GoB g) is set
g /. x is Relation-like NAT -defined Function-like V38() V45(2) FinSequence-like FinSubsequence-like V166() Element of the carrier of (TOP-REAL 2)
g /. (x + 1) is Relation-like NAT -defined Function-like V38() V45(2) FinSequence-like FinSubsequence-like V166() Element of the carrier of (TOP-REAL 2)
x is ordinal natural V28() real ext-real non negative integer V108() V174() V175() V176() V177() V178() V179() Element of NAT
b is ordinal natural V28() real ext-real non negative integer V108() V174() V175() V176() V177() V178() V179() Element of NAT
[x,b] is non empty set
{x,b} is non empty V174() V175() V176() V177() V178() V179() set
{x} is non empty V12() V174() V175() V176() V177() V178() V179() set
{{x,b},{x}} is non empty set
(GoB g) * (x,b) is Relation-like NAT -defined Function-like V38() V45(2) FinSequence-like FinSubsequence-like V166() Element of the carrier of (TOP-REAL 2)
c is ordinal natural V28() real ext-real non negative integer V108() V174() V175() V176() V177() V178() V179() Element of NAT
c is ordinal natural V28() real ext-real non negative integer V108() V174() V175() V176() V177() V178() V179() Element of NAT
[c,c] is non empty set
{c,c} is non empty V174() V175() V176() V177() V178() V179() set
{c} is non empty V12() V174() V175() V176() V177() V178() V179() set
{{c,c},{c}} is non empty set
(GoB g) * (c,c) is Relation-like NAT -defined Function-like V38() V45(2) FinSequence-like FinSubsequence-like V166() Element of the carrier of (TOP-REAL 2)
b + 1 is non empty ordinal natural V28() real ext-real positive non negative integer V108() V174() V175() V176() V177() V178() V179() Element of NAT
x + 1 is non empty ordinal natural V28() real ext-real positive non negative integer V108() V174() V175() V176() V177() V178() V179() Element of NAT
c + 1 is non empty ordinal natural V28() real ext-real positive non negative integer V108() V174() V175() V176() V177() V178() V179() Element of NAT
c + 1 is non empty ordinal natural V28() real ext-real positive non negative integer V108() V174() V175() V176() V177() V178() V179() Element of NAT
width (GoB g) is ordinal natural V28() real ext-real non negative integer V108() V174() V175() V176() V177() V178() V179() Element of NAT
len (GoB g) is ordinal natural V28() real ext-real non negative integer V108() V174() V175() V176() V177() V178() V179() Element of NAT
x -' 1 is ordinal natural V28() real ext-real non negative integer V108() V174() V175() V176() V177() V178() V179() Element of NAT
(x -' 1) + 1 is non empty ordinal natural V28() real ext-real positive non negative integer V108() V174() V175() V176() V177() V178() V179() Element of NAT
cell ((GoB g),((x -' 1) + 1),b) is Element of K19( the carrier of (TOP-REAL 2))
Int (right_cell (g,x)) is open Element of K19( the carrier of (TOP-REAL 2))
Cl (Int (right_cell (g,x))) is closed Element of K19( the carrier of (TOP-REAL 2))
b -' 1 is ordinal natural V28() real ext-real non negative integer V108() V174() V175() V176() V177() V178() V179() Element of NAT
(b -' 1) + 1 is non empty ordinal natural V28() real ext-real positive non negative integer V108() V174() V175() V176() V177() V178() V179() Element of NAT
cell ((GoB g),x,(b -' 1)) is Element of K19( the carrier of (TOP-REAL 2))
Int (right_cell (g,x)) is open Element of K19( the carrier of (TOP-REAL 2))
Cl (Int (right_cell (g,x))) is closed Element of K19( the carrier of (TOP-REAL 2))
b -' 1 is ordinal natural V28() real ext-real non negative integer V108() V174() V175() V176() V177() V178() V179() Element of NAT
(b -' 1) + 1 is non empty ordinal natural V28() real ext-real positive non negative integer V108() V174() V175() V176() V177() V178() V179() Element of NAT
cell ((GoB g),c,((b -' 1) + 1)) is Element of K19( the carrier of (TOP-REAL 2))
Int (right_cell (g,x)) is open Element of K19( the carrier of (TOP-REAL 2))
Cl (Int (right_cell (g,x))) is closed Element of K19( the carrier of (TOP-REAL 2))
x -' 1 is ordinal natural V28() real ext-real non negative integer V108() V174() V175() V176() V177() V178() V179() Element of NAT
(x -' 1) + 1 is non empty ordinal natural V28() real ext-real positive non negative integer V108() V174() V175() V176() V177() V178() V179() Element of NAT
cell ((GoB g),(x -' 1),c) is Element of K19( the carrier of (TOP-REAL 2))
Int (right_cell (g,x)) is open Element of K19( the carrier of (TOP-REAL 2))
Cl (Int (right_cell (g,x))) is closed Element of K19( the carrier of (TOP-REAL 2))
Int (right_cell (g,x)) is open Element of K19( the carrier of (TOP-REAL 2))
Cl (Int (right_cell (g,x))) is closed Element of K19( the carrier of (TOP-REAL 2))
Int (right_cell (g,x)) is open Element of K19( the carrier of (TOP-REAL 2))
Cl (Int (right_cell (g,x))) is closed Element of K19( the carrier of (TOP-REAL 2))
O is Element of K19( the carrier of (TOP-REAL 2))
A is set
A is Relation-like NAT -defined Function-like V38() V45(2) FinSequence-like FinSubsequence-like V166() Element of the carrier of (TOP-REAL 2)
LeftComp g is non empty open connected V222( TOP-REAL 2) Element of K19( the carrier of (TOP-REAL 2))
g is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like non constant non empty V12() V38() FinSequence-like FinSubsequence-like circular special unfolded s.c.c. standard FinSequence of the carrier of (TOP-REAL 2)
L~ g is non empty boundary compact bounded non horizontal non vertical Element of K19( the carrier of (TOP-REAL 2))
LeftComp g is non empty open connected V222( TOP-REAL 2) Element of K19( the carrier of (TOP-REAL 2))
Cl (LeftComp g) is closed Element of K19( the carrier of (TOP-REAL 2))
(Cl (LeftComp g)) \ (LeftComp g) is Element of K19( the carrier of (TOP-REAL 2))
A is set
len g is ordinal natural V28() real ext-real non negative integer V108() V174() V175() V176() V177() V178() V179() Element of NAT
A is Relation-like NAT -defined Function-like V38() V45(2) FinSequence-like FinSubsequence-like V166() Element of the carrier of (TOP-REAL 2)
x is ordinal natural V28() real ext-real non negative integer V108() V174() V175() V176() V177() V178() V179() Element of NAT
x + 1 is non empty ordinal natural V28() real ext-real positive non negative integer V108() V174() V175() V176() V177() V178() V179() Element of NAT
LSeg (g,x) is Element of K19( the carrier of (TOP-REAL 2))
left_cell (g,x) is Element of K19( the carrier of (TOP-REAL 2))
right_cell (g,x) is Element of K19( the carrier of (TOP-REAL 2))
(left_cell (g,x)) /\ (right_cell (g,x)) is Element of K19( the carrier of (TOP-REAL 2))
GoB g is Relation-like non empty-yielding NAT -defined the carrier of (TOP-REAL 2) * -valued Function-like V38() FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of the carrier of (TOP-REAL 2) *
Indices (GoB g) is set
g /. x is Relation-like NAT -defined Function-like V38() V45(2) FinSequence-like FinSubsequence-like V166() Element of the carrier of (TOP-REAL 2)
g /. (x + 1) is Relation-like NAT -defined Function-like V38() V45(2) FinSequence-like FinSubsequence-like V166() Element of the carrier of (TOP-REAL 2)
x is ordinal natural V28() real ext-real non negative integer V108() V174() V175() V176() V177() V178() V179() Element of NAT
b is ordinal natural V28() real ext-real non negative integer V108() V174() V175() V176() V177() V178() V179() Element of NAT
[x,b] is non empty set
{x,b} is non empty V174() V175() V176() V177() V178() V179() set
{x} is non empty V12() V174() V175() V176() V177() V178() V179() set
{{x,b},{x}} is non empty set
(GoB g) * (x,b) is Relation-like NAT -defined Function-like V38() V45(2) FinSequence-like FinSubsequence-like V166() Element of the carrier of (TOP-REAL 2)
c is ordinal natural V28() real ext-real non negative integer V108() V174() V175() V176() V177() V178() V179() Element of NAT
c is ordinal natural V28() real ext-real non negative integer V108() V174() V175() V176() V177() V178() V179() Element of NAT
[c,c] is non empty set
{c,c} is non empty V174() V175() V176() V177() V178() V179() set
{c} is non empty V12() V174() V175() V176() V177() V178() V179() set
{{c,c},{c}} is non empty set
(GoB g) * (c,c) is Relation-like NAT -defined Function-like V38() V45(2) FinSequence-like FinSubsequence-like V166() Element of the carrier of (TOP-REAL 2)
b + 1 is non empty ordinal natural V28() real ext-real positive non negative integer V108() V174() V175() V176() V177() V178() V179() Element of NAT
x + 1 is non empty ordinal natural V28() real ext-real positive non negative integer V108() V174() V175() V176() V177() V178() V179() Element of NAT
c + 1 is non empty ordinal natural V28() real ext-real positive non negative integer V108() V174() V175() V176() V177() V178() V179() Element of NAT
c + 1 is non empty ordinal natural V28() real ext-real positive non negative integer V108() V174() V175() V176() V177() V178() V179() Element of NAT
width (GoB g) is ordinal natural V28() real ext-real non negative integer V108() V174() V175() V176() V177() V178() V179() Element of NAT
len (GoB g) is ordinal natural V28() real ext-real non negative integer V108() V174() V175() V176() V177() V178() V179() Element of NAT
x -' 1 is ordinal natural V28() real ext-real non negative integer V108() V174() V175() V176() V177() V178() V179() Element of NAT
(x -' 1) + 1 is non empty ordinal natural V28() real ext-real positive non negative integer V108() V174() V175() V176() V177() V178() V179() Element of NAT
cell ((GoB g),(x -' 1),b) is Element of K19( the carrier of (TOP-REAL 2))
Int (left_cell (g,x)) is open Element of K19( the carrier of (TOP-REAL 2))
Cl (Int (left_cell (g,x))) is closed Element of K19( the carrier of (TOP-REAL 2))
b -' 1 is ordinal natural V28() real ext-real non negative integer V108() V174() V175() V176() V177() V178() V179() Element of NAT
(b -' 1) + 1 is non empty ordinal natural V28() real ext-real positive non negative integer V108() V174() V175() V176() V177() V178() V179() Element of NAT
cell ((GoB g),x,((b -' 1) + 1)) is Element of K19( the carrier of (TOP-REAL 2))
Int (left_cell (g,x)) is open Element of K19( the carrier of (TOP-REAL 2))
Cl (Int (left_cell (g,x))) is closed Element of K19( the carrier of (TOP-REAL 2))
b -' 1 is ordinal natural V28() real ext-real non negative integer V108() V174() V175() V176() V177() V178() V179() Element of NAT
(b -' 1) + 1 is non empty ordinal natural V28() real ext-real positive non negative integer V108() V174() V175() V176() V177() V178() V179() Element of NAT
cell ((GoB g),c,(b -' 1)) is Element of K19( the carrier of (TOP-REAL 2))
Int (left_cell (g,x)) is open Element of K19( the carrier of (TOP-REAL 2))
Cl (Int (left_cell (g,x))) is closed Element of K19( the carrier of (TOP-REAL 2))
x -' 1 is ordinal natural V28() real ext-real non negative integer V108() V174() V175() V176() V177() V178() V179() Element of NAT
(x -' 1) + 1 is non empty ordinal natural V28() real ext-real positive non negative integer V108() V174() V175() V176() V177() V178() V179() Element of NAT
cell ((GoB g),((x -' 1) + 1),c) is Element of K19( the carrier of (TOP-REAL 2))
Int (left_cell (g,x)) is open Element of K19( the carrier of (TOP-REAL 2))
Cl (Int (left_cell (g,x))) is closed Element of K19( the carrier of (TOP-REAL 2))
Int (left_cell (g,x)) is open Element of K19( the carrier of (TOP-REAL 2))
Cl (Int (left_cell (g,x))) is closed Element of K19( the carrier of (TOP-REAL 2))
Int (left_cell (g,x)) is open Element of K19( the carrier of (TOP-REAL 2))
Cl (Int (left_cell (g,x))) is closed Element of K19( the carrier of (TOP-REAL 2))
O is Element of K19( the carrier of (TOP-REAL 2))
A is set
A is Relation-like NAT -defined Function-like V38() V45(2) FinSequence-like FinSubsequence-like V166() Element of the carrier of (TOP-REAL 2)
RightComp g is non empty open connected V222( TOP-REAL 2) Element of K19( the carrier of (TOP-REAL 2))
g is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like non constant non empty V12() V38() FinSequence-like FinSubsequence-like circular special unfolded s.c.c. standard FinSequence of the carrier of (TOP-REAL 2)
RightComp g is non empty open connected V222( TOP-REAL 2) Element of K19( the carrier of (TOP-REAL 2))
Cl (RightComp g) is closed Element of K19( the carrier of (TOP-REAL 2))
L~ g is non empty boundary compact bounded non horizontal non vertical Element of K19( the carrier of (TOP-REAL 2))
(RightComp g) \/ (L~ g) is non empty Element of K19( the carrier of (TOP-REAL 2))
A is set
LeftComp g is non empty open connected V222( TOP-REAL 2) Element of K19( the carrier of (TOP-REAL 2))
(Cl (RightComp g)) \ (RightComp g) is Element of K19( the carrier of (TOP-REAL 2))
g is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like non constant non empty V12() V38() FinSequence-like FinSubsequence-like circular special unfolded s.c.c. standard FinSequence of the carrier of (TOP-REAL 2)
LeftComp g is non empty open connected V222( TOP-REAL 2) Element of K19( the carrier of (TOP-REAL 2))
Cl (LeftComp g) is closed Element of K19( the carrier of (TOP-REAL 2))
L~ g is non empty boundary compact bounded non horizontal non vertical Element of K19( the carrier of (TOP-REAL 2))
(LeftComp g) \/ (L~ g) is non empty Element of K19( the carrier of (TOP-REAL 2))
A is set
RightComp g is non empty open connected V222( TOP-REAL 2) Element of K19( the carrier of (TOP-REAL 2))
(Cl (LeftComp g)) \ (LeftComp g) is Element of K19( the carrier of (TOP-REAL 2))
g is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like non constant non empty V12() V38() FinSequence-like FinSubsequence-like circular special unfolded s.c.c. standard FinSequence of the carrier of (TOP-REAL 2)
L~ g is non empty boundary compact bounded non horizontal non vertical Element of K19( the carrier of (TOP-REAL 2))
(L~ g) ` is non empty Element of K19( the carrier of (TOP-REAL 2))
the carrier of (TOP-REAL 2) \ (L~ g) is set
RightComp g is non empty open connected V222( TOP-REAL 2) Element of K19( the carrier of (TOP-REAL 2))
A is non empty open connected V222( TOP-REAL 2) Element of K19( the carrier of (TOP-REAL 2))
Cl A is closed Element of K19( the carrier of (TOP-REAL 2))
(Cl A) \ A is Element of K19( the carrier of (TOP-REAL 2))
LeftComp g is non empty open connected V222( TOP-REAL 2) Element of K19( the carrier of (TOP-REAL 2))
A is non empty open connected V222( TOP-REAL 2) Element of K19( the carrier of (TOP-REAL 2))
A \/ A is non empty open Element of K19( the carrier of (TOP-REAL 2))
Cl A is closed Element of K19( the carrier of (TOP-REAL 2))
(Cl A) \ A is Element of K19( the carrier of (TOP-REAL 2))
g is Relation-like NAT -defined Function-like V38() V45(2) FinSequence-like FinSubsequence-like V166() Element of the carrier of (TOP-REAL 2)
g `1 is V28() real ext-real Element of REAL
K526(g,1) is V28() real ext-real Element of REAL
A is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like non constant non empty V12() V38() FinSequence-like FinSubsequence-like circular special unfolded s.c.c. standard clockwise_oriented FinSequence of the carrier of (TOP-REAL 2)
RightComp A is non empty open connected V222( TOP-REAL 2) Element of K19( the carrier of (TOP-REAL 2))
L~ A is non empty boundary compact bounded non horizontal non vertical Jordan Element of K19( the carrier of (TOP-REAL 2))
W-bound (L~ A) is V28() real ext-real Element of REAL
N-min (L~ A) is Relation-like NAT -defined Function-like V38() V45(2) FinSequence-like FinSubsequence-like V166() Element of the carrier of (TOP-REAL 2)
Rotate (A,(N-min (L~ A))) is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like non constant non empty V12() V38() FinSequence-like FinSubsequence-like circular special unfolded s.c.c. standard clockwise_oriented FinSequence of the carrier of (TOP-REAL 2)
L~ (Rotate (A,(N-min (L~ A)))) is non empty boundary compact bounded non horizontal non vertical Jordan Element of K19( the carrier of (TOP-REAL 2))
RightComp (Rotate (A,(N-min (L~ A)))) is non empty open connected V222( TOP-REAL 2) Element of K19( the carrier of (TOP-REAL 2))
x is Element of the carrier of (Euclid 2)
Int (RightComp (Rotate (A,(N-min (L~ A))))) is open Element of K19( the carrier of (TOP-REAL 2))
x is V28() real ext-real set
Ball (x,x) is Element of K19( the carrier of (Euclid 2))
K19( the carrier of (Euclid 2)) is non empty set
b is V28() real ext-real Element of REAL
b / 2 is V28() real ext-real Element of REAL
(g `1) - (b / 2) is V28() real ext-real Element of REAL
g `2 is V28() real ext-real Element of REAL
K526(g,2) is V28() real ext-real Element of REAL
|[((g `1) - (b / 2)),(g `2)]| is Relation-like NAT -defined Function-like non empty V38() V45(2) FinSequence-like FinSubsequence-like V166() Element of the carrier of (TOP-REAL 2)
c is Element of the carrier of (Euclid 2)
dist (x,c) is V28() real ext-real Element of REAL
(Pitag_dist 2) . (x,c) is set
|[((g `1) - (b / 2)),(g `2)]| `1 is V28() real ext-real Element of REAL
K526(|[((g `1) - (b / 2)),(g `2)]|,1) is V28() real ext-real Element of REAL
(g `1) - (|[((g `1) - (b / 2)),(g `2)]| `1) is V28() real ext-real Element of REAL
((g `1) - (|[((g `1) - (b / 2)),(g `2)]| `1)) ^2 is V28() real ext-real Element of REAL
K104(((g `1) - (|[((g `1) - (b / 2)),(g `2)]| `1)),((g `1) - (|[((g `1) - (b / 2)),(g `2)]| `1))) is V28() real ext-real set
|[((g `1) - (b / 2)),(g `2)]| `2 is V28() real ext-real Element of REAL
K526(|[((g `1) - (b / 2)),(g `2)]|,2) is V28() real ext-real Element of REAL
(g `2) - (|[((g `1) - (b / 2)),(g `2)]| `2) is V28() real ext-real Element of REAL
((g `2) - (|[((g `1) - (b / 2)),(g `2)]| `2)) ^2 is V28() real ext-real Element of REAL
K104(((g `2) - (|[((g `1) - (b / 2)),(g `2)]| `2)),((g `2) - (|[((g `1) - (b / 2)),(g `2)]| `2))) is V28() real ext-real set
(((g `1) - (|[((g `1) - (b / 2)),(g `2)]| `1)) ^2) + (((g `2) - (|[((g `1) - (b / 2)),(g `2)]| `2)) ^2) is V28() real ext-real Element of REAL
sqrt ((((g `1) - (|[((g `1) - (b / 2)),(g `2)]| `1)) ^2) + (((g `2) - (|[((g `1) - (b / 2)),(g `2)]| `2)) ^2)) is V28() real ext-real Element of REAL
(g `1) - ((g `1) - (b / 2)) is V28() real ext-real Element of REAL
((g `1) - ((g `1) - (b / 2))) ^2 is V28() real ext-real Element of REAL
K104(((g `1) - ((g `1) - (b / 2))),((g `1) - ((g `1) - (b / 2)))) is V28() real ext-real set
(((g `1) - ((g `1) - (b / 2))) ^2) + (((g `2) - (|[((g `1) - (b / 2)),(g `2)]| `2)) ^2) is V28() real ext-real Element of REAL
sqrt ((((g `1) - ((g `1) - (b / 2))) ^2) + (((g `2) - (|[((g `1) - (b / 2)),(g `2)]| `2)) ^2)) is V28() real ext-real Element of REAL
(g `2) - (g `2) is V28() real ext-real Element of REAL
((g `2) - (g `2)) ^2 is V28() real ext-real Element of REAL
K104(((g `2) - (g `2)),((g `2) - (g `2))) is V28() real ext-real set
(((g `1) - ((g `1) - (b / 2))) ^2) + (((g `2) - (g `2)) ^2) is V28() real ext-real Element of REAL
sqrt ((((g `1) - ((g `1) - (b / 2))) ^2) + (((g `2) - (g `2)) ^2)) is V28() real ext-real Element of REAL
b / 1 is V28() real ext-real Element of REAL
Ball (x,b) is Element of K19( the carrier of (Euclid 2))
LeftComp (Rotate (A,(N-min (L~ A)))) is non empty open connected V222( TOP-REAL 2) Element of K19( the carrier of (TOP-REAL 2))
SpStSeq (L~ (Rotate (A,(N-min (L~ A))))) is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like non constant non empty V12() V38() FinSequence-like FinSubsequence-like circular special unfolded s.c.c. standard rectangular clockwise_oriented FinSequence of the carrier of (TOP-REAL 2)
L~ (SpStSeq (L~ (Rotate (A,(N-min (L~ A)))))) is non empty boundary compact bounded non horizontal non vertical Jordan Element of K19( the carrier of (TOP-REAL 2))
N-bound (L~ (SpStSeq (L~ (Rotate (A,(N-min (L~ A))))))) is V28() real ext-real Element of REAL
|[((g `1) - (b / 2)),(N-bound (L~ (SpStSeq (L~ (Rotate (A,(N-min (L~ A))))))))]| is Relation-like NAT -defined Function-like non empty V38() V45(2) FinSequence-like FinSubsequence-like V166() Element of the carrier of (TOP-REAL 2)
NW-corner (L~ (Rotate (A,(N-min (L~ A))))) is Relation-like NAT -defined Function-like V38() V45(2) FinSequence-like FinSubsequence-like V166() Element of the carrier of (TOP-REAL 2)
NE-corner (L~ (Rotate (A,(N-min (L~ A))))) is Relation-like NAT -defined Function-like V38() V45(2) FinSequence-like FinSubsequence-like V166() Element of the carrier of (TOP-REAL 2)
LSeg ((NW-corner (L~ (Rotate (A,(N-min (L~ A)))))),(NE-corner (L~ (Rotate (A,(N-min (L~ A))))))) is boundary connected horizontal Element of K19( the carrier of (TOP-REAL 2))
proj1 . |[((g `1) - (b / 2)),(N-bound (L~ (SpStSeq (L~ (Rotate (A,(N-min (L~ A))))))))]| is set
|[((g `1) - (b / 2)),(N-bound (L~ (SpStSeq (L~ (Rotate (A,(N-min (L~ A))))))))]| `1 is V28() real ext-real Element of REAL
K526(|[((g `1) - (b / 2)),(N-bound (L~ (SpStSeq (L~ (Rotate (A,(N-min (L~ A))))))))]|,1) is V28() real ext-real Element of REAL
rng A is non empty V12() Element of K19( the carrier of (TOP-REAL 2))
(Rotate (A,(N-min (L~ A)))) /. 1 is Relation-like NAT -defined Function-like V38() V45(2) FinSequence-like FinSubsequence-like V166() Element of the carrier of (TOP-REAL 2)
N-min (L~ (Rotate (A,(N-min (L~ A))))) is Relation-like NAT -defined Function-like V38() V45(2) FinSequence-like FinSubsequence-like V166() Element of the carrier of (TOP-REAL 2)
E-bound (L~ (Rotate (A,(N-min (L~ A))))) is V28() real ext-real Element of REAL
|[((g `1) - (b / 2)),(N-bound (L~ (SpStSeq (L~ (Rotate (A,(N-min (L~ A))))))))]| `2 is V28() real ext-real Element of REAL
K526(|[((g `1) - (b / 2)),(N-bound (L~ (SpStSeq (L~ (Rotate (A,(N-min (L~ A))))))))]|,2) is V28() real ext-real Element of REAL
N-bound (L~ (Rotate (A,(N-min (L~ A))))) is V28() real ext-real Element of REAL
W-bound (L~ (Rotate (A,(N-min (L~ A))))) is V28() real ext-real Element of REAL
{ b1 where b1 is Relation-like NAT -defined Function-like V38() V45(2) FinSequence-like FinSubsequence-like V166() Element of the carrier of (TOP-REAL 2) : ( b1 `1 <= E-bound (L~ (Rotate (A,(N-min (L~ A))))) & W-bound (L~ (Rotate (A,(N-min (L~ A))))) <= b1 `1 & b1 `2 = N-bound (L~ (Rotate (A,(N-min (L~ A))))) ) } is set
proj1 .: (L~ (SpStSeq (L~ (Rotate (A,(N-min (L~ A))))))) is V174() V175() V176() bounded_below bounded_above Element of K19(REAL)
lower_bound (proj1 .: (L~ (SpStSeq (L~ (Rotate (A,(N-min (L~ A)))))))) is V28() real ext-real Element of REAL
(g `1) - 0 is V28() real ext-real Element of REAL
W-bound (L~ (SpStSeq (L~ (Rotate (A,(N-min (L~ A))))))) is V28() real ext-real Element of REAL
g is Relation-like NAT -defined Function-like V38() V45(2) FinSequence-like FinSubsequence-like V166() Element of the carrier of (TOP-REAL 2)
g `1 is V28() real ext-real Element of REAL
K526(g,1) is V28() real ext-real Element of REAL
A is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like non constant non empty V12() V38() FinSequence-like FinSubsequence-like circular special unfolded s.c.c. standard clockwise_oriented FinSequence of the carrier of (TOP-REAL 2)
RightComp A is non empty open connected V222( TOP-REAL 2) Element of K19( the carrier of (TOP-REAL 2))
L~ A is non empty boundary compact bounded non horizontal non vertical Jordan Element of K19( the carrier of (TOP-REAL 2))
E-bound (L~ A) is V28() real ext-real Element of REAL
N-min (L~ A) is Relation-like NAT -defined Function-like V38() V45(2) FinSequence-like FinSubsequence-like V166() Element of the carrier of (TOP-REAL 2)
Rotate (A,(N-min (L~ A))) is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like non constant non empty V12() V38() FinSequence-like FinSubsequence-like circular special unfolded s.c.c. standard clockwise_oriented FinSequence of the carrier of (TOP-REAL 2)
L~ (Rotate (A,(N-min (L~ A)))) is non empty boundary compact bounded non horizontal non vertical Jordan Element of K19( the carrier of (TOP-REAL 2))
RightComp (Rotate (A,(N-min (L~ A)))) is non empty open connected V222( TOP-REAL 2) Element of K19( the carrier of (TOP-REAL 2))
x is Element of the carrier of (Euclid 2)
Int (RightComp (Rotate (A,(N-min (L~ A))))) is open Element of K19( the carrier of (TOP-REAL 2))
x is V28() real ext-real set
Ball (x,x) is Element of K19( the carrier of (Euclid 2))
K19( the carrier of (Euclid 2)) is non empty set
b is V28() real ext-real Element of REAL
b / 2 is V28() real ext-real Element of REAL
(g `1) + (b / 2) is V28() real ext-real Element of REAL
g `2 is V28() real ext-real Element of REAL
K526(g,2) is V28() real ext-real Element of REAL
|[((g `1) + (b / 2)),(g `2)]| is Relation-like NAT -defined Function-like non empty V38() V45(2) FinSequence-like FinSubsequence-like V166() Element of the carrier of (TOP-REAL 2)
c is Element of the carrier of (Euclid 2)
dist (x,c) is V28() real ext-real Element of REAL
(Pitag_dist 2) . (x,c) is set
|[((g `1) + (b / 2)),(g `2)]| `1 is V28() real ext-real Element of REAL
K526(|[((g `1) + (b / 2)),(g `2)]|,1) is V28() real ext-real Element of REAL
(g `1) - (|[((g `1) + (b / 2)),(g `2)]| `1) is V28() real ext-real Element of REAL
((g `1) - (|[((g `1) + (b / 2)),(g `2)]| `1)) ^2 is V28() real ext-real Element of REAL
K104(((g `1) - (|[((g `1) + (b / 2)),(g `2)]| `1)),((g `1) - (|[((g `1) + (b / 2)),(g `2)]| `1))) is V28() real ext-real set
|[((g `1) + (b / 2)),(g `2)]| `2 is V28() real ext-real Element of REAL
K526(|[((g `1) + (b / 2)),(g `2)]|,2) is V28() real ext-real Element of REAL
(g `2) - (|[((g `1) + (b / 2)),(g `2)]| `2) is V28() real ext-real Element of REAL
((g `2) - (|[((g `1) + (b / 2)),(g `2)]| `2)) ^2 is V28() real ext-real Element of REAL
K104(((g `2) - (|[((g `1) + (b / 2)),(g `2)]| `2)),((g `2) - (|[((g `1) + (b / 2)),(g `2)]| `2))) is V28() real ext-real set
(((g `1) - (|[((g `1) + (b / 2)),(g `2)]| `1)) ^2) + (((g `2) - (|[((g `1) + (b / 2)),(g `2)]| `2)) ^2) is V28() real ext-real Element of REAL
sqrt ((((g `1) - (|[((g `1) + (b / 2)),(g `2)]| `1)) ^2) + (((g `2) - (|[((g `1) + (b / 2)),(g `2)]| `2)) ^2)) is V28() real ext-real Element of REAL
(g `1) - ((g `1) + (b / 2)) is V28() real ext-real Element of REAL
((g `1) - ((g `1) + (b / 2))) ^2 is V28() real ext-real Element of REAL
K104(((g `1) - ((g `1) + (b / 2))),((g `1) - ((g `1) + (b / 2)))) is V28() real ext-real set
(((g `1) - ((g `1) + (b / 2))) ^2) + (((g `2) - (|[((g `1) + (b / 2)),(g `2)]| `2)) ^2) is V28() real ext-real Element of REAL
sqrt ((((g `1) - ((g `1) + (b / 2))) ^2) + (((g `2) - (|[((g `1) + (b / 2)),(g `2)]| `2)) ^2)) is V28() real ext-real Element of REAL
(g `2) - (g `2) is V28() real ext-real Element of REAL
((g `2) - (g `2)) ^2 is V28() real ext-real Element of REAL
K104(((g `2) - (g `2)),((g `2) - (g `2))) is V28() real ext-real set
(((g `1) - ((g `1) + (b / 2))) ^2) + (((g `2) - (g `2)) ^2) is V28() real ext-real Element of REAL
sqrt ((((g `1) - ((g `1) + (b / 2))) ^2) + (((g `2) - (g `2)) ^2)) is V28() real ext-real Element of REAL
(b / 2) ^2 is V28() real ext-real Element of REAL
K104((b / 2),(b / 2)) is V28() real ext-real set
sqrt ((b / 2) ^2) is V28() real ext-real Element of REAL
b / 1 is V28() real ext-real Element of REAL
Ball (x,b) is Element of K19( the carrier of (Euclid 2))
LeftComp (Rotate (A,(N-min (L~ A)))) is non empty open connected V222( TOP-REAL 2) Element of K19( the carrier of (TOP-REAL 2))
SpStSeq (L~ (Rotate (A,(N-min (L~ A))))) is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like non constant non empty V12() V38() FinSequence-like FinSubsequence-like circular special unfolded s.c.c. standard rectangular clockwise_oriented FinSequence of the carrier of (TOP-REAL 2)
L~ (SpStSeq (L~ (Rotate (A,(N-min (L~ A)))))) is non empty boundary compact bounded non horizontal non vertical Jordan Element of K19( the carrier of (TOP-REAL 2))
N-bound (L~ (SpStSeq (L~ (Rotate (A,(N-min (L~ A))))))) is V28() real ext-real Element of REAL
|[((g `1) + (b / 2)),(N-bound (L~ (SpStSeq (L~ (Rotate (A,(N-min (L~ A))))))))]| is Relation-like NAT -defined Function-like non empty V38() V45(2) FinSequence-like FinSubsequence-like V166() Element of the carrier of (TOP-REAL 2)
NW-corner (L~ (Rotate (A,(N-min (L~ A))))) is Relation-like NAT -defined Function-like V38() V45(2) FinSequence-like FinSubsequence-like V166() Element of the carrier of (TOP-REAL 2)
NE-corner (L~ (Rotate (A,(N-min (L~ A))))) is Relation-like NAT -defined Function-like V38() V45(2) FinSequence-like FinSubsequence-like V166() Element of the carrier of (TOP-REAL 2)
LSeg ((NW-corner (L~ (Rotate (A,(N-min (L~ A)))))),(NE-corner (L~ (Rotate (A,(N-min (L~ A))))))) is boundary connected horizontal Element of K19( the carrier of (TOP-REAL 2))
proj1 . |[((g `1) + (b / 2)),(N-bound (L~ (SpStSeq (L~ (Rotate (A,(N-min (L~ A))))))))]| is set
|[((g `1) + (b / 2)),(N-bound (L~ (SpStSeq (L~ (Rotate (A,(N-min (L~ A))))))))]| `1 is V28() real ext-real Element of REAL
K526(|[((g `1) + (b / 2)),(N-bound (L~ (SpStSeq (L~ (Rotate (A,(N-min (L~ A))))))))]|,1) is V28() real ext-real Element of REAL
rng A is non empty V12() Element of K19( the carrier of (TOP-REAL 2))
(Rotate (A,(N-min (L~ A)))) /. 1 is Relation-like NAT -defined Function-like V38() V45(2) FinSequence-like FinSubsequence-like V166() Element of the carrier of (TOP-REAL 2)
N-min (L~ (Rotate (A,(N-min (L~ A))))) is Relation-like NAT -defined Function-like V38() V45(2) FinSequence-like FinSubsequence-like V166() Element of the carrier of (TOP-REAL 2)
E-bound (L~ (Rotate (A,(N-min (L~ A))))) is V28() real ext-real Element of REAL
|[((g `1) + (b / 2)),(N-bound (L~ (SpStSeq (L~ (Rotate (A,(N-min (L~ A))))))))]| `2 is V28() real ext-real Element of REAL
K526(|[((g `1) + (b / 2)),(N-bound (L~ (SpStSeq (L~ (Rotate (A,(N-min (L~ A))))))))]|,2) is V28() real ext-real Element of REAL
N-bound (L~ (Rotate (A,(N-min (L~ A))))) is V28() real ext-real Element of REAL
W-bound (L~ (Rotate (A,(N-min (L~ A))))) is V28() real ext-real Element of REAL
{ b1 where b1 is Relation-like NAT -defined Function-like V38() V45(2) FinSequence-like FinSubsequence-like V166() Element of the carrier of (TOP-REAL 2) : ( b1 `1 <= E-bound (L~ (Rotate (A,(N-min (L~ A))))) & W-bound (L~ (Rotate (A,(N-min (L~ A))))) <= b1 `1 & b1 `2 = N-bound (L~ (Rotate (A,(N-min (L~ A))))) ) } is set
proj1 .: (L~ (SpStSeq (L~ (Rotate (A,(N-min (L~ A))))))) is V174() V175() V176() bounded_below bounded_above Element of K19(REAL)
upper_bound (proj1 .: (L~ (SpStSeq (L~ (Rotate (A,(N-min (L~ A)))))))) is V28() real ext-real Element of REAL
(g `1) + 0 is V28() real ext-real Element of REAL
E-bound (L~ (SpStSeq (L~ (Rotate (A,(N-min (L~ A))))))) is V28() real ext-real Element of REAL
g is Relation-like NAT -defined Function-like V38() V45(2) FinSequence-like FinSubsequence-like V166() Element of the carrier of (TOP-REAL 2)
g `2 is V28() real ext-real Element of REAL
K526(g,2) is V28() real ext-real Element of REAL
A is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like non constant non empty V12() V38() FinSequence-like FinSubsequence-like circular special unfolded s.c.c. standard clockwise_oriented FinSequence of the carrier of (TOP-REAL 2)
RightComp A is non empty open connected V222( TOP-REAL 2) Element of K19( the carrier of (TOP-REAL 2))
L~ A is non empty boundary compact bounded non horizontal non vertical Jordan Element of K19( the carrier of (TOP-REAL 2))
N-bound (L~ A) is V28() real ext-real Element of REAL
N-min (L~ A) is Relation-like NAT -defined Function-like V38() V45(2) FinSequence-like FinSubsequence-like V166() Element of the carrier of (TOP-REAL 2)
Rotate (A,(N-min (L~ A))) is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like non constant non empty V12() V38() FinSequence-like FinSubsequence-like circular special unfolded s.c.c. standard clockwise_oriented FinSequence of the carrier of (TOP-REAL 2)
L~ (Rotate (A,(N-min (L~ A)))) is non empty boundary compact bounded non horizontal non vertical Jordan Element of K19( the carrier of (TOP-REAL 2))
RightComp (Rotate (A,(N-min (L~ A)))) is non empty open connected V222( TOP-REAL 2) Element of K19( the carrier of (TOP-REAL 2))
x is Element of the carrier of (Euclid 2)
Int (RightComp (Rotate (A,(N-min (L~ A))))) is open Element of K19( the carrier of (TOP-REAL 2))
x is V28() real ext-real set
Ball (x,x) is Element of K19( the carrier of (Euclid 2))
K19( the carrier of (Euclid 2)) is non empty set
g `1 is V28() real ext-real Element of REAL
K526(g,1) is V28() real ext-real Element of REAL
b is V28() real ext-real Element of REAL
b / 2 is V28() real ext-real Element of REAL
(g `2) + (b / 2) is V28() real ext-real Element of REAL
|[(g `1),((g `2) + (b / 2))]| is Relation-like NAT -defined Function-like non empty V38() V45(2) FinSequence-like FinSubsequence-like V166() Element of the carrier of (TOP-REAL 2)
c is Element of the carrier of (Euclid 2)
dist (x,c) is V28() real ext-real Element of REAL
(Pitag_dist 2) . (x,c) is set
|[(g `1),((g `2) + (b / 2))]| `1 is V28() real ext-real Element of REAL
K526(|[(g `1),((g `2) + (b / 2))]|,1) is V28() real ext-real Element of REAL
(g `1) - (|[(g `1),((g `2) + (b / 2))]| `1) is V28() real ext-real Element of REAL
((g `1) - (|[(g `1),((g `2) + (b / 2))]| `1)) ^2 is V28() real ext-real Element of REAL
K104(((g `1) - (|[(g `1),((g `2) + (b / 2))]| `1)),((g `1) - (|[(g `1),((g `2) + (b / 2))]| `1))) is V28() real ext-real set
|[(g `1),((g `2) + (b / 2))]| `2 is V28() real ext-real Element of REAL
K526(|[(g `1),((g `2) + (b / 2))]|,2) is V28() real ext-real Element of REAL
(g `2) - (|[(g `1),((g `2) + (b / 2))]| `2) is V28() real ext-real Element of REAL
((g `2) - (|[(g `1),((g `2) + (b / 2))]| `2)) ^2 is V28() real ext-real Element of REAL
K104(((g `2) - (|[(g `1),((g `2) + (b / 2))]| `2)),((g `2) - (|[(g `1),((g `2) + (b / 2))]| `2))) is V28() real ext-real set
(((g `1) - (|[(g `1),((g `2) + (b / 2))]| `1)) ^2) + (((g `2) - (|[(g `1),((g `2) + (b / 2))]| `2)) ^2) is V28() real ext-real Element of REAL
sqrt ((((g `1) - (|[(g `1),((g `2) + (b / 2))]| `1)) ^2) + (((g `2) - (|[(g `1),((g `2) + (b / 2))]| `2)) ^2)) is V28() real ext-real Element of REAL
(g `1) - (g `1) is V28() real ext-real Element of REAL
((g `1) - (g `1)) ^2 is V28() real ext-real Element of REAL
K104(((g `1) - (g `1)),((g `1) - (g `1))) is V28() real ext-real set
(((g `1) - (g `1)) ^2) + (((g `2) - (|[(g `1),((g `2) + (b / 2))]| `2)) ^2) is V28() real ext-real Element of REAL
sqrt ((((g `1) - (g `1)) ^2) + (((g `2) - (|[(g `1),((g `2) + (b / 2))]| `2)) ^2)) is V28() real ext-real Element of REAL
(g `2) - ((g `2) + (b / 2)) is V28() real ext-real Element of REAL
((g `2) - ((g `2) + (b / 2))) ^2 is V28() real ext-real Element of REAL
K104(((g `2) - ((g `2) + (b / 2))),((g `2) - ((g `2) + (b / 2)))) is V28() real ext-real set
sqrt (((g `2) - ((g `2) + (b / 2))) ^2) is V28() real ext-real Element of REAL
(b / 2) ^2 is V28() real ext-real Element of REAL
K104((b / 2),(b / 2)) is V28() real ext-real set
sqrt ((b / 2) ^2) is V28() real ext-real Element of REAL
b / 1 is V28() real ext-real Element of REAL
Ball (x,b) is Element of K19( the carrier of (Euclid 2))
LeftComp (Rotate (A,(N-min (L~ A)))) is non empty open connected V222( TOP-REAL 2) Element of K19( the carrier of (TOP-REAL 2))
SpStSeq (L~ (Rotate (A,(N-min (L~ A))))) is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like non constant non empty V12() V38() FinSequence-like FinSubsequence-like circular special unfolded s.c.c. standard rectangular clockwise_oriented FinSequence of the carrier of (TOP-REAL 2)
L~ (SpStSeq (L~ (Rotate (A,(N-min (L~ A)))))) is non empty boundary compact bounded non horizontal non vertical Jordan Element of K19( the carrier of (TOP-REAL 2))
E-bound (L~ (SpStSeq (L~ (Rotate (A,(N-min (L~ A))))))) is V28() real ext-real Element of REAL
|[(E-bound (L~ (SpStSeq (L~ (Rotate (A,(N-min (L~ A)))))))),((g `2) + (b / 2))]| is Relation-like NAT -defined Function-like non empty V38() V45(2) FinSequence-like FinSubsequence-like V166() Element of the carrier of (TOP-REAL 2)
SE-corner (L~ (Rotate (A,(N-min (L~ A))))) is Relation-like NAT -defined Function-like V38() V45(2) FinSequence-like FinSubsequence-like V166() Element of the carrier of (TOP-REAL 2)
NE-corner (L~ (Rotate (A,(N-min (L~ A))))) is Relation-like NAT -defined Function-like V38() V45(2) FinSequence-like FinSubsequence-like V166() Element of the carrier of (TOP-REAL 2)
LSeg ((SE-corner (L~ (Rotate (A,(N-min (L~ A)))))),(NE-corner (L~ (Rotate (A,(N-min (L~ A))))))) is boundary connected Element of K19( the carrier of (TOP-REAL 2))
proj2 . |[(E-bound (L~ (SpStSeq (L~ (Rotate (A,(N-min (L~ A)))))))),((g `2) + (b / 2))]| is set
|[(E-bound (L~ (SpStSeq (L~ (Rotate (A,(N-min (L~ A)))))))),((g `2) + (b / 2))]| `2 is V28() real ext-real Element of REAL
K526(|[(E-bound (L~ (SpStSeq (L~ (Rotate (A,(N-min (L~ A)))))))),((g `2) + (b / 2))]|,2) is V28() real ext-real Element of REAL
rng A is non empty V12() Element of K19( the carrier of (TOP-REAL 2))
(Rotate (A,(N-min (L~ A)))) /. 1 is Relation-like NAT -defined Function-like V38() V45(2) FinSequence-like FinSubsequence-like V166() Element of the carrier of (TOP-REAL 2)
N-min (L~ (Rotate (A,(N-min (L~ A))))) is Relation-like NAT -defined Function-like V38() V45(2) FinSequence-like FinSubsequence-like V166() Element of the carrier of (TOP-REAL 2)
N-bound (L~ (Rotate (A,(N-min (L~ A))))) is V28() real ext-real Element of REAL
|[(E-bound (L~ (SpStSeq (L~ (Rotate (A,(N-min (L~ A)))))))),((g `2) + (b / 2))]| `1 is V28() real ext-real Element of REAL
K526(|[(E-bound (L~ (SpStSeq (L~ (Rotate (A,(N-min (L~ A)))))))),((g `2) + (b / 2))]|,1) is V28() real ext-real Element of REAL
E-bound (L~ (Rotate (A,(N-min (L~ A))))) is V28() real ext-real Element of REAL
S-bound (L~ (Rotate (A,(N-min (L~ A))))) is V28() real ext-real Element of REAL
{ b1 where b1 is Relation-like NAT -defined Function-like V38() V45(2) FinSequence-like FinSubsequence-like V166() Element of the carrier of (TOP-REAL 2) : ( b1 `1 = E-bound (L~ (Rotate (A,(N-min (L~ A))))) & b1 `2 <= N-bound (L~ (Rotate (A,(N-min (L~ A))))) & S-bound (L~ (Rotate (A,(N-min (L~ A))))) <= b1 `2 ) } is set
proj2 .: (L~ (SpStSeq (L~ (Rotate (A,(N-min (L~ A))))))) is V174() V175() V176() bounded_below bounded_above Element of K19(REAL)
upper_bound (proj2 .: (L~ (SpStSeq (L~ (Rotate (A,(N-min (L~ A)))))))) is V28() real ext-real Element of REAL
(g `2) + 0 is V28() real ext-real Element of REAL
N-bound (L~ (SpStSeq (L~ (Rotate (A,(N-min (L~ A))))))) is V28() real ext-real Element of REAL
g is Relation-like NAT -defined Function-like V38() V45(2) FinSequence-like FinSubsequence-like V166() Element of the carrier of (TOP-REAL 2)
g `2 is V28() real ext-real Element of REAL
K526(g,2) is V28() real ext-real Element of REAL
A is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like non constant non empty V12() V38() FinSequence-like FinSubsequence-like circular special unfolded s.c.c. standard clockwise_oriented FinSequence of the carrier of (TOP-REAL 2)
RightComp A is non empty open connected V222( TOP-REAL 2) Element of K19( the carrier of (TOP-REAL 2))
L~ A is non empty boundary compact bounded non horizontal non vertical Jordan Element of K19( the carrier of (TOP-REAL 2))
S-bound (L~ A) is V28() real ext-real Element of REAL
N-min (L~ A) is Relation-like NAT -defined Function-like V38() V45(2) FinSequence-like FinSubsequence-like V166() Element of the carrier of (TOP-REAL 2)
Rotate (A,(N-min (L~ A))) is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like non constant non empty V12() V38() FinSequence-like FinSubsequence-like circular special unfolded s.c.c. standard clockwise_oriented FinSequence of the carrier of (TOP-REAL 2)
L~ (Rotate (A,(N-min (L~ A)))) is non empty boundary compact bounded non horizontal non vertical Jordan Element of K19( the carrier of (TOP-REAL 2))
RightComp (Rotate (A,(N-min (L~ A)))) is non empty open connected V222( TOP-REAL 2) Element of K19( the carrier of (TOP-REAL 2))
x is Element of the carrier of (Euclid 2)
Int (RightComp (Rotate (A,(N-min (L~ A))))) is open Element of K19( the carrier of (TOP-REAL 2))
x is V28() real ext-real set
Ball (x,x) is Element of K19( the carrier of (Euclid 2))
K19( the carrier of (Euclid 2)) is non empty set
g `1 is V28() real ext-real Element of REAL
K526(g,1) is V28() real ext-real Element of REAL
b is V28() real ext-real Element of REAL
b / 2 is V28() real ext-real Element of REAL
(g `2) - (b / 2) is V28() real ext-real Element of REAL
|[(g `1),((g `2) - (b / 2))]| is Relation-like NAT -defined Function-like non empty V38() V45(2) FinSequence-like FinSubsequence-like V166() Element of the carrier of (TOP-REAL 2)
c is Element of the carrier of (Euclid 2)
dist (x,c) is V28() real ext-real Element of REAL
(Pitag_dist 2) . (x,c) is set
|[(g `1),((g `2) - (b / 2))]| `1 is V28() real ext-real Element of REAL
K526(|[(g `1),((g `2) - (b / 2))]|,1) is V28() real ext-real Element of REAL
(g `1) - (|[(g `1),((g `2) - (b / 2))]| `1) is V28() real ext-real Element of REAL
((g `1) - (|[(g `1),((g `2) - (b / 2))]| `1)) ^2 is V28() real ext-real Element of REAL
K104(((g `1) - (|[(g `1),((g `2) - (b / 2))]| `1)),((g `1) - (|[(g `1),((g `2) - (b / 2))]| `1))) is V28() real ext-real set
|[(g `1),((g `2) - (b / 2))]| `2 is V28() real ext-real Element of REAL
K526(|[(g `1),((g `2) - (b / 2))]|,2) is V28() real ext-real Element of REAL
(g `2) - (|[(g `1),((g `2) - (b / 2))]| `2) is V28() real ext-real Element of REAL
((g `2) - (|[(g `1),((g `2) - (b / 2))]| `2)) ^2 is V28() real ext-real Element of REAL
K104(((g `2) - (|[(g `1),((g `2) - (b / 2))]| `2)),((g `2) - (|[(g `1),((g `2) - (b / 2))]| `2))) is V28() real ext-real set
(((g `1) - (|[(g `1),((g `2) - (b / 2))]| `1)) ^2) + (((g `2) - (|[(g `1),((g `2) - (b / 2))]| `2)) ^2) is V28() real ext-real Element of REAL
sqrt ((((g `1) - (|[(g `1),((g `2) - (b / 2))]| `1)) ^2) + (((g `2) - (|[(g `1),((g `2) - (b / 2))]| `2)) ^2)) is V28() real ext-real Element of REAL
(g `1) - (g `1) is V28() real ext-real Element of REAL
((g `1) - (g `1)) ^2 is V28() real ext-real Element of REAL
K104(((g `1) - (g `1)),((g `1) - (g `1))) is V28() real ext-real set
(((g `1) - (g `1)) ^2) + (((g `2) - (|[(g `1),((g `2) - (b / 2))]| `2)) ^2) is V28() real ext-real Element of REAL
sqrt ((((g `1) - (g `1)) ^2) + (((g `2) - (|[(g `1),((g `2) - (b / 2))]| `2)) ^2)) is V28() real ext-real Element of REAL
(g `2) - ((g `2) - (b / 2)) is V28() real ext-real Element of REAL
((g `2) - ((g `2) - (b / 2))) ^2 is V28() real ext-real Element of REAL
K104(((g `2) - ((g `2) - (b / 2))),((g `2) - ((g `2) - (b / 2)))) is V28() real ext-real set
sqrt (((g `2) - ((g `2) - (b / 2))) ^2) is V28() real ext-real Element of REAL
b / 1 is V28() real ext-real Element of REAL
Ball (x,b) is Element of K19( the carrier of (Euclid 2))
LeftComp (Rotate (A,(N-min (L~ A)))) is non empty open connected V222( TOP-REAL 2) Element of K19( the carrier of (TOP-REAL 2))
SpStSeq (L~ (Rotate (A,(N-min (L~ A))))) is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like non constant non empty V12() V38() FinSequence-like FinSubsequence-like circular special unfolded s.c.c. standard rectangular clockwise_oriented FinSequence of the carrier of (TOP-REAL 2)
L~ (SpStSeq (L~ (Rotate (A,(N-min (L~ A)))))) is non empty boundary compact bounded non horizontal non vertical Jordan Element of K19( the carrier of (TOP-REAL 2))
E-bound (L~ (SpStSeq (L~ (Rotate (A,(N-min (L~ A))))))) is V28() real ext-real Element of REAL
|[(E-bound (L~ (SpStSeq (L~ (Rotate (A,(N-min (L~ A)))))))),((g `2) - (b / 2))]| is Relation-like NAT -defined Function-like non empty V38() V45(2) FinSequence-like FinSubsequence-like V166() Element of the carrier of (TOP-REAL 2)
SE-corner (L~ (Rotate (A,(N-min (L~ A))))) is Relation-like NAT -defined Function-like V38() V45(2) FinSequence-like FinSubsequence-like V166() Element of the carrier of (TOP-REAL 2)
NE-corner (L~ (Rotate (A,(N-min (L~ A))))) is Relation-like NAT -defined Function-like V38() V45(2) FinSequence-like FinSubsequence-like V166() Element of the carrier of (TOP-REAL 2)
LSeg ((SE-corner (L~ (Rotate (A,(N-min (L~ A)))))),(NE-corner (L~ (Rotate (A,(N-min (L~ A))))))) is boundary connected Element of K19( the carrier of (TOP-REAL 2))
proj2 . |[(E-bound (L~ (SpStSeq (L~ (Rotate (A,(N-min (L~ A)))))))),((g `2) - (b / 2))]| is set
|[(E-bound (L~ (SpStSeq (L~ (Rotate (A,(N-min (L~ A)))))))),((g `2) - (b / 2))]| `2 is V28() real ext-real Element of REAL
K526(|[(E-bound (L~ (SpStSeq (L~ (Rotate (A,(N-min (L~ A)))))))),((g `2) - (b / 2))]|,2) is V28() real ext-real Element of REAL
rng A is non empty V12() Element of K19( the carrier of (TOP-REAL 2))
(Rotate (A,(N-min (L~ A)))) /. 1 is Relation-like NAT -defined Function-like V38() V45(2) FinSequence-like FinSubsequence-like V166() Element of the carrier of (TOP-REAL 2)
N-min (L~ (Rotate (A,(N-min (L~ A))))) is Relation-like NAT -defined Function-like V38() V45(2) FinSequence-like FinSubsequence-like V166() Element of the carrier of (TOP-REAL 2)
N-bound (L~ (Rotate (A,(N-min (L~ A))))) is V28() real ext-real Element of REAL
|[(E-bound (L~ (SpStSeq (L~ (Rotate (A,(N-min (L~ A)))))))),((g `2) - (b / 2))]| `1 is V28() real ext-real Element of REAL
K526(|[(E-bound (L~ (SpStSeq (L~ (Rotate (A,(N-min (L~ A)))))))),((g `2) - (b / 2))]|,1) is V28() real ext-real Element of REAL
E-bound (L~ (Rotate (A,(N-min (L~ A))))) is V28() real ext-real Element of REAL
S-bound (L~ (Rotate (A,(N-min (L~ A))))) is V28() real ext-real Element of REAL
{ b1 where b1 is Relation-like NAT -defined Function-like V38() V45(2) FinSequence-like FinSubsequence-like V166() Element of the carrier of (TOP-REAL 2) : ( b1 `1 = E-bound (L~ (Rotate (A,(N-min (L~ A))))) & b1 `2 <= N-bound (L~ (Rotate (A,(N-min (L~ A))))) & S-bound (L~ (Rotate (A,(N-min (L~ A))))) <= b1 `2 ) } is set
proj2 .: (L~ (SpStSeq (L~ (Rotate (A,(N-min (L~ A))))))) is V174() V175() V176() bounded_below bounded_above Element of K19(REAL)
lower_bound (proj2 .: (L~ (SpStSeq (L~ (Rotate (A,(N-min (L~ A)))))))) is V28() real ext-real Element of REAL
(g `2) - 0 is V28() real ext-real Element of REAL
S-bound (L~ (SpStSeq (L~ (Rotate (A,(N-min (L~ A))))))) is V28() real ext-real Element of REAL
g is Relation-like NAT -defined Function-like V38() V45(2) FinSequence-like FinSubsequence-like V166() Element of the carrier of (TOP-REAL 2)
A is Relation-like NAT -defined Function-like V38() V45(2) FinSequence-like FinSubsequence-like V166() Element of the carrier of (TOP-REAL 2)
LSeg (g,A) is boundary connected Element of K19( the carrier of (TOP-REAL 2))
A is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like non constant non empty V12() V38() FinSequence-like FinSubsequence-like circular special unfolded s.c.c. standard clockwise_oriented FinSequence of the carrier of (TOP-REAL 2)
RightComp A is non empty open connected V222( TOP-REAL 2) Element of K19( the carrier of (TOP-REAL 2))
LeftComp A is non empty open connected V222( TOP-REAL 2) Element of K19( the carrier of (TOP-REAL 2))
L~ A is non empty boundary compact bounded non horizontal non vertical Jordan Element of K19( the carrier of (TOP-REAL 2))
(L~ A) ` is non empty Element of K19( the carrier of (TOP-REAL 2))
the carrier of (TOP-REAL 2) \ (L~ A) is set
(TOP-REAL 2) | ((L~ A) `) is non empty strict TopSpace-like SubSpace of TOP-REAL 2
the carrier of ((TOP-REAL 2) | ((L~ A) `)) is non empty set
K19( the carrier of ((TOP-REAL 2) | ((L~ A) `))) is non empty set
x is Element of K19( the carrier of ((TOP-REAL 2) | ((L~ A) `)))
x is Element of K19( the carrier of ((TOP-REAL 2) | ((L~ A) `)))
b is Element of K19( the carrier of ((TOP-REAL 2) | ((L~ A) `)))
g is non empty compact bounded non horizontal non vertical Element of K19( the carrier of (TOP-REAL 2))
SpStSeq g is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like non constant non empty V12() V38() FinSequence-like FinSubsequence-like circular special unfolded s.c.c. standard rectangular clockwise_oriented FinSequence of the carrier of (TOP-REAL 2)
RightComp (SpStSeq g) is non empty open connected V222( TOP-REAL 2) Element of K19( the carrier of (TOP-REAL 2))
Cl (RightComp (SpStSeq g)) is closed Element of K19( the carrier of (TOP-REAL 2))
L~ (SpStSeq g) is non empty boundary compact bounded non horizontal non vertical Jordan Element of K19( the carrier of (TOP-REAL 2))
W-bound (L~ (SpStSeq g)) is V28() real ext-real Element of REAL
E-bound (L~ (SpStSeq g)) is V28() real ext-real Element of REAL
[.(W-bound (L~ (SpStSeq g))),(E-bound (L~ (SpStSeq g))).] is compact V174() V175() V176() real-bounded Element of K19(REAL)
S-bound (L~ (SpStSeq g)) is V28() real ext-real Element of REAL
N-bound (L~ (SpStSeq g)) is V28() real ext-real Element of REAL
[.(S-bound (L~ (SpStSeq g))),(N-bound (L~ (SpStSeq g))).] is compact V174() V175() V176() real-bounded Element of K19(REAL)
(1,2) --> ([.(W-bound (L~ (SpStSeq g))),(E-bound (L~ (SpStSeq g))).],[.(S-bound (L~ (SpStSeq g))),(N-bound (L~ (SpStSeq g))).]) is Relation-like {1,2} -defined K19(REAL) -valued Function-like V18({1,2},K19(REAL)) Element of K19(K20({1,2},K19(REAL)))
K20({1,2},K19(REAL)) is non empty set
K19(K20({1,2},K19(REAL))) is non empty set
product ((1,2) --> ([.(W-bound (L~ (SpStSeq g))),(E-bound (L~ (SpStSeq g))).],[.(S-bound (L~ (SpStSeq g))),(N-bound (L~ (SpStSeq g))).])) is set
dom ((1,2) --> ([.(W-bound (L~ (SpStSeq g))),(E-bound (L~ (SpStSeq g))).],[.(S-bound (L~ (SpStSeq g))),(N-bound (L~ (SpStSeq g))).])) is V174() V175() V176() V177() V178() V179() Element of K19({1,2})
K19({1,2}) is non empty set
(RightComp (SpStSeq g)) \/ (L~ (SpStSeq g)) is non empty Element of K19( the carrier of (TOP-REAL 2))
A is set
x is Relation-like NAT -defined Function-like V38() FinSequence-like FinSubsequence-like set
b is set
x . b is set
((1,2) --> ([.(W-bound (L~ (SpStSeq g))),(E-bound (L~ (SpStSeq g))).],[.(S-bound (L~ (SpStSeq g))),(N-bound (L~ (SpStSeq g))).])) . b is set
x is Relation-like NAT -defined Function-like V38() V45(2) FinSequence-like FinSubsequence-like V166() Element of the carrier of (TOP-REAL 2)
x `1 is V28() real ext-real Element of REAL
K526(x,1) is V28() real ext-real Element of REAL
x is Relation-like NAT -defined Function-like V38() V45(2) FinSequence-like FinSubsequence-like V166() Element of the carrier of (TOP-REAL 2)
x `1 is V28() real ext-real Element of REAL
K526(x,1) is V28() real ext-real Element of REAL
x is Relation-like NAT -defined Function-like V38() V45(2) FinSequence-like FinSubsequence-like V166() Element of the carrier of (TOP-REAL 2)
x `2 is V28() real ext-real Element of REAL
K526(x,2) is V28() real ext-real Element of REAL
x is Relation-like NAT -defined Function-like V38() V45(2) FinSequence-like FinSubsequence-like V166() Element of the carrier of (TOP-REAL 2)
x `2 is V28() real ext-real Element of REAL
K526(x,2) is V28() real ext-real Element of REAL
dom x is V174() V175() V176() V177() V178() V179() Element of K19(NAT)
b is V28() real ext-real Element of REAL
c is V28() real ext-real Element of REAL
<*b,c*> is Relation-like NAT -defined Function-like non empty V38() V45(2) FinSequence-like FinSubsequence-like set
A is set
x is Relation-like Function-like set
dom x is set
{ b1 where b1 is V28() real ext-real Element of REAL : ( S-bound (L~ (SpStSeq g)) <= b1 & b1 <= N-bound (L~ (SpStSeq g)) ) } is set
x . 2 is set
((1,2) --> ([.(W-bound (L~ (SpStSeq g))),(E-bound (L~ (SpStSeq g))).],[.(S-bound (L~ (SpStSeq g))),(N-bound (L~ (SpStSeq g))).])) . 2 is set
x is V28() real ext-real Element of REAL
{ b1 where b1 is V28() real ext-real Element of REAL : ( W-bound (L~ (SpStSeq g)) <= b1 & b1 <= E-bound (L~ (SpStSeq g)) ) } is set
x . 1 is set
((1,2) --> ([.(W-bound (L~ (SpStSeq g))),(E-bound (L~ (SpStSeq g))).],[.(S-bound (L~ (SpStSeq g))),(N-bound (L~ (SpStSeq g))).])) . 1 is set
b is V28() real ext-real Element of REAL
LeftComp (SpStSeq g) is non empty open connected V222( TOP-REAL 2) Element of K19( the carrier of (TOP-REAL 2))
{ b1 where b1 is Relation-like NAT -defined Function-like V38() V45(2) FinSequence-like FinSubsequence-like V166() Element of the carrier of (TOP-REAL 2) : ( not W-bound (L~ (SpStSeq g)) <= b1 `1 or not b1 `1 <= E-bound (L~ (SpStSeq g)) or not S-bound (L~ (SpStSeq g)) <= b1 `2 or not b1 `2 <= N-bound (L~ (SpStSeq g)) ) } is set
<*b,x*> is Relation-like NAT -defined Function-like non empty V38() V45(2) FinSequence-like FinSubsequence-like set
c is set
x . c is set
<*b,x*> . c is set
dom <*b,x*> is V174() V175() V176() V177() V178() V179() Element of K19(NAT)
|[b,x]| is Relation-like NAT -defined Function-like non empty V38() V45(2) FinSequence-like FinSubsequence-like V166() Element of the carrier of (TOP-REAL 2)
c is Relation-like NAT -defined Function-like V38() V45(2) FinSequence-like FinSubsequence-like V166() Element of the carrier of (TOP-REAL 2)
c `1 is V28() real ext-real Element of REAL
K526(c,1) is V28() real ext-real Element of REAL
c `2 is V28() real ext-real Element of REAL
K526(c,2) is V28() real ext-real Element of REAL
g is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like non constant non empty V12() V38() FinSequence-like FinSubsequence-like circular special unfolded s.c.c. standard clockwise_oriented FinSequence of the carrier of (TOP-REAL 2)
RightComp g is non empty open connected V222( TOP-REAL 2) Element of K19( the carrier of (TOP-REAL 2))
Cl (RightComp g) is closed Element of K19( the carrier of (TOP-REAL 2))
proj1 .: (Cl (RightComp g)) is V174() V175() V176() Element of K19(REAL)
L~ g is non empty boundary compact bounded non horizontal non vertical Jordan Element of K19( the carrier of (TOP-REAL 2))
proj1 .: (L~ g) is V174() V175() V176() bounded_below bounded_above Element of K19(REAL)
N-min (L~ g) is Relation-like NAT -defined Function-like V38() V45(2) FinSequence-like FinSubsequence-like V166() Element of the carrier of (TOP-REAL 2)
Rotate (g,(N-min (L~ g))) is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like non constant non empty V12() V38() FinSequence-like FinSubsequence-like circular special unfolded s.c.c. standard clockwise_oriented FinSequence of the carrier of (TOP-REAL 2)
L~ (Rotate (g,(N-min (L~ g)))) is non empty boundary compact bounded non horizontal non vertical Jordan Element of K19( the carrier of (TOP-REAL 2))
rng g is non empty V12() Element of K19( the carrier of (TOP-REAL 2))
(Rotate (g,(N-min (L~ g)))) /. 1 is Relation-like NAT -defined Function-like V38() V45(2) FinSequence-like FinSubsequence-like V166() Element of the carrier of (TOP-REAL 2)
N-min (L~ (Rotate (g,(N-min (L~ g))))) is Relation-like NAT -defined Function-like V38() V45(2) FinSequence-like FinSubsequence-like V166() Element of the carrier of (TOP-REAL 2)
(RightComp g) \/ (L~ g) is non empty Element of K19( the carrier of (TOP-REAL 2))
A is set
x is set
proj1 . x is set
x is Relation-like NAT -defined Function-like V38() V45(2) FinSequence-like FinSubsequence-like V166() Element of the carrier of (TOP-REAL 2)
x `1 is V28() real ext-real Element of REAL
K526(x,1) is V28() real ext-real Element of REAL
N-bound (L~ g) is V28() real ext-real Element of REAL
(N-bound (L~ g)) + 1 is V28() real ext-real Element of REAL
|[(x `1),((N-bound (L~ g)) + 1)]| is Relation-like NAT -defined Function-like non empty V38() V45(2) FinSequence-like FinSubsequence-like V166() Element of the carrier of (TOP-REAL 2)
|[(x `1),((N-bound (L~ g)) + 1)]| `2 is V28() real ext-real Element of REAL
K526(|[(x `1),((N-bound (L~ g)) + 1)]|,2) is V28() real ext-real Element of REAL
(N-bound (L~ g)) + 0 is V28() real ext-real Element of REAL
LeftComp (Rotate (g,(N-min (L~ g)))) is non empty open connected V222( TOP-REAL 2) Element of K19( the carrier of (TOP-REAL 2))
LeftComp g is non empty open connected V222( TOP-REAL 2) Element of K19( the carrier of (TOP-REAL 2))
LSeg (x,|[(x `1),((N-bound (L~ g)) + 1)]|) is boundary connected Element of K19( the carrier of (TOP-REAL 2))
c is set
|[(x `1),((N-bound (L~ g)) + 1)]| `1 is V28() real ext-real Element of REAL
K526(|[(x `1),((N-bound (L~ g)) + 1)]|,1) is V28() real ext-real Element of REAL
c is Relation-like NAT -defined Function-like V38() V45(2) FinSequence-like FinSubsequence-like V166() Element of the carrier of (TOP-REAL 2)
proj1 . c is set
c `1 is V28() real ext-real Element of REAL
K526(c,1) is V28() real ext-real Element of REAL
(Cl (RightComp g)) \ (RightComp g) is Element of K19( the carrier of (TOP-REAL 2))
g is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like non constant non empty V12() V38() FinSequence-like FinSubsequence-like circular special unfolded s.c.c. standard clockwise_oriented FinSequence of the carrier of (TOP-REAL 2)
RightComp g is non empty open connected V222( TOP-REAL 2) Element of K19( the carrier of (TOP-REAL 2))
Cl (RightComp g) is closed Element of K19( the carrier of (TOP-REAL 2))
proj2 .: (Cl (RightComp g)) is V174() V175() V176() Element of K19(REAL)
L~ g is non empty boundary compact bounded non horizontal non vertical Jordan Element of K19( the carrier of (TOP-REAL 2))
proj2 .: (L~ g) is V174() V175() V176() bounded_below bounded_above Element of K19(REAL)
N-min (L~ g) is Relation-like NAT -defined Function-like V38() V45(2) FinSequence-like FinSubsequence-like V166() Element of the carrier of (TOP-REAL 2)
Rotate (g,(N-min (L~ g))) is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like non constant non empty V12() V38() FinSequence-like FinSubsequence-like circular special unfolded s.c.c. standard clockwise_oriented FinSequence of the carrier of (TOP-REAL 2)
L~ (Rotate (g,(N-min (L~ g)))) is non empty boundary compact bounded non horizontal non vertical Jordan Element of K19( the carrier of (TOP-REAL 2))
rng g is non empty V12() Element of K19( the carrier of (TOP-REAL 2))
(Rotate (g,(N-min (L~ g)))) /. 1 is Relation-like NAT -defined Function-like V38() V45(2) FinSequence-like FinSubsequence-like V166() Element of the carrier of (TOP-REAL 2)
N-min (L~ (Rotate (g,(N-min (L~ g))))) is Relation-like NAT -defined Function-like V38() V45(2) FinSequence-like FinSubsequence-like V166() Element of the carrier of (TOP-REAL 2)
(RightComp g) \/ (L~ g) is non empty Element of K19( the carrier of (TOP-REAL 2))
A is set
x is set
proj2 . x is set
E-bound (L~ g) is V28() real ext-real Element of REAL
(E-bound (L~ g)) + 1 is V28() real ext-real Element of REAL
x is Relation-like NAT -defined Function-like V38() V45(2) FinSequence-like FinSubsequence-like V166() Element of the carrier of (TOP-REAL 2)
x `2 is V28() real ext-real Element of REAL
K526(x,2) is V28() real ext-real Element of REAL
|[((E-bound (L~ g)) + 1),(x `2)]| is Relation-like NAT -defined Function-like non empty V38() V45(2) FinSequence-like FinSubsequence-like V166() Element of the carrier of (TOP-REAL 2)
|[((E-bound (L~ g)) + 1),(x `2)]| `1 is V28() real ext-real Element of REAL
K526(|[((E-bound (L~ g)) + 1),(x `2)]|,1) is V28() real ext-real Element of REAL
(E-bound (L~ g)) + 0 is V28() real ext-real Element of REAL
LeftComp (Rotate (g,(N-min (L~ g)))) is non empty open connected V222( TOP-REAL 2) Element of K19( the carrier of (TOP-REAL 2))
LeftComp g is non empty open connected V222( TOP-REAL 2) Element of K19( the carrier of (TOP-REAL 2))
LSeg (x,|[((E-bound (L~ g)) + 1),(x `2)]|) is boundary connected Element of K19( the carrier of (TOP-REAL 2))
c is set
|[((E-bound (L~ g)) + 1),(x `2)]| `2 is V28() real ext-real Element of REAL
K526(|[((E-bound (L~ g)) + 1),(x `2)]|,2) is V28() real ext-real Element of REAL
c is Relation-like NAT -defined Function-like V38() V45(2) FinSequence-like FinSubsequence-like V166() Element of the carrier of (TOP-REAL 2)
proj2 . c is set
c `2 is V28() real ext-real Element of REAL
K526(c,2) is V28() real ext-real Element of REAL
(Cl (RightComp g)) \ (RightComp g) is Element of K19( the carrier of (TOP-REAL 2))
g is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like non constant non empty V12() V38() FinSequence-like FinSubsequence-like circular special unfolded s.c.c. standard clockwise_oriented FinSequence of the carrier of (TOP-REAL 2)
RightComp g is non empty open connected V222( TOP-REAL 2) Element of K19( the carrier of (TOP-REAL 2))
L~ g is non empty boundary compact bounded non horizontal non vertical Jordan Element of K19( the carrier of (TOP-REAL 2))
SpStSeq (L~ g) is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like non constant non empty V12() V38() FinSequence-like FinSubsequence-like circular special unfolded s.c.c. standard rectangular clockwise_oriented FinSequence of the carrier of (TOP-REAL 2)
RightComp (SpStSeq (L~ g)) is non empty open connected V222( TOP-REAL 2) Element of K19( the carrier of (TOP-REAL 2))
A is set
A is Relation-like NAT -defined Function-like V38() V45(2) FinSequence-like FinSubsequence-like V166() Element of the carrier of (TOP-REAL 2)
A `1 is V28() real ext-real Element of REAL
K526(A,1) is V28() real ext-real Element of REAL
W-bound (L~ g) is V28() real ext-real Element of REAL
L~ (SpStSeq (L~ g)) is non empty boundary compact bounded non horizontal non vertical Jordan Element of K19( the carrier of (TOP-REAL 2))
W-bound (L~ (SpStSeq (L~ g))) is V28() real ext-real Element of REAL
A `2 is V28() real ext-real Element of REAL
K526(A,2) is V28() real ext-real Element of REAL
S-bound (L~ g) is V28() real ext-real Element of REAL
S-bound (L~ (SpStSeq (L~ g))) is V28() real ext-real Element of REAL
E-bound (L~ g) is V28() real ext-real Element of REAL
E-bound (L~ (SpStSeq (L~ g))) is V28() real ext-real Element of REAL
N-bound (L~ g) is V28() real ext-real Element of REAL
N-bound (L~ (SpStSeq (L~ g))) is V28() real ext-real Element of REAL
{ b1 where b1 is Relation-like NAT -defined Function-like V38() V45(2) FinSequence-like FinSubsequence-like V166() Element of the carrier of (TOP-REAL 2) : ( not b1 `1 <= W-bound (L~ (SpStSeq (L~ g))) & not E-bound (L~ (SpStSeq (L~ g))) <= b1 `1 & not b1 `2 <= S-bound (L~ (SpStSeq (L~ g))) & not N-bound (L~ (SpStSeq (L~ g))) <= b1 `2 ) } is set
g is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like non constant non empty V12() V38() FinSequence-like FinSubsequence-like circular special unfolded s.c.c. standard clockwise_oriented FinSequence of the carrier of (TOP-REAL 2)
RightComp g is non empty open connected V222( TOP-REAL 2) Element of K19( the carrier of (TOP-REAL 2))
Cl (RightComp g) is closed Element of K19( the carrier of (TOP-REAL 2))
L~ g is non empty boundary compact bounded non horizontal non vertical Jordan Element of K19( the carrier of (TOP-REAL 2))
SpStSeq (L~ g) is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like non constant non empty V12() V38() FinSequence-like FinSubsequence-like circular special unfolded s.c.c. standard rectangular clockwise_oriented FinSequence of the carrier of (TOP-REAL 2)
RightComp (SpStSeq (L~ g)) is non empty open connected V222( TOP-REAL 2) Element of K19( the carrier of (TOP-REAL 2))
Cl (RightComp (SpStSeq (L~ g))) is closed Element of K19( the carrier of (TOP-REAL 2))
L~ (SpStSeq (L~ g)) is non empty boundary compact bounded non horizontal non vertical Jordan Element of K19( the carrier of (TOP-REAL 2))
W-bound (L~ (SpStSeq (L~ g))) is V28() real ext-real Element of REAL
E-bound (L~ (SpStSeq (L~ g))) is V28() real ext-real Element of REAL
[.(W-bound (L~ (SpStSeq (L~ g)))),(E-bound (L~ (SpStSeq (L~ g)))).] is compact V174() V175() V176() real-bounded Element of K19(REAL)
S-bound (L~ (SpStSeq (L~ g))) is V28() real ext-real Element of REAL
N-bound (L~ (SpStSeq (L~ g))) is V28() real ext-real Element of REAL
[.(S-bound (L~ (SpStSeq (L~ g)))),(N-bound (L~ (SpStSeq (L~ g)))).] is compact V174() V175() V176() real-bounded Element of K19(REAL)
(1,2) --> ([.(W-bound (L~ (SpStSeq (L~ g)))),(E-bound (L~ (SpStSeq (L~ g)))).],[.(S-bound (L~ (SpStSeq (L~ g)))),(N-bound (L~ (SpStSeq (L~ g)))).]) is Relation-like {1,2} -defined K19(REAL) -valued Function-like V18({1,2},K19(REAL)) Element of K19(K20({1,2},K19(REAL)))
K20({1,2},K19(REAL)) is non empty set
K19(K20({1,2},K19(REAL))) is non empty set
product ((1,2) --> ([.(W-bound (L~ (SpStSeq (L~ g)))),(E-bound (L~ (SpStSeq (L~ g)))).],[.(S-bound (L~ (SpStSeq (L~ g)))),(N-bound (L~ (SpStSeq (L~ g)))).])) is set
g is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like non constant non empty V12() V38() FinSequence-like FinSubsequence-like circular special unfolded s.c.c. standard clockwise_oriented FinSequence of the carrier of (TOP-REAL 2)
LeftComp g is non empty open connected V222( TOP-REAL 2) Element of K19( the carrier of (TOP-REAL 2))
RightComp g is non empty open connected V222( TOP-REAL 2) Element of K19( the carrier of (TOP-REAL 2))
Cl (RightComp g) is closed Element of K19( the carrier of (TOP-REAL 2))
L~ g is non empty boundary compact bounded non horizontal non vertical Jordan Element of K19( the carrier of (TOP-REAL 2))
(L~ g) \/ (RightComp g) is non empty Element of K19( the carrier of (TOP-REAL 2))
((L~ g) \/ (RightComp g)) \/ (LeftComp g) is non empty Element of K19( the carrier of (TOP-REAL 2))
g is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like non constant non empty V12() V38() FinSequence-like FinSubsequence-like circular special unfolded s.c.c. standard clockwise_oriented FinSequence of the carrier of (TOP-REAL 2)
L~ g is non empty boundary compact bounded non horizontal non vertical Jordan Element of K19( the carrier of (TOP-REAL 2))
LeftComp g is non empty open connected V222( TOP-REAL 2) Element of K19( the carrier of (TOP-REAL 2))
(L~ g) ` is non empty Element of K19( the carrier of (TOP-REAL 2))
the carrier of (TOP-REAL 2) \ (L~ g) is set
g is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like non constant non empty V12() V38() FinSequence-like FinSubsequence-like circular special unfolded s.c.c. standard clockwise_oriented FinSequence of the carrier of (TOP-REAL 2)
L~ g is non empty boundary compact bounded non horizontal non vertical Jordan Element of K19( the carrier of (TOP-REAL 2))
RightComp g is non empty open connected V222( TOP-REAL 2) Element of K19( the carrier of (TOP-REAL 2))
(L~ g) ` is non empty Element of K19( the carrier of (TOP-REAL 2))
the carrier of (TOP-REAL 2) \ (L~ g) is set
Cl (RightComp g) is closed Element of K19( the carrier of (TOP-REAL 2))
g is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like non constant non empty V12() V38() FinSequence-like FinSubsequence-like circular special unfolded s.c.c. standard clockwise_oriented FinSequence of the carrier of (TOP-REAL 2)
L~ g is non empty boundary compact bounded non horizontal non vertical Jordan Element of K19( the carrier of (TOP-REAL 2))
UBD (L~ g) is non empty connected Element of K19( the carrier of (TOP-REAL 2))
{ b1 where b1 is Element of K19( the carrier of (TOP-REAL 2)) : b1 is_outside_component_of L~ g } is set
union { b1 where b1 is Element of K19( the carrier of (TOP-REAL 2)) : b1 is_outside_component_of L~ g } is set
LeftComp g is non empty open connected V222( TOP-REAL 2) Element of K19( the carrier of (TOP-REAL 2))
g is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like non constant non empty V12() V38() FinSequence-like FinSubsequence-like circular special unfolded s.c.c. standard clockwise_oriented FinSequence of the carrier of (TOP-REAL 2)
L~ g is non empty boundary compact bounded non horizontal non vertical Jordan Element of K19( the carrier of (TOP-REAL 2))
BDD (L~ g) is Element of K19( the carrier of (TOP-REAL 2))
{ b1 where b1 is Element of K19( the carrier of (TOP-REAL 2)) : b1 is_inside_component_of L~ g } is set
union { b1 where b1 is Element of K19( the carrier of (TOP-REAL 2)) : b1 is_inside_component_of L~ g } is set
RightComp g is non empty open connected V222( TOP-REAL 2) Element of K19( the carrier of (TOP-REAL 2))
UBD (L~ g) is non empty connected Element of K19( the carrier of (TOP-REAL 2))
{ b1 where b1 is Element of K19( the carrier of (TOP-REAL 2)) : b1 is_outside_component_of L~ g } is set
union { b1 where b1 is Element of K19( the carrier of (TOP-REAL 2)) : b1 is_outside_component_of L~ g } is set
(L~ g) ` is non empty Element of K19( the carrier of (TOP-REAL 2))
the carrier of (TOP-REAL 2) \ (L~ g) is set
(BDD (L~ g)) \/ (UBD (L~ g)) is non empty Element of K19( the carrier of (TOP-REAL 2))
LeftComp g is non empty open connected V222( TOP-REAL 2) Element of K19( the carrier of (TOP-REAL 2))
(LeftComp g) \/ (RightComp g) is non empty open Element of K19( the carrier of (TOP-REAL 2))
g is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like non constant non empty V12() V38() FinSequence-like FinSubsequence-like circular special unfolded s.c.c. standard clockwise_oriented FinSequence of the carrier of (TOP-REAL 2)
L~ g is non empty boundary compact bounded non horizontal non vertical Jordan Element of K19( the carrier of (TOP-REAL 2))
LeftComp g is non empty open connected V222( TOP-REAL 2) Element of K19( the carrier of (TOP-REAL 2))
A is Element of K19( the carrier of (TOP-REAL 2))
UBD (L~ g) is non empty connected Element of K19( the carrier of (TOP-REAL 2))
{ b1 where b1 is Element of K19( the carrier of (TOP-REAL 2)) : b1 is_outside_component_of L~ g } is set
union { b1 where b1 is Element of K19( the carrier of (TOP-REAL 2)) : b1 is_outside_component_of L~ g } is set
g is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like non constant non empty V12() V38() FinSequence-like FinSubsequence-like circular special unfolded s.c.c. standard clockwise_oriented FinSequence of the carrier of (TOP-REAL 2)
L~ g is non empty boundary compact bounded non horizontal non vertical Jordan Element of K19( the carrier of (TOP-REAL 2))
RightComp g is non empty open connected V222( TOP-REAL 2) Element of K19( the carrier of (TOP-REAL 2))
A is Element of K19( the carrier of (TOP-REAL 2))
BDD (L~ g) is Element of K19( the carrier of (TOP-REAL 2))
{ b1 where b1 is Element of K19( the carrier of (TOP-REAL 2)) : b1 is_inside_component_of L~ g } is set
union { b1 where b1 is Element of K19( the carrier of (TOP-REAL 2)) : b1 is_inside_component_of L~ g } is set
(L~ g) ` is non empty Element of K19( the carrier of (TOP-REAL 2))
the carrier of (TOP-REAL 2) \ (L~ g) is set
g is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like non constant non empty V12() V38() FinSequence-like FinSubsequence-like circular special unfolded s.c.c. standard clockwise_oriented FinSequence of the carrier of (TOP-REAL 2)
L~ g is non empty boundary compact bounded non horizontal non vertical Jordan Element of K19( the carrier of (TOP-REAL 2))
BDD (L~ g) is Element of K19( the carrier of (TOP-REAL 2))
{ b1 where b1 is Element of K19( the carrier of (TOP-REAL 2)) : b1 is_inside_component_of L~ g } is set
union { b1 where b1 is Element of K19( the carrier of (TOP-REAL 2)) : b1 is_inside_component_of L~ g } is set
A is Element of K19( the carrier of (TOP-REAL 2))
RightComp g is non empty open connected V222( TOP-REAL 2) Element of K19( the carrier of (TOP-REAL 2))
(L~ g) ` is non empty Element of K19( the carrier of (TOP-REAL 2))
the carrier of (TOP-REAL 2) \ (L~ g) is set
g is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like non constant non empty V12() V38() FinSequence-like FinSubsequence-like circular special unfolded s.c.c. standard clockwise_oriented FinSequence of the carrier of (TOP-REAL 2)
L~ g is non empty boundary compact bounded non horizontal non vertical Jordan Element of K19( the carrier of (TOP-REAL 2))
W-bound (L~ g) is V28() real ext-real Element of REAL
RightComp g is non empty open connected V222( TOP-REAL 2) Element of K19( the carrier of (TOP-REAL 2))
W-bound (RightComp g) is V28() real ext-real Element of REAL
Cl (RightComp g) is closed Element of K19( the carrier of (TOP-REAL 2))
(Cl (RightComp g)) \ (RightComp g) is Element of K19( the carrier of (TOP-REAL 2))
W-bound (Cl (RightComp g)) is V28() real ext-real Element of REAL
proj1 .: (Cl (RightComp g)) is V174() V175() V176() Element of K19(REAL)
lower_bound (proj1 .: (Cl (RightComp g))) is V28() real ext-real Element of REAL
proj1 .: (L~ g) is V174() V175() V176() bounded_below bounded_above Element of K19(REAL)
A is non empty Element of K19( the carrier of (TOP-REAL 2))
W-bound A is V28() real ext-real Element of REAL
proj1 .: A is V174() V175() V176() Element of K19(REAL)
lower_bound (proj1 .: A) is V28() real ext-real Element of REAL
g is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like non constant non empty V12() V38() FinSequence-like FinSubsequence-like circular special unfolded s.c.c. standard clockwise_oriented FinSequence of the carrier of (TOP-REAL 2)
L~ g is non empty boundary compact bounded non horizontal non vertical Jordan Element of K19( the carrier of (TOP-REAL 2))
E-bound (L~ g) is V28() real ext-real Element of REAL
RightComp g is non empty open connected V222( TOP-REAL 2) Element of K19( the carrier of (TOP-REAL 2))
E-bound (RightComp g) is V28() real ext-real Element of REAL
Cl (RightComp g) is closed Element of K19( the carrier of (TOP-REAL 2))
(Cl (RightComp g)) \ (RightComp g) is Element of K19( the carrier of (TOP-REAL 2))
E-bound (Cl (RightComp g)) is V28() real ext-real Element of REAL
proj1 .: (Cl (RightComp g)) is V174() V175() V176() Element of K19(REAL)
upper_bound (proj1 .: (Cl (RightComp g))) is V28() real ext-real Element of REAL
proj1 .: (L~ g) is V174() V175() V176() bounded_below bounded_above Element of K19(REAL)
A is non empty Element of K19( the carrier of (TOP-REAL 2))
E-bound A is V28() real ext-real Element of REAL
proj1 .: A is V174() V175() V176() Element of K19(REAL)
upper_bound (proj1 .: A) is V28() real ext-real Element of REAL
g is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like non constant non empty V12() V38() FinSequence-like FinSubsequence-like circular special unfolded s.c.c. standard clockwise_oriented FinSequence of the carrier of (TOP-REAL 2)
L~ g is non empty boundary compact bounded non horizontal non vertical Jordan Element of K19( the carrier of (TOP-REAL 2))
N-bound (L~ g) is V28() real ext-real Element of REAL
RightComp g is non empty open connected V222( TOP-REAL 2) Element of K19( the carrier of (TOP-REAL 2))
N-bound (RightComp g) is V28() real ext-real Element of REAL
Cl (RightComp g) is closed Element of K19( the carrier of (TOP-REAL 2))
(Cl (RightComp g)) \ (RightComp g) is Element of K19( the carrier of (TOP-REAL 2))
N-bound (Cl (RightComp g)) is V28() real ext-real Element of REAL
proj2 .: (Cl (RightComp g)) is V174() V175() V176() Element of K19(REAL)
upper_bound (proj2 .: (Cl (RightComp g))) is V28() real ext-real Element of REAL
proj2 .: (L~ g) is V174() V175() V176() bounded_below bounded_above Element of K19(REAL)
A is non empty Element of K19( the carrier of (TOP-REAL 2))
N-bound A is V28() real ext-real Element of REAL
proj2 .: A is V174() V175() V176() Element of K19(REAL)
upper_bound (proj2 .: A) is V28() real ext-real Element of REAL
g is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like non constant non empty V12() V38() FinSequence-like FinSubsequence-like circular special unfolded s.c.c. standard clockwise_oriented FinSequence of the carrier of (TOP-REAL 2)
L~ g is non empty boundary compact bounded non horizontal non vertical Jordan Element of K19( the carrier of (TOP-REAL 2))
S-bound (L~ g) is V28() real ext-real Element of REAL
RightComp g is non empty open connected V222( TOP-REAL 2) Element of K19( the carrier of (TOP-REAL 2))
S-bound (RightComp g) is V28() real ext-real Element of REAL
Cl (RightComp g) is closed Element of K19( the carrier of (TOP-REAL 2))
(Cl (RightComp g)) \ (RightComp g) is Element of K19( the carrier of (TOP-REAL 2))
S-bound (Cl (RightComp g)) is V28() real ext-real Element of REAL
proj2 .: (Cl (RightComp g)) is V174() V175() V176() Element of K19(REAL)
lower_bound (proj2 .: (Cl (RightComp g))) is V28() real ext-real Element of REAL
proj2 .: (L~ g) is V174() V175() V176() bounded_below bounded_above Element of K19(REAL)
A is non empty Element of K19( the carrier of (TOP-REAL 2))
S-bound A is V28() real ext-real Element of REAL
proj2 .: A is V174() V175() V176() Element of K19(REAL)
lower_bound (proj2 .: A) is V28() real ext-real Element of REAL