:: 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 (TOP-REAL 2) is non empty set
K452() is V200() TopStruct
the carrier of K452() is V47() V48() V49() set
RealSpace is non empty strict Reflexive discerning V122() triangle Discerning V200() MetrStruct
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
{} is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real ext-real functional V47() V48() V49() V50() V51() V52() V53() finite V58() FinSequence-membered 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
union {} is epsilon-transitive epsilon-connected ordinal finite set
K7(NAT,REAL) is non empty set
K6(K7(NAT,REAL)) is non empty set
0 is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real ext-real functional V45() V46() V47() V48() V49() V50() V51() V52() V53() finite V58() FinSequence-membered Element of NAT
the carrier of RealSpace is non empty V47() V48() V49() set
TopSpaceMetr RealSpace is non empty strict TopSpace-like TopStruct
the carrier of R^1 is non empty V47() V48() V49() set
real_dist is Relation-like K7(REAL,REAL) -defined REAL -valued Function-like V30(K7(REAL,REAL), REAL ) Element of K6(K7(K7(REAL,REAL),REAL))
MetrStruct(# REAL,real_dist #) is strict MetrStruct
M is Reflexive discerning V122() triangle MetrStruct
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)
c₈ 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
M is Reflexive discerning V122() triangle MetrStruct
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 epsilon-transitive epsilon-connected ordinal natural V11() real ext-real 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)
x1 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
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)
x1 | (Seg P) is Relation-like finite FinSubsequence-like set
y is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
rng y is finite set
c₈ is Element of K6(K6( the carrier of M))
len x1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V45() V46() V47() V48() V49() V50() V51() V52() Element of NAT
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)
(union z) \/ (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)
(union z) \/ (Ball (z,q)) is Element of K6( the carrier of M)
M is Reflexive discerning V122() triangle MetrStruct
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)
Q is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
rng Q is finite set
x1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real 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)
z is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real set
Seg z is V47() V48() V49() V50() V51() V52() finite V71(z) Element of K6(NAT)
y is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
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)
c₈ is Element of K6(K6( the carrier of M))
union c₈ is Element of K6( the carrier of M)
z is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
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 c₈) \/ (Ball (z,q)) is Element of K6( the carrier of M)
z is Element of the carrier of M
z is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
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 c₈) \/ (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 c₈) \/ (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 c₈) \/ (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)
x2 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real set
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
y is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
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)
z is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
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))
z is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
rng z is finite set
dom z is V47() V48() V49() V50() V51() V52() finite Element of K6(NAT)
x2 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real set
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)
x1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real set
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
x2 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like 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
x2 * z is Relation-like finite set
z .: x1 is Element of K6((bool ([#] M)))
K6((bool ([#] M))) is non empty set
c₈ 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
y is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
rng y is finite set
c₈ is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
rng c₈ 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
x2 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like 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
x2 * z is Relation-like finite set
z .: x1 is Element of K6((bool ([#] P)))
K6((bool ([#] P))) is non empty set
c₈ 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
y is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
rng y is finite set
c₈ is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
rng c₈ 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)
y is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
rng y is finite set
c₈ 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 c₈
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 c₈
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(c₈,(bool ([#] P))) is non empty set
K6(K7(c₈,(bool ([#] P)))) is non empty set
z is Relation-like c₈ -defined bool ([#] P) -valued Function-like V30(c₈, bool ([#] P)) Element of K6(K7(c₈,(bool ([#] P))))
z is Element of c₈
z . z is Element of bool ([#] P)
q is Element of c₈
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
y * z is Relation-like finite set
q is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like 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))
c₈ 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))
c₈ 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)
c₈ is set
Q . c₈ is set
z is set
Q " z is Element of K6( the carrier of M)
z is set
Q . y is set
c₈ is Element of the carrier of M
Q . c₈ is Element of the carrier of P
{(Q . c₈)} is non empty finite set
Q " {(Q . c₈)} 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 (TOP-REAL 2), the carrier of R^1) is non empty set
K6(K7( the carrier of (TOP-REAL 2), the carrier of R^1)) is non empty set
K6( the carrier of (TOP-REAL 2)) is non empty set
P is Element of K6( the carrier of (TOP-REAL 2))
M is Relation-like the carrier of (TOP-REAL 2) -defined the carrier of R^1 -valued Function-like V30( the carrier of (TOP-REAL 2), the carrier of R^1) Element of K6(K7( the carrier of (TOP-REAL 2), 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,(Family_open_set 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
c₈ 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,(Family_open_set 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)
c₈ is V11() real ext-real Element of REAL
c₈ - y is V11() real ext-real Element of REAL
c₈ + 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
c₈ - z is V11() real ext-real Element of REAL
abs (c₈ - 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
c₈ - (- 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)
P is Relation-like NAT -defined REAL -valued Function-like V30( NAT , REAL ) Element of K6(K7(NAT,REAL))
rng P is V47() V48() V49() Element of K6(REAL)
lim P is V11() real ext-real Element of 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,(Family_open_set RealSpace) #) is strict TopStruct
y is V11() real ext-real Element of the carrier of RealSpace
c₈ is V11() real ext-real set
Ball (y,c₈) 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)
{ b₁ where b₁ is V11() real ext-real Element of the carrier of RealSpace : not z <= dist (y,b₁) } is set
z is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V45() V46() V47() V48() V49() V50() V51() V52() Element of NAT
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)
P is Relation-like NAT -defined REAL -valued Function-like V30( NAT , REAL ) Element of K6(K7(NAT,REAL))
rng P is V47() V48() V49() Element of K6(REAL)
lim P is V11() real ext-real Element of 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
Q is Relation-like NAT -defined REAL -valued Function-like V30( NAT , REAL ) Element of K6(K7(NAT,REAL))
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
c₈ is Element of the carrier of M
P . c₈ 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
M is non empty Reflexive discerning V122() triangle Discerning MetrStruct
the carrier of M is non empty set
TopSpaceMetr M is non empty strict TopSpace-like TopStruct
the carrier of (TopSpaceMetr M) is non empty set
K7( the carrier of (TopSpaceMetr M), the carrier of R^1) is non empty set
K6(K7( the carrier of (TopSpaceMetr M), 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,(Family_open_set M) #) is strict TopStruct
x1 is Relation-like the carrier of (TopSpaceMetr M) -defined the carrier of R^1 -valued Function-like V30( the carrier of (TopSpaceMetr M), the carrier of R^1) Element of K6(K7( the carrier of (TopSpaceMetr M), 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 (TopSpaceMetr M) -defined the carrier of R^1 -valued Function-like V30( the carrier of (TopSpaceMetr M), the carrier of R^1) Element of K6(K7( the carrier of (TopSpaceMetr M), the carrier of R^1))
x1 is Relation-like the carrier of (TopSpaceMetr M) -defined the carrier of R^1 -valued Function-like V30( the carrier of (TopSpaceMetr M), the carrier of R^1) Element of K6(K7( the carrier of (TopSpaceMetr M), 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,(Family_open_set 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
M is non empty Reflexive discerning V122() triangle Discerning MetrStruct
the carrier of M is non empty set
TopSpaceMetr M is non empty strict TopSpace-like TopStruct
P is Element of the carrier of M
(M,P) is Relation-like the carrier of (TopSpaceMetr M) -defined the carrier of R^1 -valued Function-like V30( the carrier of (TopSpaceMetr M), the carrier of R^1) Element of K6(K7( the carrier of (TopSpaceMetr M), the carrier of R^1))
the carrier of (TopSpaceMetr M) is non empty set
K7( the carrier of (TopSpaceMetr M), the carrier of R^1) is non empty set
K6(K7( the carrier of (TopSpaceMetr M), 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 (TopSpaceMetr M))
K6( the carrier of (TopSpaceMetr M)) 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 (TopSpaceMetr RealSpace) is non empty set
K6( the carrier of (TopSpaceMetr RealSpace)) is non empty set
z is Element of K6( the carrier of (TopSpaceMetr RealSpace))
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
c₈ is V11() real ext-real Element of REAL
Ball (x1,c₈) 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 (TopSpaceMetr M))
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
c₈ + (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,c₈) 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 (TopSpaceMetr M))
[#] R^1 is non empty non proper V47() V48() V49() Element of K6( the carrier of R^1)
M is non empty Reflexive discerning V122() triangle Discerning MetrStruct
the carrier of M is non empty set
TopSpaceMetr M is non empty strict TopSpace-like TopStruct
the carrier of (TopSpaceMetr M) is non empty set
K6( the carrier of (TopSpaceMetr M)) is non empty set
Q is Element of K6( the carrier of (TopSpaceMetr M))
P is Element of the carrier of M
(M,P) is Relation-like the carrier of (TopSpaceMetr M) -defined the carrier of R^1 -valued Function-like V30( the carrier of (TopSpaceMetr M), the carrier of R^1) Element of K6(K7( the carrier of (TopSpaceMetr M), the carrier of R^1))
K7( the carrier of (TopSpaceMetr M), the carrier of R^1) is non empty set
K6(K7( the carrier of (TopSpaceMetr M), 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
M is non empty Reflexive discerning V122() triangle Discerning MetrStruct
the carrier of M is non empty set
TopSpaceMetr M is non empty strict TopSpace-like TopStruct
the carrier of (TopSpaceMetr M) is non empty set
K6( the carrier of (TopSpaceMetr M)) is non empty set
Q is Element of K6( the carrier of (TopSpaceMetr M))
P is Element of the carrier of M
(M,P) is Relation-like the carrier of (TopSpaceMetr M) -defined the carrier of R^1 -valued Function-like V30( the carrier of (TopSpaceMetr M), the carrier of R^1) Element of K6(K7( the carrier of (TopSpaceMetr M), the carrier of R^1))
K7( the carrier of (TopSpaceMetr M), the carrier of R^1) is non empty set
K6(K7( the carrier of (TopSpaceMetr M), 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
M is non empty Reflexive discerning V122() triangle Discerning MetrStruct
TopSpaceMetr M is non empty strict TopSpace-like TopStruct
the carrier of (TopSpaceMetr M) is non empty set
K6( the carrier of (TopSpaceMetr M)) is non empty set
K7( the carrier of (TopSpaceMetr M), the carrier of R^1) is non empty set
K6(K7( the carrier of (TopSpaceMetr M), 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 (TopSpaceMetr M))
Q is Element of the carrier of M
(M,Q) is Relation-like the carrier of (TopSpaceMetr M) -defined the carrier of R^1 -valued Function-like V30( the carrier of (TopSpaceMetr M), the carrier of R^1) Element of K6(K7( the carrier of (TopSpaceMetr M), 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 (TopSpaceMetr M) -defined the carrier of R^1 -valued Function-like V30( the carrier of (TopSpaceMetr M), the carrier of R^1) Element of K6(K7( the carrier of (TopSpaceMetr M), 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 (TopSpaceMetr M) -defined the carrier of R^1 -valued Function-like V30( the carrier of (TopSpaceMetr M), the carrier of R^1) Element of K6(K7( the carrier of (TopSpaceMetr M), 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,(Family_open_set M) #) is strict TopStruct
x1 is Relation-like the carrier of (TopSpaceMetr M) -defined the carrier of R^1 -valued Function-like V30( the carrier of (TopSpaceMetr M), the carrier of R^1) Element of K6(K7( the carrier of (TopSpaceMetr M), 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 (TopSpaceMetr M) -defined the carrier of R^1 -valued Function-like V30( the carrier of (TopSpaceMetr M), the carrier of R^1) Element of K6(K7( the carrier of (TopSpaceMetr M), 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 (TopSpaceMetr M) -defined the carrier of R^1 -valued Function-like V30( the carrier of (TopSpaceMetr M), the carrier of R^1) Element of K6(K7( the carrier of (TopSpaceMetr M), the carrier of R^1))
x1 is Relation-like the carrier of (TopSpaceMetr M) -defined the carrier of R^1 -valued Function-like V30( the carrier of (TopSpaceMetr M), the carrier of R^1) Element of K6(K7( the carrier of (TopSpaceMetr M), 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,(Family_open_set M) #) is strict TopStruct
z is Element of the carrier of M
Q . z is set
(M,z) is Relation-like the carrier of (TopSpaceMetr M) -defined the carrier of R^1 -valued Function-like V30( the carrier of (TopSpaceMetr M), the carrier of R^1) Element of K6(K7( the carrier of (TopSpaceMetr M), 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 (TopSpaceMetr M) -defined the carrier of R^1 -valued Function-like V30( the carrier of (TopSpaceMetr M), the carrier of R^1) Element of K6(K7( the carrier of (TopSpaceMetr M), 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 (TopSpaceMetr M) -defined the carrier of R^1 -valued Function-like V30( the carrier of (TopSpaceMetr M), the carrier of R^1) Element of K6(K7( the carrier of (TopSpaceMetr M), 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 (TopSpaceMetr M) -defined the carrier of R^1 -valued Function-like V30( the carrier of (TopSpaceMetr M), the carrier of R^1) Element of K6(K7( the carrier of (TopSpaceMetr M), 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,(Family_open_set M) #) is strict TopStruct
x1 is Relation-like the carrier of (TopSpaceMetr M) -defined the carrier of R^1 -valued Function-like V30( the carrier of (TopSpaceMetr M), the carrier of R^1) Element of K6(K7( the carrier of (TopSpaceMetr M), 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 (TopSpaceMetr M) -defined the carrier of R^1 -valued Function-like V30( the carrier of (TopSpaceMetr M), the carrier of R^1) Element of K6(K7( the carrier of (TopSpaceMetr M), 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 (TopSpaceMetr M) -defined the carrier of R^1 -valued Function-like V30( the carrier of (TopSpaceMetr M), the carrier of R^1) Element of K6(K7( the carrier of (TopSpaceMetr M), the carrier of R^1))
x1 is Relation-like the carrier of (TopSpaceMetr M) -defined the carrier of R^1 -valued Function-like V30( the carrier of (TopSpaceMetr M), the carrier of R^1) Element of K6(K7( the carrier of (TopSpaceMetr M), 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,(Family_open_set M) #) is strict TopStruct
z is Element of the carrier of M
Q . z is set
(M,z) is Relation-like the carrier of (TopSpaceMetr M) -defined the carrier of R^1 -valued Function-like V30( the carrier of (TopSpaceMetr M), the carrier of R^1) Element of K6(K7( the carrier of (TopSpaceMetr M), 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
M is non empty Reflexive discerning V122() triangle Discerning MetrStruct
TopSpaceMetr M is non empty strict TopSpace-like TopStruct
the carrier of (TopSpaceMetr M) is non empty set
K6( the carrier of (TopSpaceMetr M)) is non empty set
the carrier of M is non empty set
P is Element of K6( the carrier of (TopSpaceMetr M))
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 (TopSpaceMetr M) -defined the carrier of R^1 -valued Function-like V30( the carrier of (TopSpaceMetr M), the carrier of R^1) Element of K6(K7( the carrier of (TopSpaceMetr M), the carrier of R^1))
K7( the carrier of (TopSpaceMetr M), the carrier of R^1) is non empty set
K6(K7( the carrier of (TopSpaceMetr M), 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 (TopSpaceMetr M))
M is non empty Reflexive discerning V122() triangle Discerning MetrStruct
TopSpaceMetr M is non empty strict TopSpace-like TopStruct
the carrier of (TopSpaceMetr M) is non empty set
K6( the carrier of (TopSpaceMetr M)) is non empty set
the carrier of M is non empty set
P is Element of K6( the carrier of (TopSpaceMetr M))
Q is Element of the carrier of M
(M,Q) is Relation-like the carrier of (TopSpaceMetr M) -defined the carrier of R^1 -valued Function-like V30( the carrier of (TopSpaceMetr M), the carrier of R^1) Element of K6(K7( the carrier of (TopSpaceMetr M), the carrier of R^1))
K7( the carrier of (TopSpaceMetr M), the carrier of R^1) is non empty set
K6(K7( the carrier of (TopSpaceMetr M), 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 (TopSpaceMetr M) -defined the carrier of R^1 -valued Function-like V30( the carrier of (TopSpaceMetr M), the carrier of R^1) Element of K6(K7( the carrier of (TopSpaceMetr M), 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 (TopSpaceMetr M)
(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,(Family_open_set M) #) is strict TopStruct
y is Element of the carrier of (TopSpaceMetr M)
(M,x1) . y is V11() real ext-real Element of the carrier of R^1
c₈ is Element of the carrier of M
dist (c₈,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 (c₈,Q) is V11() real ext-real Element of REAL
(dist (c₈,Q)) + (dist (Q,x1)) is V11() real ext-real Element of REAL
(dist (c₈,x1)) - (dist (z,Q)) is V11() real ext-real Element of REAL
((dist (c₈,Q)) + (dist (Q,x1))) - (dist (c₈,Q)) is V11() real ext-real Element of REAL
- (dist (Q,x1)) is V11() real ext-real Element of REAL
- ((dist (c₈,x1)) - (dist (z,Q))) is V11() real ext-real Element of REAL
(M,x1) . c₈ 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 (c₈,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
M is non empty Reflexive discerning V122() triangle Discerning MetrStruct
TopSpaceMetr M is non empty strict TopSpace-like TopStruct
the carrier of (TopSpaceMetr M) is non empty set
K6( the carrier of (TopSpaceMetr M)) is non empty set
the carrier of M is non empty set
P is Element of K6( the carrier of (TopSpaceMetr M))
(M,P) is Relation-like the carrier of (TopSpaceMetr M) -defined the carrier of R^1 -valued Function-like V30( the carrier of (TopSpaceMetr M), the carrier of R^1) Element of K6(K7( the carrier of (TopSpaceMetr M), the carrier of R^1))
K7( the carrier of (TopSpaceMetr M), the carrier of R^1) is non empty set
K6(K7( the carrier of (TopSpaceMetr M), 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 (TopSpaceMetr M) -defined the carrier of R^1 -valued Function-like V30( the carrier of (TopSpaceMetr M), the carrier of R^1) Element of K6(K7( the carrier of (TopSpaceMetr M), 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 (TopSpaceMetr M) -defined the carrier of R^1 -valued Function-like V30( the carrier of (TopSpaceMetr M), the carrier of R^1) Element of K6(K7( the carrier of (TopSpaceMetr M), 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 is non empty Reflexive discerning V122() triangle Discerning MetrStruct
TopSpaceMetr M is non empty strict TopSpace-like TopStruct
the carrier of (TopSpaceMetr M) is non empty set
K6( the carrier of (TopSpaceMetr M)) is non empty set
the carrier of M is non empty set
P is Element of K6( the carrier of (TopSpaceMetr M))
Q is Element of the carrier of M
(M,Q) is Relation-like the carrier of (TopSpaceMetr M) -defined the carrier of R^1 -valued Function-like V30( the carrier of (TopSpaceMetr M), the carrier of R^1) Element of K6(K7( the carrier of (TopSpaceMetr M), the carrier of R^1))
K7( the carrier of (TopSpaceMetr M), the carrier of R^1) is non empty set
K6(K7( the carrier of (TopSpaceMetr M), 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 (TopSpaceMetr M) -defined the carrier of R^1 -valued Function-like V30( the carrier of (TopSpaceMetr M), the carrier of R^1) Element of K6(K7( the carrier of (TopSpaceMetr M), 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 (TopSpaceMetr M)
(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,(Family_open_set M) #) is strict TopStruct
y is Element of the carrier of (TopSpaceMetr M)
(M,x1) . y is V11() real ext-real Element of the carrier of R^1
c₈ is Element of the carrier of M
dist (c₈,x1) is V11() real ext-real Element of REAL
(M,x1) . c₈ 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 (c₈,x1)) - (dist (z,Q)) is V11() real ext-real Element of REAL
- (dist (Q,x1)) is V11() real ext-real Element of REAL
- ((dist (c₈,x1)) - (dist (z,Q))) is V11() real ext-real Element of REAL
(M,Q) . z is set
dist (c₈,Q) is V11() real ext-real Element of REAL
dist (x1,Q) is V11() real ext-real Element of REAL
(dist (c₈,x1)) + (dist (x1,Q)) is V11() real ext-real Element of REAL
(dist (c₈,x1)) + (dist (Q,x1)) is V11() real ext-real Element of REAL
(dist (z,Q)) - (dist (c₈,x1)) is V11() real ext-real Element of REAL
M is non empty Reflexive discerning V122() triangle Discerning MetrStruct
TopSpaceMetr M is non empty strict TopSpace-like TopStruct
the carrier of (TopSpaceMetr M) is non empty set
K6( the carrier of (TopSpaceMetr M)) is non empty set
the carrier of M is non empty set
P is Element of K6( the carrier of (TopSpaceMetr M))
(M,P) is Relation-like the carrier of (TopSpaceMetr M) -defined the carrier of R^1 -valued Function-like V30( the carrier of (TopSpaceMetr M), the carrier of R^1) Element of K6(K7( the carrier of (TopSpaceMetr M), the carrier of R^1))
K7( the carrier of (TopSpaceMetr M), the carrier of R^1) is non empty set
K6(K7( the carrier of (TopSpaceMetr M), 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 (TopSpaceMetr M) -defined the carrier of R^1 -valued Function-like V30( the carrier of (TopSpaceMetr M), the carrier of R^1) Element of K6(K7( the carrier of (TopSpaceMetr M), 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 (TopSpaceMetr M) -defined the carrier of R^1 -valued Function-like V30( the carrier of (TopSpaceMetr M), the carrier of R^1) Element of K6(K7( the carrier of (TopSpaceMetr M), 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)
M is non empty Reflexive discerning V122() triangle Discerning MetrStruct
TopSpaceMetr M is non empty strict TopSpace-like TopStruct
the carrier of (TopSpaceMetr M) is non empty set
K6( the carrier of (TopSpaceMetr M)) is non empty set
P is Element of K6( the carrier of (TopSpaceMetr M))
(M,P) is Relation-like the carrier of (TopSpaceMetr M) -defined the carrier of R^1 -valued Function-like V30( the carrier of (TopSpaceMetr M), the carrier of R^1) Element of K6(K7( the carrier of (TopSpaceMetr M), the carrier of R^1))
K7( the carrier of (TopSpaceMetr M), the carrier of R^1) is non empty set
K6(K7( the carrier of (TopSpaceMetr M), 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 (TopSpaceMetr M))
the carrier of M is non empty set
x1 is Element of the carrier of M
(M,x1) is Relation-like the carrier of (TopSpaceMetr M) -defined the carrier of R^1 -valued Function-like V30( the carrier of (TopSpaceMetr M), the carrier of R^1) Element of K6(K7( the carrier of (TopSpaceMetr M), 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 (TopSpaceMetr RealSpace) is non empty set
K6( the carrier of (TopSpaceMetr RealSpace)) is non empty set
z is Element of K6( the carrier of (TopSpaceMetr RealSpace))
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
c₈ is V11() real ext-real Element of REAL
Ball (x1,c₈) 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 (TopSpaceMetr M))
z is set
z is Element of the carrier of M
(M,z) is Relation-like the carrier of (TopSpaceMetr M) -defined the carrier of R^1 -valued Function-like V30( the carrier of (TopSpaceMetr M), the carrier of R^1) Element of K6(K7( the carrier of (TopSpaceMetr M), 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
c₈ + (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,c₈) is V47() V48() V49() Element of K6( the carrier of RealSpace)
dom (M,P) is Element of K6( the carrier of (TopSpaceMetr M))
(M,P) . z is set
M is non empty Reflexive discerning V122() triangle Discerning MetrStruct
TopSpaceMetr M is non empty strict TopSpace-like TopStruct
the carrier of (TopSpaceMetr M) is non empty set
K6( the carrier of (TopSpaceMetr M)) is non empty set
P is Element of K6( the carrier of (TopSpaceMetr M))
Q is Element of K6( the carrier of (TopSpaceMetr M))
(M,P) is Relation-like the carrier of (TopSpaceMetr M) -defined the carrier of R^1 -valued Function-like V30( the carrier of (TopSpaceMetr M), the carrier of R^1) Element of K6(K7( the carrier of (TopSpaceMetr M), the carrier of R^1))
K7( the carrier of (TopSpaceMetr M), the carrier of R^1) is non empty set
K6(K7( the carrier of (TopSpaceMetr M), 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
M is non empty Reflexive discerning V122() triangle Discerning MetrStruct
TopSpaceMetr M is non empty strict TopSpace-like TopStruct
the carrier of (TopSpaceMetr M) is non empty set
K6( the carrier of (TopSpaceMetr M)) is non empty set
P is Element of K6( the carrier of (TopSpaceMetr M))
Q is Element of K6( the carrier of (TopSpaceMetr M))
(M,P) is Relation-like the carrier of (TopSpaceMetr M) -defined the carrier of R^1 -valued Function-like V30( the carrier of (TopSpaceMetr M), the carrier of R^1) Element of K6(K7( the carrier of (TopSpaceMetr M), the carrier of R^1))
K7( the carrier of (TopSpaceMetr M), the carrier of R^1) is non empty set
K6(K7( the carrier of (TopSpaceMetr M), 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
M is non empty Reflexive discerning V122() triangle Discerning MetrStruct
TopSpaceMetr M is non empty strict TopSpace-like TopStruct
the carrier of (TopSpaceMetr M) is non empty set
K6( the carrier of (TopSpaceMetr M)) is non empty set
P is Element of K6( the carrier of (TopSpaceMetr M))
(M,P) is Relation-like the carrier of (TopSpaceMetr M) -defined the carrier of R^1 -valued Function-like V30( the carrier of (TopSpaceMetr M), the carrier of R^1) Element of K6(K7( the carrier of (TopSpaceMetr M), the carrier of R^1))
K7( the carrier of (TopSpaceMetr M), the carrier of R^1) is non empty set
K6(K7( the carrier of (TopSpaceMetr M), 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 (TopSpaceMetr M))
the carrier of M is non empty set
x1 is Element of the carrier of M
(M,P) . x1 is set
the carrier of (TopSpaceMetr RealSpace) is non empty set
K6( the carrier of (TopSpaceMetr RealSpace)) is non empty set
(M,x1) is Relation-like the carrier of (TopSpaceMetr M) -defined the carrier of R^1 -valued Function-like V30( the carrier of (TopSpaceMetr M), the carrier of R^1) Element of K6(K7( the carrier of (TopSpaceMetr M), 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 (TopSpaceMetr RealSpace))
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
c₈ is V11() real ext-real Element of REAL
Ball (x1,c₈) 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 (TopSpaceMetr M))
z is set
z is Element of the carrier of M
(M,z) is Relation-like the carrier of (TopSpaceMetr M) -defined the carrier of R^1 -valued Function-like V30( the carrier of (TopSpaceMetr M), the carrier of R^1) Element of K6(K7( the carrier of (TopSpaceMetr M), 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
c₈ + (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,c₈) is V47() V48() V49() Element of K6( the carrier of RealSpace)
dom (M,P) is Element of K6( the carrier of (TopSpaceMetr M))
(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
M is non empty Reflexive discerning V122() triangle Discerning MetrStruct
TopSpaceMetr M is non empty strict TopSpace-like TopStruct
the carrier of (TopSpaceMetr M) is non empty set
K6( the carrier of (TopSpaceMetr M)) is non empty set
P is Element of K6( the carrier of (TopSpaceMetr M))
Q is Element of K6( the carrier of (TopSpaceMetr M))
(M,P) is Relation-like the carrier of (TopSpaceMetr M) -defined the carrier of R^1 -valued Function-like V30( the carrier of (TopSpaceMetr M), the carrier of R^1) Element of K6(K7( the carrier of (TopSpaceMetr M), the carrier of R^1))
K7( the carrier of (TopSpaceMetr M), the carrier of R^1) is non empty set
K6(K7( the carrier of (TopSpaceMetr M), 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
M is non empty Reflexive discerning V122() triangle Discerning MetrStruct
TopSpaceMetr M is non empty strict TopSpace-like TopStruct
the carrier of (TopSpaceMetr M) is non empty set
K6( the carrier of (TopSpaceMetr M)) is non empty set
P is Element of K6( the carrier of (TopSpaceMetr M))
Q is Element of K6( the carrier of (TopSpaceMetr M))
(M,P) is Relation-like the carrier of (TopSpaceMetr M) -defined the carrier of R^1 -valued Function-like V30( the carrier of (TopSpaceMetr M), the carrier of R^1) Element of K6(K7( the carrier of (TopSpaceMetr M), the carrier of R^1))
K7( the carrier of (TopSpaceMetr M), the carrier of R^1) is non empty set
K6(K7( the carrier of (TopSpaceMetr M), 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
M is non empty Reflexive discerning V122() triangle Discerning MetrStruct
TopSpaceMetr M is non empty strict TopSpace-like TopStruct
the carrier of (TopSpaceMetr M) is non empty set
K6( the carrier of (TopSpaceMetr M)) is non empty set
P is Element of K6( the carrier of (TopSpaceMetr M))
(M,P) is Relation-like the carrier of (TopSpaceMetr M) -defined the carrier of R^1 -valued Function-like V30( the carrier of (TopSpaceMetr M), the carrier of R^1) Element of K6(K7( the carrier of (TopSpaceMetr M), the carrier of R^1))
K7( the carrier of (TopSpaceMetr M), the carrier of R^1) is non empty set
K6(K7( the carrier of (TopSpaceMetr M), the carrier of R^1)) is non empty set
Q is Element of K6( the carrier of (TopSpaceMetr M))
(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
(((M,P) .: Q)) is V11() real ext-real Element of REAL
upper_bound (((M,P) .: Q)) is V11() real ext-real Element of REAL
(M,P) is Relation-like the carrier of (TopSpaceMetr M) -defined the carrier of R^1 -valued Function-like V30( the carrier of (TopSpaceMetr M), the carrier of R^1) Element of K6(K7( the carrier of (TopSpaceMetr M), the carrier of R^1))
(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
(((M,P) .: Q)) is V11() real ext-real Element of REAL
upper_bound (((M,P) .: Q)) is V11() real ext-real Element of REAL
M is non empty Reflexive discerning V122() triangle Discerning MetrStruct
TopSpaceMetr M is non empty strict TopSpace-like TopStruct
the carrier of (TopSpaceMetr M) is non empty set
K6( the carrier of (TopSpaceMetr M)) is non empty set
the carrier of M is non empty set
P is Element of K6( the carrier of (TopSpaceMetr M))
Q is Element of K6( the carrier of (TopSpaceMetr M))
(M,P,Q) is V11() real ext-real Element of REAL
(M,P) is Relation-like the carrier of (TopSpaceMetr M) -defined the carrier of R^1 -valued Function-like V30( the carrier of (TopSpaceMetr M), the carrier of R^1) Element of K6(K7( the carrier of (TopSpaceMetr M), the carrier of R^1))
K7( the carrier of (TopSpaceMetr M), the carrier of R^1) is non empty set
K6(K7( the carrier of (TopSpaceMetr M), 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
x1 is Element of the carrier of (TopSpaceMetr M)
(M,P) . x1 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,(Family_open_set M) #) is strict TopStruct
x2 is Element of the carrier of M
(M,x2) is Relation-like the carrier of (TopSpaceMetr M) -defined the carrier of R^1 -valued Function-like V30( the carrier of (TopSpaceMetr M), the carrier of R^1) Element of K6(K7( the carrier of (TopSpaceMetr M), 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
z is Element of the carrier of (TopSpaceMetr M)
(M,x2) . z is V11() real ext-real Element of the carrier of R^1
y is Element of the carrier of M
dist (y,x2) is V11() real ext-real Element of REAL
(M,x2) . y is set
M is non empty Reflexive discerning V122() triangle Discerning MetrStruct
TopSpaceMetr M is non empty strict TopSpace-like TopStruct
the carrier of (TopSpaceMetr M) is non empty set
K6( the carrier of (TopSpaceMetr M)) is non empty set
the carrier of M is non empty set
P is Element of K6( the carrier of (TopSpaceMetr M))
Q is Element of K6( the carrier of (TopSpaceMetr M))
(M,P,Q) is V11() real ext-real Element of REAL
(M,P) is Relation-like the carrier of (TopSpaceMetr M) -defined the carrier of R^1 -valued Function-like V30( the carrier of (TopSpaceMetr M), the carrier of R^1) Element of K6(K7( the carrier of (TopSpaceMetr M), the carrier of R^1))
K7( the carrier of (TopSpaceMetr M), the carrier of R^1) is non empty set
K6(K7( the carrier of (TopSpaceMetr M), 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
x1 is Element of the carrier of (TopSpaceMetr M)
(M,P) . x1 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,(Family_open_set M) #) is strict TopStruct
x2 is Element of the carrier of M
(M,x2) is Relation-like the carrier of (TopSpaceMetr M) -defined the carrier of R^1 -valued Function-like V30( the carrier of (TopSpaceMetr M), the carrier of R^1) Element of K6(K7( the carrier of (TopSpaceMetr M), 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
z is Element of the carrier of (TopSpaceMetr M)
(M,x2) . z is V11() real ext-real Element of the carrier of R^1
y is Element of the carrier of M
dist (y,x2) is V11() real ext-real Element of REAL
(M,x2) . y is set
M is non empty Reflexive discerning V122() triangle Discerning MetrStruct
TopSpaceMetr M is non empty strict TopSpace-like TopStruct
the carrier of (TopSpaceMetr M) is non empty set
K6( the carrier of (TopSpaceMetr M)) is non empty set
the carrier of M is non empty set
P is Element of K6( the carrier of (TopSpaceMetr M))
Q is Element of K6( the carrier of (TopSpaceMetr M))
(M,P,Q) is V11() real ext-real Element of REAL
(M,P) is Relation-like the carrier of (TopSpaceMetr M) -defined the carrier of R^1 -valued Function-like V30( the carrier of (TopSpaceMetr M), the carrier of R^1) Element of K6(K7( the carrier of (TopSpaceMetr M), the carrier of R^1))
K7( the carrier of (TopSpaceMetr M), the carrier of R^1) is non empty set
K6(K7( the carrier of (TopSpaceMetr M), 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
x1 is Element of the carrier of (TopSpaceMetr M)
(M,P) . x1 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,(Family_open_set M) #) is strict TopStruct
x2 is Element of the carrier of M
(M,x2) is Relation-like the carrier of (TopSpaceMetr M) -defined the carrier of R^1 -valued Function-like V30( the carrier of (TopSpaceMetr M), the carrier of R^1) Element of K6(K7( the carrier of (TopSpaceMetr M), 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
z is Element of the carrier of (TopSpaceMetr M)
(M,x2) . z is V11() real ext-real Element of the carrier of R^1
y is Element of the carrier of M
dist (y,x2) is V11() real ext-real Element of REAL
(M,x2) . y is set
M is non empty Reflexive discerning V122() triangle Discerning MetrStruct
TopSpaceMetr M is non empty strict TopSpace-like TopStruct
the carrier of (TopSpaceMetr M) is non empty set
K6( the carrier of (TopSpaceMetr M)) is non empty set
the carrier of M is non empty set
P is Element of K6( the carrier of (TopSpaceMetr M))
Q is Element of K6( the carrier of (TopSpaceMetr M))
(M,P,Q) is V11() real ext-real Element of REAL
(M,P) is Relation-like the carrier of (TopSpaceMetr M) -defined the carrier of R^1 -valued Function-like V30( the carrier of (TopSpaceMetr M), the carrier of R^1) Element of K6(K7( the carrier of (TopSpaceMetr M), the carrier of R^1))
K7( the carrier of (TopSpaceMetr M), the carrier of R^1) is non empty set
K6(K7( the carrier of (TopSpaceMetr M), 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
x1 is Element of the carrier of (TopSpaceMetr M)
(M,P) . x1 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,(Family_open_set M) #) is strict TopStruct
x2 is Element of the carrier of M
(M,x2) is Relation-like the carrier of (TopSpaceMetr M) -defined the carrier of R^1 -valued Function-like V30( the carrier of (TopSpaceMetr M), the carrier of R^1) Element of K6(K7( the carrier of (TopSpaceMetr M), 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
z is Element of the carrier of (TopSpaceMetr M)
(M,x2) . z is V11() real ext-real Element of the carrier of R^1
y is Element of the carrier of M
dist (y,x2) is V11() real ext-real Element of REAL
(M,x2) . y is set
M is non empty Reflexive discerning V122() triangle Discerning MetrStruct
TopSpaceMetr M is non empty strict TopSpace-like TopStruct
the carrier of (TopSpaceMetr M) is non empty set
K6( the carrier of (TopSpaceMetr M)) is non empty set
the carrier of M is non empty set
P is Element of K6( the carrier of (TopSpaceMetr M))
Q is Element of K6( the carrier of (TopSpaceMetr M))
(M,P,Q) is V11() real ext-real Element of REAL
(M,P) is Relation-like the carrier of (TopSpaceMetr M) -defined the carrier of R^1 -valued Function-like V30( the carrier of (TopSpaceMetr M), the carrier of R^1) Element of K6(K7( the carrier of (TopSpaceMetr M), the carrier of R^1))
K7( the carrier of (TopSpaceMetr M), the carrier of R^1) is non empty set
K6(K7( the carrier of (TopSpaceMetr M), 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
(M,P,Q) is V11() real ext-real Element of REAL
(M,P) is Relation-like the carrier of (TopSpaceMetr M) -defined the carrier of R^1 -valued Function-like V30( the carrier of (TopSpaceMetr M), the carrier of R^1) Element of K6(K7( the carrier of (TopSpaceMetr M), the carrier of R^1))
(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
x1 is Element of the carrier of M
x2 is Element of the carrier of M
dist (x1,x2) is V11() real ext-real Element of REAL
(M,P) . x2 is set
z is V11() real ext-real Element of REAL
dom (M,P) is Element of K6( the carrier of (TopSpaceMetr M))
(M,P) . x2 is set
y is V11() real ext-real Element of REAL
dom (M,P) is Element of K6( the carrier of (TopSpaceMetr M))
(M,x2) is Relation-like the carrier of (TopSpaceMetr M) -defined the carrier of R^1 -valued Function-like V30( the carrier of (TopSpaceMetr M), the carrier of R^1) Element of K6(K7( the carrier of (TopSpaceMetr M), 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
(((M,x2) .: P)) is V11() real ext-real Element of REAL
upper_bound (((M,x2) .: P)) is V11() real ext-real Element of REAL