:: GOBOARD6 semantic presentation

REAL is V157() V158() V159() V163() set

NAT is V157() V158() V159() V160() V161() V162() V163() Element of K6(REAL)

K6(REAL) is set

COMPLEX is V157() V163() set

omega is V157() V158() V159() V160() V161() V162() V163() set

K6(omega) is set

1 is non empty natural V11() real ext-real positive non negative V33() V156() V157() V158() V159() V160() V161() V162() Element of NAT

K7(1,1) is set

K6(K7(1,1)) is set

K7(K7(1,1),1) is set

K6(K7(K7(1,1),1)) is set

K7(K7(1,1),REAL) is set

K6(K7(K7(1,1),REAL)) is set

K7(REAL,REAL) is set

K7(K7(REAL,REAL),REAL) is set

K6(K7(K7(REAL,REAL),REAL)) is set

2 is non empty natural V11() real ext-real positive non negative V33() V156() V157() V158() V159() V160() V161() V162() Element of NAT

K7(2,2) is set

K7(K7(2,2),REAL) is set

K6(K7(K7(2,2),REAL)) is set

K6(NAT) is set

RAT is V157() V158() V159() V160() V163() set

INT is V157() V158() V159() V160() V161() V163() set

K6(K7(REAL,REAL)) is set

TOP-REAL 2 is non empty TopSpace-like V111() V136() V137() V138() V139() V140() V141() V142() strict RLTopStruct

the carrier of (TOP-REAL 2) is non empty set

K246( the carrier of (TOP-REAL 2)) is M11( the carrier of (TOP-REAL 2))

K6( the carrier of (TOP-REAL 2)) is set

K7(COMPLEX,COMPLEX) is set

K6(K7(COMPLEX,COMPLEX)) is set

K7(K7(COMPLEX,COMPLEX),COMPLEX) is set

K6(K7(K7(COMPLEX,COMPLEX),COMPLEX)) is set

K7(RAT,RAT) is set

K6(K7(RAT,RAT)) is set

K7(K7(RAT,RAT),RAT) is set

K6(K7(K7(RAT,RAT),RAT)) is set

K7(INT,INT) is set

K6(K7(INT,INT)) is set

K7(K7(INT,INT),INT) is set

K6(K7(K7(INT,INT),INT)) is set

K7(NAT,NAT) is set

K7(K7(NAT,NAT),NAT) is set

K6(K7(K7(NAT,NAT),NAT)) is set

{} is empty V157() V158() V159() V160() V161() V162() V163() set

the empty V157() V158() V159() V160() V161() V162() V163() set is empty V157() V158() V159() V160() V161() V162() V163() set

0 is empty natural V11() real ext-real non positive non negative V33() V156() V157() V158() V159() V160() V161() V162() V163() Element of NAT

Euclid 2 is non empty strict Reflexive discerning V88() triangle Discerning MetrStruct

REAL 2 is non empty FinSequence-membered M11( REAL )

K247(2,REAL) is FinSequence-membered M11( REAL )

Pitag_dist 2 is V16() V19(K7((REAL 2),(REAL 2))) V20( REAL ) V21() V30(K7((REAL 2),(REAL 2)), REAL ) Element of K6(K7(K7((REAL 2),(REAL 2)),REAL))

K7((REAL 2),(REAL 2)) is set

K7(K7((REAL 2),(REAL 2)),REAL) is set

K6(K7(K7((REAL 2),(REAL 2)),REAL)) is set

