:: WEIERSTR semantic presentation

REAL is non empty non trivial V47() V48() V49() V53() non finite set
NAT is non empty epsilon-transitive epsilon-connected ordinal V47() V48() V49() V50() V51() V52() V53() Element of K6(REAL)
K6(REAL) is non empty set
COMPLEX is non empty non trivial V47() V53() non finite set
RAT is non empty non trivial V47() V48() V49() V50() V53() non finite set
INT is non empty non trivial V47() V48() V49() V50() V51() V53() non finite set
omega is non empty epsilon-transitive epsilon-connected ordinal V47() V48() V49() V50() V51() V52() V53() set
K6(omega) is non empty set
K6(NAT) is non empty set
K7(COMPLEX,COMPLEX) is non empty set
K6(K7(COMPLEX,COMPLEX)) is non empty set
K7(COMPLEX,REAL) is non empty set
K6(K7(COMPLEX,REAL)) is non empty set
1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive V45() V46() V47() V48() V49() V50() V51() V52() Element of NAT
K7(1,1) is non empty set
K6(K7(1,1)) is non empty set
K7(K7(1,1),1) is non empty set
K6(K7(K7(1,1),1)) is non empty set
K7(K7(1,1),REAL) is non empty set
K6(K7(K7(1,1),REAL)) is non empty set
K7(REAL,REAL) is non empty set
K7(K7(REAL,REAL),REAL) is non empty set
K6(K7(K7(REAL,REAL),REAL)) is non empty set
2 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive V45() V46() V47() V48() V49() V50() V51() V52() Element of NAT
K7(2,2) is non empty set
K7(K7(2,2),REAL) is non empty set
K6(K7(K7(2,2),REAL)) is non empty set
K6(K7(REAL,REAL)) is non empty set
TOP-REAL 2 is non empty TopSpace-like V139() V164() V165() V166() V167() V168() V169() V170() V176() L15()
the carrier of () is non empty set
K452() is V200() TopStruct
the carrier of K452() is V47() V48() V49() set

R^1 is non empty strict TopSpace-like V200() TopStruct
K7(K7(COMPLEX,COMPLEX),COMPLEX) is non empty set
K6(K7(K7(COMPLEX,COMPLEX),COMPLEX)) is non empty set
K7(RAT,RAT) is non empty set
K6(K7(RAT,RAT)) is non empty set
K7(K7(RAT,RAT),RAT) is non empty set
K6(K7(K7(RAT,RAT),RAT)) is non empty set
K7(INT,INT) is non empty set
K6(K7(INT,INT)) is non empty set
K7(K7(INT,INT),INT) is non empty set
K6(K7(K7(INT,INT),INT)) is non empty set
K7(NAT,NAT) is non empty set
K7(K7(NAT,NAT),NAT) is non empty set
K6(K7(K7(NAT,NAT),NAT)) is non empty set

3 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive V45() V46() V47() V48() V49() V50() V51() V52() Element of NAT

K7(NAT,REAL) is non empty set
K6(K7(NAT,REAL)) is non empty set

the carrier of RealSpace is non empty V47() V48() V49() set

the carrier of R^1 is non empty V47() V48() V49() set

the carrier of M is set
P is Element of the carrier of M
Q is Element of the carrier of M
x1 is V11() real ext-real Element of REAL
Ball (P,x1) is Element of K6( the carrier of M)
K6( the carrier of M) is non empty set
x2 is V11() real ext-real Element of REAL
Ball (Q,x2) is Element of K6( the carrier of M)
(Ball (P,x1)) \/ (Ball (Q,x2)) is Element of K6( the carrier of M)
abs x1 is V11() real ext-real Element of REAL
abs x2 is V11() real ext-real Element of REAL
(abs x1) + (abs x2) is V11() real ext-real Element of REAL
dist (P,Q) is V11() real ext-real Element of REAL
((abs x1) + (abs x2)) + (dist (P,Q)) is V11() real ext-real Element of REAL
z is Element of the carrier of M
y is V11() real ext-real Element of REAL
Ball (z,y) is Element of K6( the carrier of M)
c8 is set
z is Element of the carrier of M
x1 + 0 is V11() real ext-real Element of REAL
dist (z,z) is V11() real ext-real Element of REAL
x1 - x1 is V11() real ext-real Element of REAL
(dist (z,z)) - y is V11() real ext-real Element of REAL
0 + y is V11() real ext-real Element of REAL
((dist (z,z)) - y) + y is V11() real ext-real Element of REAL
z is Element of the carrier of M
dist (Q,z) is V11() real ext-real Element of REAL
x2 - x2 is V11() real ext-real Element of REAL
(dist (Q,z)) - (abs x2) is V11() real ext-real Element of REAL
dist (z,z) is V11() real ext-real Element of REAL
(dist (P,Q)) + (dist (Q,z)) is V11() real ext-real Element of REAL
0 + (abs x2) is V11() real ext-real Element of REAL
((dist (Q,z)) - (abs x2)) + (abs x2) is V11() real ext-real Element of REAL
((dist (P,Q)) + (dist (Q,z))) - (dist (Q,z)) is V11() real ext-real Element of REAL
(dist (z,z)) - (abs x2) is V11() real ext-real Element of REAL
(dist (P,Q)) - 0 is V11() real ext-real Element of REAL
((dist (z,z)) - (abs x2)) - (abs x1) is V11() real ext-real Element of REAL
(dist (z,z)) - ((abs x1) + (abs x2)) is V11() real ext-real Element of REAL
((dist (z,z)) - ((abs x1) + (abs x2))) + ((abs x1) + (abs x2)) is V11() real ext-real Element of REAL
z is Element of the carrier of M
z is Element of the carrier of M

the carrier of M is set
K6( the carrier of M) is non empty set
K6(K6( the carrier of M)) is non empty set

P + 1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V45() V46() V47() V48() V49() V50() V51() V52() Element of NAT
Seg (P + 1) is V47() V48() V49() V50() V51() V52() finite V71(P + 1) Element of K6(NAT)
Seg P is V47() V48() V49() V50() V51() V52() finite V71(P) Element of K6(NAT)
Q is Element of K6(K6( the carrier of M))
union Q is Element of K6( the carrier of M)

rng x1 is finite set
dom x1 is V47() V48() V49() V50() V51() V52() finite Element of K6(NAT)
x1 . (P + 1) is set
x2 is Element of the carrier of M
z is V11() real ext-real Element of REAL
Ball (x2,z) is Element of K6( the carrier of M)
z is V11() real ext-real Element of REAL
Ball (x2,z) is Element of K6( the carrier of M)

rng y is finite set
c8 is Element of K6(K6( the carrier of M))

dom y is V47() V48() V49() V50() V51() V52() finite Element of K6(NAT)
{(P + 1)} is non empty V47() V48() V49() V50() V51() V52() finite Element of K6(REAL)
(dom y) \/ {(P + 1)} is non empty V47() V48() V49() V50() V51() V52() finite set
z is Element of K6(K6( the carrier of M))
union z is Element of K6( the carrier of M)
() \/ (Ball (x2,z)) is Element of K6( the carrier of M)
z is set
q is set
y is set
x1 . y is set
y . y is set
z is set
z is Element of the carrier of M
q is V11() real ext-real Element of REAL
Ball (z,q) is Element of K6( the carrier of M)
() \/ (Ball (z,q)) is Element of K6( the carrier of M)

the carrier of M is set
K6( the carrier of M) is non empty set
K6(K6( the carrier of M)) is non empty set
P is Element of K6(K6( the carrier of M))
union P is Element of K6( the carrier of M)

rng Q is finite set

x1 + 1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V45() V46() V47() V48() V49() V50() V51() V52() Element of NAT
x2 is Element of K6(K6( the carrier of M))
union x2 is Element of K6( the carrier of M)

Seg z is V47() V48() V49() V50() V51() V52() finite V71(z) Element of K6(NAT)

rng y is finite set
dom y is V47() V48() V49() V50() V51() V52() finite Element of K6(NAT)
Seg x1 is V47() V48() V49() V50() V51() V52() finite V71(x1) Element of K6(NAT)
c8 is Element of K6(K6( the carrier of M))
union c8 is Element of K6( the carrier of M)

