REAL is non empty V34() V155() V156() V157() V161() set
NAT is V155() V156() V157() V158() V159() V160() V161() Element of K6(REAL)
K6(REAL) is set
COMPLEX is non empty V34() V155() V161() set
omega is V155() V156() V157() V158() V159() V160() V161() set
K6(omega) is set
K6(NAT) is set
1 is non empty ordinal natural V11() real ext-real positive non negative integer V108() V155() V156() V157() V158() V159() V160() Element of NAT
INT is non empty V34() V155() V156() V157() V158() V159() V161() set
K7(1,1) is V23( RAT ) V23( INT ) V145() V146() V147() V148() set
RAT is non empty V34() V155() V156() V157() V158() V161() set
K6(K7(1,1)) is set
K7(K7(1,1),1) is V23( RAT ) V23( INT ) V145() V146() V147() V148() set
K6(K7(K7(1,1),1)) is set
K7(K7(1,1),REAL) is V145() V146() V147() set
K6(K7(K7(1,1),REAL)) is set
K7(REAL,REAL) is V145() V146() V147() set
K7(K7(REAL,REAL),REAL) is V145() V146() V147() set
K6(K7(K7(REAL,REAL),REAL)) is set
2 is non empty ordinal natural V11() real ext-real positive non negative integer V108() V155() V156() V157() V158() V159() V160() Element of NAT
K7(2,2) is V23( RAT ) V23( INT ) V145() V146() V147() V148() set
K7(K7(2,2),REAL) is V145() V146() V147() set
K6(K7(K7(2,2),REAL)) is set
K6(K7(REAL,REAL)) is set
TOP-REAL 2 is non empty TopSpace-like T_0 T_1 T_2 V121() V167() V168() V169() V170() V171() V172() V173() strict V180() V181() L15()
the carrier of (TOP-REAL 2) is non empty V27() set
K333( the carrier of (TOP-REAL 2)) is M12( the carrier of (TOP-REAL 2))
K6( the carrier of (TOP-REAL 2)) is set
K7( the carrier of (TOP-REAL 2),REAL) is V145() V146() V147() set
K6(K7( the carrier of (TOP-REAL 2),REAL)) is set
K7(COMPLEX,COMPLEX) is V145() set
K6(K7(COMPLEX,COMPLEX)) is set
K7(COMPLEX,REAL) is V145() V146() V147() set
K6(K7(COMPLEX,REAL)) is set
{} is empty V155() V156() V157() V158() V159() V160() V161() set
the empty V155() V156() V157() V158() V159() V160() V161() set is empty V155() V156() V157() V158() V159() V160() V161() set
3 is non empty ordinal natural V11() real ext-real positive non negative integer V108() V155() V156() V157() V158() V159() V160() Element of NAT
4 is non empty ordinal natural V11() real ext-real positive non negative integer V108() V155() V156() V157() V158() V159() V160() Element of NAT
proj1 is V19() V22( the carrier of (TOP-REAL 2)) V23( REAL ) V24() V46( the carrier of (TOP-REAL 2), REAL ) V145() V146() V147() V203( TOP-REAL 2) Element of K6(K7( the carrier of (TOP-REAL 2),REAL))
proj2 is V19() V22( the carrier of (TOP-REAL 2)) V23( REAL ) V24() V46( the carrier of (TOP-REAL 2), REAL ) V145() V146() V147() V203( TOP-REAL 2) Element of K6(K7( the carrier of (TOP-REAL 2),REAL))
Euclid 2 is non empty strict Reflexive discerning V97() triangle MetrStruct
the carrier of (Euclid 2) is non empty set
0 is empty ordinal natural V11() real ext-real non positive non negative integer V108() V155() V156() V157() V158() V159() V160() V161() Element of NAT
C is V11() real ext-real set
p is ordinal natural V11() real ext-real non negative integer V108() V155() V156() V157() V158() V159() V160() Element of NAT
C + p is V11() real ext-real set
[\(C + p)/] is V11() real ext-real integer set
[\(C + p)/] - p is V11() real ext-real integer set
[\C/] is V11() real ext-real integer set
[\C/] + p is V11() real ext-real integer set
([\C/] + p) - p is V11() real ext-real integer set
C is V11() real ext-real set
p is V11() real ext-real set
C / p is V11() real ext-real Element of COMPLEX
P is V11() real ext-real set
P / C is V11() real ext-real Element of COMPLEX
(P / C) * p is V11() real ext-real set
(C / p) * ((P / C) * p) is V11() real ext-real set
(C / p) * p is V11() real ext-real set
((C / p) * p) * (P / C) is V11() real ext-real set
C * (P / C) is V11() real ext-real set
C is V41(2) FinSequence-like V147() Element of the carrier of (TOP-REAL 2)
TopSpaceMetr (Euclid 2) is TopStruct
the topology of (TOP-REAL 2) is non empty Element of K6(K6( the carrier of (TOP-REAL 2)))
K6(K6( the carrier of (TOP-REAL 2))) is set
TopStruct(# the carrier of (TOP-REAL 2), the topology of (TOP-REAL 2) #) is non empty strict TopSpace-like TopStruct
Family_open_set (Euclid 2) is Element of K6(K6( the carrier of (Euclid 2)))
K6( the carrier of (Euclid 2)) is set
K6(K6( the carrier of (Euclid 2))) is set
TopStruct(# the carrier of (Euclid 2),(Family_open_set (Euclid 2)) #) is non empty strict TopStruct
C is V11() real ext-real set
C / 4 is V11() real ext-real Element of REAL
2 * (C / 4) is V11() real ext-real Element of REAL
C / 2 is V11() real ext-real Element of REAL
C is non empty closed V83( TOP-REAL 2) compact bounded being_simple_closed_curve non horizontal non vertical Element of K6( the carrier of (TOP-REAL 2))
p is ordinal natural V11() real ext-real non negative integer V108() V155() V156() V157() V158() V159() V160() Element of NAT
p + 1 is non empty ordinal natural V11() real ext-real positive non negative integer Element of REAL
P is ordinal natural V11() real ext-real non negative integer V108() V155() V156() V157() V158() V159() V160() Element of NAT
[p,P] is set
{p,P} is non empty V155() V156() V157() V158() V159() V160() set
{p} is non empty V155() V156() V157() V158() V159() V160() set
{{p,P},{p}} is non empty set
[(p + 1),P] is set
{(p + 1),P} is non empty V155() V156() V157() V158() V159() V160() set
{(p + 1)} is non empty V155() V156() V157() V158() V159() V160() set
{{(p + 1),P},{(p + 1)}} is non empty set
W is ordinal natural V11() real ext-real non negative integer V108() V155() V156() V157() V158() V159() V160() Element of NAT
Gauge (C,W) is V19() V21() V22( NAT ) V23(K333( the carrier of (TOP-REAL 2))) V24() FinSequence-like tabular V188() V189() V190() V191() FinSequence of K333( the carrier of (TOP-REAL 2))
Indices (Gauge (C,W)) is set
(Gauge (C,W)) * (1,1) is V41(2) FinSequence-like V147() Element of the carrier of (TOP-REAL 2)
(Gauge (C,W)) * (2,1) is V41(2) FinSequence-like V147() Element of the carrier of (TOP-REAL 2)
dist (((Gauge (C,W)) * (1,1)),((Gauge (C,W)) * (2,1))) is V11() real ext-real Element of REAL
(Gauge (C,W)) * ((p + 1),P) is V41(2) FinSequence-like V147() Element of the carrier of (TOP-REAL 2)
((Gauge (C,W)) * ((p + 1),P)) `1 is V11() real ext-real Element of REAL
(Gauge (C,W)) * (p,P) is V41(2) FinSequence-like V147() Element of the carrier of (TOP-REAL 2)
((Gauge (C,W)) * (p,P)) `1 is V11() real ext-real Element of REAL
(((Gauge (C,W)) * ((p + 1),P)) `1) - (((Gauge (C,W)) * (p,P)) `1) is V11() real ext-real Element of REAL
width (Gauge (C,W)) is ordinal natural V11() real ext-real non negative integer V108() V155() V156() V157() V158() V159() V160() Element of NAT
len (Gauge (C,W)) is ordinal natural V11() real ext-real non negative integer V108() V155() V156() V157() V158() V159() V160() Element of NAT
[2,1] is set
{2,1} is non empty V155() V156() V157() V158() V159() V160() set
{2} is non empty V155() V156() V157() V158() V159() V160() set
{{2,1},{2}} is non empty set
dist (((Gauge (C,W)) * (p,P)),((Gauge (C,W)) * ((p + 1),P))) is V11() real ext-real Element of REAL
E-bound C is V11() real ext-real Element of REAL
W-bound C is V11() real ext-real Element of REAL
(E-bound C) - (W-bound C) is V11() real ext-real Element of REAL
2 |^ W is ordinal natural V11() real ext-real non negative integer V108() V155() V156() V157() V158() V159() V160() Element of NAT
((E-bound C) - (W-bound C)) / (2 |^ W) is V11() real ext-real Element of REAL
[1,1] is set
{1,1} is non empty V155() V156() V157() V158() V159() V160() set
{1} is non empty V155() V156() V157() V158() V159() V160() set
{{1,1},{1}} is non empty set
1 + 1 is non empty ordinal natural V11() real ext-real positive non negative integer Element of REAL
(Gauge (C,W)) * ((1 + 1),1) is V41(2) FinSequence-like V147() Element of the carrier of (TOP-REAL 2)
dist (((Gauge (C,W)) * (1,1)),((Gauge (C,W)) * ((1 + 1),1))) is V11() real ext-real Element of REAL
C is non empty closed V83( TOP-REAL 2) compact bounded being_simple_closed_curve non horizontal non vertical Element of K6( the carrier of (TOP-REAL 2))
p is ordinal natural V11() real ext-real non negative integer V108() V155() V156() V157() V158() V159() V160() Element of NAT
P is ordinal natural V11() real ext-real non negative integer V108() V155() V156() V157() V158() V159() V160() Element of NAT
[p,P] is set
{p,P} is non empty V155() V156() V157() V158() V159() V160() set
{p} is non empty V155() V156() V157() V158() V159() V160() set
{{p,P},{p}} is non empty set
P + 1 is non empty ordinal natural V11() real ext-real positive non negative integer Element of REAL
[p,(P + 1)] is set
{p,(P + 1)} is non empty V155() V156() V157() V158() V159() V160() set
{{p,(P + 1)},{p}} is non empty set
W is ordinal natural V11() real ext-real non negative integer V108() V155() V156() V157() V158() V159() V160() Element of NAT
Gauge (C,W) is V19() V21() V22( NAT ) V23(K333( the carrier of (TOP-REAL 2))) V24() FinSequence-like tabular V188() V189() V190() V191() FinSequence of K333( the carrier of (TOP-REAL 2))
Indices (Gauge (C,W)) is set
(Gauge (C,W)) * (1,1) is V41(2) FinSequence-like V147() Element of the carrier of (TOP-REAL 2)
(Gauge (C,W)) * (1,2) is V41(2) FinSequence-like V147() Element of the carrier of (TOP-REAL 2)
dist (((Gauge (C,W)) * (1,1)),((Gauge (C,W)) * (1,2))) is V11() real ext-real Element of REAL
(Gauge (C,W)) * (p,(P + 1)) is V41(2) FinSequence-like V147() Element of the carrier of (TOP-REAL 2)
((Gauge (C,W)) * (p,(P + 1))) `2 is V11() real ext-real Element of REAL
(Gauge (C,W)) * (p,P) is V41(2) FinSequence-like V147() Element of the carrier of (TOP-REAL 2)
((Gauge (C,W)) * (p,P)) `2 is V11() real ext-real Element of REAL
(((Gauge (C,W)) * (p,(P + 1))) `2) - (((Gauge (C,W)) * (p,P)) `2) is V11() real ext-real Element of REAL
len (Gauge (C,W)) is ordinal natural V11() real ext-real non negative integer V108() V155() V156() V157() V158() V159() V160() Element of NAT
2 |^ W is ordinal natural V11() real ext-real non negative integer V108() V155() V156() V157() V158() V159() V160() Element of NAT
(2 |^ W) + 3 is non empty ordinal natural V11() real ext-real positive non negative integer Element of REAL
width (Gauge (C,W)) is ordinal natural V11() real ext-real non negative integer V108() V155() V156() V157() V158() V159() V160() Element of NAT
[1,2] is set
{1,2} is non empty V155() V156() V157() V158() V159() V160() set
{1} is non empty V155() V156() V157() V158() V159() V160() set
{{1,2},{1}} is non empty set
[1,1] is set
{1,1} is non empty V155() V156() V157() V158() V159() V160() set
{{1,1},{1}} is non empty set
dist (((Gauge (C,W)) * (p,P)),((Gauge (C,W)) * (p,(P + 1)))) is V11() real ext-real Element of REAL
N-bound C is V11() real ext-real Element of REAL
S-bound C is V11() real ext-real Element of REAL
(N-bound C) - (S-bound C) is V11() real ext-real Element of REAL
((N-bound C) - (S-bound C)) / (2 |^ W) is V11() real ext-real Element of REAL
1 + 1 is non empty ordinal natural V11() real ext-real positive non negative integer Element of REAL
(Gauge (C,W)) * (1,(1 + 1)) is V41(2) FinSequence-like V147() Element of the carrier of (TOP-REAL 2)
dist (((Gauge (C,W)) * (1,1)),((Gauge (C,W)) * (1,(1 + 1)))) is V11() real ext-real Element of REAL
TopSpaceMetr (Euclid 2) is TopStruct
the topology of (TOP-REAL 2) is non empty Element of K6(K6( the carrier of (TOP-REAL 2)))
K6(K6( the carrier of (TOP-REAL 2))) is set
TopStruct(# the carrier of (TOP-REAL 2), the topology of (TOP-REAL 2) #) is non empty strict TopSpace-like TopStruct
Family_open_set (Euclid 2) is Element of K6(K6( the carrier of (Euclid 2)))
K6( the carrier of (Euclid 2)) is set
K6(K6( the carrier of (Euclid 2))) is set
TopStruct(# the carrier of (Euclid 2),(Family_open_set (Euclid 2)) #) is non empty strict TopStruct
C is non empty closed V83( TOP-REAL 2) compact bounded being_simple_closed_curve non horizontal non vertical Element of K6( the carrier of (TOP-REAL 2))
p is ordinal natural V11() real ext-real non negative integer V108() V155() V156() V157() V158() V159() V160() Element of NAT
p + 1 is non empty ordinal natural V11() real ext-real positive non negative integer Element of REAL
P is ordinal natural V11() real ext-real non negative integer V108() V155() V156() V157() V158() V159() V160() Element of NAT
Gauge (C,P) is V19() V21() V22( NAT ) V23(K333( the carrier of (TOP-REAL 2))) V24() FinSequence-like tabular V188() V189() V190() V191() FinSequence of K333( the carrier of (TOP-REAL 2))
len (Gauge (C,P)) is ordinal natural V11() real ext-real non negative integer V108() V155() V156() V157() V158() V159() V160() Element of NAT
width (Gauge (C,P)) is ordinal natural V11() real ext-real non negative integer V108() V155() V156() V157() V158() V159() V160() Element of NAT
(Gauge (C,P)) * (1,1) is V41(2) FinSequence-like V147() Element of the carrier of (TOP-REAL 2)
(Gauge (C,P)) * (1,2) is V41(2) FinSequence-like V147() Element of the carrier of (TOP-REAL 2)
dist (((Gauge (C,P)) * (1,1)),((Gauge (C,P)) * (1,2))) is V11() real ext-real Element of REAL
(Gauge (C,P)) * (2,1) is V41(2) FinSequence-like V147() Element of the carrier of (TOP-REAL 2)
dist (((Gauge (C,P)) * (1,1)),((Gauge (C,P)) * (2,1))) is V11() real ext-real Element of REAL
W is ordinal natural V11() real ext-real non negative integer V108() V155() V156() V157() V158() V159() V160() Element of NAT
W + 1 is non empty ordinal natural V11() real ext-real positive non negative integer Element of REAL
cell ((Gauge (C,P)),p,W) is Element of K6( the carrier of (TOP-REAL 2))
E is V41(2) FinSequence-like V147() Element of the carrier of (TOP-REAL 2)
S is V11() real ext-real set
S / 4 is V11() real ext-real Element of REAL
N is Element of the carrier of (Euclid 2)
Ball (N,S) is Element of K6( the carrier of (Euclid 2))
n is set
I is V41(2) FinSequence-like V147() Element of the carrier of (TOP-REAL 2)
I `1 is V11() real ext-real Element of REAL
(Gauge (C,P)) * ((p + 1),W) is V41(2) FinSequence-like V147() Element of the carrier of (TOP-REAL 2)
((Gauge (C,P)) * ((p + 1),W)) `1 is V11() real ext-real Element of REAL
(Gauge (C,P)) * (p,W) is V41(2) FinSequence-like V147() Element of the carrier of (TOP-REAL 2)
((Gauge (C,P)) * (p,W)) `2 is V11() real ext-real Element of REAL
I `2 is V11() real ext-real Element of REAL
((Gauge (C,P)) * (p,W)) `1 is V11() real ext-real Element of REAL
J is V41(2) FinSequence-like V147() Element of the carrier of (TOP-REAL 2)
J `1 is V11() real ext-real Element of REAL
[p,W] is set
{p,W} is non empty V155() V156() V157() V158() V159() V160() set
{p} is non empty V155() V156() V157() V158() V159() V160() set
{{p,W},{p}} is non empty set
Indices (Gauge (C,P)) is set
J `2 is V11() real ext-real Element of REAL
(Gauge (C,P)) * (p,(W + 1)) is V41(2) FinSequence-like V147() Element of the carrier of (TOP-REAL 2)
((Gauge (C,P)) * (p,(W + 1))) `2 is V11() real ext-real Element of REAL
[p,(W + 1)] is set
{p,(W + 1)} is non empty V155() V156() V157() V158() V159() V160() set
{{p,(W + 1)},{p}} is non empty set
(((Gauge (C,P)) * (p,(W + 1))) `2) - (((Gauge (C,P)) * (p,W)) `2) is V11() real ext-real Element of REAL
1 + p is non empty ordinal natural V11() real ext-real positive non negative integer Element of REAL
[(p + 1),W] is set
{(p + 1),W} is non empty V155() V156() V157() V158() V159() V160() set
{(p + 1)} is non empty V155() V156() V157() V158() V159() V160() set
{{(p + 1),W},{(p + 1)}} is non empty set
(((Gauge (C,P)) * ((p + 1),W)) `1) - (((Gauge (C,P)) * (p,W)) `1) is V11() real ext-real Element of REAL
((((Gauge (C,P)) * ((p + 1),W)) `1) - (((Gauge (C,P)) * (p,W)) `1)) + ((((Gauge (C,P)) * (p,(W + 1))) `2) - (((Gauge (C,P)) * (p,W)) `2)) is V11() real ext-real Element of REAL
(S / 4) + (S / 4) is V11() real ext-real Element of REAL
dist (I,J) is V11() real ext-real Element of REAL
dist (E,J) is V11() real ext-real Element of REAL
2 * (S / 4) is V11() real ext-real Element of REAL
dist (J,E) is V11() real ext-real Element of REAL
G is Element of the carrier of (Euclid 2)
dist (G,N) is V11() real ext-real Element of REAL
C is Element of K6( the carrier of (TOP-REAL 2))
proj1 .: C is V155() V156() V157() Element of K6(REAL)
p is bounded Element of K6( the carrier of (Euclid 2))
P is V11() real ext-real Element of REAL
W is Element of the carrier of (Euclid 2)
Ball (W,P) is Element of K6( the carrier of (Euclid 2))
S is V41(2) FinSequence-like V147() Element of the carrier of (TOP-REAL 2)
S `1 is V11() real ext-real Element of REAL
(S `1) - P is V11() real ext-real Element of REAL
abs ((S `1) - P) is V11() real ext-real Element of REAL
(S `1) + P is V11() real ext-real Element of REAL
abs ((S `1) + P) is V11() real ext-real Element of REAL
max ((abs ((S `1) - P)),(abs ((S `1) + P))) is V11() real ext-real set
P - (S `1) is V11() real ext-real Element of REAL
abs (P - (S `1)) is V11() real ext-real Element of REAL
E is Element of K6( the carrier of (TOP-REAL 2))
proj1 .: E is V155() V156() V157() Element of K6(REAL)
].((S `1) - P),((S `1) + P).[ is V155() V156() V157() Element of K6(REAL)
EW is V11() real ext-real set
abs EW is V11() real ext-real Element of REAL
C is non empty closed compact bounded Element of K6( the carrier of (TOP-REAL 2))
W-bound C is V11() real ext-real Element of REAL
P is non empty Element of K6( the carrier of (TOP-REAL 2))
p is non empty Element of K6( the carrier of (TOP-REAL 2))
C \/ p is non empty Element of K6( the carrier of (TOP-REAL 2))
proj1 .: p is non empty V155() V156() V157() Element of K6(REAL)
W-bound P is V11() real ext-real Element of REAL
W-bound p is V11() real ext-real Element of REAL
min ((W-bound C),(W-bound p)) is V11() real ext-real set
proj1 .: C is non empty V155() V156() V157() bounded_below bounded_above Element of K6(REAL)
proj1 .: P is non empty V155() V156() V157() Element of K6(REAL)
lower_bound (proj1 .: C) is V11() real ext-real Element of REAL
lower_bound (proj1 .: p) is V11() real ext-real Element of REAL
lower_bound (proj1 .: P) is V11() real ext-real Element of REAL
(proj1 .: C) \/ (proj1 .: p) is non empty V155() V156() V157() Element of K6(REAL)
lower_bound ((proj1 .: C) \/ (proj1 .: p)) is V11() real ext-real Element of REAL
C is V41(2) FinSequence-like V147() Element of the carrier of (TOP-REAL 2)
C `1 is V11() real ext-real Element of REAL
P is Element of K6( the carrier of (TOP-REAL 2))
(TOP-REAL 2) | P is strict TopSpace-like T_0 T_1 T_2 SubSpace of TOP-REAL 2
proj1 | P is V19() V22( the carrier of ((TOP-REAL 2) | P)) V23( REAL ) V24() V46( the carrier of ((TOP-REAL 2) | P), REAL ) V145() V146() V147() V203((TOP-REAL 2) | P) Element of K6(K7( the carrier of ((TOP-REAL 2) | P),REAL))
the carrier of ((TOP-REAL 2) | P) is set
K7( the carrier of ((TOP-REAL 2) | P),REAL) is V145() V146() V147() set
K6(K7( the carrier of ((TOP-REAL 2) | P),REAL)) is set
lower_bound (proj1 | P) is V11() real ext-real Element of REAL
upper_bound (proj1 | P) is V11() real ext-real Element of REAL
W is non empty Element of K6( the carrier of (TOP-REAL 2))
(TOP-REAL 2) | W is non empty strict TopSpace-like T_0 T_1 T_2 SubSpace of TOP-REAL 2
the carrier of ((TOP-REAL 2) | W) is non empty set
proj1 | W is V19() V22( the carrier of ((TOP-REAL 2) | W)) V23( REAL ) V24() V46( the carrier of ((TOP-REAL 2) | W), REAL ) V145() V146() V147() V203((TOP-REAL 2) | W) Element of K6(K7( the carrier of ((TOP-REAL 2) | W),REAL))
K7( the carrier of ((TOP-REAL 2) | W),REAL) is V145() V146() V147() set
K6(K7( the carrier of ((TOP-REAL 2) | W),REAL)) is set
(proj1 | W) .: W is V155() V156() V157() Element of K6(REAL)
proj1 .: W is non empty V155() V156() V157() Element of K6(REAL)
S is Element of the carrier of ((TOP-REAL 2) | W)
(proj1 | W) . S is V11() real ext-real Element of REAL
E is V19() V22( the carrier of ((TOP-REAL 2) | W)) V23( REAL ) V24() V46( the carrier of ((TOP-REAL 2) | W), REAL ) V145() V146() V147() bounded_above bounded_below bounded Element of K6(K7( the carrier of ((TOP-REAL 2) | W),REAL))
lower_bound E is V11() real ext-real Element of REAL
C is V41(2) FinSequence-like V147() Element of the carrier of (TOP-REAL 2)
C `2 is V11() real ext-real Element of REAL
P is Element of K6( the carrier of (TOP-REAL 2))
(TOP-REAL 2) | P is strict TopSpace-like T_0 T_1 T_2 SubSpace of TOP-REAL 2
proj2 | P is V19() V22( the carrier of ((TOP-REAL 2) | P)) V23( REAL ) V24() V46( the carrier of ((TOP-REAL 2) | P), REAL ) V145() V146() V147() V203((TOP-REAL 2) | P) Element of K6(K7( the carrier of ((TOP-REAL 2) | P),REAL))
the carrier of ((TOP-REAL 2) | P) is set
K7( the carrier of ((TOP-REAL 2) | P),REAL) is V145() V146() V147() set
K6(K7( the carrier of ((TOP-REAL 2) | P),REAL)) is set
lower_bound (proj2 | P) is V11() real ext-real Element of REAL
upper_bound (proj2 | P) is V11() real ext-real Element of REAL
W is non empty Element of K6( the carrier of (TOP-REAL 2))
(TOP-REAL 2) | W is non empty strict TopSpace-like T_0 T_1 T_2 SubSpace of TOP-REAL 2
the carrier of ((TOP-REAL 2) | W) is non empty set
proj2 | W is V19() V22( the carrier of ((TOP-REAL 2) | W)) V23( REAL ) V24() V46( the carrier of ((TOP-REAL 2) | W), REAL ) V145() V146() V147() V203((TOP-REAL 2) | W) Element of K6(K7( the carrier of ((TOP-REAL 2) | W),REAL))
K7( the carrier of ((TOP-REAL 2) | W),REAL) is V145() V146() V147() set
K6(K7( the carrier of ((TOP-REAL 2) | W),REAL)) is set
(proj2 | W) .: W is V155() V156() V157() Element of K6(REAL)
proj2 .: W is non empty V155() V156() V157() Element of K6(REAL)
S is Element of the carrier of ((TOP-REAL 2) | W)
(proj2 | W) . S is V11() real ext-real Element of REAL
E is V19() V22( the carrier of ((TOP-REAL 2) | W)) V23( REAL ) V24() V46( the carrier of ((TOP-REAL 2) | W), REAL ) V145() V146() V147() bounded_above bounded_below bounded Element of K6(K7( the carrier of ((TOP-REAL 2) | W),REAL))
lower_bound E is V11() real ext-real Element of REAL
C is V41(2) FinSequence-like V147() Element of the carrier of (TOP-REAL 2)
C `1 is V11() real ext-real Element of REAL
C `2 is V11() real ext-real Element of REAL
p is Element of K6( the carrier of (TOP-REAL 2))
W-bound p is V11() real ext-real Element of REAL
E-bound p is V11() real ext-real Element of REAL
S-bound p is V11() real ext-real Element of REAL
N-bound p is V11() real ext-real Element of REAL
(TOP-REAL 2) | p is strict TopSpace-like T_0 T_1 T_2 SubSpace of TOP-REAL 2
proj1 | p is V19() V22( the carrier of ((TOP-REAL 2) | p)) V23( REAL ) V24() V46( the carrier of ((TOP-REAL 2) | p), REAL ) V145() V146() V147() V203((TOP-REAL 2) | p) Element of K6(K7( the carrier of ((TOP-REAL 2) | p),REAL))
the carrier of ((TOP-REAL 2) | p) is set
K7( the carrier of ((TOP-REAL 2) | p),REAL) is V145() V146() V147() set
K6(K7( the carrier of ((TOP-REAL 2) | p),REAL)) is set
lower_bound (proj1 | p) is V11() real ext-real Element of REAL
upper_bound (proj1 | p) is V11() real ext-real Element of REAL
proj2 | p is V19() V22( the carrier of ((TOP-REAL 2) | p)) V23( REAL ) V24() V46( the carrier of ((TOP-REAL 2) | p), REAL ) V145() V146() V147() V203((TOP-REAL 2) | p) Element of K6(K7( the carrier of ((TOP-REAL 2) | p),REAL))
lower_bound (proj2 | p) is V11() real ext-real Element of REAL
upper_bound (proj2 | p) is V11() real ext-real Element of REAL
C is Element of K6( the carrier of (TOP-REAL 2))
BDD C is Element of K6( the carrier of (TOP-REAL 2))
W-bound (BDD C) is V11() real ext-real Element of REAL
proj1 | (BDD C) is V19() V22( the carrier of ((TOP-REAL 2) | (BDD C))) V23( REAL ) V24() V46( the carrier of ((TOP-REAL 2) | (BDD C)), REAL ) V145() V146() V147() V203((TOP-REAL 2) | (BDD C)) Element of K6(K7( the carrier of ((TOP-REAL 2) | (BDD C)),REAL))
(TOP-REAL 2) | (BDD C) is strict TopSpace-like T_0 T_1 T_2 SubSpace of TOP-REAL 2
the carrier of ((TOP-REAL 2) | (BDD C)) is set
K7( the carrier of ((TOP-REAL 2) | (BDD C)),REAL) is V145() V146() V147() set
K6(K7( the carrier of ((TOP-REAL 2) | (BDD C)),REAL)) is set
P is V11() real ext-real set
W is non empty TopSpace-like TopStruct
the carrier of W is non empty set
(proj1 | (BDD C)) .: the carrier of W is V155() V156() V157() Element of K6(REAL)
proj1 .: (BDD C) is V155() V156() V157() Element of K6(REAL)
K7( the carrier of W,REAL) is V145() V146() V147() set
K6(K7( the carrier of W,REAL)) is set
E is V19() V22( the carrier of W) V23( REAL ) V24() V46( the carrier of W, REAL ) V145() V146() V147() bounded_below Element of K6(K7( the carrier of W,REAL))
S is Element of the carrier of W
E . S is V11() real ext-real Element of REAL
N is V41(2) FinSequence-like V147() Element of the carrier of (TOP-REAL 2)
proj1 . N is V11() real ext-real Element of REAL
N `1 is V11() real ext-real Element of REAL
lower_bound E is V11() real ext-real Element of REAL
C is Element of K6( the carrier of (TOP-REAL 2))
BDD C is Element of K6( the carrier of (TOP-REAL 2))
E-bound (BDD C) is V11() real ext-real Element of REAL
proj1 | (BDD C) is V19() V22( the carrier of ((TOP-REAL 2) | (BDD C))) V23( REAL ) V24() V46( the carrier of ((TOP-REAL 2) | (BDD C)), REAL ) V145() V146() V147() V203((TOP-REAL 2) | (BDD C)) Element of K6(K7( the carrier of ((TOP-REAL 2) | (BDD C)),REAL))
(TOP-REAL 2) | (BDD C) is strict TopSpace-like T_0 T_1 T_2 SubSpace of TOP-REAL 2
the carrier of ((TOP-REAL 2) | (BDD C)) is set
K7( the carrier of ((TOP-REAL 2) | (BDD C)),REAL) is V145() V146() V147() set
K6(K7( the carrier of ((TOP-REAL 2) | (BDD C)),REAL)) is set
P is V11() real ext-real set
W is non empty TopSpace-like TopStruct
the carrier of W is non empty set
(proj1 | (BDD C)) .: the carrier of W is V155() V156() V157() Element of K6(REAL)
proj1 .: (BDD C) is V155() V156() V157() Element of K6(REAL)
K7( the carrier of W,REAL) is V145() V146() V147() set
K6(K7( the carrier of W,REAL)) is set
E is V19() V22( the carrier of W) V23( REAL ) V24() V46( the carrier of W, REAL ) V145() V146() V147() bounded_above Element of K6(K7( the carrier of W,REAL))
S is Element of the carrier of W
E . S is V11() real ext-real Element of REAL
N is V41(2) FinSequence-like V147() Element of the carrier of (TOP-REAL 2)
proj1 . N is V11() real ext-real Element of REAL
N `1 is V11() real ext-real Element of REAL
upper_bound E is V11() real ext-real Element of REAL
C is Element of K6( the carrier of (TOP-REAL 2))
BDD C is Element of K6( the carrier of (TOP-REAL 2))
N-bound (BDD C) is V11() real ext-real Element of REAL
proj2 | (BDD C) is V19() V22( the carrier of ((TOP-REAL 2) | (BDD C))) V23( REAL ) V24() V46( the carrier of ((TOP-REAL 2) | (BDD C)), REAL ) V145() V146() V147() V203((TOP-REAL 2) | (BDD C)) Element of K6(K7( the carrier of ((TOP-REAL 2) | (BDD C)),REAL))
(TOP-REAL 2) | (BDD C) is strict TopSpace-like T_0 T_1 T_2 SubSpace of TOP-REAL 2
the carrier of ((TOP-REAL 2) | (BDD C)) is set
K7( the carrier of ((TOP-REAL 2) | (BDD C)),REAL) is V145() V146() V147() set
K6(K7( the carrier of ((TOP-REAL 2) | (BDD C)),REAL)) is set
P is V11() real ext-real set
W is non empty TopSpace-like TopStruct
the carrier of W is non empty set
(proj2 | (BDD C)) .: the carrier of W is V155() V156() V157() Element of K6(REAL)
proj2 .: (BDD C) is V155() V156() V157() Element of K6(REAL)
K7( the carrier of W,REAL) is V145() V146() V147() set
K6(K7( the carrier of W,REAL)) is set
E is V19() V22( the carrier of W) V23( REAL ) V24() V46( the carrier of W, REAL ) V145() V146() V147() bounded_above Element of K6(K7( the carrier of W,REAL))
S is Element of the carrier of W
E . S is V11() real ext-real Element of REAL
N is V41(2) FinSequence-like V147() Element of the carrier of (TOP-REAL 2)
proj2 . N is V11() real ext-real Element of REAL
N `2 is V11() real ext-real Element of REAL
upper_bound E is V11() real ext-real Element of REAL
C is Element of K6( the carrier of (TOP-REAL 2))
BDD C is Element of K6( the carrier of (TOP-REAL 2))
S-bound (BDD C) is V11() real ext-real Element of REAL
proj2 | (BDD C) is V19() V22( the carrier of ((TOP-REAL 2) | (BDD C))) V23( REAL ) V24() V46( the carrier of ((TOP-REAL 2) | (BDD C)), REAL ) V145() V146() V147() V203((TOP-REAL 2) | (BDD C)) Element of K6(K7( the carrier of ((TOP-REAL 2) | (BDD C)),REAL))
(TOP-REAL 2) | (BDD C) is strict TopSpace-like T_0 T_1 T_2 SubSpace of TOP-REAL 2
the carrier of ((TOP-REAL 2) | (BDD C)) is set
K7( the carrier of ((TOP-REAL 2) | (BDD C)),REAL) is V145() V146() V147() set
K6(K7( the carrier of ((TOP-REAL 2) | (BDD C)),REAL)) is set
P is V11() real ext-real set
W is non empty TopSpace-like TopStruct
the carrier of W is non empty set
(proj2 | (BDD C)) .: the carrier of W is V155() V156() V157() Element of K6(REAL)
proj2 .: (BDD C) is V155() V156() V157() Element of K6(REAL)
K7( the carrier of W,REAL) is V145() V146() V147() set
K6(K7( the carrier of W,REAL)) is set
E is V19() V22( the carrier of W) V23( REAL ) V24() V46( the carrier of W, REAL ) V145() V146() V147() bounded_below Element of K6(K7( the carrier of W,REAL))
S is Element of the carrier of W
E . S is V11() real ext-real Element of REAL
N is V41(2) FinSequence-like V147() Element of the carrier of (TOP-REAL 2)
proj2 . N is V11() real ext-real Element of REAL
N `2 is V11() real ext-real Element of REAL
lower_bound E is V11() real ext-real Element of REAL
C is Element of K6( the carrier of (TOP-REAL 2))
UBD C is Element of K6( the carrier of (TOP-REAL 2))
C is closed compact bounded Element of K6( the carrier of (TOP-REAL 2))
BDD C is open Element of K6( the carrier of (TOP-REAL 2))
W-bound C is V11() real ext-real Element of REAL
W-bound (BDD C) is V11() real ext-real Element of REAL
(W-bound (BDD C)) + (W-bound C) is V11() real ext-real Element of REAL
((W-bound (BDD C)) + (W-bound C)) / 2 is V11() real ext-real Element of REAL
E is V41(2) FinSequence-like V147() Element of the carrier of (TOP-REAL 2)
E `1 is V11() real ext-real Element of REAL
E is V41(2) FinSequence-like V147() Element of the carrier of (TOP-REAL 2)
E `1 is V11() real ext-real Element of REAL
(W-bound C) + (E `1) is V11() real ext-real Element of REAL
((W-bound C) + (E `1)) / 2 is V11() real ext-real Element of REAL
E `2 is V11() real ext-real Element of REAL
|[(((W-bound C) + (E `1)) / 2),(E `2)]| is V41(2) FinSequence-like V147() Element of the carrier of (TOP-REAL 2)
west_halfline |[(((W-bound C) + (E `1)) / 2),(E `2)]| is non empty Element of K6( the carrier of (TOP-REAL 2))
|[(((W-bound C) + (E `1)) / 2),(E `2)]| `1 is V11() real ext-real Element of REAL
(west_halfline |[(((W-bound C) + (E `1)) / 2),(E `2)]|) /\ C is Element of K6( the carrier of (TOP-REAL 2))
EW is set
NS is V41(2) FinSequence-like V147() Element of the carrier of (TOP-REAL 2)
NS `1 is V11() real ext-real Element of REAL
UBD C is non empty open V83( TOP-REAL 2) Element of K6( the carrier of (TOP-REAL 2))
|[(((W-bound C) + (E `1)) / 2),(E `2)]| `2 is V11() real ext-real Element of REAL
(BDD C) /\ (UBD C) is Element of K6( the carrier of (TOP-REAL 2))
E is V41(2) FinSequence-like V147() Element of the carrier of (TOP-REAL 2)
E `1 is V11() real ext-real Element of REAL
C is closed compact bounded Element of K6( the carrier of (TOP-REAL 2))
BDD C is open Element of K6( the carrier of (TOP-REAL 2))
E-bound (BDD C) is V11() real ext-real Element of REAL
E-bound C is V11() real ext-real Element of REAL
(E-bound C) + (E-bound (BDD C)) is V11() real ext-real Element of REAL
((E-bound C) + (E-bound (BDD C))) / 2 is V11() real ext-real Element of REAL
E is V41(2) FinSequence-like V147() Element of the carrier of (TOP-REAL 2)
E `1 is V11() real ext-real Element of REAL
E is V41(2) FinSequence-like V147() Element of the carrier of (TOP-REAL 2)
E `1 is V11() real ext-real Element of REAL
(E-bound C) + (E `1) is V11() real ext-real Element of REAL
((E-bound C) + (E `1)) / 2 is V11() real ext-real Element of REAL
E `2 is V11() real ext-real Element of REAL
|[(((E-bound C) + (E `1)) / 2),(E `2)]| is V41(2) FinSequence-like V147() Element of the carrier of (TOP-REAL 2)
east_halfline |[(((E-bound C) + (E `1)) / 2),(E `2)]| is non empty Element of K6( the carrier of (TOP-REAL 2))
|[(((E-bound C) + (E `1)) / 2),(E `2)]| `1 is V11() real ext-real Element of REAL
(east_halfline |[(((E-bound C) + (E `1)) / 2),(E `2)]|) /\ C is Element of K6( the carrier of (TOP-REAL 2))
EW is set
NS is V41(2) FinSequence-like V147() Element of the carrier of (TOP-REAL 2)
NS `1 is V11() real ext-real Element of REAL
UBD C is non empty open V83( TOP-REAL 2) Element of K6( the carrier of (TOP-REAL 2))
|[(((E-bound C) + (E `1)) / 2),(E `2)]| `2 is V11() real ext-real Element of REAL
(BDD C) /\ (UBD C) is Element of K6( the carrier of (TOP-REAL 2))
E is V41(2) FinSequence-like V147() Element of the carrier of (TOP-REAL 2)
E `1 is V11() real ext-real Element of REAL
C is closed compact bounded Element of K6( the carrier of (TOP-REAL 2))
BDD C is open Element of K6( the carrier of (TOP-REAL 2))
S-bound C is V11() real ext-real Element of REAL
S-bound (BDD C) is V11() real ext-real Element of REAL
(S-bound (BDD C)) + (S-bound C) is V11() real ext-real Element of REAL
((S-bound (BDD C)) + (S-bound C)) / 2 is V11() real ext-real Element of REAL
E is V41(2) FinSequence-like V147() Element of the carrier of (TOP-REAL 2)
E `2 is V11() real ext-real Element of REAL
E is V41(2) FinSequence-like V147() Element of the carrier of (TOP-REAL 2)
E `2 is V11() real ext-real Element of REAL
E `1 is V11() real ext-real Element of REAL
(S-bound C) + (E `2) is V11() real ext-real Element of REAL
((S-bound C) + (E `2)) / 2 is V11() real ext-real Element of REAL
|[(E `1),(((S-bound C) + (E `2)) / 2)]| is V41(2) FinSequence-like V147() Element of the carrier of (TOP-REAL 2)
south_halfline |[(E `1),(((S-bound C) + (E `2)) / 2)]| is non empty Element of K6( the carrier of (TOP-REAL 2))
|[(E `1),(((S-bound C) + (E `2)) / 2)]| `2 is V11() real ext-real Element of REAL
(south_halfline |[(E `1),(((S-bound C) + (E `2)) / 2)]|) /\ C is Element of K6( the carrier of (TOP-REAL 2))
EW is set
NS is V41(2) FinSequence-like V147() Element of the carrier of (TOP-REAL 2)
NS `2 is V11() real ext-real Element of REAL
UBD C is non empty open V83( TOP-REAL 2) Element of K6( the carrier of (TOP-REAL 2))
|[(E `1),(((S-bound C) + (E `2)) / 2)]| `1 is V11() real ext-real Element of REAL
(BDD C) /\ (UBD C) is Element of K6( the carrier of (TOP-REAL 2))
E is V41(2) FinSequence-like V147() Element of the carrier of (TOP-REAL 2)
E `2 is V11() real ext-real Element of REAL
C is closed compact bounded Element of K6( the carrier of (TOP-REAL 2))
BDD C is open Element of K6( the carrier of (TOP-REAL 2))
N-bound (BDD C) is V11() real ext-real Element of REAL
N-bound C is V11() real ext-real Element of REAL
(N-bound C) + (N-bound (BDD C)) is V11() real ext-real Element of REAL
((N-bound C) + (N-bound (BDD C))) / 2 is V11() real ext-real Element of REAL
E is V41(2) FinSequence-like V147() Element of the carrier of (TOP-REAL 2)
E `2 is V11() real ext-real Element of REAL
E is V41(2) FinSequence-like V147() Element of the carrier of (TOP-REAL 2)
E `2 is V11() real ext-real Element of REAL
E `1 is V11() real ext-real Element of REAL
(N-bound C) + (E `2) is V11() real ext-real Element of REAL
((N-bound C) + (E `2)) / 2 is V11() real ext-real Element of REAL
|[(E `1),(((N-bound C) + (E `2)) / 2)]| is V41(2) FinSequence-like V147() Element of the carrier of (TOP-REAL 2)
north_halfline |[(E `1),(((N-bound C) + (E `2)) / 2)]| is non empty Element of K6( the carrier of (TOP-REAL 2))
|[(E `1),(((N-bound C) + (E `2)) / 2)]| `2 is V11() real ext-real Element of REAL
(north_halfline |[(E `1),(((N-bound C) + (E `2)) / 2)]|) /\ C is Element of K6( the carrier of (TOP-REAL 2))
EW is set
NS is V41(2) FinSequence-like V147() Element of the carrier of (TOP-REAL 2)
NS `2 is V11() real ext-real Element of REAL
UBD C is non empty open V83( TOP-REAL 2) Element of K6( the carrier of (TOP-REAL 2))
|[(E `1),(((N-bound C) + (E `2)) / 2)]| `1 is V11() real ext-real Element of REAL
(BDD C) /\ (UBD C) is Element of K6( the carrier of (TOP-REAL 2))
E is V41(2) FinSequence-like V147() Element of the carrier of (TOP-REAL 2)
E `2 is V11() real ext-real Element of REAL
C is ordinal natural V11() real ext-real non negative integer V108() V155() V156() V157() V158() V159() V160() Element of NAT
2 |^ C is ordinal natural V11() real ext-real non negative integer V108() V155() V156() V157() V158() V159() V160() Element of NAT
p is V41(2) FinSequence-like V147() Element of the carrier of (TOP-REAL 2)
p `1 is V11() real ext-real Element of REAL
P is non empty closed compact bounded non vertical Element of K6( the carrier of (TOP-REAL 2))
BDD P is open Element of K6( the carrier of (TOP-REAL 2))
W-bound P is V11() real ext-real Element of REAL
(p `1) - (W-bound P) is V11() real ext-real Element of REAL
E-bound P is V11() real ext-real Element of REAL
(E-bound P) - (W-bound P) is V11() real ext-real Element of REAL
((p `1) - (W-bound P)) / ((E-bound P) - (W-bound P)) is V11() real ext-real Element of REAL
(((p `1) - (W-bound P)) / ((E-bound P) - (W-bound P))) * (2 |^ C) is V11() real ext-real Element of REAL
((((p `1) - (W-bound P)) / ((E-bound P) - (W-bound P))) * (2 |^ C)) + 2 is V11() real ext-real Element of REAL
[\(((((p `1) - (W-bound P)) / ((E-bound P) - (W-bound P))) * (2 |^ C)) + 2)/] is V11() real ext-real integer set
EW is V11() real ext-real integer set
W-bound (BDD P) is V11() real ext-real Element of REAL
[\((((p `1) - (W-bound P)) / ((E-bound P) - (W-bound P))) * (2 |^ C))/] is V11() real ext-real integer set
((((p `1) - (W-bound P)) / ((E-bound P) - (W-bound P))) * (2 |^ C)) - 1 is V11() real ext-real Element of REAL
[\((((p `1) - (W-bound P)) / ((E-bound P) - (W-bound P))) * (2 |^ C))/] + 2 is V11() real ext-real integer Element of REAL
(((((p `1) - (W-bound P)) / ((E-bound P) - (W-bound P))) * (2 |^ C)) - 1) + 2 is V11() real ext-real Element of REAL
0 + 1 is non empty ordinal natural V11() real ext-real positive non negative integer Element of REAL
((((p `1) - (W-bound P)) / ((E-bound P) - (W-bound P))) * (2 |^ C)) + 1 is V11() real ext-real Element of REAL
C is ordinal natural V11() real ext-real non negative integer V108() V155() V156() V157() V158() V159() V160() Element of NAT
2 |^ C is ordinal natural V11() real ext-real non negative integer V108() V155() V156() V157() V158() V159() V160() Element of NAT
p is V41(2) FinSequence-like V147() Element of the carrier of (TOP-REAL 2)
p `1 is V11() real ext-real Element of REAL
P is non empty closed compact bounded non vertical Element of K6( the carrier of (TOP-REAL 2))
BDD P is open Element of K6( the carrier of (TOP-REAL 2))
W-bound P is V11() real ext-real Element of REAL
(p `1) - (W-bound P) is V11() real ext-real Element of REAL
E-bound P is V11() real ext-real Element of REAL
(E-bound P) - (W-bound P) is V11() real ext-real Element of REAL
((p `1) - (W-bound P)) / ((E-bound P) - (W-bound P)) is V11() real ext-real Element of REAL
(((p `1) - (W-bound P)) / ((E-bound P) - (W-bound P))) * (2 |^ C) is V11() real ext-real Element of REAL
((((p `1) - (W-bound P)) / ((E-bound P) - (W-bound P))) * (2 |^ C)) + 2 is V11() real ext-real Element of REAL
[\(((((p `1) - (W-bound P)) / ((E-bound P) - (W-bound P))) * (2 |^ C)) + 2)/] is V11() real ext-real integer set
Gauge (P,C) is V19() V21() V22( NAT ) V23(K333( the carrier of (TOP-REAL 2))) V24() FinSequence-like tabular V188() V189() FinSequence of K333( the carrier of (TOP-REAL 2))
len (Gauge (P,C)) is ordinal natural V11() real ext-real non negative integer V108() V155() V156() V157() V158() V159() V160() Element of NAT
EW is V11() real ext-real integer set
EW + 1 is V11() real ext-real integer Element of REAL
E-bound (BDD P) is V11() real ext-real Element of REAL
1 * (2 |^ C) is ordinal natural V11() real ext-real non negative integer Element of REAL
((((p `1) - (W-bound P)) / ((E-bound P) - (W-bound P))) * (2 |^ C)) + 3 is V11() real ext-real Element of REAL
(2 |^ C) + 3 is non empty ordinal natural V11() real ext-real positive non negative integer Element of REAL
(((((p `1) - (W-bound P)) / ((E-bound P) - (W-bound P))) * (2 |^ C)) + 2) + 1 is V11() real ext-real Element of REAL
C is ordinal natural V11() real ext-real non negative integer V108() V155() V156() V157() V158() V159() V160() Element of NAT
2 |^ C is ordinal natural V11() real ext-real non negative integer V108() V155() V156() V157() V158() V159() V160() Element of NAT
p is V41(2) FinSequence-like V147() Element of the carrier of (TOP-REAL 2)
p `2 is V11() real ext-real Element of REAL
P is non empty closed compact bounded non horizontal Element of K6( the carrier of (TOP-REAL 2))
BDD P is open Element of K6( the carrier of (TOP-REAL 2))
S-bound P is V11() real ext-real Element of REAL
(p `2) - (S-bound P) is V11() real ext-real Element of REAL
N-bound P is V11() real ext-real Element of REAL
(N-bound P) - (S-bound P) is V11() real ext-real Element of REAL
((p `2) - (S-bound P)) / ((N-bound P) - (S-bound P)) is V11() real ext-real Element of REAL
(((p `2) - (S-bound P)) / ((N-bound P) - (S-bound P))) * (2 |^ C) is V11() real ext-real Element of REAL
((((p `2) - (S-bound P)) / ((N-bound P) - (S-bound P))) * (2 |^ C)) + 2 is V11() real ext-real Element of REAL
[\(((((p `2) - (S-bound P)) / ((N-bound P) - (S-bound P))) * (2 |^ C)) + 2)/] is V11() real ext-real integer set
Gauge (P,C) is V19() V21() V22( NAT ) V23(K333( the carrier of (TOP-REAL 2))) V24() FinSequence-like tabular V188() V189() FinSequence of K333( the carrier of (TOP-REAL 2))
width (Gauge (P,C)) is ordinal natural V11() real ext-real non negative integer V108() V155() V156() V157() V158() V159() V160() Element of NAT
EW is V11() real ext-real integer set
EW + 1 is V11() real ext-real integer Element of REAL
[\((((p `2) - (S-bound P)) / ((N-bound P) - (S-bound P))) * (2 |^ C))/] is V11() real ext-real integer set
((((p `2) - (S-bound P)) / ((N-bound P) - (S-bound P))) * (2 |^ C)) - 1 is V11() real ext-real Element of REAL
[\((((p `2) - (S-bound P)) / ((N-bound P) - (S-bound P))) * (2 |^ C))/] + 2 is V11() real ext-real integer Element of REAL
(((((p `2) - (S-bound P)) / ((N-bound P) - (S-bound P))) * (2 |^ C)) - 1) + 2 is V11() real ext-real Element of REAL
S-bound (BDD P) is V11() real ext-real Element of REAL
0 + 1 is non empty ordinal natural V11() real ext-real positive non negative integer Element of REAL
((((p `2) - (S-bound P)) / ((N-bound P) - (S-bound P))) * (2 |^ C)) + 1 is V11() real ext-real Element of REAL
len (Gauge (P,C)) is ordinal natural V11() real ext-real non negative integer V108() V155() V156() V157() V158() V159() V160() Element of NAT
N-bound (BDD P) is V11() real ext-real Element of REAL
1 * (2 |^ C) is ordinal natural V11() real ext-real non negative integer Element of REAL
((((p `2) - (S-bound P)) / ((N-bound P) - (S-bound P))) * (2 |^ C)) + 3 is V11() real ext-real Element of REAL
(2 |^ C) + 3 is non empty ordinal natural V11() real ext-real positive non negative integer Element of REAL
(((((p `2) - (S-bound P)) / ((N-bound P) - (S-bound P))) * (2 |^ C)) + 2) + 1 is V11() real ext-real Element of REAL
C is non empty closed V83( TOP-REAL 2) compact bounded being_simple_closed_curve non horizontal non vertical Element of K6( the carrier of (TOP-REAL 2))
W-bound C is V11() real ext-real Element of REAL
E-bound C is V11() real ext-real Element of REAL
(E-bound C) - (W-bound C) is V11() real ext-real Element of REAL
p is ordinal natural V11() real ext-real non negative integer V108() V155() V156() V157() V158() V159() V160() Element of NAT
2 |^ p is ordinal natural V11() real ext-real non negative integer V108() V155() V156() V157() V158() V159() V160() Element of NAT
((E-bound C) - (W-bound C)) / (2 |^ p) is V11() real ext-real Element of REAL
P is V41(2) FinSequence-like V147() Element of the carrier of (TOP-REAL 2)
P `1 is V11() real ext-real Element of REAL
(P `1) - (W-bound C) is V11() real ext-real Element of REAL
((P `1) - (W-bound C)) / ((E-bound C) - (W-bound C)) is V11() real ext-real Element of REAL
(((P `1) - (W-bound C)) / ((E-bound C) - (W-bound C))) * (2 |^ p) is V11() real ext-real Element of REAL
((((P `1) - (W-bound C)) / ((E-bound C) - (W-bound C))) * (2 |^ p)) + 2 is V11() real ext-real Element of REAL
[\(((((P `1) - (W-bound C)) / ((E-bound C) - (W-bound C))) * (2 |^ p)) + 2)/] is V11() real ext-real integer set
[\((((P `1) - (W-bound C)) / ((E-bound C) - (W-bound C))) * (2 |^ p))/] is V11() real ext-real integer set
EW is V11() real ext-real integer set
EW - 2 is V11() real ext-real integer Element of REAL
(((E-bound C) - (W-bound C)) / (2 |^ p)) * (EW - 2) is V11() real ext-real Element of REAL
(W-bound C) + ((((E-bound C) - (W-bound C)) / (2 |^ p)) * (EW - 2)) is V11() real ext-real Element of REAL
(((E-bound C) - (W-bound C)) / (2 |^ p)) * ((((P `1) - (W-bound C)) / ((E-bound C) - (W-bound C))) * (2 |^ p)) is V11() real ext-real Element of REAL
(((E-bound C) - (W-bound C)) / (2 |^ p)) * [\((((P `1) - (W-bound C)) / ((E-bound C) - (W-bound C))) * (2 |^ p))/] is V11() real ext-real Element of REAL
(W-bound C) + ((P `1) - (W-bound C)) is V11() real ext-real Element of REAL
C is non empty closed V83( TOP-REAL 2) compact bounded being_simple_closed_curve non horizontal non vertical Element of K6( the carrier of (TOP-REAL 2))
W-bound C is V11() real ext-real Element of REAL
E-bound C is V11() real ext-real Element of REAL
(E-bound C) - (W-bound C) is V11() real ext-real Element of REAL
p is ordinal natural V11() real ext-real non negative integer V108() V155() V156() V157() V158() V159() V160() Element of NAT
2 |^ p is ordinal natural V11() real ext-real non negative integer V108() V155() V156() V157() V158() V159() V160() Element of NAT
((E-bound C) - (W-bound C)) / (2 |^ p) is V11() real ext-real Element of REAL
P is V41(2) FinSequence-like V147() Element of the carrier of (TOP-REAL 2)
P `1 is V11() real ext-real Element of REAL
(P `1) - (W-bound C) is V11() real ext-real Element of REAL
((P `1) - (W-bound C)) / ((E-bound C) - (W-bound C)) is V11() real ext-real Element of REAL
(((P `1) - (W-bound C)) / ((E-bound C) - (W-bound C))) * (2 |^ p) is V11() real ext-real Element of REAL
((((P `1) - (W-bound C)) / ((E-bound C) - (W-bound C))) * (2 |^ p)) + 2 is V11() real ext-real Element of REAL
[\(((((P `1) - (W-bound C)) / ((E-bound C) - (W-bound C))) * (2 |^ p)) + 2)/] is V11() real ext-real integer set
EW is V11() real ext-real integer set
EW - 1 is V11() real ext-real integer Element of REAL
(((E-bound C) - (W-bound C)) / (2 |^ p)) * (EW - 1) is V11() real ext-real Element of REAL
(W-bound C) + ((((E-bound C) - (W-bound C)) / (2 |^ p)) * (EW - 1)) is V11() real ext-real Element of REAL
(((((P `1) - (W-bound C)) / ((E-bound C) - (W-bound C))) * (2 |^ p)) + 2) - 1 is V11() real ext-real Element of REAL
((((P `1) - (W-bound C)) / ((E-bound C) - (W-bound C))) * (2 |^ p)) + 1 is V11() real ext-real Element of REAL
(((((P `1) - (W-bound C)) / ((E-bound C) - (W-bound C))) * (2 |^ p)) + 1) - 1 is V11() real ext-real Element of REAL
(((E-bound C) - (W-bound C)) / (2 |^ p)) * ((((P `1) - (W-bound C)) / ((E-bound C) - (W-bound C))) * (2 |^ p)) is V11() real ext-real Element of REAL
(W-bound C) + ((P `1) - (W-bound C)) is V11() real ext-real Element of REAL
C is non empty closed V83( TOP-REAL 2) compact bounded being_simple_closed_curve non horizontal non vertical Element of K6( the carrier of (TOP-REAL 2))
S-bound C is V11() real ext-real Element of REAL
N-bound C is V11() real ext-real Element of REAL
(N-bound C) - (S-bound C) is V11() real ext-real Element of REAL
p is ordinal natural V11() real ext-real non negative integer V108() V155() V156() V157() V158() V159() V160() Element of NAT
2 |^ p is ordinal natural V11() real ext-real non negative integer V108() V155() V156() V157() V158() V159() V160() Element of NAT
((N-bound C) - (S-bound C)) / (2 |^ p) is V11() real ext-real Element of REAL
P is V41(2) FinSequence-like V147() Element of the carrier of (TOP-REAL 2)
P `2 is V11() real ext-real Element of REAL
(P `2) - (S-bound C) is V11() real ext-real Element of REAL
((P `2) - (S-bound C)) / ((N-bound C) - (S-bound C)) is V11() real ext-real Element of REAL
(((P `2) - (S-bound C)) / ((N-bound C) - (S-bound C))) * (2 |^ p) is V11() real ext-real Element of REAL
((((P `2) - (S-bound C)) / ((N-bound C) - (S-bound C))) * (2 |^ p)) + 2 is V11() real ext-real Element of REAL
[\(((((P `2) - (S-bound C)) / ((N-bound C) - (S-bound C))) * (2 |^ p)) + 2)/] is V11() real ext-real integer set
[\((((P `2) - (S-bound C)) / ((N-bound C) - (S-bound C))) * (2 |^ p))/] is V11() real ext-real integer set
EW is V11() real ext-real integer set
EW - 2 is V11() real ext-real integer Element of REAL
(((N-bound C) - (S-bound C)) / (2 |^ p)) * (EW - 2) is V11() real ext-real Element of REAL
(S-bound C) + ((((N-bound C) - (S-bound C)) / (2 |^ p)) * (EW - 2)) is V11() real ext-real Element of REAL
(((N-bound C) - (S-bound C)) / (2 |^ p)) * ((((P `2) - (S-bound C)) / ((N-bound C) - (S-bound C))) * (2 |^ p)) is V11() real ext-real Element of REAL
(((N-bound C) - (S-bound C)) / (2 |^ p)) * [\((((P `2) - (S-bound C)) / ((N-bound C) - (S-bound C))) * (2 |^ p))/] is V11() real ext-real Element of REAL
(S-bound C) + ((P `2) - (S-bound C)) is V11() real ext-real Element of REAL
C is non empty closed V83( TOP-REAL 2) compact bounded being_simple_closed_curve non horizontal non vertical Element of K6( the carrier of (TOP-REAL 2))
S-bound C is V11() real ext-real Element of REAL
N-bound C is V11() real ext-real Element of REAL
(N-bound C) - (S-bound C) is V11() real ext-real Element of REAL
p is ordinal natural V11() real ext-real non negative integer V108() V155() V156() V157() V158() V159() V160() Element of NAT
2 |^ p is ordinal natural V11() real ext-real non negative integer V108() V155() V156() V157() V158() V159() V160() Element of NAT
((N-bound C) - (S-bound C)) / (2 |^ p) is V11() real ext-real Element of REAL
P is V41(2) FinSequence-like V147() Element of the carrier of (TOP-REAL 2)
P `2 is V11() real ext-real Element of REAL
(P `2) - (S-bound C) is V11() real ext-real Element of REAL
((P `2) - (S-bound C)) / ((N-bound C) - (S-bound C)) is V11() real ext-real Element of REAL
(((P `2) - (S-bound C)) / ((N-bound C) - (S-bound C))) * (2 |^ p) is V11() real ext-real Element of REAL
((((P `2) - (S-bound C)) / ((N-bound C) - (S-bound C))) * (2 |^ p)) + 2 is V11() real ext-real Element of REAL
[\(((((P `2) - (S-bound C)) / ((N-bound C) - (S-bound C))) * (2 |^ p)) + 2)/] is V11() real ext-real integer set
EW is V11() real ext-real integer set
EW - 1 is V11() real ext-real integer Element of REAL
(((N-bound C) - (S-bound C)) / (2 |^ p)) * (EW - 1) is V11() real ext-real Element of REAL
(S-bound C) + ((((N-bound C) - (S-bound C)) / (2 |^ p)) * (EW - 1)) is V11() real ext-real Element of REAL
(((((P `2) - (S-bound C)) / ((N-bound C) - (S-bound C))) * (2 |^ p)) + 2) - 1 is V11() real ext-real Element of REAL
((((P `2) - (S-bound C)) / ((N-bound C) - (S-bound C))) * (2 |^ p)) + 1 is V11() real ext-real Element of REAL
(((((P `2) - (S-bound C)) / ((N-bound C) - (S-bound C))) * (2 |^ p)) + 1) - 1 is V11() real ext-real Element of REAL
(S-bound C) + ((P `2) - (S-bound C)) is V11() real ext-real Element of REAL
(((N-bound C) - (S-bound C)) / (2 |^ p)) * ((((P `2) - (S-bound C)) / ((N-bound C) - (S-bound C))) * (2 |^ p)) is V11() real ext-real Element of REAL
C is closed Element of K6( the carrier of (TOP-REAL 2))
BDD C is open Element of K6( the carrier of (TOP-REAL 2))
p is Element of the carrier of (Euclid 2)
Int (BDD C) is Element of K6( the carrier of (TOP-REAL 2))
W is V11() real ext-real set
Ball (p,W) is Element of K6( the carrier of (Euclid 2))
E is V11() real ext-real Element of REAL
Ball (p,E) is Element of K6( the carrier of (Euclid 2))
C is non empty closed V83( TOP-REAL 2) compact bounded being_simple_closed_curve non horizontal non vertical Element of K6( the carrier of (TOP-REAL 2))
p is ordinal natural V11() real ext-real non negative integer V108() V155() V156() V157() V158() V159() V160() Element of NAT
Gauge (C,p) is V19() V21() V22( NAT ) V23(K333( the carrier of (TOP-REAL 2))) V24() FinSequence-like tabular V188() V189() V190() V191() FinSequence of K333( the carrier of (TOP-REAL 2))
(Gauge (C,p)) * (1,1) is V41(2) FinSequence-like V147() Element of the carrier of (TOP-REAL 2)
(Gauge (C,p)) * (1,2) is V41(2) FinSequence-like V147() Element of the carrier of (TOP-REAL 2)
dist (((Gauge (C,p)) * (1,1)),((Gauge (C,p)) * (1,2))) is V11() real ext-real Element of REAL
(Gauge (C,p)) * (2,1) is V41(2) FinSequence-like V147() Element of the carrier of (TOP-REAL 2)
dist (((Gauge (C,p)) * (1,1)),((Gauge (C,p)) * (2,1))) is V11() real ext-real Element of REAL
len (Gauge (C,p)) is ordinal natural V11() real ext-real non negative integer V108() V155() V156() V157() V158() V159() V160() Element of NAT
width (Gauge (C,p)) is ordinal natural V11() real ext-real non negative integer V108() V155() V156() V157() V158() V159() V160() Element of NAT
P is ordinal natural V11() real ext-real non negative integer V108() V155() V156() V157() V158() V159() V160() Element of NAT
P + 1 is non empty ordinal natural V11() real ext-real positive non negative integer Element of REAL
W is ordinal natural V11() real ext-real non negative integer V108() V155() V156() V157() V158() V159() V160() Element of NAT
cell ((Gauge (C,p)),P,W) is Element of K6( the carrier of (TOP-REAL 2))
W + 1 is non empty ordinal natural V11() real ext-real positive non negative integer Element of REAL
S is V41(2) FinSequence-like V147() Element of the carrier of (TOP-REAL 2)
N is V41(2) FinSequence-like V147() Element of the carrier of (TOP-REAL 2)
dist (S,N) is V11() real ext-real Element of REAL
EW is V11() real ext-real set
2 * EW is V11() real ext-real Element of REAL
S `1 is V11() real ext-real Element of REAL
(Gauge (C,p)) * ((P + 1),W) is V41(2) FinSequence-like V147() Element of the carrier of (TOP-REAL 2)
((Gauge (C,p)) * ((P + 1),W)) `1 is V11() real ext-real Element of REAL
S `2 is V11() real ext-real Element of REAL
(Gauge (C,p)) * (P,(W + 1)) is V41(2) FinSequence-like V147() Element of the carrier of (TOP-REAL 2)
((Gauge (C,p)) * (P,(W + 1))) `2 is V11() real ext-real Element of REAL
(Gauge (C,p)) * (P,W) is V41(2) FinSequence-like V147() Element of the carrier of (TOP-REAL 2)
((Gauge (C,p)) * (P,W)) `2 is V11() real ext-real Element of REAL
[P,W] is set
{P,W} is non empty V155() V156() V157() V158() V159() V160() set
{P} is non empty V155() V156() V157() V158() V159() V160() set
{{P,W},{P}} is non empty set
Indices (Gauge (C,p)) is set
N `2 is V11() real ext-real Element of REAL
N `1 is V11() real ext-real Element of REAL
((Gauge (C,p)) * (P,W)) `1 is V11() real ext-real Element of REAL
[P,(W + 1)] is set
{P,(W + 1)} is non empty V155() V156() V157() V158() V159() V160() set
{{P,(W + 1)},{P}} is non empty set
(((Gauge (C,p)) * (P,(W + 1))) `2) - (((Gauge (C,p)) * (P,W)) `2) is V11() real ext-real Element of REAL
[(P + 1),W] is set
{(P + 1),W} is non empty V155() V156() V157() V158() V159() V160() set
{(P + 1)} is non empty V155() V156() V157() V158() V159() V160() set
{{(P + 1),W},{(P + 1)}} is non empty set
(((Gauge (C,p)) * ((P + 1),W)) `1) - (((Gauge (C,p)) * (P,W)) `1) is V11() real ext-real Element of REAL
EW + EW is V11() real ext-real set
((((Gauge (C,p)) * ((P + 1),W)) `1) - (((Gauge (C,p)) * (P,W)) `1)) + ((((Gauge (C,p)) * (P,(W + 1))) `2) - (((Gauge (C,p)) * (P,W)) `2)) is V11() real ext-real Element of REAL
C is V41(2) FinSequence-like V147() Element of the carrier of (TOP-REAL 2)
C `2 is V11() real ext-real Element of REAL
P is closed compact bounded Element of K6( the carrier of (TOP-REAL 2))
BDD P is open Element of K6( the carrier of (TOP-REAL 2))
N-bound (BDD P) is V11() real ext-real Element of REAL
p is Element of the carrier of (Euclid 2)
W is V11() real ext-real Element of REAL
Ball (p,W) is Element of K6( the carrier of (Euclid 2))
C `1 is V11() real ext-real Element of REAL
W / 2 is V11() real ext-real Element of REAL
(C `2) + (W / 2) is V11() real ext-real Element of REAL
|[(C `1),((C `2) + (W / 2))]| is V41(2) FinSequence-like V147() Element of the carrier of (TOP-REAL 2)
(C `2) + 0 is V11() real ext-real Element of REAL
|[(C `1),((C `2) + (W / 2))]| `2 is V11() real ext-real Element of REAL
|[(C `1),(C `2)]| is V41(2) FinSequence-like V147() Element of the carrier of (TOP-REAL 2)
C is V41(2) FinSequence-like V147() Element of the carrier of (TOP-REAL 2)
C `1 is V11() real ext-real Element of REAL
P is closed compact bounded Element of K6( the carrier of (TOP-REAL 2))
BDD P is open Element of K6( the carrier of (TOP-REAL 2))
E-bound (BDD P) is V11() real ext-real Element of REAL
p is Element of the carrier of (Euclid 2)
W is V11() real ext-real Element of REAL
Ball (p,W) is Element of K6( the carrier of (Euclid 2))
W / 2 is V11() real ext-real Element of REAL
(C `1) + (W / 2) is V11() real ext-real Element of REAL
C `2 is V11() real ext-real Element of REAL
|[((C `1) + (W / 2)),(C `2)]| is V41(2) FinSequence-like V147() Element of the carrier of (TOP-REAL 2)
(C `1) + 0 is V11() real ext-real Element of REAL
|[((C `1) + (W / 2)),(C `2)]| `1 is V11() real ext-real Element of REAL
|[(C `1),(C `2)]| is V41(2) FinSequence-like V147() Element of the carrier of (TOP-REAL 2)
C is V41(2) FinSequence-like V147() Element of the carrier of (TOP-REAL 2)
C `2 is V11() real ext-real Element of REAL
P is closed compact bounded Element of K6( the carrier of (TOP-REAL 2))
BDD P is open Element of K6( the carrier of (TOP-REAL 2))
S-bound (BDD P) is V11() real ext-real Element of REAL
p is Element of the carrier of (Euclid 2)
W is V11() real ext-real Element of REAL
Ball (p,W) is Element of K6( the carrier of (Euclid 2))
C `1 is V11() real ext-real Element of REAL
W / 2 is V11() real ext-real Element of REAL
(C `2) - (W / 2) is V11() real ext-real Element of REAL
|[(C `1),((C `2) - (W / 2))]| is V41(2) FinSequence-like V147() Element of the carrier of (TOP-REAL 2)
(C `2) + (W / 2) is V11() real ext-real Element of REAL
(C `2) + 0 is V11() real ext-real Element of REAL
|[(C `1),((C `2) - (W / 2))]| `2 is V11() real ext-real Element of REAL
|[(C `1),(C `2)]| is V41(2) FinSequence-like V147() Element of the carrier of (TOP-REAL 2)
C is V41(2) FinSequence-like V147() Element of the carrier of (TOP-REAL 2)
C `1 is V11() real ext-real Element of REAL
P is closed compact bounded Element of K6( the carrier of (TOP-REAL 2))
BDD P is open Element of K6( the carrier of (TOP-REAL 2))
W-bound (BDD P) is V11() real ext-real Element of REAL
p is Element of the carrier of (Euclid 2)
W is V11() real ext-real Element of REAL
Ball (p,W) is Element of K6( the carrier of (Euclid 2))
W / 2 is V11() real ext-real Element of REAL
(C `1) - (W / 2) is V11() real ext-real Element of REAL
C `2 is V11() real ext-real Element of REAL
|[((C `1) - (W / 2)),(C `2)]| is V41(2) FinSequence-like V147() Element of the carrier of (TOP-REAL 2)
(C `1) + (W / 2) is V11() real ext-real Element of REAL
(C `1) + 0 is V11() real ext-real Element of REAL
|[((C `1) - (W / 2)),(C `2)]| `1 is V11() real ext-real Element of REAL
|[(C `1),(C `2)]| is V41(2) FinSequence-like V147() Element of the carrier of (TOP-REAL 2)
C is non empty closed V83( TOP-REAL 2) compact bounded being_simple_closed_curve non horizontal non vertical Element of K6( the carrier of (TOP-REAL 2))
BDD C is open Element of K6( the carrier of (TOP-REAL 2))
p is V41(2) FinSequence-like V147() Element of the carrier of (TOP-REAL 2)
p `1 is V11() real ext-real Element of REAL
W-bound C is V11() real ext-real Element of REAL
E-bound C is V11() real ext-real Element of REAL
S-bound C is V11() real ext-real Element of REAL
N-bound C is V11() real ext-real Element of REAL
(E-bound C) - (W-bound C) is V11() real ext-real Element of REAL
(N-bound C) - (S-bound C) is V11() real ext-real Element of REAL
P is Element of the carrier of (Euclid 2)
r is V11() real ext-real Element of REAL
Ball (P,r) is Element of K6( the carrier of (Euclid 2))
r / 4 is V11() real ext-real Element of REAL
n is ordinal natural V11() real ext-real non negative integer V108() V155() V156() V157() V158() V159() V160() Element of NAT
Gauge (C,n) is V19() V21() V22( NAT ) V23(K333( the carrier of (TOP-REAL 2))) V24() FinSequence-like tabular V188() V189() V190() V191() FinSequence of K333( the carrier of (TOP-REAL 2))
(Gauge (C,n)) * (1,1) is V41(2) FinSequence-like V147() Element of the carrier of (TOP-REAL 2)
(Gauge (C,n)) * (1,2) is V41(2) FinSequence-like V147() Element of the carrier of (TOP-REAL 2)
dist (((Gauge (C,n)) * (1,1)),((Gauge (C,n)) * (1,2))) is V11() real ext-real Element of REAL
(Gauge (C,n)) * (2,1) is V41(2) FinSequence-like V147() Element of the carrier of (TOP-REAL 2)
dist (((Gauge (C,n)) * (1,1)),((Gauge (C,n)) * (2,1))) is V11() real ext-real Element of REAL
(p `1) - (W-bound C) is V11() real ext-real Element of REAL
((p `1) - (W-bound C)) / ((E-bound C) - (W-bound C)) is V11() real ext-real Element of REAL
2 |^ n is ordinal natural V11() real ext-real non negative integer V108() V155() V156() V157() V158() V159() V160() Element of NAT
(((p `1) - (W-bound C)) / ((E-bound C) - (W-bound C))) * (2 |^ n) is V11() real ext-real Element of REAL
((((p `1) - (W-bound C)) / ((E-bound C) - (W-bound C))) * (2 |^ n)) + 2 is V11() real ext-real Element of REAL
[\(((((p `1) - (W-bound C)) / ((E-bound C) - (W-bound C))) * (2 |^ n)) + 2)/] is V11() real ext-real integer set
p `2 is V11() real ext-real Element of REAL
(p `2) - (S-bound C) is V11() real ext-real Element of REAL
((p `2) - (S-bound C)) / ((N-bound C) - (S-bound C)) is V11() real ext-real Element of REAL
(((p `2) - (S-bound C)) / ((N-bound C) - (S-bound C))) * (2 |^ n) is V11() real ext-real Element of REAL
((((p `2) - (S-bound C)) / ((N-bound C) - (S-bound C))) * (2 |^ n)) + 2 is V11() real ext-real Element of REAL
[\(((((p `2) - (S-bound C)) / ((N-bound C) - (S-bound C))) * (2 |^ n)) + 2)/] is V11() real ext-real integer set
[\(((((p `1) - (W-bound C)) / ((E-bound C) - (W-bound C))) * (2 |^ n)) + 2)/] + 1 is V11() real ext-real integer Element of REAL
len (Gauge (C,n)) is ordinal natural V11() real ext-real non negative integer V108() V155() V156() V157() V158() V159() V160() Element of NAT
[\(((((p `2) - (S-bound C)) / ((N-bound C) - (S-bound C))) * (2 |^ n)) + 2)/] + 1 is V11() real ext-real integer Element of REAL
width (Gauge (C,n)) is ordinal natural V11() real ext-real non negative integer V108() V155() V156() V157() V158() V159() V160() Element of NAT
I is ordinal natural V11() real ext-real non negative integer V108() V155() V156() V157() V158() V159() V160() Element of NAT
I + 1 is non empty ordinal natural V11() real ext-real positive non negative integer Element of REAL
J is ordinal natural V11() real ext-real non negative integer V108() V155() V156() V157() V158() V159() V160() Element of NAT
J + 1 is non empty ordinal natural V11() real ext-real positive non negative integer Element of REAL
[I,(J + 1)] is set
{I,(J + 1)} is non empty V155() V156() V157() V158() V159() V160() set
{I} is non empty V155() V156() V157() V158() V159() V160() set
{{I,(J + 1)},{I}} is non empty set
Indices (Gauge (C,n)) is set
(Gauge (C,n)) * (I,(J + 1)) is V41(2) FinSequence-like V147() Element of the carrier of (TOP-REAL 2)
((E-bound C) - (W-bound C)) / (2 |^ n) is V11() real ext-real Element of REAL
I - 2 is V11() real ext-real integer Element of REAL
(((E-bound C) - (W-bound C)) / (2 |^ n)) * (I - 2) is V11() real ext-real Element of REAL
(W-bound C) + ((((E-bound C) - (W-bound C)) / (2 |^ n)) * (I - 2)) is V11() real ext-real Element of REAL
((N-bound C) - (S-bound C)) / (2 |^ n) is V11() real ext-real Element of REAL
(J + 1) - 2 is V11() real ext-real integer Element of REAL
(((N-bound C) - (S-bound C)) / (2 |^ n)) * ((J + 1) - 2) is V11() real ext-real Element of REAL
(S-bound C) + ((((N-bound C) - (S-bound C)) / (2 |^ n)) * ((J + 1) - 2)) is V11() real ext-real Element of REAL
|[((W-bound C) + ((((E-bound C) - (W-bound C)) / (2 |^ n)) * (I - 2))),((S-bound C) + ((((N-bound C) - (S-bound C)) / (2 |^ n)) * ((J + 1) - 2)))]| is V41(2) FinSequence-like V147() Element of the carrier of (TOP-REAL 2)
((Gauge (C,n)) * (I,(J + 1))) `2 is V11() real ext-real Element of REAL
J - 1 is V11() real ext-real integer Element of REAL
(((N-bound C) - (S-bound C)) / (2 |^ n)) * (J - 1) is V11() real ext-real Element of REAL
(S-bound C) + ((((N-bound C) - (S-bound C)) / (2 |^ n)) * (J - 1)) is V11() real ext-real Element of REAL
[I,J] is set
{I,J} is non empty V155() V156() V157() V158() V159() V160() set
{{I,J},{I}} is non empty set
(Gauge (C,n)) * (I,J) is V41(2) FinSequence-like V147() Element of the carrier of (TOP-REAL 2)
J - 2 is V11() real ext-real integer Element of REAL
(((N-bound C) - (S-bound C)) / (2 |^ n)) * (J - 2) is V11() real ext-real Element of REAL
(S-bound C) + ((((N-bound C) - (S-bound C)) / (2 |^ n)) * (J - 2)) is V11() real ext-real Element of REAL
|[((W-bound C) + ((((E-bound C) - (W-bound C)) / (2 |^ n)) * (I - 2))),((S-bound C) + ((((N-bound C) - (S-bound C)) / (2 |^ n)) * (J - 2)))]| is V41(2) FinSequence-like V147() Element of the carrier of (TOP-REAL 2)
((Gauge (C,n)) * (I,J)) `1 is V11() real ext-real Element of REAL
[(I + 1),J] is set
{(I + 1),J} is non empty V155() V156() V157() V158() V159() V160() set
{(I + 1)} is non empty V155() V156() V157() V158() V159() V160() set
{{(I + 1),J},{(I + 1)}} is non empty set
(Gauge (C,n)) * ((I + 1),J) is V41(2) FinSequence-like V147() Element of the carrier of (TOP-REAL 2)
(I + 1) - 2 is V11() real ext-real integer Element of REAL
(((E-bound C) - (W-bound C)) / (2 |^ n)) * ((I + 1) - 2) is V11() real ext-real Element of REAL
(W-bound C) + ((((E-bound C) - (W-bound C)) / (2 |^ n)) * ((I + 1) - 2)) is V11() real ext-real Element of REAL
|[((W-bound C) + ((((E-bound C) - (W-bound C)) / (2 |^ n)) * ((I + 1) - 2))),((S-bound C) + ((((N-bound C) - (S-bound C)) / (2 |^ n)) * (J - 2)))]| is V41(2) FinSequence-like V147() Element of the carrier of (TOP-REAL 2)
((Gauge (C,n)) * ((I + 1),J)) `1 is V11() real ext-real Element of REAL
I - 1 is V11() real ext-real integer Element of REAL
(((E-bound C) - (W-bound C)) / (2 |^ n)) * (I - 1) is V11() real ext-real Element of REAL
(W-bound C) + ((((E-bound C) - (W-bound C)) / (2 |^ n)) * (I - 1)) is V11() real ext-real Element of REAL
((Gauge (C,n)) * (I,J)) `2 is V11() real ext-real Element of REAL
cell ((Gauge (C,n)),I,J) is Element of K6( the carrier of (TOP-REAL 2))
I -' 1 is ordinal natural V11() real ext-real non negative integer V108() V155() V156() V157() V158() V159() V160() Element of NAT
(I -' 1) + 1 is non empty ordinal natural V11() real ext-real positive non negative integer Element of REAL
(Gauge (C,n)) * (((I -' 1) + 1),J) is V41(2) FinSequence-like V147() Element of the carrier of (TOP-REAL 2)
((Gauge (C,n)) * (((I -' 1) + 1),J)) `1 is V11() real ext-real Element of REAL
(Gauge (C,n)) * ((I -' 1),J) is V41(2) FinSequence-like V147() Element of the carrier of (TOP-REAL 2)
((Gauge (C,n)) * ((I -' 1),J)) `1 is V11() real ext-real Element of REAL
cell ((Gauge (C,n)),(I -' 1),J) is Element of K6( the carrier of (TOP-REAL 2))
W-bound (BDD C) is V11() real ext-real Element of REAL
((Gauge (C,n)) * ((I -' 1),J)) `2 is V11() real ext-real Element of REAL
(Gauge (C,n)) * ((I -' 1),(J + 1)) is V41(2) FinSequence-like V147() Element of the carrier of (TOP-REAL 2)
((Gauge (C,n)) * ((I -' 1),(J + 1))) `2 is V11() real ext-real Element of REAL
C is Element of K6( the carrier of (TOP-REAL 2))
UBD C is Element of K6( the carrier of (TOP-REAL 2))