MetrStruct(# (REAL 2),(Pitag_dist 2) #) is strict MetrStruct

the carrier of (Euclid 2) is non empty set

n is V42(2) FinSequence-like V148() Element of the carrier of (TOP-REAL 2)

n `1 is V11() real ext-real Element of REAL

n `2 is V11() real ext-real Element of REAL

A is V42(2) FinSequence-like V148() Element of the carrier of (TOP-REAL 2)

n + A is V42(2) FinSequence-like V148() Element of the carrier of (TOP-REAL 2)

(n + A) `1 is V11() real ext-real Element of REAL

A `1 is V11() real ext-real Element of REAL

(n `1) + (A `1) is V11() real ext-real Element of REAL

(n + A) `2 is V11() real ext-real Element of REAL

A `2 is V11() real ext-real Element of REAL

(n `2) + (A `2) is V11() real ext-real Element of REAL

|[((n `1) + (A `1)),((n `2) + (A `2))]| is V42(2) FinSequence-like V148() Element of the carrier of (TOP-REAL 2)

n is V42(2) FinSequence-like V148() Element of the carrier of (TOP-REAL 2)

n `1 is V11() real ext-real Element of REAL

n `2 is V11() real ext-real Element of REAL

A is V42(2) FinSequence-like V148() Element of the carrier of (TOP-REAL 2)

n - A is V42(2) FinSequence-like V148() Element of the carrier of (TOP-REAL 2)

(n - A) `1 is V11() real ext-real Element of REAL

A `1 is V11() real ext-real Element of REAL

(n `1) - (A `1) is V11() real ext-real Element of REAL

K38((A `1)) is V11() real ext-real set

K36((n `1),K38((A `1))) is V11() real ext-real set

(n - A) `2 is V11() real ext-real Element of REAL

A `2 is V11() real ext-real Element of REAL

(n `2) - (A `2) is V11() real ext-real Element of REAL

K38((A `2)) is V11() real ext-real set

K36((n `2),K38((A `2))) is V11() real ext-real set

|[((n `1) - (A `1)),((n `2) - (A `2))]| is V42(2) FinSequence-like V148() Element of the carrier of (TOP-REAL 2)

n is V11() real ext-real Element of REAL

A is V42(2) FinSequence-like V148() Element of the carrier of (TOP-REAL 2)

n * A is V42(2) FinSequence-like V148() Element of the carrier of (TOP-REAL 2)

(n * A) `1 is V11() real ext-real Element of REAL

A `1 is V11() real ext-real Element of REAL

n * (A `1) is V11() real ext-real Element of REAL

(n * A) `2 is V11() real ext-real Element of REAL

A `2 is V11() real ext-real Element of REAL

n * (A `2) is V11() real ext-real Element of REAL

|[(n * (A `1)),(n * (A `2))]| is V42(2) FinSequence-like V148() Element of the carrier of (TOP-REAL 2)

n is non empty Reflexive MetrStruct

the carrier of n is non empty set

A is Element of the carrier of n

p is V11() real ext-real set

Ball (A,p) is Element of K6( the carrier of n)

K6( the carrier of n) is set

{ b

dist (A,A) is V11() real ext-real Element of REAL

n is Reflexive discerning V88() triangle MetrStruct

TopSpaceMetr n is strict TopSpace-like TopStruct

the carrier of (TopSpaceMetr n) is set

K6( the carrier of (TopSpaceMetr n)) is set

the carrier of n is set

A is Element of K6( the carrier of (TopSpaceMetr n))

p is V11() real ext-real set

p9 is Element of the carrier of n

Ball (p9,p) is Element of K6( the carrier of n)

K6( the carrier of n) is set

Family_open_set n is Element of K6(K6( the carrier of n))

K6(K6( the carrier of n)) is set

TopStruct(# the carrier of n,(Family_open_set n) #) is strict TopStruct

n is natural V11() real ext-real set

Euclid n is non empty strict Reflexive discerning V88() triangle Discerning MetrStruct

REAL n is non empty FinSequence-membered M11( REAL )

K247(n,REAL) is FinSequence-membered M11( REAL )

Pitag_dist n is V16() V19(K7((REAL n),(REAL n))) V20( REAL ) V21() V30(K7((REAL n),(REAL n)), REAL ) Element of K6(K7(K7((REAL n),(REAL n)),REAL))

K7((REAL n),(REAL n)) is set

K7(K7((REAL n),(REAL n)),REAL) is set

K6(K7(K7((REAL n),(REAL n)),REAL)) is set

MetrStruct(# (REAL n),(Pitag_dist n) #) is strict MetrStruct

the carrier of (Euclid n) is non empty set

TOP-REAL n is non empty TopSpace-like V111() V136() V137() V138() V139() V140() V141() V142() strict RLTopStruct

the carrier of (TOP-REAL n) is non empty set

A is Element of the carrier of (Euclid n)

p is V42(n) FinSequence-like V148() Element of the carrier of (TOP-REAL n)

p9 is V11() real ext-real set

Ball (A,p9) is Element of K6( the carrier of (Euclid n))

K6( the carrier of (Euclid n)) is set

K6( the carrier of (TOP-REAL n)) is set

the topology of (TOP-REAL n) is non empty Element of K6(K6( the carrier of (TOP-REAL n)))

K6(K6( the carrier of (TOP-REAL n))) is set

TopStruct(# the carrier of (TOP-REAL n), the topology of (TOP-REAL n) #) is non empty strict TopSpace-like TopStruct

TopSpaceMetr (Euclid n) is non empty strict TopSpace-like TopStruct

the carrier of (TopSpaceMetr (Euclid n)) is non empty set

K6( the carrier of (TopSpaceMetr (Euclid n))) is set

s is Element of K6( the carrier of (TOP-REAL n))

s1 is Element of K6( the carrier of (TopSpaceMetr (Euclid n)))

n is natural V11() real ext-real set

TOP-REAL n is non empty TopSpace-like V111() V136() V137() V138() V139() V140() V141() V142() strict RLTopStruct

the carrier of (TOP-REAL n) is non empty set

K6( the carrier of (TOP-REAL n)) is set

Euclid n is non empty strict Reflexive discerning V88() triangle Discerning MetrStruct

REAL n is non empty FinSequence-membered M11( REAL )

K247(n,REAL) is FinSequence-membered M11( REAL )

Pitag_dist n is V16() V19(K7((REAL n),(REAL n))) V20( REAL ) V21() V30(K7((REAL n),(REAL n)), REAL ) Element of K6(K7(K7((REAL n),(REAL n)),REAL))

K7((REAL n),(REAL n)) is set

K7(K7((REAL n),(REAL n)),REAL) is set

K6(K7(K7((REAL n),(REAL n)),REAL)) is set

MetrStruct(# (REAL n),(Pitag_dist n) #) is strict MetrStruct

the carrier of (Euclid n) is non empty set

A is V11() real ext-real Element of REAL

p is Element of K6( the carrier of (TOP-REAL n))

p9 is Element of the carrier of (Euclid n)

Ball (p9,A) is Element of K6( the carrier of (Euclid n))

K6( the carrier of (Euclid n)) is set

the topology of (TOP-REAL n) is non empty Element of K6(K6( the carrier of (TOP-REAL n)))

K6(K6( the carrier of (TOP-REAL n))) is set

TopStruct(# the carrier of (TOP-REAL n), the topology of (TOP-REAL n) #) is non empty strict TopSpace-like TopStruct

TopSpaceMetr (Euclid n) is non empty strict TopSpace-like TopStruct

the carrier of (TopSpaceMetr (Euclid n)) is non empty set

K6( the carrier of (TopSpaceMetr (Euclid n))) is set

s is Element of K6( the carrier of (TopSpaceMetr (Euclid n)))

n is non empty Reflexive discerning V88() triangle Discerning MetrStruct

the carrier of n is non empty set

TopSpaceMetr n is non empty strict TopSpace-like TopStruct

the carrier of (TopSpaceMetr n) is non empty set

K6( the carrier of (TopSpaceMetr n)) is set

A is Element of the carrier of n

p is Element of K6( the carrier of (TopSpaceMetr n))

Int p is open Element of K6( the carrier of (TopSpaceMetr n))

p9 is V11() real ext-real set

Ball (A,p9) is Element of K6( the carrier of n)

K6( the carrier of n) is set

s is V11() real ext-real set

Ball (A,s) is Element of K6( the carrier of n)

p9 is V11() real ext-real set

Ball (A,p9) is Element of K6( the carrier of n)

Family_open_set n is Element of K6(K6( the carrier of n))

K6(K6( the carrier of n)) is set

TopStruct(# the carrier of n,(Family_open_set n) #) is non empty strict TopStruct

s is Element of K6( the carrier of (TopSpaceMetr n))

n is TopSpace-like TopStruct

the carrier of n is set

K6( the carrier of n) is set

the topology of n is non empty Element of K6(K6( the carrier of n))

K6(K6( the carrier of n)) is set

TopStruct(# the carrier of n, the topology of n #) is strict TopSpace-like TopStruct

the carrier of TopStruct(# the carrier of n, the topology of n #) is set

K6( the carrier of TopStruct(# the carrier of n, the topology of n #)) is set

A is Element of K6( the carrier of n)

Int A is open Element of K6( the carrier of n)

p is Element of K6( the carrier of TopStruct(# the carrier of n, the topology of n #))

Int p is open Element of K6( the carrier of TopStruct(# the carrier of n, the topology of n #))

p9 is Element of K6( the carrier of TopStruct(# the carrier of n, the topology of n #))

s is Element of K6( the carrier of n)

n is natural V11() real ext-real set

Euclid n is non empty strict Reflexive discerning V88() triangle Discerning MetrStruct

REAL n is non empty FinSequence-membered M11( REAL )

K247(n,REAL) is FinSequence-membered M11( REAL )

Pitag_dist n is V16() V19(K7((REAL n),(REAL n))) V20( REAL ) V21() V30(K7((REAL n),(REAL n)), REAL ) Element of K6(K7(K7((REAL n),(REAL n)),REAL))

K7((REAL n),(REAL n)) is set

K7(K7((REAL n),(REAL n)),REAL) is set

K6(K7(K7((REAL n),(REAL n)),REAL)) is set

MetrStruct(# (REAL n),(Pitag_dist n) #) is strict MetrStruct

the carrier of (Euclid n) is non empty set

TOP-REAL n is non empty TopSpace-like V111() V136() V137() V138() V139() V140() V141() V142() strict RLTopStruct

the carrier of (TOP-REAL n) is non empty set

K6( the carrier of (TOP-REAL n)) is set

A is Element of the carrier of (Euclid n)

p is Element of K6( the carrier of (TOP-REAL n))

Int p is open Element of K6( the carrier of (TOP-REAL n))

the topology of (TOP-REAL n) is non empty Element of K6(K6( the carrier of (TOP-REAL n)))

K6(K6( the carrier of (TOP-REAL n))) is set

TopStruct(# the carrier of (TOP-REAL n), the topology of (TOP-REAL n) #) is non empty strict TopSpace-like TopStruct

TopSpaceMetr (Euclid n) is non empty strict TopSpace-like TopStruct

the carrier of (TopSpaceMetr (Euclid n)) is non empty set

K6( the carrier of (TopSpaceMetr (Euclid n))) is set

p9 is Element of K6( the carrier of (TopSpaceMetr (Euclid n)))

Int p9 is open Element of K6( the carrier of (TopSpaceMetr (Euclid n)))

s is V11() real ext-real set

Ball (A,s) is Element of K6( the carrier of (Euclid n))

K6( the carrier of (Euclid n)) is set

s is V11() real ext-real set

Ball (A,s) is Element of K6( the carrier of (Euclid n))

K6( the carrier of (Euclid n)) is set

s1 is V11() real ext-real set

Ball (A,s1) is Element of K6( the carrier of (Euclid n))

n is V11() real ext-real Element of REAL

A is V11() real ext-real Element of REAL

|[n,A]| is V42(2) FinSequence-like V148() Element of the carrier of (TOP-REAL 2)

p is V11() real ext-real Element of REAL

n - p is V11() real ext-real Element of REAL

K38(p) is V11() real ext-real set

K36(n,K38(p)) is V11() real ext-real set

(n - p) ^2 is V11() real ext-real Element of REAL

K37((n - p),(n - p)) is V11() real ext-real set

p9 is V11() real ext-real Element of REAL

|[p,p9]| is V42(2) FinSequence-like V148() Element of the carrier of (TOP-REAL 2)

A - p9 is V11() real ext-real Element of REAL

K38(p9) is V11() real ext-real set

K36(A,K38(p9)) is V11() real ext-real set

(A - p9) ^2 is V11() real ext-real Element of REAL

K37((A - p9),(A - p9)) is V11() real ext-real set

((n - p) ^2) + ((A - p9) ^2) is V11() real ext-real Element of REAL

sqrt (((n - p) ^2) + ((A - p9) ^2)) is V11() real ext-real Element of REAL

s is Element of the carrier of (Euclid 2)

s1 is Element of the carrier of (Euclid 2)

dist (s,s1) is V11() real ext-real Element of REAL

|[n,A]| `1 is V11() real ext-real Element of REAL

|[n,A]| `2 is V11() real ext-real Element of REAL

|[p,p9]| `1 is V11() real ext-real Element of REAL

|[p,p9]| `2 is V11() real ext-real Element of REAL

(Pitag_dist 2) . (s,s1) is set

n is V11() real ext-real Element of REAL

A is V11() real ext-real Element of REAL

|[n,A]| is V42(2) FinSequence-like V148() Element of the carrier of (TOP-REAL 2)

p is V11() real ext-real Element of REAL

n + p is V11() real ext-real Element of REAL

|[(n + p),A]| is V42(2) FinSequence-like V148() Element of the carrier of (TOP-REAL 2)

p9 is V11() real ext-real Element of REAL

s is Element of the carrier of (Euclid 2)

Ball (s,p9) is Element of K6( the carrier of (Euclid 2))

K6( the carrier of (Euclid 2)) is set

s1 is Element of the carrier of (Euclid 2)

dist (s,s1) is V11() real ext-real Element of REAL

n - (n + p) is V11() real ext-real Element of REAL

K38((n + p)) is V11() real ext-real set

K36(n,K38((n + p))) is V11() real ext-real set

(n - (n + p)) ^2 is V11() real ext-real Element of REAL

K37((n - (n + p)),(n - (n + p))) is V11() real ext-real set

A - A is V11() real ext-real Element of REAL

K38(A) is V11() real ext-real set

K36(A,K38(A)) is V11() real ext-real set

(A - A) ^2 is V11() real ext-real Element of REAL

K37((A - A),(A - A)) is V11() real ext-real set

((n - (n + p)) ^2) + ((A - A) ^2) is V11() real ext-real Element of REAL

sqrt (((n - (n + p)) ^2) + ((A - A) ^2)) is V11() real ext-real Element of REAL

- (n - (n + p)) is V11() real ext-real Element of REAL

(- (n - (n + p))) ^2 is V11() real ext-real Element of REAL

K37((- (n - (n + p))),(- (n - (n + p)))) is V11() real ext-real set

sqrt ((- (n - (n + p))) ^2) is V11() real ext-real Element of REAL

n is V11() real ext-real Element of REAL

A is V11() real ext-real Element of REAL

|[n,A]| is V42(2) FinSequence-like V148() Element of the carrier of (TOP-REAL 2)

p is V11() real ext-real Element of REAL

A + p is V11() real ext-real Element of REAL

|[n,(A + p)]| is V42(2) FinSequence-like V148() Element of the carrier of (TOP-REAL 2)

p9 is V11() real ext-real Element of REAL

s is Element of the carrier of (Euclid 2)

Ball (s,p9) is Element of K6( the carrier of (Euclid 2))

K6( the carrier of (Euclid 2)) is set

s1 is Element of the carrier of (Euclid 2)

dist (s,s1) is V11() real ext-real Element of REAL

n - n is V11() real ext-real Element of REAL

K38(n) is V11() real ext-real set

K36(n,K38(n)) is V11() real ext-real set

(n - n) ^2 is V11() real ext-real Element of REAL

K37((n - n),(n - n)) is V11() real ext-real set

A - (A + p) is V11() real ext-real Element of REAL

K38((A + p)) is V11() real ext-real set

K36(A,K38((A + p))) is V11() real ext-real set

(A - (A + p)) ^2 is V11() real ext-real Element of REAL

K37((A - (A + p)),(A - (A + p))) is V11() real ext-real set

((n - n) ^2) + ((A - (A + p)) ^2) is V11() real ext-real Element of REAL

sqrt (((n - n) ^2) + ((A - (A + p)) ^2)) is V11() real ext-real Element of REAL

- (A - (A + p)) is V11() real ext-real Element of REAL

(- (A - (A + p))) ^2 is V11() real ext-real Element of REAL

K37((- (A - (A + p))),(- (A - (A + p)))) is V11() real ext-real set

sqrt ((- (A - (A + p))) ^2) is V11() real ext-real Element of REAL

n is V11() real ext-real Element of REAL

A is V11() real ext-real Element of REAL

|[n,A]| is V42(2) FinSequence-like V148() Element of the carrier of (TOP-REAL 2)

p is V11() real ext-real Element of REAL

n - p is V11() real ext-real Element of REAL

K38(p) is V11() real ext-real set

K36(n,K38(p)) is V11() real ext-real set

|[(n - p),A]| is V42(2) FinSequence-like V148() Element of the carrier of (TOP-REAL 2)

p9 is V11() real ext-real Element of REAL

s is Element of the carrier of (Euclid 2)

Ball (s,p9) is Element of K6( the carrier of (Euclid 2))

K6( the carrier of (Euclid 2)) is set

s1 is Element of the carrier of (Euclid 2)

dist (s,s1) is V11() real ext-real Element of REAL

n - (n - p) is V11() real ext-real Element of REAL

K38((n - p)) is V11() real ext-real set

K36(n,K38((n - p))) is V11() real ext-real set

(n - (n - p)) ^2 is V11() real ext-real Element of REAL

K37((n - (n - p)),(n - (n - p))) is V11() real ext-real set

A - A is V11() real ext-real Element of REAL

K38(A) is V11() real ext-real set

K36(A,K38(A)) is V11() real ext-real set

(A - A) ^2 is V11() real ext-real Element of REAL

K37((A - A),(A - A)) is V11() real ext-real set

((n - (n - p)) ^2) + ((A - A) ^2) is V11() real ext-real Element of REAL

sqrt (((n - (n - p)) ^2) + ((A - A) ^2)) is V11() real ext-real Element of REAL

n is V11() real ext-real Element of REAL

A is V11() real ext-real Element of REAL

|[n,A]| is V42(2) FinSequence-like V148() Element of the carrier of (TOP-REAL 2)

p is V11() real ext-real Element of REAL

A - p is V11() real ext-real Element of REAL

K38(p) is V11() real ext-real set

K36(A,K38(p)) is V11() real ext-real set

|[n,(A - p)]| is V42(2) FinSequence-like V148() Element of the carrier of (TOP-REAL 2)

p9 is V11() real ext-real Element of REAL

s is Element of the carrier of (Euclid 2)

Ball (s,p9) is Element of K6( the carrier of (Euclid 2))

K6( the carrier of (Euclid 2)) is set

s1 is Element of the carrier of (Euclid 2)

dist (s,s1) is V11() real ext-real Element of REAL

A - (A - p) is V11() real ext-real Element of REAL

K38((A - p)) is V11() real ext-real set

K36(A,K38((A - p))) is V11() real ext-real set

(A - (A - p)) ^2 is V11() real ext-real Element of REAL

K37((A - (A - p)),(A - (A - p))) is V11() real ext-real set

n - n is V11() real ext-real Element of REAL

K38(n) is V11() real ext-real set

K36(n,K38(n)) is V11() real ext-real set

(n - n) ^2 is V11() real ext-real Element of REAL

K37((n - n),(n - n)) is V11() real ext-real set

((A - (A - p)) ^2) + ((n - n) ^2) is V11() real ext-real Element of REAL

sqrt (((A - (A - p)) ^2) + ((n - n) ^2)) is V11() real ext-real Element of REAL

n is natural V11() real ext-real V33() V156() V157() V158() V159() V160() V161() V162() Element of NAT

n + 1 is natural V11() real ext-real V33() V156() V157() V158() V159() V160() V161() V162() Element of NAT

A is natural V11() real ext-real V33() V156() V157() V158() V159() V160() V161() V162() Element of NAT

A + 1 is natural V11() real ext-real V33() V156() V157() V158() V159() V160() V161() V162() Element of NAT

p is V16() V18() V19( NAT ) V20(K246( the carrier of (TOP-REAL 2))) V21() FinSequence-like V144() X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of K246( the carrier of (TOP-REAL 2))

len p is natural V11() real ext-real V33() V156() V157() V158() V159() V160() V161() V162() Element of NAT

width p is natural V11() real ext-real V33() V156() V157() V158() V159() V160() V161() V162() Element of NAT

p * (n,A) is V42(2) FinSequence-like V148() Element of the carrier of (TOP-REAL 2)

p * ((n + 1),(A + 1)) is V42(2) FinSequence-like V148() Element of the carrier of (TOP-REAL 2)

(p * (n,A)) + (p * ((n + 1),(A + 1))) is V42(2) FinSequence-like V148() Element of the carrier of (TOP-REAL 2)

p * (n,(A + 1)) is V42(2) FinSequence-like V148() Element of the carrier of (TOP-REAL 2)

p * ((n + 1),A) is V42(2) FinSequence-like V148() Element of the carrier of (TOP-REAL 2)

(p * (n,(A + 1))) + (p * ((n + 1),A)) is V42(2) FinSequence-like V148() Element of the carrier of (TOP-REAL 2)

(p * ((n + 1),(A + 1))) `1 is V11() real ext-real Element of REAL

p * ((n + 1),1) is V42(2) FinSequence-like V148() Element of the carrier of (TOP-REAL 2)

(p * ((n + 1),1)) `1 is V11() real ext-real Element of REAL

(p * ((n + 1),A)) `1 is V11() real ext-real Element of REAL

(p * ((n + 1),(A + 1))) `2 is V11() real ext-real Element of REAL

p * (1,(A + 1)) is V42(2) FinSequence-like V148() Element of the carrier of (TOP-REAL 2)

(p * (1,(A + 1))) `2 is V11() real ext-real Element of REAL

(p * (n,(A + 1))) `2 is V11() real ext-real Element of REAL

(p * (n,A)) `2 is V11() real ext-real Element of REAL

p * (1,A) is V42(2) FinSequence-like V148() Element of the carrier of (TOP-REAL 2)

(p * (1,A)) `2 is V11() real ext-real Element of REAL

(p * ((n + 1),A)) `2 is V11() real ext-real Element of REAL

((p * (n,A)) + (p * ((n + 1),(A + 1)))) `2 is V11() real ext-real Element of REAL

((p * (n,A)) `2) + ((p * ((n + 1),(A + 1))) `2) is V11() real ext-real Element of REAL

((p * (n,(A + 1))) + (p * ((n + 1),A))) `2 is V11() real ext-real Element of REAL

(p * (n,A)) `1 is V11() real ext-real Element of REAL

p * (n,1) is V42(2) FinSequence-like V148() Element of the carrier of (TOP-REAL 2)

(p * (n,1)) `1 is V11() real ext-real Element of REAL

(p * (n,(A + 1))) `1 is V11() real ext-real Element of REAL

((p * (n,A)) + (p * ((n + 1),(A + 1)))) `1 is V11() real ext-real Element of REAL

((p * (n,A)) `1) + ((p * ((n + 1),(A + 1))) `1) is V11() real ext-real Element of REAL

((p * (n,(A + 1))) + (p * ((n + 1),A))) `1 is V11() real ext-real Element of REAL

|[(((p * (n,(A + 1))) + (p * ((n + 1),A))) `1),(((p * (n,(A + 1))) + (p * ((n + 1),A))) `2)]| is V42(2) FinSequence-like V148() Element of the carrier of (TOP-REAL 2)

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

TopSpaceMetr (Euclid 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

n is V16() V18() V19( NAT ) V20(K246( the carrier of (TOP-REAL 2))) V21() FinSequence-like V144() X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of K246( the carrier of (TOP-REAL 2))

v_strip (n,0) is Element of K6( the carrier of (TOP-REAL 2))

Int (v_strip (n,0)) is open Element of K6( the carrier of (TOP-REAL 2))

n * (1,1) is V42(2) FinSequence-like V148() Element of the carrier of (TOP-REAL 2)

(n * (1,1)) `1 is V11() real ext-real Element of REAL

{ |[b

width n is natural V11() real ext-real V33() V156() V157() V158() V159() V160() V161() V162() Element of NAT

{ |[b

A is set

p is Element of the carrier of (Euclid 2)

p9 is V11() real ext-real set

Ball (p,p9) is Element of K6( the carrier of (Euclid 2))

s is V42(2) FinSequence-like V148() Element of the carrier of (TOP-REAL 2)

s `1 is V11() real ext-real Element of REAL

s `2 is V11() real ext-real Element of REAL

|[(s `1),(s `2)]| is V42(2) FinSequence-like V148() Element of the carrier of (TOP-REAL 2)

s1 is V11() real ext-real Element of REAL

s1 / 2 is V11() real ext-real Element of REAL

K39(2) is non empty V11() real ext-real positive non negative set

K37(s1,K39(2)) is V11() real ext-real set

(s `1) + (s1 / 2) is V11() real ext-real Element of REAL

(s `2) + 0 is V11() real ext-real Element of REAL

|[((s `1) + (s1 / 2)),((s `2) + 0)]| is V42(2) FinSequence-like V148() Element of the carrier of (TOP-REAL 2)

Ball (p,s1) is Element of K6( the carrier of (Euclid 2))

r9 is V11() real ext-real Element of REAL

r is V11() real ext-real Element of REAL

|[r9,r]| is V42(2) FinSequence-like V148() Element of the carrier of (TOP-REAL 2)

A is set

p is V11() real ext-real Element of REAL

p9 is V11() real ext-real Element of REAL

|[p,p9]| is V42(2) FinSequence-like V148() Element of the carrier of (TOP-REAL 2)

s is Element of the carrier of (Euclid 2)

((n * (1,1)) `1) - p is V11() real ext-real Element of REAL

K38(p) is V11() real ext-real set

K36(((n * (1,1)) `1),K38(p)) is V11() real ext-real set

Ball (s,(((n * (1,1)) `1) - p)) is Element of K6( the carrier of (Euclid 2))

s1 is set

{ b

G is Element of the carrier of (Euclid 2)

dist (s,G) is V11() real ext-real Element of REAL

r9 is V42(2) FinSequence-like V148() Element of the carrier of (TOP-REAL 2)

r9 `1 is V11() real ext-real Element of REAL

p - (r9 `1) is V11() real ext-real Element of REAL

K38((r9 `1)) is V11() real ext-real set

K36(p,K38((r9 `1))) is V11() real ext-real set

(p - (r9 `1)) ^2 is V11() real ext-real Element of REAL

K37((p - (r9 `1)),(p - (r9 `1))) is V11() real ext-real set

((p - (r9 `1)) ^2) + 0 is V11() real ext-real Element of REAL

r9 `2 is V11() real ext-real Element of REAL

p9 - (r9 `2) is V11() real ext-real Element of REAL

K38((r9 `2)) is V11() real ext-real set

K36(p9,K38((r9 `2))) is V11() real ext-real set

(p9 - (r9 `2)) ^2 is V11() real ext-real Element of REAL

K37((p9 - (r9 `2)),(p9 - (r9 `2))) is V11() real ext-real set

((p - (r9 `1)) ^2) + ((p9 - (r9 `2)) ^2) is V11() real ext-real Element of REAL

sqrt ((p - (r9 `1)) ^2) is V11() real ext-real Element of REAL

sqrt (((p - (r9 `1)) ^2) + ((p9 - (r9 `2)) ^2)) is V11() real ext-real Element of REAL

|[(r9 `1),(r9 `2)]| is V42(2) FinSequence-like V148() Element of the carrier of (TOP-REAL 2)

abs (p - (r9 `1)) is V11() real ext-real Element of REAL

(r9 `1) - p is V11() real ext-real Element of REAL

K36((r9 `1),K38(p)) is V11() real ext-real set

- (p - (r9 `1)) is V11() real ext-real Element of REAL

abs (- (p - (r9 `1))) is V11() real ext-real Element of REAL

s1 is Element of K6( the carrier of (TOP-REAL 2))

n is V16() V18() V19( NAT ) V20(K246( the carrier of (TOP-REAL 2))) V21() FinSequence-like V144() X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of K246( the carrier of (TOP-REAL 2))

len n is natural V11() real ext-real V33() V156() V157() V158() V159() V160() V161() V162() Element of NAT

v_strip (n,(len n)) is Element of K6( the carrier of (TOP-REAL 2))

Int (v_strip (n,(len n))) is open Element of K6( the carrier of (TOP-REAL 2))

n * ((len n),1) is V42(2) FinSequence-like V148() Element of the carrier of (TOP-REAL 2)

(n * ((len n),1)) `1 is V11() real ext-real Element of REAL

{ |[b

width n is natural V11() real ext-real V33() V156() V157() V158() V159() V160() V161() V162() Element of NAT

{ |[b

A is set

p is Element of the carrier of (Euclid 2)

p9 is V11() real ext-real set

Ball (p,p9) is Element of K6( the carrier of (Euclid 2))

s is V42(2) FinSequence-like V148() Element of the carrier of (TOP-REAL 2)

s `1 is V11() real ext-real Element of REAL

s `2 is V11() real ext-real Element of REAL

|[(s `1),(s `2)]| is V42(2) FinSequence-like V148() Element of the carrier of (TOP-REAL 2)

s1 is V11() real ext-real Element of REAL

s1 / 2 is V11() real ext-real Element of REAL

K39(2) is non empty V11() real ext-real positive non negative set

K37(s1,K39(2)) is V11() real ext-real set

(s `1) - (s1 / 2) is V11() real ext-real Element of REAL

K38((s1 / 2)) is V11() real ext-real set

K36((s `1),K38((s1 / 2))) is V11() real ext-real set

(s `2) + 0 is V11() real ext-real Element of REAL

|[((s `1) - (s1 / 2)),((s `2) + 0)]| is V42(2) FinSequence-like V148() Element of the carrier of (TOP-REAL 2)

Ball (p,s1) is Element of K6( the carrier of (Euclid 2))

r9 is V11() real ext-real Element of REAL

r is V11() real ext-real Element of REAL

|[r9,r]| is V42(2) FinSequence-like V148() Element of the carrier of (TOP-REAL 2)

((n * ((len n),1)) `1) + (s1 / 2) is V11() real ext-real Element of REAL

A is set

p is V11() real ext-real Element of REAL

p9 is V11() real ext-real Element of REAL

|[p,p9]| is V42(2) FinSequence-like V148() Element of the carrier of (TOP-REAL 2)

s is Element of the carrier of (Euclid 2)

p - ((n * ((len n),1)) `1) is V11() real ext-real Element of REAL

K38(((n * ((len n),1)) `1)) is V11() real ext-real set

K36(p,K38(((n * ((len n),1)) `1))) is V11() real ext-real set

Ball (s,(p - ((n * ((len n),1)) `1))) is Element of K6( the carrier of (Euclid 2))

s1 is set

{ b

G is Element of the carrier of (Euclid 2)

dist (s,G) is V11() real ext-real Element of REAL

r9 is V42(2) FinSequence-like V148() Element of the carrier of (TOP-REAL 2)

r9 `1 is V11() real ext-real Element of REAL

p - (r9 `1) is V11() real ext-real Element of REAL

K38((r9 `1)) is V11() real ext-real set

K36(p,K38((r9 `1))) is V11() real ext-real set

(p - (r9 `1)) ^2 is V11() real ext-real Element of REAL

K37((p - (r9 `1)),(p - (r9 `1))) is V11() real ext-real set

((p - (r9 `1)) ^2) + 0 is V11() real ext-real Element of REAL

r9 `2 is V11() real ext-real Element of REAL

p9 - (r9 `2) is V11() real ext-real Element of REAL

K38((r9 `2)) is V11() real ext-real set

K36(p9,K38((r9 `2))) is V11() real ext-real set

(p9 - (r9 `2)) ^2 is V11() real ext-real Element of REAL

K37((p9 - (r9 `2)),(p9 - (r9 `2))) is V11() real ext-real set

((p - (r9 `1)) ^2) + ((p9 - (r9 `2)) ^2) is V11() real ext-real Element of REAL

sqrt ((p - (r9 `1)) ^2) is V11() real ext-real Element of REAL

sqrt (((p - (r9 `1)) ^2) + ((p9 - (r9 `2)) ^2)) is V11() real ext-real Element of REAL

|[(r9 `1),(r9 `2)]| is V42(2) FinSequence-like V148() Element of the carrier of (TOP-REAL 2)

abs (p - (r9 `1)) is V11() real ext-real Element of REAL

s1 is Element of K6( the carrier of (TOP-REAL 2))

n is natural V11() real ext-real V33() V156() V157() V158() V159() V160() V161() V162() Element of NAT

n + 1 is natural V11() real ext-real V33() V156() V157() V158() V159() V160() V161() V162() Element of NAT

A is V16() V18() V19( NAT ) V20(K246( the carrier of (TOP-REAL 2))) V21() FinSequence-like V144() X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of K246( the carrier of (TOP-REAL 2))

len A is natural V11() real ext-real V33() V156() V157() V158() V159() V160() V161() V162() Element of NAT

v_strip (A,n) is Element of K6( the carrier of (TOP-REAL 2))

Int (v_strip (A,n)) is open Element of K6( the carrier of (TOP-REAL 2))

A * (n,1) is V42(2) FinSequence-like V148() Element of the carrier of (TOP-REAL 2)

(A * (n,1)) `1 is V11() real ext-real Element of REAL

A * ((n + 1),1) is V42(2) FinSequence-like V148() Element of the carrier of (TOP-REAL 2)

(A * ((n + 1),1)) `1 is V11() real ext-real Element of REAL

{ |[b

width A is natural V11() real ext-real V33() V156() V157() V158() V159() V160() V161() V162() Element of NAT

{ |[b

p is set

p9 is Element of the carrier of (Euclid 2)

s is V11() real ext-real set

Ball (p9,s) is Element of K6( the carrier of (Euclid 2))

s1 is V42(2) FinSequence-like V148() Element of the carrier of (TOP-REAL 2)

s1 `1 is V11() real ext-real Element of REAL

s1 `2 is V11() real ext-real Element of REAL

|[(s1 `1),(s1 `2)]| is V42(2) FinSequence-like V148() Element of the carrier of (TOP-REAL 2)

G is V11() real ext-real Element of REAL

G / 2 is V11() real ext-real Element of REAL

K39(2) is non empty V11() real ext-real positive non negative set

K37(G,K39(2)) is V11() real ext-real set

(s1 `1) - (G / 2) is V11() real ext-real Element of REAL

K38((G / 2)) is V11() real ext-real set

K36((s1 `1),K38((G / 2))) is V11() real ext-real set

(s1 `2) + 0 is V11() real ext-real Element of REAL

|[((s1 `1) - (G / 2)),((s1 `2) + 0)]| is V42(2) FinSequence-like V148() Element of the carrier of (TOP-REAL 2)

Ball (p9,G) is Element of K6( the carrier of (Euclid 2))

r is V11() real ext-real Element of REAL

rr is V11() real ext-real Element of REAL

|[r,rr]| is V42(2) FinSequence-like V148() Element of the carrier of (TOP-REAL 2)

((A * (n,1)) `1) + (G / 2) is V11() real ext-real Element of REAL

(s1 `1) + (G / 2) is V11() real ext-real Element of REAL

|[((s1 `1) + (G / 2)),((s1 `2) + 0)]| is V42(2) FinSequence-like V148() Element of the carrier of (TOP-REAL 2)

rr is V11() real ext-real Element of REAL

rr9 is V11() real ext-real Element of REAL

|[rr,rr9]| is V42(2) FinSequence-like V148() Element of the carrier of (TOP-REAL 2)

p is set

p9 is V11() real ext-real Element of REAL

s is V11() real ext-real Element of REAL

|[p9,s]| is V42(2) FinSequence-like V148() Element of the carrier of (TOP-REAL 2)

((A * ((n + 1),1)) `1) - p9 is V11() real ext-real Element of REAL

K38(p9) is V11() real ext-real set

K36(((A * ((n + 1),1)) `1),K38(p9)) is V11() real ext-real set

p9 - ((A * (n,1)) `1) is V11() real ext-real Element of REAL

K38(((A * (n,1)) `1)) is V11() real ext-real set

K36(p9,K38(((A * (n,1)) `1))) is V11() real ext-real set

min ((p9 - ((A * (n,1)) `1)),(((A * ((n + 1),1)) `1) - p9)) is V11() real ext-real Element of REAL

s1 is Element of the carrier of (Euclid 2)

Ball (s1,(min ((p9 - ((A * (n,1)) `1)),(((A * ((n + 1),1)) `1) - p9)))) is Element of K6( the carrier of (Euclid 2))

G is set

{ b

r9 is Element of the carrier of (Euclid 2)

dist (s1,r9) is V11() real ext-real Element of REAL

r is V42(2) FinSequence-like V148() Element of the carrier of (TOP-REAL 2)

r `1 is V11() real ext-real Element of REAL

p9 - (r `1) is V11() real ext-real Element of REAL

K38((r `1)) is V11() real ext-real set

K36(p9,K38((r `1))) is V11() real ext-real set

(p9 - (r `1)) ^2 is V11() real ext-real Element of REAL

K37((p9 - (r `1)),(p9 - (r `1))) is V11() real ext-real set

((p9 - (r `1)) ^2) + 0 is V11() real ext-real Element of REAL

r `2 is V11() real ext-real Element of REAL

s - (r `2) is V11() real ext-real Element of REAL

K38((r `2)) is V11() real ext-real set

K36(s,K38((r `2))) is V11() real ext-real set

(s - (r `2)) ^2 is V11() real ext-real Element of REAL

K37((s - (r `2)),(s - (r `2))) is V11() real ext-real set

((p9 - (r `1)) ^2) + ((s - (r `2)) ^2) is V11() real ext-real Element of REAL

sqrt ((p9 - (r `1)) ^2) is V11() real ext-real Element of REAL

sqrt (((p9 - (r `1)) ^2) + ((s - (r `2)) ^2)) is V11() real ext-real Element of REAL

|[(r `1),(r `2)]| is V42(2) FinSequence-like V148() Element of the carrier of (TOP-REAL 2)

abs (p9 - (r `1)) is V11() real ext-real Element of REAL

(r `1) - p9 is V11() real ext-real Element of REAL

K36((r `1),K38(p9)) is V11() real ext-real set

- (p9 - (r `1)) is V11() real ext-real Element of REAL

abs (- (p9 - (r `1))) is V11() real ext-real Element of REAL

G is Element of K6( the carrier of (TOP-REAL 2))

n is V16() V18() V19( NAT ) V20(K246( the carrier of (TOP-REAL 2))) V21() FinSequence-like V144() X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of K246( the carrier of (TOP-REAL 2))

h_strip (n,0) is Element of K6( the carrier of (TOP-REAL 2))

Int (h_strip (n,0)) is open Element of K6( the carrier of (TOP-REAL 2))

n * (1,1) is V42(2) FinSequence-like V148() Element of the carrier of (TOP-REAL 2)

(n * (1,1)) `2 is V11() real ext-real Element of REAL

{ |[b

len n is natural V11() real ext-real V33() V156() V157() V158() V159() V160() V161() V162() Element of NAT

{ |[b

A is set

p is Element of the carrier of (Euclid 2)

p9 is V11() real ext-real set

Ball (p,p9) is Element of K6( the carrier of (Euclid 2))

s is V42(2) FinSequence-like V148() Element of the carrier of (TOP-REAL 2)

s `1 is V11() real ext-real Element of REAL

s `2 is V11() real ext-real Element of REAL

|[(s `1),(s `2)]| is V42(2) FinSequence-like V148() Element of the carrier of (TOP-REAL 2)

(s `1) + 0 is V11() real ext-real Element of REAL

s1 is V11() real ext-real Element of REAL

s1 / 2 is V11() real ext-real Element of REAL

K39(2) is non empty V11() real ext-real positive non negative set

K37(s1,K39(2)) is V11() real ext-real set

(s `2) + (s1 / 2) is V11() real ext-real Element of REAL

|[((s `1) + 0),((s `2) + (s1 / 2))]| is V42(2) FinSequence-like V148() Element of the carrier of (TOP-REAL 2)

Ball (p,s1) is Element of K6( the carrier of (Euclid 2))

r9 is V11() real ext-real Element of REAL

r is V11() real ext-real Element of REAL

|[r9,r]| is V42(2) FinSequence-like V148() Element of the carrier of (TOP-REAL 2)

A is set

p is V11() real ext-real Element of REAL

p9 is V11() real ext-real Element of REAL

|[p,p9]| is V42(2) FinSequence-like V148() Element of the carrier of (TOP-REAL 2)

s is Element of the carrier of (Euclid 2)

((n * (1,1)) `2) - p9 is V11() real ext-real Element of REAL

K38(p9) is V11() real ext-real set

K36(((n * (1,1)) `2),K38(p9)) is V11() real ext-real set

Ball (s,(((n * (1,1)) `2) - p9)) is Element of K6( the carrier of (Euclid 2))

s1 is set

{ b

G is Element of the carrier of (Euclid 2)

dist (s,G) is V11() real ext-real Element of REAL

r9 is V42(2) FinSequence-like V148() Element of the carrier of (TOP-REAL 2)

r9 `2 is V11() real ext-real Element of REAL

p9 - (r9 `2) is V11() real ext-real Element of REAL

K38((r9 `2)) is V11() real ext-real set

K36(p9,K38((r9 `2))) is V11() real ext-real set

(p9 - (r9 `2)) ^2 is V11() real ext-real Element of REAL

K37((p9 - (r9 `2)),(p9 - (r9 `2))) is V11() real ext-real set

((p9 - (r9 `2)) ^2) + 0 is V11() real ext-real Element of REAL

r9 `1 is V11() real ext-real Element of REAL

p - (r9 `1) is V11() real ext-real Element of REAL

K38((r9 `1)) is V11() real ext-real set

K36(p,K38((r9 `1))) is V11() real ext-real set

(p - (r9 `1)) ^2 is V11() real ext-real Element of REAL

K37((p - (r9 `1)),(p - (r9 `1))) is V11() real ext-real set

((p - (r9 `1)) ^2) + ((p9 - (r9 `2)) ^2) is V11() real ext-real Element of REAL

sqrt ((p9 - (r9 `2)) ^2) is V11() real ext-real Element of REAL

sqrt (((p - (r9 `1)) ^2) + ((p9 - (r9 `2)) ^2)) is V11() real ext-real Element of REAL

|[(r9 `1),(r9 `2)]| is V42(2) FinSequence-like V148() Element of the carrier of (TOP-REAL 2)

abs (p9 - (r9 `2)) is V11() real ext-real Element of REAL

(r9 `2) - p9 is V11() real ext-real Element of REAL

K36((r9 `2),K38(p9)) is V11() real ext-real set

- (p9 - (r9 `2)) is V11() real ext-real Element of REAL

abs (- (p9 - (r9 `2))) is V11() real ext-real Element of REAL

s1 is Element of K6( the carrier of (TOP-REAL 2))

n is V16() V18() V19( NAT ) V20(K246( the carrier of (TOP-REAL 2))) V21() FinSequence-like V144() X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of K246( the carrier of (TOP-REAL 2))

width n is natural V11() real ext-real V33() V156() V157() V158() V159() V160() V161() V162() Element of NAT

h_strip (n,(width n)) is Element of K6( the carrier of (TOP-REAL 2))

Int (h_strip (n,(width n))) is open Element of K6( the carrier of (TOP-REAL 2))

n * (1,(width n)) is V42(2) FinSequence-like V148() Element of the carrier of (TOP-REAL 2)

(n * (1,(width n))) `2 is V11() real ext-real Element of REAL

{ |[b

len n is natural V11() real ext-real V33() V156() V157() V158() V159() V160() V161() V162() Element of NAT

{ |[b

A is set

p is Element of the carrier of (Euclid 2)

p9 is V11() real ext-real set

Ball (p,p9) is Element of K6( the carrier of (Euclid 2))

s is V42(2) FinSequence-like V148() Element of the carrier of (TOP-REAL 2)

s `1 is V11() real ext-real Element of REAL

s `2 is V11() real ext-real Element of REAL

|[(s `1),(s `2)]| is V42(2) FinSequence-like V148() Element of the carrier of (TOP-REAL 2)

(s `1) + 0 is V11() real ext-real Element of REAL

s1 is V11() real ext-real Element of REAL

s1 / 2 is V11() real ext-real Element of REAL

K39(2) is non empty V11() real ext-real positive non negative set

K37(s1,K39(2)) is V11() real ext-real set

(s `2) - (s1 / 2) is V11() real ext-real Element of REAL

K38((s1 / 2)) is V11() real ext-real set

K36((s `2),K38((s1 / 2))) is V11() real ext-real set

|[((s `1) + 0),((s `2) - (s1 / 2))]| is V42(2) FinSequence-like V148() Element of the carrier of (TOP-REAL 2)

Ball (p,s1) is Element of K6( the carrier of (Euclid 2))

r9 is V11() real ext-real Element of REAL

r is V11() real ext-real Element of REAL

|[r9,r]| is V42(2) FinSequence-like V148() Element of the carrier of (TOP-REAL 2)

((n * (1,(width n))) `2) + (s1 / 2) is V11() real ext-real Element of REAL

A is set

p is V11() real ext-real Element of REAL

p9 is V11() real ext-real Element of REAL

|[p,p9]| is V42(2) FinSequence-like V148() Element of the carrier of (TOP-REAL 2)

s is Element of the carrier of (Euclid 2)

p9 - ((n * (1,(width n))) `2) is V11() real ext-real Element of REAL

K38(((n * (1,(width n))) `2)) is V11() real ext-real set

K36(p9,K38(((n * (1,(width n))) `2))) is V11() real ext-real set

Ball (s,(p9 - ((n * (1,(width n))) `2))) is Element of K6( the carrier of (Euclid 2))

s1 is set

{ b

G is Element of the carrier of (Euclid 2)

dist (s,G) is V11() real ext-real Element of REAL

r9 is V42(2) FinSequence-like V148() Element of the carrier of (TOP-REAL 2)

r9 `2 is V11() real ext-real Element of REAL

p9 - (r9 `2) is V11() real ext-real Element of REAL

K38((r9 `2)) is V11() real ext-real set

K36(p9,K38((r9 `2))) is V11() real ext-real set

(p9 - (r9 `2)) ^2 is V11() real ext-real Element of REAL

K37((p9 - (r9 `2)),(p9 - (r9 `2))) is V11() real ext-real set

((p9 - (r9 `2)) ^2) + 0 is V11() real ext-real Element of REAL

r9 `1 is V11() real ext-real Element of REAL

p - (r9 `1) is V11() real ext-real Element of REAL

K38((r9 `1)) is V11() real ext-real set

K36(p,K38((r9 `1))) is V11() real ext-real set

(p - (r9 `1)) ^2 is V11() real ext-real Element of REAL

K37((p - (r9 `1)),(p - (r9 `1))) is V11() real ext-real set

((p - (r9 `1)) ^2) + ((p9 - (r9 `2)) ^2) is V11() real ext-real Element of REAL

sqrt ((p9 - (r9 `2)) ^2) is V11() real ext-real Element of REAL

sqrt (((p - (r9 `1)) ^2) + ((p9 - (r9 `2)) ^2)) is V11() real ext-real Element of REAL

|[(r9 `1),(r9 `2)]| is V42(2) FinSequence-like V148() Element of the carrier of (TOP-REAL 2)

abs (p9 - (r9 `2)) is V11() real ext-real Element of REAL

s1 is Element of K6( the carrier of (TOP-REAL 2))

n is natural V11() real ext-real V33() V156() V157() V158() V159() V160() V161() V162() Element of NAT

n + 1 is natural V11() real ext-real V33() V156() V157() V158() V159() V160() V161() V162() Element of NAT

A is V16() V18() V19( NAT ) V20(K246( the carrier of (TOP-REAL 2))) V21() FinSequence-like V144() X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of K246( the carrier of (TOP-REAL 2))

width A is natural V11() real ext-real V33() V156() V157() V158() V159() V160() V161() V162() Element of NAT

h_strip (A,n) is Element of K6( the carrier of (TOP-REAL 2))

Int (h_strip (A,n)) is open Element of K6( the carrier of (TOP-REAL 2))

A * (1,n) is V42(2) FinSequence-like V148() Element of the carrier of (TOP-REAL 2)

(A * (1,n)) `2 is V11() real ext-real Element of REAL

A * (1,(n + 1)) is V42(2) FinSequence-like V148() Element of the carrier of (TOP-REAL 2)

(A * (1,(n + 1))) `2 is V11() real ext-real Element of REAL

{ |[b

len A is natural V11() real ext-real V33() V156() V157() V158() V159() V160() V161() V162() Element of NAT

{ |[b

p is set

p9 is Element of the carrier of (Euclid 2)

s is V11() real ext-real set

Ball (p9,s) is Element of K6( the carrier of (Euclid 2))

s1 is V42(2) FinSequence-like V148() Element of the carrier of (TOP-REAL 2)

s1 `1 is V11() real ext-real Element of REAL

s1 `2 is V11() real ext-real Element of REAL

|[(s1 `1),(s1 `2)]| is V42(2) FinSequence-like V148() Element of the carrier of (TOP-REAL 2)

(s1 `1) + 0 is V11() real ext-real Element of REAL

G is V11() real ext-real Element of REAL

G / 2 is V11() real ext-real Element of REAL

K39(2) is non empty V11() real ext-real positive non negative set

K37(G,K39(2)) is V11() real ext-real set

(s1 `2) - (G / 2) is V11() real ext-real Element of REAL

K38((G / 2)) is V11() real ext-real set

K36((s1 `2),K38((G / 2))) is V11() real ext-real set

|[((s1 `1) + 0),((s1 `2) - (G / 2))]| is V42(2) FinSequence-like V148() Element of the carrier of (TOP-REAL 2)

Ball (p9,G) is Element of K6( the carrier of (Euclid 2))

r is V11() real ext-real Element of REAL

rr is V11() real ext-real Element of REAL

|[r,rr]| is V42(2) FinSequence-like V148() Element of the carrier of (TOP-REAL 2)

((A * (1,n)) `2) + (G / 2) is V11() real ext-real Element of REAL

(s1 `2) + (G / 2) is V11() real ext-real Element of REAL

|[((s1 `1) + 0),((s1 `2) + (G / 2))]| is V42(2) FinSequence-like V148() Element of the carrier of (TOP-REAL 2)

rr is V11() real ext-real Element of REAL

rr9 is V11() real ext-real Element of REAL

|[rr,rr9]| is V42(2) FinSequence-like V148() Element of the carrier of (TOP-REAL 2)

p is set

p9 is V11() real ext-real Element of REAL

s is V11() real ext-real Element of REAL

|[p9,s]| is V42(2) FinSequence-like V148() Element of the carrier of (TOP-REAL 2)

((A * (1,(n + 1))) `2) - s is V11() real ext-real Element of REAL

K38(s) is V11() real ext-real set

K36(((A * (1,(n + 1))) `2),K38(s)) is V11() real ext-real set

s - ((A * (1,n)) `2) is V11() real ext-real Element of REAL

K38(((A * (1,n)) `2)) is V11() real ext-real set

K36(s,K38(((A * (1,n)) `2))) is V11() real ext-real set

min ((s - ((A * (1,n)) `2)),(((A * (1,(n + 1))) `2) - s)) is V11() real ext-real Element of REAL

s1 is Element of the carrier of (Euclid 2)

Ball (s1,(min ((s - ((A * (1,n)) `2)),(((A * (1,(n + 1))) `2) - s)))) is Element of K6( the carrier of (Euclid 2))

G is set

{ b

r9 is Element of the carrier of (Euclid 2)

dist (s1,r9) is V11() real ext-real Element of REAL

r is V42(2) FinSequence-like V148() Element of the carrier of (TOP-REAL 2)

r `2 is V11() real ext-real Element of REAL

s - (r `2) is V11() real ext-real Element of REAL

K38((r `2)) is V11() real ext-real set

K36(s,K38((r `2))) is V11() real ext-real set

(s - (r `2)) ^2 is V11() real ext-real Element of REAL

K37((s - (r `2)),(s - (r `2))) is V11() real ext-real set

((s - (r `2)) ^2) + 0 is V11() real ext-real Element of REAL

r `1 is V11() real ext-real Element of REAL

p9 - (r `1) is V11() real ext-real Element of REAL

K38((r `1)) is V11() real ext-real set

K36(p9,K38((r `1))) is V11() real ext-real set

(p9 - (r `1)) ^2 is V11() real ext-real Element of REAL

K37((p9 - (r `1)),(p9 - (r `1))) is V11() real ext-real set

((p9 - (r `1)) ^2) + ((s - (r `2)) ^2) is V11() real ext-real Element of REAL

sqrt ((s - (r `2)) ^2) is V11() real ext-real Element of REAL

sqrt (((p9 - (r `1)) ^2) + ((s - (r `2)) ^2)) is V11() real ext-real Element of REAL

|[(r `1),(r `2)]| is V42(2) FinSequence-like V148() Element of the carrier of (TOP-REAL 2)

abs (s - (r `2)) is V11() real ext-real Element of REAL

(r `2) - s is V11() real ext-real Element of REAL

K36((r `2),K38(s)) is V11() real ext-real set

- (s - (r `2)) is V11() real ext-real Element of REAL

abs (- (s - (r `2))) is V11() real ext-real Element of REAL

G is Element of K6( the carrier of (TOP-REAL 2))

n is V16() V18() V19( NAT ) V20(K246( the carrier of (TOP-REAL 2))) V21() FinSequence-like V144() X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of K246( the carrier of (TOP-REAL 2))

cell (n,0,0) is Element of K6( the carrier of (TOP-REAL 2))

Int (cell (n,0,0)) is open Element of K6( the carrier of (TOP-REAL 2))

n * (1,1) is V42(2) FinSequence-like V148() Element of the carrier of (TOP-REAL 2)

(n * (1,1)) `1 is V11() real ext-real Element of REAL

(n * (1,1)) `2 is V11() real ext-real Element of REAL

{ |[b

v_strip (n,0) is Element of K6( the carrier of (TOP-REAL 2))

h_strip (n,0) is Element of K6( the carrier of (TOP-REAL 2))

(v_strip (n,0)) /\ (h_strip (n,0)) is Element of K6( the carrier of (TOP-REAL 2))

Int (v_strip (n,0)) is open Element of K6( the carrier of (TOP-REAL 2))

Int (h_strip (n,0)) is open Element of K6( the carrier of (TOP-REAL 2))

(Int (v_strip (n,0))) /\ (Int (h_strip (n,0))) is open Element of K6( the carrier of (TOP-REAL 2))

{ |[b

{ |[b

A is set

p is V11() real ext-real Element of REAL

p9 is V11() real ext-real Element of REAL

|[p,p9]| is V42(2) FinSequence-like V148() Element of the carrier of (TOP-REAL 2)

s is V11() real ext-real Element of REAL

s1 is V11() real ext-real Element of REAL

|[s,s1]| is V42(2) FinSequence-like V148() Element of the carrier of (TOP-REAL 2)

A is set

p is V11() real ext-real Element of REAL

p9 is V11() real ext-real Element of REAL

|[p,p9]| is V42(2) FinSequence-like V148() Element of the carrier of (TOP-REAL 2)

p is V11() real ext-real Element of REAL

p9 is V11() real ext-real Element of REAL

|[p,p9]| is V42(2) FinSequence-like V148() Element of the carrier of (TOP-REAL 2)

n is V16() V18() V19( NAT ) V20(K246( the carrier of (TOP-REAL 2))) V21() FinSequence-like V144() X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of K246( the carrier of (TOP-REAL 2))

width n is natural V11() real ext-real V33() V156() V157() V158() V159() V160() V161() V162() Element of NAT

cell (n,0,(width n)) is Element of K6( the carrier of (TOP-REAL 2))

Int (cell (n,0,(width n))) is open Element of K6( the carrier of (TOP-REAL 2))

n * (1,1) is V42(2) FinSequence-like V148() Element of the carrier of (TOP-REAL 2)

(n * (1,1)) `1 is V11() real ext-real Element of REAL

n * (1,(width n)) is V42(2) FinSequence-like V148() Element of the carrier of (TOP-REAL 2)

(n * (1,(width n))) `2 is V11() real ext-real Element of REAL

{ |[b

v_strip (n,0) is Element of K6( the carrier of (TOP-REAL 2))

h_strip (n,(width n)) is Element of K6( the carrier of (TOP-REAL 2))

(v_strip (n,0)) /\ (h_strip (n,(width n))) is Element of K6( the carrier of (TOP-REAL 2))

Int (v_strip (n,0)) is open Element of K6( the carrier of (TOP-REAL 2))

Int (h_strip (n,(width n))) is open Element of K6( the carrier of (TOP-REAL 2))

(Int (v_strip (n,0))) /\ (Int (h_strip (n,(width n)))) is open Element of K6( the carrier of (TOP-REAL 2))

{ |[b

{ |[b

A is set

p is V11() real ext-real Element of REAL

p9 is V11() real ext-real Element of REAL

|[p,p9]| is V42(2) FinSequence-like V148() Element of the carrier of (TOP-REAL 2)

s is V11() real ext-real Element of REAL

s1 is V11() real ext-real Element of REAL

|[s,s1]| is V42(2) FinSequence-like V148() Element of the carrier of (TOP-REAL 2)

A is set

p is V11() real ext-real Element of REAL

p9 is V11() real ext-real Element of REAL

|[p,p9]| is V42(2) FinSequence-like V148() Element of the carrier of (TOP-REAL 2)

p is V11() real ext-real Element of REAL

p9 is V11() real ext-real Element of REAL

|[p,p9]| is V42(2) FinSequence-like V148() Element of the carrier of (TOP-REAL 2)

n is natural V11() real ext-real V33() V156() V157() V158() V159() V160() V161() V162() Element of NAT

n + 1 is natural V11() real ext-real V33() V156() V157() V158() V159() V160() V161() V162() Element of NAT

A is V16() V18() V19( NAT ) V20(K246( the carrier of (TOP-REAL 2))) V21() FinSequence-like V144() X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of K246( the carrier of (TOP-REAL 2))

width A is natural V11() real ext-real V33() V156() V157() V158() V159() V160() V161() V162() Element of NAT

cell (A,0,n) is Element of K6( the carrier of (TOP-REAL 2))

Int (cell (A,0,n)) is open Element of K6( the carrier of (TOP-REAL 2))

A * (1,1) is V42(2) FinSequence-like V148() Element of the carrier of (TOP-REAL 2)

(A * (1,1)) `1 is V11() real ext-real Element of REAL

A * (1,n) is V42(2) FinSequence-like V148() Element of the carrier of (TOP-REAL 2)

(A * (1,n)) `2 is V11() real ext-real Element of REAL

A * (1,(n + 1)) is V42(2) FinSequence-like V148() Element of the carrier of (TOP-REAL 2)

(A * (1,(n + 1))) `2 is V11() real ext-real Element of REAL

{ |[b

v_strip (A,0) is Element of K6( the carrier of (TOP-REAL 2))

h_strip (A,n) is Element of K6( the carrier of (TOP-REAL 2))

(v_strip (A,0)) /\ (h_strip (A,n)) is Element of K6( the carrier of (TOP-REAL 2))

Int (v_strip (A,0)) is open Element of K6( the carrier of (TOP-REAL 2))

Int (h_strip (A,n)) is open Element of K6( the carrier of (TOP-REAL 2))

(Int (v_strip (A,0))) /\ (Int (h_strip (A,n))) is open Element of K6( the carrier of (TOP-REAL 2))

{ |[b

{ |[b

p is set

p9 is V11() real ext-real Element of REAL

s is V11() real ext-real Element of REAL

|[p9,s]| is V42(2) FinSequence-like V148() Element of the carrier of (TOP-REAL 2)

s1 is V11() real ext-real Element of REAL

G is V11() real ext-real Element of REAL

|[s1,G]| is V42(2) FinSequence-like V148() Element of the carrier of (TOP-REAL 2)

p is set

p9 is V11() real ext-real Element of REAL

s is V11() real ext-real Element of REAL

|[p9,s]| is V42(2) FinSequence-like V148() Element of the carrier of (TOP-REAL 2)

p9 is V11() real ext-real Element of REAL

s is V11() real ext-real Element of REAL

|[p9,s]| is V42(2) FinSequence-like V148() Element of the carrier of (TOP-REAL 2)

n is V16() V18() V19( NAT ) V20(K246( the carrier of (TOP-REAL 2))) V21() FinSequence-like V144() X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of K246( the carrier of (TOP-REAL 2))

len n is natural V11() real ext-real V33() V156() V157() V158() V159() V160() V161() V162() Element of NAT

cell (n,(len n),0) is Element of K6( the carrier of (TOP-REAL 2))

Int (cell (n,(len n),0)) is open Element of K6( the carrier of (TOP-REAL 2))

n * ((len n),1) is V42(2) FinSequence-like V148() Element of the carrier of (TOP-REAL 2)

(n * ((len n),1)) `1 is V11() real ext-real Element of REAL

n * (1,1) is V42(2) FinSequence-like V148() Element of the carrier of (TOP-REAL 2)

(n * (1,1)) `2 is V11() real ext-real Element of REAL

{ |[b

v_strip (n,(len n)) is Element of K6( the carrier of (TOP-REAL 2))

h_strip (n,0) is Element of K6( the carrier of (TOP-REAL 2))

(v_strip (n,(len n))) /\ (h_strip (n,0)) is Element of K6( the carrier of (TOP-REAL 2))

Int (v_strip (n,(len n))) is open Element of K6( the carrier of (TOP-REAL 2))

Int (h_strip (n,0)) is open Element of K6( the carrier of (TOP-REAL 2))

(Int (v_strip (n,(len n)))) /\ (Int (h_strip (n,0))) is open Element of K6( the carrier of (TOP-REAL 2))

{ |[b

{ |[b

A is set

p is V11() real ext-real Element of REAL

p9 is V11() real ext-real Element of REAL

|[p,p9]| is V42(2) FinSequence-like V148() Element of the carrier of (TOP-REAL 2)

s is V11() real ext-real Element of REAL

s1 is V11() real ext-real Element of REAL

|[s,s1]| is V42(2) FinSequence-like V148() Element of the carrier of (TOP-REAL 2)

A is set

p is V11() real ext-real Element of REAL

p9 is V11() real ext-real Element of REAL

|[p,p9]| is V42(2) FinSequence-like V148() Element of the carrier of (TOP-REAL 2)

p is V11() real ext-real Element of REAL

p9 is V11() real ext-real Element of REAL

|[p,p9]| is V42(2) FinSequence-like V148() Element of the carrier of (TOP-REAL 2)

n is V16() V18() V19( NAT ) V20(K246( the carrier of (TOP-REAL 2))) V21() FinSequence-like V144() X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of K246( the carrier of (TOP-REAL 2))

len n is natural V11() real ext-real V33() V156() V157() V158() V159() V160() V161() V162() Element of NAT

width n is natural V11() real ext-real V33() V156() V157() V158() V159() V160() V161() V162() Element of NAT

cell (n,(len n),(width n)) is Element of K6( the carrier of (TOP-REAL 2))

Int (cell (n,(len n),(width n))) is open Element of K6( the carrier of (TOP-REAL 2))

n * ((len n),1) is V42(2) FinSequence-like V148() Element of the carrier of (TOP-REAL 2)

(n * ((len n),1)) `1 is V11() real ext-real Element of REAL

n * (1,(width n)) is V42(2) FinSequence-like V148() Element of the carrier of (TOP-REAL 2)

(n * (1,(width n))) `2 is V11() real ext-real Element of REAL

{ |[b

v_strip (n,(len n)) is Element of K6( the carrier of (TOP-REAL 2))

h_strip (n,(width n)) is Element of K6( the carrier of (TOP-REAL 2))

(v_strip (n,(len n))) /\ (h_strip (n,(width n))) is Element of K6( the carrier of (