rng z is finite set
dom z is V47() V48() V49() V50() V51() V52() finite Element of K6(NAT)
z is Element of the carrier of M
q is V11() real ext-real Element of REAL
Ball (z,q) is Element of K6( the carrier of M)
(union c8) \/ (Ball (z,q)) is Element of K6( the carrier of M)
z is Element of the carrier of M

rng z is finite set
dom z is V47() V48() V49() V50() V51() V52() finite Element of K6(NAT)
q is Element of the carrier of M
y is V11() real ext-real Element of REAL
Ball (q,y) is Element of K6( the carrier of M)
(union c8) \/ (Ball (q,y)) is Element of K6( the carrier of M)
z is Element of the carrier of M
q is V11() real ext-real Element of REAL
Ball (z,q) is Element of K6( the carrier of M)
(union c8) \/ (Ball (z,q)) is Element of K6( the carrier of M)
q is V11() real ext-real Element of REAL
Ball (z,q) is Element of K6( the carrier of M)
(union c8) \/ (Ball (z,q)) is Element of K6( the carrier of M)
y is V11() real ext-real Element of REAL
Ball (z,y) is Element of K6( the carrier of M)
y is V11() real ext-real Element of REAL
Ball (z,y) is Element of K6( the carrier of M)
(Ball (z,y)) \/ (Ball (z,q)) is Element of K6( the carrier of M)
G is Element of the carrier of M
G is V11() real ext-real Element of REAL
Ball (G,G) is Element of K6( the carrier of M)
G is V11() real ext-real Element of REAL
Ball (G,G) is Element of K6( the carrier of M)
x1 is Element of K6(K6( the carrier of M))
union x1 is Element of K6( the carrier of M)

Seg x2 is V47() V48() V49() V50() V51() V52() finite V71(x2) Element of K6(NAT)
the Element of the carrier of M is Element of the carrier of M

rng y is finite set
dom y is V47() V48() V49() V50() V51() V52() finite Element of K6(NAT)
Ball ( the Element of the carrier of M,0) is Element of K6( the carrier of M)

rng z is finite set
dom z is V47() V48() V49() V50() V51() V52() finite Element of K6(NAT)
x1 is Element of K6(K6( the carrier of M))

rng z is finite set
dom z is V47() V48() V49() V50() V51() V52() finite Element of K6(NAT)

Seg x2 is V47() V48() V49() V50() V51() V52() finite V71(x2) Element of K6(NAT)
union x1 is Element of K6( the carrier of M)
dom Q is V47() V48() V49() V50() V51() V52() finite Element of K6(NAT)

Seg x1 is V47() V48() V49() V50() V51() V52() finite V71(x1) Element of K6(NAT)
M is non empty TopSpace-like TopStruct
the carrier of M is non empty set
P is non empty TopSpace-like TopStruct
the carrier of P is non empty set
K7( the carrier of M, the carrier of P) is non empty set
K6(K7( the carrier of M, the carrier of P)) is non empty set
K6( the carrier of P) is non empty set
K6(K6( the carrier of P)) is non empty set
Q is Relation-like the carrier of M -defined the carrier of P -valued Function-like V30( the carrier of M, the carrier of P) Element of K6(K7( the carrier of M, the carrier of P))
x1 is Element of K6(K6( the carrier of P))
Q " x1 is Element of K6(K6( the carrier of M))
K6( the carrier of M) is non empty set
K6(K6( the carrier of M)) is non empty set
x2 is Element of K6( the carrier of M)
z is Element of K6( the carrier of P)
Q " z is Element of K6( the carrier of M)
[#] P is non empty non proper Element of K6( the carrier of P)
y is Element of K6( the carrier of P)
M is non empty TopSpace-like TopStruct
the carrier of M is non empty set
P is non empty TopSpace-like TopStruct
the carrier of P is non empty set
K7( the carrier of M, the carrier of P) is non empty set
K6(K7( the carrier of M, the carrier of P)) is non empty set
K6( the carrier of P) is non empty set
K6(K6( the carrier of P)) is non empty set
Q is Relation-like the carrier of M -defined the carrier of P -valued Function-like V30( the carrier of M, the carrier of P) Element of K6(K7( the carrier of M, the carrier of P))
x1 is Element of K6(K6( the carrier of P))
Q " x1 is Element of K6(K6( the carrier of M))
K6( the carrier of M) is non empty set
K6(K6( the carrier of M)) is non empty set
[#] P is non empty non proper Element of K6( the carrier of P)
K6(([#] P)) is non empty set
[#] M is non empty non proper Element of K6( the carrier of M)
K6(([#] M)) is non empty set

rng x2 is finite set
z is Element of K6(([#] P))
y is set
Q " y is Element of K6( the carrier of M)
z is Element of K6(([#] M))
z is set
q is set
Q " z is Element of K6( the carrier of M)
bool ([#] P) is non empty Element of K6(K6(([#] P)))
K6(K6(([#] P))) is non empty set
bool ([#] M) is non empty Element of K6(K6(([#] M)))
K6(K6(([#] M))) is non empty set
K7((bool ([#] P)),(bool ([#] M))) is non empty set
K6(K7((bool ([#] P)),(bool ([#] M)))) is non empty set
z is Relation-like bool ([#] P) -defined bool ([#] M) -valued Function-like V30( bool ([#] P), bool ([#] M)) Element of K6(K7((bool ([#] P)),(bool ([#] M))))
dom z is Element of K6((bool ([#] P)))
K6((bool ([#] P))) is non empty set

z .: x1 is Element of K6((bool ([#] M)))
K6((bool ([#] M))) is non empty set
c8 is set
z is set
z . z is set
z is Element of K6( the carrier of P)
z . z is set
Q " z is Element of K6( the carrier of M)
z is Element of K6( the carrier of M)
z is Element of K6( the carrier of P)
Q " z is Element of K6( the carrier of M)
z . z is set

rng y is finite set

rng c8 is finite set
M is non empty TopSpace-like TopStruct
the carrier of M is non empty set
P is non empty TopSpace-like TopStruct
the carrier of P is non empty set
K7( the carrier of M, the carrier of P) is non empty set
K6(K7( the carrier of M, the carrier of P)) is non empty set
K6( the carrier of M) is non empty set
K6(K6( the carrier of M)) is non empty set
Q is Relation-like the carrier of M -defined the carrier of P -valued Function-like V30( the carrier of M, the carrier of P) Element of K6(K7( the carrier of M, the carrier of P))
x1 is Element of K6(K6( the carrier of M))
Q .: x1 is Element of K6(K6( the carrier of P))
K6( the carrier of P) is non empty set
K6(K6( the carrier of P)) is non empty set
[#] M is non empty non proper Element of K6( the carrier of M)
K6(([#] M)) is non empty set
[#] P is non empty non proper Element of K6( the carrier of P)
K6(([#] P)) is non empty set

rng x2 is finite set
z is Element of K6(([#] M))
y is set
Q .: y is Element of K6( the carrier of P)
z is Element of K6(([#] P))
z is set
q is set
Q .: z is Element of K6( the carrier of P)
bool ([#] M) is non empty Element of K6(K6(([#] M)))
K6(K6(([#] M))) is non empty set
bool ([#] P) is non empty Element of K6(K6(([#] P)))
K6(K6(([#] P))) is non empty set
K7((bool ([#] M)),(bool ([#] P))) is non empty set
K6(K7((bool ([#] M)),(bool ([#] P)))) is non empty set
z is Relation-like bool ([#] M) -defined bool ([#] P) -valued Function-like V30( bool ([#] M), bool ([#] P)) Element of K6(K7((bool ([#] M)),(bool ([#] P))))
dom z is Element of K6((bool ([#] M)))
K6((bool ([#] M))) is non empty set

z .: x1 is Element of K6((bool ([#] P)))
K6((bool ([#] P))) is non empty set
c8 is set
z is set
z . z is set
z is Element of K6( the carrier of M)
z . z is set
Q .: z is Element of K6( the carrier of P)
z is Element of K6( the carrier of P)
z is Element of K6( the carrier of M)
Q .: z is Element of K6( the carrier of P)
z . z is set

rng y is finite set

rng c8 is finite set
M is non empty TopSpace-like TopStruct
the carrier of M is non empty set
P is non empty TopSpace-like TopStruct
the carrier of P is non empty set
K7( the carrier of M, the carrier of P) is non empty set
K6(K7( the carrier of M, the carrier of P)) is non empty set
K6( the carrier of M) is non empty set
K6( the carrier of P) is non empty set
K6(K6( the carrier of P)) is non empty set
K6(K6( the carrier of M)) is non empty set
Q is Relation-like the carrier of M -defined the carrier of P -valued Function-like V30( the carrier of M, the carrier of P) Element of K6(K7( the carrier of M, the carrier of P))
x1 is Element of K6( the carrier of M)
Q .: x1 is Element of K6( the carrier of P)
x2 is Element of K6(K6( the carrier of P))
Q " x2 is Element of K6(K6( the carrier of M))
z is Element of K6(K6( the carrier of M))
union z is Element of K6( the carrier of M)

rng y is finite set
c8 is non empty set
[#] P is non empty non proper Element of K6( the carrier of P)
K6(([#] P)) is non empty set
z is Element of c8
z is Element of K6( the carrier of M)
q is Element of K6( the carrier of P)
Q " q is Element of K6( the carrier of M)
y is Element of K6(([#] P))
G is Element of c8
G is Element of K6(([#] P))
Q " G is Element of K6( the carrier of M)
bool ([#] P) is non empty Element of K6(K6(([#] P)))
K6(K6(([#] P))) is non empty set
K7(c8,(bool ([#] P))) is non empty set
K6(K7(c8,(bool ([#] P)))) is non empty set
z is Relation-like c8 -defined bool ([#] P) -valued Function-like V30(c8, bool ([#] P)) Element of K6(K7(c8,(bool ([#] P))))
z is Element of c8
z . z is Element of bool ([#] P)
q is Element of c8
z . q is Element of bool ([#] P)
Q " (z . q) is Element of K6( the carrier of M)
K7(z,(bool ([#] P))) is set
K6(K7(z,(bool ([#] P)))) is non empty set
z is Relation-like z -defined bool ([#] P) -valued Function-like V30(z, bool ([#] P)) Element of K6(K7(z,(bool ([#] P))))
dom z is Element of K6(z)
K6(z) is non empty set

rng q is finite set
G is set
dom q is V47() V48() V49() V50() V51() V52() finite Element of K6(NAT)
G is set
q . G is set
y . G is set
z . (y . G) is set
G is Element of K6(K6( the carrier of P))
G is Element of K6(K6( the carrier of P))
union G is Element of K6( the carrier of P)
x is set
dom Q is Element of K6( the carrier of M)
y is set
Q . y is set
C is set
z . C is set
Q " (z . C) is Element of K6( the carrier of M)
Q .: (Q " (z . C)) is Element of K6( the carrier of P)
rng z is Element of K6((bool ([#] P)))
K6((bool ([#] P))) is non empty set
y is set
y is Element of K6(K6( the carrier of P))
c8 is Element of K6(K6( the carrier of P))
z is Element of K6(K6( the carrier of P))
z is set
dom Q is Element of K6( the carrier of M)
q is set
Q . q is set
y is Element of K6(K6( the carrier of P))
y is Element of K6(K6( the carrier of P))
c8 is Element of K6(K6( the carrier of P))
z is Element of K6(K6( the carrier of P))
M is non empty TopSpace-like TopStruct
the carrier of M is non empty set
P is non empty TopSpace-like TopStruct
the carrier of P is non empty set
K7( the carrier of M, the carrier of P) is non empty set
K6(K7( the carrier of M, the carrier of P)) is non empty set
K6( the carrier of M) is non empty set
Q is Relation-like the carrier of M -defined the carrier of P -valued Function-like V30( the carrier of M, the carrier of P) Element of K6(K7( the carrier of M, the carrier of P))
x1 is Element of K6( the carrier of M)
Q .: x1 is Element of K6( the carrier of P)
K6( the carrier of P) is non empty set
[#] M is non empty non proper Element of K6( the carrier of M)
dom Q is Element of K6( the carrier of M)
K6(K6( the carrier of P)) is non empty set
x2 is Element of K6(K6( the carrier of P))
Q " x2 is Element of K6(K6( the carrier of M))
K6(K6( the carrier of M)) is non empty set
union x2 is Element of K6( the carrier of P)
union (Q " x2) is Element of K6( the carrier of M)
y is set
Q " (union x2) is Element of K6( the carrier of M)
c8 is set
Q . c8 is set
z is set
Q " z is Element of K6( the carrier of M)
z is set
Q . y is set
c8 is Element of the carrier of M
Q . c8 is Element of the carrier of P
{(Q . c8)} is non empty finite set
Q " {(Q . c8)} is Element of K6( the carrier of M)
z is set
Q . z is set
y is Element of K6(K6( the carrier of M))
y is Element of K6(K6( the carrier of P))
M is non empty TopSpace-like TopStruct
the carrier of M is non empty set
K7( the carrier of M, the carrier of R^1) is non empty set
K6(K7( the carrier of M, the carrier of R^1)) is non empty set
K6( the carrier of M) is non empty set
Q is Element of K6( the carrier of M)
P is Relation-like the carrier of M -defined the carrier of R^1 -valued Function-like V30( the carrier of M, the carrier of R^1) Element of K6(K7( the carrier of M, the carrier of R^1))
P .: Q is V47() V48() V49() Element of K6( the carrier of R^1)
K6( the carrier of R^1) is non empty set
K7( the carrier of (), the carrier of R^1) is non empty set
K6(K7( the carrier of (), the carrier of R^1)) is non empty set
K6( the carrier of ()) is non empty set
P is Element of K6( the carrier of ())
M is Relation-like the carrier of () -defined the carrier of R^1 -valued Function-like V30( the carrier of (), the carrier of R^1) Element of K6(K7( the carrier of (), the carrier of R^1))
M .: P is V47() V48() V49() Element of K6( the carrier of R^1)
K6( the carrier of R^1) is non empty set
K6( the carrier of R^1) is non empty set
M is V47() V48() V49() Element of K6( the carrier of R^1)
M is V47() V48() V49() Element of K6( the carrier of R^1)
(M) is V47() V48() V49() Element of K6(REAL)
K6(K6( the carrier of R^1)) is non empty set
Q is Element of K6(K6( the carrier of R^1))
union Q is V47() V48() V49() Element of K6( the carrier of R^1)
x1 is set
K6( the carrier of RealSpace) is non empty set
x2 is V11() real ext-real Element of the carrier of RealSpace
Ball (x2,1) is V47() V48() V49() Element of K6( the carrier of RealSpace)
z is V47() V48() V49() Element of K6( the carrier of RealSpace)
Family_open_set RealSpace is Element of K6(K6( the carrier of RealSpace))
K6(K6( the carrier of RealSpace)) is non empty set
TopStruct(# the carrier of RealSpace, #) is strict TopStruct
y is V47() V48() V49() Element of K6( the carrier of R^1)
dist (x2,x2) is V11() real ext-real Element of REAL
c8 is set
x1 is V47() V48() V49() Element of K6( the carrier of R^1)
x2 is V11() real ext-real Element of the carrier of RealSpace
Ball (x2,1) is V47() V48() V49() Element of K6( the carrier of RealSpace)
K6( the carrier of RealSpace) is non empty set
x1 is Element of K6(K6( the carrier of R^1))
union x1 is V47() V48() V49() Element of K6( the carrier of R^1)
x2 is set
z is V47() V48() V49() Element of K6( the carrier of R^1)
y is V11() real ext-real Element of the carrier of RealSpace
Ball (y,1) is V47() V48() V49() Element of K6( the carrier of RealSpace)
K6( the carrier of RealSpace) is non empty set
Family_open_set RealSpace is Element of K6(K6( the carrier of RealSpace))
K6( the carrier of RealSpace) is non empty set
K6(K6( the carrier of RealSpace)) is non empty set
TopStruct(# the carrier of RealSpace, #) is strict TopStruct
x2 is Element of K6(K6( the carrier of RealSpace))
union x2 is V47() V48() V49() Element of K6( the carrier of RealSpace)
z is V11() real ext-real Element of the carrier of RealSpace
y is V11() real ext-real Element of REAL
Ball (z,y) is V47() V48() V49() Element of K6( the carrier of RealSpace)
y is V11() real ext-real Element of REAL
Ball (z,y) is V47() V48() V49() Element of K6( the carrier of RealSpace)
c8 is V11() real ext-real Element of REAL
c8 - y is V11() real ext-real Element of REAL
c8 + y is V11() real ext-real Element of REAL
z is V11() real ext-real Element of REAL
z is V11() real ext-real Element of the carrier of RealSpace
q is V11() real ext-real Element of the carrier of RealSpace
dist (z,q) is V11() real ext-real Element of REAL
c8 - z is V11() real ext-real Element of REAL
abs (c8 - z) is V11() real ext-real Element of REAL
- y is V11() real ext-real Element of REAL
(- y) + z is V11() real ext-real Element of REAL
c8 - (- y) is V11() real ext-real Element of REAL
z + y is V11() real ext-real Element of REAL
z is ext-real set
z is ext-real set
P is ext-real set
P is ext-real set
M is V47() V48() V49() Element of K6( the carrier of R^1)
(M) is V47() V48() V49() Element of K6(REAL)

rng P is V47() V48() V49() Element of K6(REAL)

x1 is V11() real ext-real Element of the carrier of R^1
M ` is V47() V48() V49() Element of K6( the carrier of R^1)
x2 is V47() V48() V49() Element of K6( the carrier of R^1)
z is V47() V48() V49() Element of K6( the carrier of R^1)
Family_open_set RealSpace is Element of K6(K6( the carrier of RealSpace))
K6( the carrier of RealSpace) is non empty set
K6(K6( the carrier of RealSpace)) is non empty set
TopStruct(# the carrier of RealSpace, #) is strict TopStruct
y is V11() real ext-real Element of the carrier of RealSpace
c8 is V11() real ext-real set
Ball (y,c8) is V47() V48() V49() Element of K6( the carrier of RealSpace)
z is V11() real ext-real Element of REAL
Ball (y,z) is V47() V48() V49() Element of K6( the carrier of RealSpace)
{ b1 where b1 is V11() real ext-real Element of the carrier of RealSpace : not z <= dist (y,b1) } is set

z + 1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V45() V46() V47() V48() V49() V50() V51() V52() Element of NAT
P . (z + 1) is V11() real ext-real Element of REAL
(P . (z + 1)) - (lim P) is V11() real ext-real Element of REAL
abs ((P . (z + 1)) - (lim P)) is V11() real ext-real Element of REAL
real_dist . ((P . (z + 1)),(lim P)) is V11() real ext-real Element of REAL
real_dist . ((lim P),(P . (z + 1))) is V11() real ext-real Element of REAL
y is V11() real ext-real Element of the carrier of RealSpace
dist (y,y) is V11() real ext-real Element of REAL
the distance of RealSpace is Relation-like K7( the carrier of RealSpace, the carrier of RealSpace) -defined REAL -valued Function-like V30(K7( the carrier of RealSpace, the carrier of RealSpace), REAL ) Element of K6(K7(K7( the carrier of RealSpace, the carrier of RealSpace),REAL))
K7( the carrier of RealSpace, the carrier of RealSpace) is non empty set
K7(K7( the carrier of RealSpace, the carrier of RealSpace),REAL) is non empty set
K6(K7(K7( the carrier of RealSpace, the carrier of RealSpace),REAL)) is non empty set
the distance of RealSpace . (y,y) is V11() real ext-real Element of REAL
(Ball (y,z)) /\ (rng P) is V47() V48() V49() Element of K6(REAL)

rng P is V47() V48() V49() Element of K6(REAL)

Q is set
M is V47() V48() V49() Element of K6( the carrier of R^1)
(M) is V47() V48() V49() Element of K6(REAL)
P is set

rng Q is V47() V48() V49() Element of K6(REAL)
M is non empty TopSpace-like TopStruct
the carrier of M is non empty set
K7( the carrier of M, the carrier of R^1) is non empty set
K6(K7( the carrier of M, the carrier of R^1)) is non empty set
K6( the carrier of M) is non empty set
P is Relation-like the carrier of M -defined the carrier of R^1 -valued Function-like V30( the carrier of M, the carrier of R^1) Element of K6(K7( the carrier of M, the carrier of R^1))
Q is Element of K6( the carrier of M)
P .: Q is V47() V48() V49() Element of K6( the carrier of R^1)
((P .: Q)) is V47() V48() V49() Element of K6(REAL)
upper_bound ((P .: Q)) is V11() real ext-real Element of REAL
lower_bound ((P .: Q)) is V11() real ext-real Element of REAL
x1 is set
dom P is Element of K6( the carrier of M)
P . x1 is set
x1 is V11() real ext-real Element of REAL
x2 is V11() real ext-real Element of REAL
dom P is Element of K6( the carrier of M)
z is set
P . z is set
y is set
P . y is set
c8 is Element of the carrier of M
P . c8 is V11() real ext-real Element of the carrier of R^1
z is Element of the carrier of M
P . z is V11() real ext-real Element of the carrier of R^1
M is V47() V48() V49() Element of K6( the carrier of R^1)
(M) is V47() V48() V49() Element of K6(REAL)
upper_bound (M) is V11() real ext-real Element of REAL
lower_bound (M) is V11() real ext-real Element of REAL
M is non empty TopSpace-like TopStruct
the carrier of M is non empty set
K7( the carrier of M, the carrier of R^1) is non empty set
K6(K7( the carrier of M, the carrier of R^1)) is non empty set
K6( the carrier of M) is non empty set
P is Relation-like the carrier of M -defined the carrier of R^1 -valued Function-like V30( the carrier of M, the carrier of R^1) Element of K6(K7( the carrier of M, the carrier of R^1))
Q is Element of K6( the carrier of M)
P .: Q is V47() V48() V49() Element of K6( the carrier of R^1)
((P .: Q)) is V11() real ext-real Element of REAL
((P .: Q)) is V47() V48() V49() Element of K6(REAL)
upper_bound ((P .: Q)) is V11() real ext-real Element of REAL
lower_bound ((P .: Q)) is V11() real ext-real Element of REAL
x1 is Element of the carrier of M
x2 is Element of the carrier of M
P . x1 is V11() real ext-real Element of the carrier of R^1
P . x2 is V11() real ext-real Element of the carrier of R^1
M is non empty TopSpace-like TopStruct
the carrier of M is non empty set
K7( the carrier of M, the carrier of R^1) is non empty set
K6(K7( the carrier of M, the carrier of R^1)) is non empty set
K6( the carrier of M) is non empty set
P is Relation-like the carrier of M -defined the carrier of R^1 -valued Function-like V30( the carrier of M, the carrier of R^1) Element of K6(K7( the carrier of M, the carrier of R^1))
Q is Element of K6( the carrier of M)
P .: Q is V47() V48() V49() Element of K6( the carrier of R^1)
((P .: Q)) is V11() real ext-real Element of REAL
((P .: Q)) is V47() V48() V49() Element of K6(REAL)
lower_bound ((P .: Q)) is V11() real ext-real Element of REAL
upper_bound ((P .: Q)) is V11() real ext-real Element of REAL
x1 is Element of the carrier of M
x2 is Element of the carrier of M
P . x1 is V11() real ext-real Element of the carrier of R^1
P . x2 is V11() real ext-real Element of the carrier of R^1

the carrier of M is non empty set

the carrier of () is non empty set
K7( the carrier of (), the carrier of R^1) is non empty set
K6(K7( the carrier of (), the carrier of R^1)) is non empty set
P is Element of the carrier of M
Q is Element of the carrier of M
dist (Q,P) is V11() real ext-real Element of REAL
x1 is V11() real ext-real Element of REAL
x2 is V11() real ext-real Element of the carrier of R^1
z is Element of the carrier of M
y is V11() real ext-real Element of the carrier of R^1
dist (z,P) is V11() real ext-real Element of REAL
K7( the carrier of M, the carrier of R^1) is non empty set
K6(K7( the carrier of M, the carrier of R^1)) is non empty set
Q is Relation-like the carrier of M -defined the carrier of R^1 -valued Function-like V30( the carrier of M, the carrier of R^1) Element of K6(K7( the carrier of M, the carrier of R^1))
x1 is Element of the carrier of M
Q . x1 is V11() real ext-real Element of the carrier of R^1
dist (x1,P) is V11() real ext-real Element of REAL
Family_open_set M is Element of K6(K6( the carrier of M))
K6( the carrier of M) is non empty set
K6(K6( the carrier of M)) is non empty set
TopStruct(# the carrier of M,() #) is strict TopStruct
x1 is Relation-like the carrier of () -defined the carrier of R^1 -valued Function-like V30( the carrier of (), the carrier of R^1) Element of K6(K7( the carrier of (), the carrier of R^1))
x2 is Element of the carrier of M
x1 . x2 is set
dist (x2,P) is V11() real ext-real Element of REAL
Q is Relation-like the carrier of () -defined the carrier of R^1 -valued Function-like V30( the carrier of (), the carrier of R^1) Element of K6(K7( the carrier of (), the carrier of R^1))
x1 is Relation-like the carrier of () -defined the carrier of R^1 -valued Function-like V30( the carrier of (), the carrier of R^1) Element of K6(K7( the carrier of (), the carrier of R^1))
x2 is set
Q . x2 is set
x1 . x2 is set
Family_open_set M is Element of K6(K6( the carrier of M))
K6( the carrier of M) is non empty set
K6(K6( the carrier of M)) is non empty set
TopStruct(# the carrier of M,() #) is strict TopStruct
z is Element of the carrier of M
Q . z is set
dist (z,P) is V11() real ext-real Element of REAL
x1 . z is set

the carrier of M is non empty set

P is Element of the carrier of M
(M,P) is Relation-like the carrier of () -defined the carrier of R^1 -valued Function-like V30( the carrier of (), the carrier of R^1) Element of K6(K7( the carrier of (), the carrier of R^1))
the carrier of () is non empty set
K7( the carrier of (), the carrier of R^1) is non empty set
K6(K7( the carrier of (), the carrier of R^1)) is non empty set
Q is V47() V48() V49() Element of K6( the carrier of R^1)
(M,P) " Q is Element of K6( the carrier of ())
K6( the carrier of ()) is non empty set
x1 is Element of the carrier of M
dist (x1,P) is V11() real ext-real Element of REAL
x2 is V11() real ext-real Element of the carrier of RealSpace
(M,P) . x1 is set
the carrier of is non empty set
K6( the carrier of ) is non empty set
z is Element of K6( the carrier of )
y is V11() real ext-real set
Ball (x2,y) is V47() V48() V49() Element of K6( the carrier of RealSpace)
K6( the carrier of RealSpace) is non empty set
c8 is V11() real ext-real Element of REAL
Ball (x1,c8) is Element of K6( the carrier of M)
K6( the carrier of M) is non empty set
(M,P) " z is Element of K6( the carrier of ())
z is set
z is Element of the carrier of M
dist (z,P) is V11() real ext-real Element of REAL
q is V11() real ext-real Element of the carrier of RealSpace
dist (x1,z) is V11() real ext-real Element of REAL
c8 + (dist (x1,z)) is V11() real ext-real Element of REAL
(dist (x1,P)) - (dist (z,P)) is V11() real ext-real Element of REAL
abs ((dist (x1,P)) - (dist (z,P))) is V11() real ext-real Element of REAL
(abs ((dist (x1,P)) - (dist (z,P)))) + (dist (x1,z)) is V11() real ext-real Element of REAL
dist (x2,q) is V11() real ext-real Element of REAL
Ball (x2,c8) is V47() V48() V49() Element of K6( the carrier of RealSpace)
(M,P) . z is set
dom (M,P) is Element of K6( the carrier of ())
[#] R^1 is non empty non proper V47() V48() V49() Element of K6( the carrier of R^1)

the carrier of M is non empty set

the carrier of () is non empty set
K6( the carrier of ()) is non empty set
Q is Element of K6( the carrier of ())
P is Element of the carrier of M
(M,P) is Relation-like the carrier of () -defined the carrier of R^1 -valued Function-like V30( the carrier of (), the carrier of R^1) Element of K6(K7( the carrier of (), the carrier of R^1))
K7( the carrier of (), the carrier of R^1) is non empty set
K6(K7( the carrier of (), the carrier of R^1)) is non empty set
(M,P) .: Q is V47() V48() V49() Element of K6( the carrier of R^1)
(((M,P) .: Q)) is V11() real ext-real Element of REAL
(((M,P) .: Q)) is V47() V48() V49() Element of K6(REAL)
upper_bound (((M,P) .: Q)) is V11() real ext-real Element of REAL

the carrier of M is non empty set

the carrier of () is non empty set
K6( the carrier of ()) is non empty set
Q is Element of K6( the carrier of ())
P is Element of the carrier of M
(M,P) is Relation-like the carrier of () -defined the carrier of R^1 -valued Function-like V30( the carrier of (), the carrier of R^1) Element of K6(K7( the carrier of (), the carrier of R^1))
K7( the carrier of (), the carrier of R^1) is non empty set
K6(K7( the carrier of (), the carrier of R^1)) is non empty set
(M,P) .: Q is V47() V48() V49() Element of K6( the carrier of R^1)
(((M,P) .: Q)) is V11() real ext-real Element of REAL
(((M,P) .: Q)) is V47() V48() V49() Element of K6(REAL)
lower_bound (((M,P) .: Q)) is V11() real ext-real Element of REAL

the carrier of () is non empty set
K6( the carrier of ()) is non empty set
K7( the carrier of (), the carrier of R^1) is non empty set
K6(K7( the carrier of (), the carrier of R^1)) is non empty set
the carrier of M is non empty set
P is Element of K6( the carrier of ())
Q is Element of the carrier of M
(M,Q) is Relation-like the carrier of () -defined the carrier of R^1 -valued Function-like V30( the carrier of (), the carrier of R^1) Element of K6(K7( the carrier of (), the carrier of R^1))
(M,Q) .: P is V47() V48() V49() Element of K6( the carrier of R^1)
(((M,Q) .: P)) is V11() real ext-real Element of REAL
(((M,Q) .: P)) is V47() V48() V49() Element of K6(REAL)
upper_bound (((M,Q) .: P)) is V11() real ext-real Element of REAL
x1 is V11() real ext-real Element of REAL
x2 is V11() real ext-real Element of the carrier of R^1
z is Element of the carrier of M
y is V11() real ext-real Element of the carrier of R^1
(M,z) is Relation-like the carrier of () -defined the carrier of R^1 -valued Function-like V30( the carrier of (), the carrier of R^1) Element of K6(K7( the carrier of (), the carrier of R^1))
(M,z) .: P is V47() V48() V49() Element of K6( the carrier of R^1)
(((M,z) .: P)) is V11() real ext-real Element of REAL
(((M,z) .: P)) is V47() V48() V49() Element of K6(REAL)
upper_bound (((M,z) .: P)) is V11() real ext-real Element of REAL
K7( the carrier of M, the carrier of R^1) is non empty set
K6(K7( the carrier of M, the carrier of R^1)) is non empty set
Q is Relation-like the carrier of M -defined the carrier of R^1 -valued Function-like V30( the carrier of M, the carrier of R^1) Element of K6(K7( the carrier of M, the carrier of R^1))
x1 is Element of the carrier of M
Q . x1 is V11() real ext-real Element of the carrier of R^1
(M,x1) is Relation-like the carrier of () -defined the carrier of R^1 -valued Function-like V30( the carrier of (), the carrier of R^1) Element of K6(K7( the carrier of (), the carrier of R^1))
(M,x1) .: P is V47() V48() V49() Element of K6( the carrier of R^1)
(((M,x1) .: P)) is V11() real ext-real Element of REAL
(((M,x1) .: P)) is V47() V48() V49() Element of K6(REAL)
upper_bound (((M,x1) .: P)) is V11() real ext-real Element of REAL
Family_open_set M is Element of K6(K6( the carrier of M))
K6( the carrier of M) is non empty set
K6(K6( the carrier of M)) is non empty set
TopStruct(# the carrier of M,() #) is strict TopStruct
x1 is Relation-like the carrier of () -defined the carrier of R^1 -valued Function-like V30( the carrier of (), the carrier of R^1) Element of K6(K7( the carrier of (), the carrier of R^1))
x2 is Element of the carrier of M
x1 . x2 is set
(M,x2) is Relation-like the carrier of () -defined the carrier of R^1 -valued Function-like V30( the carrier of (), the carrier of R^1) Element of K6(K7( the carrier of (), the carrier of R^1))
(M,x2) .: P is V47() V48() V49() Element of K6( the carrier of R^1)
(((M,x2) .: P)) is V11() real ext-real Element of REAL
(((M,x2) .: P)) is V47() V48() V49() Element of K6(REAL)
upper_bound (((M,x2) .: P)) is V11() real ext-real Element of REAL
Q is Relation-like the carrier of () -defined the carrier of R^1 -valued Function-like V30( the carrier of (), the carrier of R^1) Element of K6(K7( the carrier of (), the carrier of R^1))
x1 is Relation-like the carrier of () -defined the carrier of R^1 -valued Function-like V30( the carrier of (), the carrier of R^1) Element of K6(K7( the carrier of (), the carrier of R^1))
x2 is set
Q . x2 is set
x1 . x2 is set
Family_open_set M is Element of K6(K6( the carrier of M))
K6( the carrier of M) is non empty set
K6(K6( the carrier of M)) is non empty set
TopStruct(# the carrier of M,() #) is strict TopStruct
z is Element of the carrier of M
Q . z is set
(M,z) is Relation-like the carrier of () -defined the carrier of R^1 -valued Function-like V30( the carrier of (), the carrier of R^1) Element of K6(K7( the carrier of (), the carrier of R^1))
(M,z) .: P is V47() V48() V49() Element of K6( the carrier of R^1)
(((M,z) .: P)) is V11() real ext-real Element of REAL
(((M,z) .: P)) is V47() V48() V49() Element of K6(REAL)
upper_bound (((M,z) .: P)) is V11() real ext-real Element of REAL
x1 . z is set
Q is Element of the carrier of M
(M,Q) is Relation-like the carrier of () -defined the carrier of R^1 -valued Function-like V30( the carrier of (), the carrier of R^1) Element of K6(K7( the carrier of (), the carrier of R^1))
(M,Q) .: P is V47() V48() V49() Element of K6( the carrier of R^1)
(((M,Q) .: P)) is V11() real ext-real Element of REAL
(((M,Q) .: P)) is V47() V48() V49() Element of K6(REAL)
lower_bound (((M,Q) .: P)) is V11() real ext-real Element of REAL
x1 is V11() real ext-real Element of REAL
x2 is V11() real ext-real Element of the carrier of R^1
z is Element of the carrier of M
y is V11() real ext-real Element of the carrier of R^1
(M,z) is Relation-like the carrier of () -defined the carrier of R^1 -valued Function-like V30( the carrier of (), the carrier of R^1) Element of K6(K7( the carrier of (), the carrier of R^1))
(M,z) .: P is V47() V48() V49() Element of K6( the carrier of R^1)
(((M,z) .: P)) is V11() real ext-real Element of REAL
(((M,z) .: P)) is V47() V48() V49() Element of K6(REAL)
lower_bound (((M,z) .: P)) is V11() real ext-real Element of REAL
K7( the carrier of M, the carrier of R^1) is non empty set
K6(K7( the carrier of M, the carrier of R^1)) is non empty set
Q is Relation-like the carrier of M -defined the carrier of R^1 -valued Function-like V30( the carrier of M, the carrier of R^1) Element of K6(K7( the carrier of M, the carrier of R^1))
x1 is Element of the carrier of M
Q . x1 is V11() real ext-real Element of the carrier of R^1
(M,x1) is Relation-like the carrier of () -defined the carrier of R^1 -valued Function-like V30( the carrier of (), the carrier of R^1) Element of K6(K7( the carrier of (), the carrier of R^1))
(M,x1) .: P is V47() V48() V49() Element of K6( the carrier of R^1)
(((M,x1) .: P)) is V11() real ext-real Element of REAL
(((M,x1) .: P)) is V47() V48() V49() Element of K6(REAL)
lower_bound (((M,x1) .: P)) is V11() real ext-real Element of REAL
Family_open_set M is Element of K6(K6( the carrier of M))
K6( the carrier of M) is non empty set
K6(K6( the carrier of M)) is non empty set
TopStruct(# the carrier of M,() #) is strict TopStruct
x1 is Relation-like the carrier of () -defined the carrier of R^1 -valued Function-like V30( the carrier of (), the carrier of R^1) Element of K6(K7( the carrier of (), the carrier of R^1))
x2 is Element of the carrier of M
x1 . x2 is set
(M,x2) is Relation-like the carrier of () -defined the carrier of R^1 -valued Function-like V30( the carrier of (), the carrier of R^1) Element of K6(K7( the carrier of (), the carrier of R^1))
(M,x2) .: P is V47() V48() V49() Element of K6( the carrier of R^1)
(((M,x2) .: P)) is V11() real ext-real Element of REAL
(((M,x2) .: P)) is V47() V48() V49() Element of K6(REAL)
lower_bound (((M,x2) .: P)) is V11() real ext-real Element of REAL
Q is Relation-like the carrier of () -defined the carrier of R^1 -valued Function-like V30( the carrier of (), the carrier of R^1) Element of K6(K7( the carrier of (), the carrier of R^1))
x1 is Relation-like the carrier of () -defined the carrier of R^1 -valued Function-like V30( the carrier of (), the carrier of R^1) Element of K6(K7( the carrier of (), the carrier of R^1))
x2 is set
Q . x2 is set
x1 . x2 is set
Family_open_set M is Element of K6(K6( the carrier of M))
K6( the carrier of M) is non empty set
K6(K6( the carrier of M)) is non empty set
TopStruct(# the carrier of M,() #) is strict TopStruct
z is Element of the carrier of M
Q . z is set
(M,z) is Relation-like the carrier of () -defined the carrier of R^1 -valued Function-like V30( the carrier of (), the carrier of R^1) Element of K6(K7( the carrier of (), the carrier of R^1))
(M,z) .: P is V47() V48() V49() Element of K6( the carrier of R^1)
(((M,z) .: P)) is V11() real ext-real Element of REAL
(((M,z) .: P)) is V47() V48() V49() Element of K6(REAL)
lower_bound (((M,z) .: P)) is V11() real ext-real Element of REAL
x1 . z is set

the carrier of () is non empty set
K6( the carrier of ()) is non empty set
the carrier of M is non empty set
P is Element of K6( the carrier of ())
Q is Element of the carrier of M
x1 is Element of the carrier of M
dist (Q,x1) is V11() real ext-real Element of REAL
(M,x1) is Relation-like the carrier of () -defined the carrier of R^1 -valued Function-like V30( the carrier of (), the carrier of R^1) Element of K6(K7( the carrier of (), the carrier of R^1))
K7( the carrier of (), the carrier of R^1) is non empty set
K6(K7( the carrier of (), the carrier of R^1)) is non empty set
(M,x1) .: P is V47() V48() V49() Element of K6( the carrier of R^1)
(((M,x1) .: P)) is V11() real ext-real Element of REAL
(((M,x1) .: P)) is V47() V48() V49() Element of K6(REAL)
upper_bound (((M,x1) .: P)) is V11() real ext-real Element of REAL
(((M,x1) .: P)) is V11() real ext-real Element of REAL
lower_bound (((M,x1) .: P)) is V11() real ext-real Element of REAL
(M,x1) . Q is set
dom (M,x1) is Element of K6( the carrier of ())

the carrier of () is non empty set
K6( the carrier of ()) is non empty set
the carrier of M is non empty set
P is Element of K6( the carrier of ())
Q is Element of the carrier of M
(M,Q) is Relation-like the carrier of () -defined the carrier of R^1 -valued Function-like V30( the carrier of (), the carrier of R^1) Element of K6(K7( the carrier of (), the carrier of R^1))
K7( the carrier of (), the carrier of R^1) is non empty set
K6(K7( the carrier of (), the carrier of R^1)) is non empty set
(M,Q) .: P is V47() V48() V49() Element of K6( the carrier of R^1)
(((M,Q) .: P)) is V11() real ext-real Element of REAL
(((M,Q) .: P)) is V47() V48() V49() Element of K6(REAL)
upper_bound (((M,Q) .: P)) is V11() real ext-real Element of REAL
x1 is Element of the carrier of M
(M,x1) is Relation-like the carrier of () -defined the carrier of R^1 -valued Function-like V30( the carrier of (), the carrier of R^1) Element of K6(K7( the carrier of (), the carrier of R^1))
(M,x1) .: P is V47() V48() V49() Element of K6( the carrier of R^1)
(((M,x1) .: P)) is V11() real ext-real Element of REAL
(((M,x1) .: P)) is V47() V48() V49() Element of K6(REAL)
upper_bound (((M,x1) .: P)) is V11() real ext-real Element of REAL
(((M,Q) .: P)) - (((M,x1) .: P)) is V11() real ext-real Element of REAL
abs ((((M,Q) .: P)) - (((M,x1) .: P))) is V11() real ext-real Element of REAL
dist (Q,x1) is V11() real ext-real Element of REAL
x2 is Element of the carrier of ()
(M,Q) . x2 is V11() real ext-real Element of the carrier of R^1
Family_open_set M is Element of K6(K6( the carrier of M))
K6( the carrier of M) is non empty set
K6(K6( the carrier of M)) is non empty set
TopStruct(# the carrier of M,() #) is strict TopStruct
y is Element of the carrier of ()
(M,x1) . y is V11() real ext-real Element of the carrier of R^1
c8 is Element of the carrier of M
dist (c8,x1) is V11() real ext-real Element of REAL
z is Element of the carrier of M
(M,Q) . z is set
dist (z,Q) is V11() real ext-real Element of REAL
dist (c8,Q) is V11() real ext-real Element of REAL
(dist (c8,Q)) + (dist (Q,x1)) is V11() real ext-real Element of REAL
(dist (c8,x1)) - (dist (z,Q)) is V11() real ext-real Element of REAL
((dist (c8,Q)) + (dist (Q,x1))) - (dist (c8,Q)) is V11() real ext-real Element of REAL
- (dist (Q,x1)) is V11() real ext-real Element of REAL
- ((dist (c8,x1)) - (dist (z,Q))) is V11() real ext-real Element of REAL
(M,x1) . c8 is set
dist (z,x1) is V11() real ext-real Element of REAL
dist (x1,Q) is V11() real ext-real Element of REAL
(dist (z,x1)) + (dist (x1,Q)) is V11() real ext-real Element of REAL
(dist (z,Q)) - (dist (c8,x1)) is V11() real ext-real Element of REAL
(dist (z,x1)) + (dist (Q,x1)) is V11() real ext-real Element of REAL
((dist (z,x1)) + (dist (Q,x1))) - (dist (z,x1)) is V11() real ext-real Element of REAL

the carrier of () is non empty set
K6( the carrier of ()) is non empty set
the carrier of M is non empty set
P is Element of K6( the carrier of ())
(M,P) is Relation-like the carrier of () -defined the carrier of R^1 -valued Function-like V30( the carrier of (), the carrier of R^1) Element of K6(K7( the carrier of (), the carrier of R^1))
K7( the carrier of (), the carrier of R^1) is non empty set
K6(K7( the carrier of (), the carrier of R^1)) is non empty set
Q is Element of the carrier of M
(M,P) . Q is set
x1 is Element of the carrier of M
(M,P) . x1 is set
dist (Q,x1) is V11() real ext-real Element of REAL
x2 is V11() real ext-real Element of REAL
z is V11() real ext-real Element of REAL
x2 - z is V11() real ext-real Element of REAL
abs (x2 - z) is V11() real ext-real Element of REAL
(M,Q) is Relation-like the carrier of () -defined the carrier of R^1 -valued Function-like V30( the carrier of (), the carrier of R^1) Element of K6(K7( the carrier of (), the carrier of R^1))
(M,Q) .: P is V47() V48() V49() Element of K6( the carrier of R^1)
(((M,Q) .: P)) is V11() real ext-real Element of REAL
(((M,Q) .: P)) is V47() V48() V49() Element of K6(REAL)
upper_bound (((M,Q) .: P)) is V11() real ext-real Element of REAL
(M,x1) is Relation-like the carrier of () -defined the carrier of R^1 -valued Function-like V30( the carrier of (), the carrier of R^1) Element of K6(K7( the carrier of (), the carrier of R^1))
(M,x1) .: P is V47() V48() V49() Element of K6( the carrier of R^1)
(((M,x1) .: P)) is V11() real ext-real Element of REAL
(((M,x1) .: P)) is V47() V48() V49() Element of K6(REAL)
upper_bound (((M,x1) .: P)) is V11() real ext-real Element of REAL

the carrier of () is non empty set
K6( the carrier of ()) is non empty set
the carrier of M is non empty set
P is Element of K6( the carrier of ())
Q is Element of the carrier of M
(M,Q) is Relation-like the carrier of () -defined the carrier of R^1 -valued Function-like V30( the carrier of (), the carrier of R^1) Element of K6(K7( the carrier of (), the carrier of R^1))
K7( the carrier of (), the carrier of R^1) is non empty set
K6(K7( the carrier of (), the carrier of R^1)) is non empty set
(M,Q) .: P is V47() V48() V49() Element of K6( the carrier of R^1)
(((M,Q) .: P)) is V11() real ext-real Element of REAL
(((M,Q) .: P)) is V47() V48() V49() Element of K6(REAL)
lower_bound (((M,Q) .: P)) is V11() real ext-real Element of REAL
x1 is Element of the carrier of M
(M,x1) is Relation-like the carrier of () -defined the carrier of R^1 -valued Function-like V30( the carrier of (), the carrier of R^1) Element of K6(K7( the carrier of (), the carrier of R^1))
(M,x1) .: P is V47() V48() V49() Element of K6( the carrier of R^1)
(((M,x1) .: P)) is V11() real ext-real Element of REAL
(((M,x1) .: P)) is V47() V48() V49() Element of K6(REAL)
lower_bound (((M,x1) .: P)) is V11() real ext-real Element of REAL
(((M,Q) .: P)) - (((M,x1) .: P)) is V11() real ext-real Element of REAL
abs ((((M,Q) .: P)) - (((M,x1) .: P))) is V11() real ext-real Element of REAL
dist (Q,x1) is V11() real ext-real Element of REAL
x2 is Element of the carrier of ()
(M,Q) . x2 is V11() real ext-real Element of the carrier of R^1
Family_open_set M is Element of K6(K6( the carrier of M))
K6( the carrier of M) is non empty set
K6(K6( the carrier of M)) is non empty set
TopStruct(# the carrier of M,() #) is strict TopStruct
y is Element of the carrier of ()
(M,x1) . y is V11() real ext-real Element of the carrier of R^1
c8 is Element of the carrier of M
dist (c8,x1) is V11() real ext-real Element of REAL
(M,x1) . c8 is set
z is Element of the carrier of M
dist (z,x1) is V11() real ext-real Element of REAL
dist (z,Q) is V11() real ext-real Element of REAL
(dist (z,Q)) + (dist (Q,x1)) is V11() real ext-real Element of REAL
(dist (c8,x1)) - (dist (z,Q)) is V11() real ext-real Element of REAL
- (dist (Q,x1)) is V11() real ext-real Element of REAL
- ((dist (c8,x1)) - (dist (z,Q))) is V11() real ext-real Element of REAL
(M,Q) . z is set
dist (c8,Q) is V11() real ext-real Element of REAL
dist (x1,Q) is V11() real ext-real Element of REAL
(dist (c8,x1)) + (dist (x1,Q)) is V11() real ext-real Element of REAL
(dist (c8,x1)) + (dist (Q,x1)) is V11() real ext-real Element of REAL
(dist (z,Q)) - (dist (c8,x1)) is V11() real ext-real Element of REAL

the carrier of () is non empty set
K6( the carrier of ()) is non empty set
the carrier of M is non empty set
P is Element of K6( the carrier of ())
(M,P) is Relation-like the carrier of () -defined the carrier of R^1 -valued Function-like V30( the carrier of (), the carrier of R^1) Element of K6(K7( the carrier of (), the carrier of R^1))
K7( the carrier of (), the carrier of R^1) is non empty set
K6(K7( the carrier of (), the carrier of R^1)) is non empty set
Q is Element of the carrier of M
(M,P) . Q is set
x1 is Element of the carrier of M
(M,P) . x1 is set
dist (Q,x1) is V11() real ext-real Element of REAL
x2 is V11() real ext-real Element of REAL
z is V11() real ext-real Element of REAL
x2 - z is V11() real ext-real Element of REAL
abs (x2 - z) is V11() real ext-real Element of REAL
(M,Q) is Relation-like the carrier of () -defined the carrier of R^1 -valued Function-like V30( the carrier of (), the carrier of R^1) Element of K6(K7( the carrier of (), the carrier of R^1))
(M,Q) .: P is V47() V48() V49() Element of K6( the carrier of R^1)
(((M,Q) .: P)) is V11() real ext-real Element of REAL
(((M,Q) .: P)) is V47() V48() V49() Element of K6(REAL)
lower_bound (((M,Q) .: P)) is V11() real ext-real Element of REAL
(M,x1) is Relation-like the carrier of () -defined the carrier of R^1 -valued Function-like V30( the carrier of (), the carrier of R^1) Element of K6(K7( the carrier of (), the carrier of R^1))
(M,x1) .: P is V47() V48() V49() Element of K6( the carrier of R^1)
(((M,x1) .: P)) is V11() real ext-real Element of REAL
(((M,x1) .: P)) is V47() V48() V49() Element of K6(REAL)
lower_bound (((M,x1) .: P)) is V11() real ext-real Element of REAL
[#] R^1 is non empty non proper V47() V48() V49() Element of K6( the carrier of R^1)

the carrier of () is non empty set
K6( the carrier of ()) is non empty set
P is Element of K6( the carrier of ())
(M,P) is Relation-like the carrier of () -defined the carrier of R^1 -valued Function-like V30( the carrier of (), the carrier of R^1) Element of K6(K7( the carrier of (), the carrier of R^1))
K7( the carrier of (), the carrier of R^1) is non empty set
K6(K7( the carrier of (), the carrier of R^1)) is non empty set
Q is V47() V48() V49() Element of K6( the carrier of R^1)
(M,P) " Q is Element of K6( the carrier of ())
the carrier of M is non empty set
x1 is Element of the carrier of M
(M,x1) is Relation-like the carrier of () -defined the carrier of R^1 -valued Function-like V30( the carrier of (), the carrier of R^1) Element of K6(K7( the carrier of (), the carrier of R^1))
(M,x1) .: P is V47() V48() V49() Element of K6( the carrier of R^1)
(((M,x1) .: P)) is V11() real ext-real Element of REAL
(((M,x1) .: P)) is V47() V48() V49() Element of K6(REAL)
upper_bound (((M,x1) .: P)) is V11() real ext-real Element of REAL
x2 is V11() real ext-real Element of the carrier of RealSpace
(M,P) . x1 is set
the carrier of is non empty set
K6( the carrier of ) is non empty set
z is Element of K6( the carrier of )
y is V11() real ext-real set
Ball (x2,y) is V47() V48() V49() Element of K6( the carrier of RealSpace)
K6( the carrier of RealSpace) is non empty set
c8 is V11() real ext-real Element of REAL
Ball (x1,c8) is Element of K6( the carrier of M)
K6( the carrier of M) is non empty set
(M,P) " z is Element of K6( the carrier of ())
z is set
z is Element of the carrier of M
(M,z) is Relation-like the carrier of () -defined the carrier of R^1 -valued Function-like V30( the carrier of (), the carrier of R^1) Element of K6(K7( the carrier of (), the carrier of R^1))
(M,z) .: P is V47() V48() V49() Element of K6( the carrier of R^1)
(((M,z) .: P)) is V11() real ext-real Element of REAL
(((M,z) .: P)) is V47() V48() V49() Element of K6(REAL)
upper_bound (((M,z) .: P)) is V11() real ext-real Element of REAL
q is V11() real ext-real Element of the carrier of RealSpace
dist (x1,z) is V11() real ext-real Element of REAL
c8 + (dist (x1,z)) is V11() real ext-real Element of REAL
(((M,x1) .: P)) - (((M,z) .: P)) is V11() real ext-real Element of REAL
abs ((((M,x1) .: P)) - (((M,z) .: P))) is V11() real ext-real Element of REAL
(abs ((((M,x1) .: P)) - (((M,z) .: P)))) + (dist (x1,z)) is V11() real ext-real Element of REAL
dist (x2,q) is V11() real ext-real Element of REAL
Ball (x2,c8) is V47() V48() V49() Element of K6( the carrier of RealSpace)
dom (M,P) is Element of K6( the carrier of ())
(M,P) . z is set

the carrier of () is non empty set
K6( the carrier of ()) is non empty set
P is Element of K6( the carrier of ())
Q is Element of K6( the carrier of ())
(M,P) is Relation-like the carrier of () -defined the carrier of R^1 -valued Function-like V30( the carrier of (), the carrier of R^1) Element of K6(K7( the carrier of (), the carrier of R^1))
K7( the carrier of (), the carrier of R^1) is non empty set
K6(K7( the carrier of (), the carrier of R^1)) is non empty set
(M,P) .: Q is V47() V48() V49() Element of K6( the carrier of R^1)
(((M,P) .: Q)) is V11() real ext-real Element of REAL
(((M,P) .: Q)) is V47() V48() V49() Element of K6(REAL)
upper_bound (((M,P) .: Q)) is V11() real ext-real Element of REAL

the carrier of () is non empty set
K6( the carrier of ()) is non empty set
P is Element of K6( the carrier of ())
Q is Element of K6( the carrier of ())
(M,P) is Relation-like the carrier of () -defined the carrier of R^1 -valued Function-like V30( the carrier of (), the carrier of R^1) Element of K6(K7( the carrier of (), the carrier of R^1))
K7( the carrier of (), the carrier of R^1) is non empty set
K6(K7( the carrier of (), the carrier of R^1)) is non empty set
(M,P) .: Q is V47() V48() V49() Element of K6( the carrier of R^1)
(((M,P) .: Q)) is V11() real ext-real Element of REAL
(((M,P) .: Q)) is V47() V48() V49() Element of K6(REAL)
lower_bound (((M,P) .: Q)) is V11() real ext-real Element of REAL

the carrier of () is non empty set
K6( the carrier of ()) is non empty set
P is Element of K6( the carrier of ())
(M,P) is Relation-like the carrier of () -defined the carrier of R^1 -valued Function-like V30( the carrier of (), the carrier of R^1) Element of K6(K7( the carrier of (), the carrier of R^1))
K7( the carrier of (), the carrier of R^1) is non empty set
K6(K7( the carrier of (), the carrier of R^1)) is non empty set
Q is V47() V48() V49() Element of K6( the carrier of R^1)
(M,P) " Q is Element of K6( the carrier of ())
the carrier of M is non empty set
x1 is Element of the carrier of M
(M,P) . x1 is set
the carrier of is non empty set
K6( the carrier of ) is non empty set
(M,x1) is Relation-like the carrier of () -defined the carrier of R^1 -valued Function-like V30( the carrier of (), the carrier of R^1) Element of K6(K7( the carrier of (), the carrier of R^1))
(M,x1) .: P is V47() V48() V49() Element of K6( the carrier of R^1)
(((M,x1) .: P)) is V11() real ext-real Element of REAL
(((M,x1) .: P)) is V47() V48() V49() Element of K6(REAL)
lower_bound (((M,x1) .: P)) is V11() real ext-real Element of REAL
z is V11() real ext-real Element of the carrier of RealSpace
x2 is Element of K6( the carrier of )
y is V11() real ext-real set
Ball (z,y) is V47() V48() V49() Element of K6( the carrier of RealSpace)
K6( the carrier of RealSpace) is non empty set
c8 is V11() real ext-real Element of REAL
Ball (x1,c8) is Element of K6( the carrier of M)
K6( the carrier of M) is non empty set
(M,P) " x2 is Element of K6( the carrier of ())
z is set
z is Element of the carrier of M
(M,z) is Relation-like the carrier of () -defined the carrier of R^1 -valued Function-like V30( the carrier of (), the carrier of R^1) Element of K6(K7( the carrier of (), the carrier of R^1))
(M,z) .: P is V47() V48() V49() Element of K6( the carrier of R^1)
(((M,z) .: P)) is V11() real ext-real Element of REAL
(((M,z) .: P)) is V47() V48() V49() Element of K6(REAL)
lower_bound (((M,z) .: P)) is V11() real ext-real Element of REAL
q is V11() real ext-real Element of the carrier of RealSpace
dist (x1,z) is V11() real ext-real Element of REAL
c8 + (dist (x1,z)) is V11() real ext-real Element of REAL
(((M,x1) .: P)) - (((M,z) .: P)) is V11() real ext-real Element of REAL
abs ((((M,x1) .: P)) - (((M,z) .: P))) is V11() real ext-real Element of REAL
(abs ((((M,x1) .: P)) - (((M,z) .: P)))) + (dist (x1,z)) is V11() real ext-real Element of REAL
dist (z,q) is V11() real ext-real Element of REAL
Ball (z,c8) is V47() V48() V49() Element of K6( the carrier of RealSpace)
dom (M,P) is Element of K6( the carrier of ())
(M,P) . z is set
x2 is V11() real ext-real Element of REAL
Ball (x1,x2) is Element of K6( the carrier of M)
K6( the carrier of M) is non empty set

the carrier of () is non empty set