:: FRECHET semantic presentation

REAL is non empty V33() V34() V35() V39() V43() set
NAT is non empty epsilon-transitive epsilon-connected ordinal V33() V34() V35() V36() V37() V38() V39() Element of K19(REAL)
K19(REAL) is non empty set
COMPLEX is non empty V33() V39() V43() set
NAT is non empty epsilon-transitive epsilon-connected ordinal V33() V34() V35() V36() V37() V38() V39() set
K19(NAT) is non empty set
1 is non empty epsilon-transitive epsilon-connected ordinal natural V28() real ext-real positive non negative V33() V34() V35() V36() V37() V38() Element of NAT
K20(1,1) is Relation-like non empty set
K19(K20(1,1)) is non empty set
K20(K20(1,1),1) is Relation-like non empty set
K19(K20(K20(1,1),1)) is non empty set
K20(K20(1,1),REAL) is Relation-like non empty set
K19(K20(K20(1,1),REAL)) is non empty set
K20(REAL,REAL) is Relation-like non empty set
K20(K20(REAL,REAL),REAL) is Relation-like non empty set
K19(K20(K20(REAL,REAL),REAL)) is non empty set
2 is non empty epsilon-transitive epsilon-connected ordinal natural V28() real ext-real positive non negative V33() V34() V35() V36() V37() V38() Element of NAT
K20(2,2) is Relation-like non empty set
K20(K20(2,2),REAL) is Relation-like non empty set
K19(K20(K20(2,2),REAL)) is non empty set
K320() is V125() TopStruct
the carrier of K320() is V33() V34() V35() set
RealSpace is non empty strict Reflexive discerning V88() triangle Discerning V125() MetrStruct
R^1 is non empty strict TopSpace-like V125() TopStruct
TopSpaceMetr RealSpace is non empty strict TopSpace-like TopStruct
{} is Relation-like non-empty empty-yielding Function-like one-to-one constant functional empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V28() real ext-real non positive non negative V33() V34() V35() V36() V37() V38() V39() set
the Relation-like non-empty empty-yielding Function-like one-to-one constant functional empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V28() real ext-real non positive non negative V33() V34() V35() V36() V37() V38() V39() set is Relation-like non-empty empty-yielding Function-like one-to-one constant functional empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V28() real ext-real non positive non negative V33() V34() V35() V36() V37() V38() V39() set
union {} is epsilon-transitive epsilon-connected ordinal set
0 is Relation-like non-empty empty-yielding Function-like one-to-one constant functional empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V28() real ext-real non positive non negative V33() V34() V35() V36() V37() V38() V39() Element of NAT
the carrier of R^1 is non empty V33() V34() V35() set
real_dist is Relation-like K20(REAL,REAL) -defined REAL -valued Function-like V18(K20(REAL,REAL), REAL ) Element of K19(K20(K20(REAL,REAL),REAL))
MetrStruct(# REAL,real_dist #) is strict MetrStruct
{{}} is functional non empty V33() V34() V35() V36() V37() V38() set
f is V28() real ext-real Element of REAL
1 / f is V28() real ext-real Element of REAL
K106(f) is V28() real ext-real set
K104(1,K106(f)) is V28() real ext-real set
g is epsilon-transitive epsilon-connected ordinal natural V28() real ext-real non negative V33() V34() V35() V36() V37() V38() Element of NAT
1 / g is V28() real ext-real non negative Element of REAL
K106(g) is V28() real ext-real non negative set
K104(1,K106(g)) is V28() real ext-real non negative set
1 / (1 / f) is V28() real ext-real Element of REAL
K106((1 / f)) is V28() real ext-real set
K104(1,K106((1 / f))) is V28() real ext-real set
f is non empty 1-sorted
the carrier of f is non empty set
K20(NAT, the carrier of f) is Relation-like non empty set
K19(K20(NAT, the carrier of f)) is non empty set
g is Relation-like NAT -defined the carrier of f -valued Function-like V18( NAT , the carrier of f) Element of K19(K20(NAT, the carrier of f))
rng g is Element of K19( the carrier of f)
K19( the carrier of f) is non empty set
f is non empty 1-sorted
the carrier of f is non empty set
K20(NAT, the carrier of f) is Relation-like non empty set
K19(K20(NAT, the carrier of f)) is non empty set
g is 1-sorted
the carrier of g is set
K20(NAT, the carrier of g) is Relation-like set
K19(K20(NAT, the carrier of g)) is non empty set
x is Relation-like NAT -defined the carrier of f -valued Function-like V18( NAT , the carrier of f) Element of K19(K20(NAT, the carrier of f))
rng x is Element of K19( the carrier of f)
K19( the carrier of f) is non empty set
dom x is V33() V34() V35() V36() V37() V38() Element of K19(NAT)
K19(NAT) is non empty set
f is non empty TopSpace-like TopStruct
the carrier of f is non empty set
K19( the carrier of f) is non empty set
K19(K19( the carrier of f)) is non empty set
g is Element of the carrier of f
x is open g -quasi_basis Element of K19(K19( the carrier of f))
the topology of f is non empty Element of K19(K19( the carrier of f))
[#] f is non empty non proper closed Element of K19( the carrier of f)
S9 is non empty TopStruct
the carrier of S9 is non empty set
K19( the carrier of S9) is non empty set
S is Element of K19( the carrier of S9)
f is non empty TopSpace-like TopStruct
the carrier of f is non empty set
g is Element of the carrier of f
K19( the carrier of f) is non empty set
K19(K19( the carrier of f)) is non empty set
x is open g -quasi_basis Element of K19(K19( the carrier of f))
f is TopStruct
the carrier of f is set
K19( the carrier of f) is non empty set
[#] f is non proper Element of K19( the carrier of f)
g is Element of K19( the carrier of f)
([#] f) \ g is Element of K19( the carrier of f)
([#] f) \ (([#] f) \ g) is Element of K19( the carrier of f)
([#] f) \ (([#] f) \ g) is Element of K19( the carrier of f)
f is TopSpace-like TopStruct
the carrier of f is set
K19( the carrier of f) is non empty set
g is Element of K19( the carrier of f)
x is Element of K19( the carrier of f)
g \ x is Element of K19( the carrier of f)
[#] f is non proper closed Element of K19( the carrier of f)
([#] f) \ x is Element of K19( the carrier of f)
g /\ (([#] f) \ x) is Element of K19( the carrier of f)
g /\ ([#] f) is Element of K19( the carrier of f)
g /\ x is Element of K19( the carrier of f)
(g /\ ([#] f)) \ (g /\ x) is Element of K19( the carrier of f)
f is TopStruct
{} f is Relation-like non-empty empty-yielding Function-like one-to-one constant functional empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V28() real ext-real non positive non negative V33() V34() V35() V36() V37() V38() V39() Element of K19( the carrier of f)
the carrier of f is set
K19( the carrier of f) is non empty set
[#] f is non proper Element of K19( the carrier of f)
K19(K19( the carrier of f)) is non empty set
the topology of f is Element of K19(K19( the carrier of f))
g is Element of K19( the carrier of f)
x is Element of K19( the carrier of f)
g /\ x is Element of K19( the carrier of f)
S9 is Element of K19( the carrier of f)
([#] f) \ S9 is Element of K19( the carrier of f)
a is Element of K19( the carrier of f)
([#] f) \ a is Element of K19( the carrier of f)
(([#] f) \ a) \/ (([#] f) \ S9) is Element of K19( the carrier of f)
a /\ S9 is Element of K19( the carrier of f)
([#] f) \ (a /\ S9) is Element of K19( the carrier of f)
g is Element of K19(K19( the carrier of f))
union g is Element of K19( the carrier of f)
([#] f) \ ({} f) is Element of K19( the carrier of f)
COMPLEMENT g is Element of K19(K19( the carrier of f))
S9 is Element of K19( the carrier of f)
([#] f) \ S9 is Element of K19( the carrier of f)
S9 is Element of K19( the carrier of f)
S9 ` is Element of K19( the carrier of f)
the carrier of f \ S9 is set
x is Element of K19(K19( the carrier of f))
([#] f) \ (S9 `) is Element of K19( the carrier of f)
a is Element of K19(K19( the carrier of f))
meet a is Element of K19( the carrier of f)
x is Element of K19(K19( the carrier of f))
union x is Element of K19( the carrier of f)
(union x) ` is Element of K19( the carrier of f)
the carrier of f \ (union x) is set
([#] f) \ (union g) is Element of K19( the carrier of f)
([#] f) \ ({} f) is Element of K19( the carrier of f)
f is TopSpace-like TopStruct
the carrier of f is set
g is non empty TopStruct
the carrier of g is non empty set
K20( the carrier of f, the carrier of g) is Relation-like set
K19(K20( the carrier of f, the carrier of g)) is non empty set
K19( the carrier of g) is non empty set
x is Relation-like the carrier of f -defined the carrier of g -valued Function-like V18( the carrier of f, the carrier of g) Element of K19(K20( the carrier of f, the carrier of g))
a is Element of K19( the carrier of g)
S9 is Element of K19( the carrier of g)
a \/ S9 is Element of K19( the carrier of g)
x " a is Element of K19( the carrier of f)
K19( the carrier of f) is non empty set
x " S9 is Element of K19( the carrier of f)
(x " a) \/ (x " S9) is Element of K19( the carrier of f)
x " (a \/ S9) is Element of K19( the carrier of f)
{} f is Relation-like non-empty empty-yielding Function-like one-to-one constant functional empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V28() real ext-real non positive non negative V33() V34() V35() V36() V37() V38() V39() closed Element of K19( the carrier of f)
K19( the carrier of f) is non empty set
x " {} is Relation-like non-empty empty-yielding Function-like one-to-one constant functional empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V28() real ext-real non positive non negative V33() V34() V35() V36() V37() V38() V39() closed Element of K19( the carrier of f)
{} g is Relation-like non-empty empty-yielding Function-like one-to-one constant functional empty proper epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V28() real ext-real non positive non negative V33() V34() V35() V36() V37() V38() V39() Element of K19( the carrier of g)
K19(K19( the carrier of g)) is non empty set
a is Element of K19(K19( the carrier of g))
meet a is Element of K19( the carrier of g)
{ (x " b₁) where b₁ is Element of K19( the carrier of g) : b₁ in a } is set
the Element of a is Element of a
S is set
S is Element of K19( the carrier of g)
U1 is Element of K19( the carrier of g)
x " U1 is Element of K19( the carrier of f)
bool the carrier of f is non empty Element of K19(K19( the carrier of f))
K19(K19( the carrier of f)) is non empty set
O is set
n is Element of K19( the carrier of g)
x " n is Element of K19( the carrier of f)
O is Element of K19(K19( the carrier of f))
meet O is Element of K19( the carrier of f)
x " (meet a) is Element of K19( the carrier of f)
n is set
x . n is set
m is set
S9 is Element of K19( the carrier of g)
x " S9 is Element of K19( the carrier of f)
dom x is Element of K19( the carrier of f)
n is Element of K19( the carrier of f)
m is Element of K19( the carrier of g)
x " m is Element of K19( the carrier of f)
n is set
x . n is set
dom x is Element of K19( the carrier of f)
m is set
S9 is Element of K19( the carrier of g)
x " S9 is Element of K19( the carrier of f)
[#] g is non empty non proper Element of K19( the carrier of g)
x " ([#] g) is Element of K19( the carrier of f)
[#] f is non proper closed Element of K19( the carrier of f)
the carrier of RealSpace is non empty V33() V34() V35() set
f is V28() real ext-real Element of the carrier of RealSpace
g is V28() real ext-real Element of REAL
Ball (f,g) is V33() V34() V35() Element of K19( the carrier of RealSpace)
K19( the carrier of RealSpace) is non empty set
f - g is V28() real ext-real Element of REAL
K105(g) is V28() real ext-real set
K103(f,K105(g)) is V28() real ext-real set
f + g is V28() real ext-real Element of REAL
].(f - g),(f + g).[ is V33() V34() V35() Element of K19(REAL)
a is set
S9 is V28() real ext-real Element of the carrier of RealSpace
dist (f,S9) is V28() real ext-real Element of REAL
x is V28() real ext-real Element of REAL
S is V28() real ext-real Element of REAL
real_dist . (x,S) is V28() real ext-real Element of REAL
x - S is V28() real ext-real Element of REAL
K105(S) is V28() real ext-real set
K103(x,K105(S)) is V28() real ext-real set
abs (x - S) is V28() real ext-real Element of REAL
S - x is V28() real ext-real Element of REAL
K105(x) is V28() real ext-real set
K103(S,K105(x)) is V28() real ext-real set
- (S - x) is V28() real ext-real Element of REAL
abs (- (S - x)) is V28() real ext-real Element of REAL
abs (S - x) is V28() real ext-real Element of REAL
a is set
S9 is V28() real ext-real Element of REAL
S9 - f is V28() real ext-real Element of REAL
K105(f) is V28() real ext-real set
K103(S9,K105(f)) is V28() real ext-real set
abs (S9 - f) is V28() real ext-real Element of REAL
- (S9 - f) is V28() real ext-real Element of REAL
abs (- (S9 - f)) is V28() real ext-real Element of REAL
f - S9 is V28() real ext-real Element of REAL
K105(S9) is V28() real ext-real set
K103(f,K105(S9)) is V28() real ext-real set
abs (f - S9) is V28() real ext-real Element of REAL
x is V28() real ext-real Element of REAL
real_dist . (x,S9) is V28() real ext-real Element of REAL
S is V28() real ext-real Element of the carrier of RealSpace
U1 is V28() real ext-real Element of the carrier of RealSpace
dist (S,U1) is V28() real ext-real Element of REAL
K19( the carrier of R^1) is non empty set
f is V33() V34() V35() Element of K19( the carrier of R^1)
K19( the carrier of RealSpace) is non empty set
the topology of R^1 is non empty Element of K19(K19( the carrier of R^1))
K19(K19( the carrier of R^1)) is non empty set
Family_open_set RealSpace is Element of K19(K19( the carrier of RealSpace))
K19(K19( the carrier of RealSpace)) is non empty set
x is V33() V34() V35() Element of K19( the carrier of R^1)
a is V28() real ext-real Element of REAL
S9 is V28() real ext-real Element of REAL
S is V28() real ext-real Element of the carrier of RealSpace
U1 is V28() real ext-real Element of REAL
Ball (S,U1) is V33() V34() V35() Element of K19( the carrier of RealSpace)
a - U1 is V28() real ext-real Element of REAL
K105(U1) is V28() real ext-real set
K103(a,K105(U1)) is V28() real ext-real set
a + U1 is V28() real ext-real Element of REAL
].(a - U1),(a + U1).[ is V33() V34() V35() Element of K19(REAL)
g is V33() V34() V35() Element of K19( the carrier of RealSpace)
x is V28() real ext-real Element of the carrier of RealSpace
a is V28() real ext-real Element of REAL
S9 is V28() real ext-real Element of REAL
a - S9 is V28() real ext-real Element of REAL
K105(S9) is V28() real ext-real set
K103(a,K105(S9)) is V28() real ext-real set
a + S9 is V28() real ext-real Element of REAL
].(a - S9),(a + S9).[ is V33() V34() V35() Element of K19(REAL)
Ball (x,S9) is V33() V34() V35() Element of K19( the carrier of RealSpace)
Family_open_set RealSpace is Element of K19(K19( the carrier of RealSpace))
K19(K19( the carrier of RealSpace)) is non empty set
the topology of R^1 is non empty Element of K19(K19( the carrier of R^1))
K19(K19( the carrier of R^1)) is non empty set
K20(NAT, the carrier of R^1) is Relation-like non empty set
K19(K20(NAT, the carrier of R^1)) is non empty set
4 is non empty epsilon-transitive epsilon-connected ordinal natural V28() real ext-real positive non negative V33() V34() V35() V36() V37() V38() Element of NAT
1 / 4 is V28() real ext-real non negative Element of REAL
K106(4) is non empty V28() real ext-real positive non negative set
K104(1,K106(4)) is V28() real ext-real non negative set
f is Relation-like NAT -defined the carrier of R^1 -valued Function-like V18( NAT , the carrier of R^1) Element of K19(K20(NAT, the carrier of R^1))
rng f is V33() V34() V35() Element of K19( the carrier of R^1)
g is V33() V34() V35() Element of K19( the carrier of R^1)
g ` is V33() V34() V35() Element of K19( the carrier of R^1)
the carrier of R^1 \ g is V33() V34() V35() set
x is V28() real ext-real Element of the carrier of RealSpace
a is V28() real ext-real Element of REAL
a - (1 / 4) is V28() real ext-real Element of REAL
K105((1 / 4)) is V28() real ext-real non positive set
K103(a,K105((1 / 4))) is V28() real ext-real set
a + (1 / 4) is V28() real ext-real Element of REAL
].(a - (1 / 4)),(a + (1 / 4)).[ is V33() V34() V35() Element of K19(REAL)
].(a - (1 / 4)),(a + (1 / 4)).[ /\ g is V33() V34() V35() Element of K19( the carrier of R^1)
Ball (x,(1 / 4)) is V33() V34() V35() Element of K19( the carrier of RealSpace)
K19( the carrier of RealSpace) is non empty set
(g `) ` is V33() V34() V35() Element of K19( the carrier of R^1)
the carrier of R^1 \ (g `) is V33() V34() V35() set
(Ball (x,(1 / 4))) /\ ((g `) `) is V33() V34() V35() Element of K19( the carrier of R^1)
S9 is V33() V34() V35() Element of K19( the carrier of R^1)
a is V28() real ext-real Element of REAL
a - (1 / 4) is V28() real ext-real Element of REAL
K105((1 / 4)) is V28() real ext-real non positive set
K103(a,K105((1 / 4))) is V28() real ext-real set
a + (1 / 4) is V28() real ext-real Element of REAL
].(a - (1 / 4)),(a + (1 / 4)).[ is V33() V34() V35() Element of K19(REAL)
].(a - (1 / 4)),(a + (1 / 4)).[ /\ g is V33() V34() V35() Element of K19( the carrier of R^1)
the V28() real ext-real Element of ].(a - (1 / 4)),(a + (1 / 4)).[ /\ g is V28() real ext-real Element of ].(a - (1 / 4)),(a + (1 / 4)).[ /\ g
dom f is V33() V34() V35() V36() V37() V38() Element of K19(NAT)
K19(NAT) is non empty set
S is V28() real ext-real Element of REAL
U1 is set
f . U1 is set
a - S is V28() real ext-real Element of REAL
K105(S) is V28() real ext-real set
K103(a,K105(S)) is V28() real ext-real set
abs (a - S) is V28() real ext-real Element of REAL
n is V28() real ext-real Element of REAL
Ball (x,n) is V33() V34() V35() Element of K19( the carrier of RealSpace)
K19( the carrier of RealSpace) is non empty set
S - a is V28() real ext-real Element of REAL
K105(a) is V28() real ext-real set
K103(S,K105(a)) is V28() real ext-real set
abs (S - a) is V28() real ext-real Element of REAL
- (a - S) is V28() real ext-real Element of REAL
abs (- (a - S)) is V28() real ext-real Element of REAL
S9 is set
z is set
f . z is set
O is epsilon-transitive epsilon-connected ordinal natural V28() real ext-real non negative V33() V34() V35() V36() V37() V38() Element of NAT
z9 is epsilon-transitive epsilon-connected ordinal natural V28() real ext-real non negative V33() V34() V35() V36() V37() V38() Element of NAT
- (S - a) is V28() real ext-real Element of REAL
0 + (- (S - a)) is V28() real ext-real Element of REAL
abs (0 + (- (S - a))) is V28() real ext-real Element of REAL
a - n is V28() real ext-real Element of REAL
K105(n) is V28() real ext-real set
K103(a,K105(n)) is V28() real ext-real set
a + n is V28() real ext-real Element of REAL
].(a - n),(a + n).[ is V33() V34() V35() Element of K19(REAL)
O is epsilon-transitive epsilon-connected ordinal natural V28() real ext-real non negative V33() V34() V35() V36() V37() V38() Element of NAT
z9 is epsilon-transitive epsilon-connected ordinal natural V28() real ext-real non negative V33() V34() V35() V36() V37() V38() Element of NAT
f . O is V28() real ext-real Element of the carrier of R^1
O - (1 / 4) is V28() real ext-real Element of REAL
K103(O,K105((1 / 4))) is V28() real ext-real set
O + (1 / 4) is V28() real ext-real non negative Element of REAL
].(O - (1 / 4)),(O + (1 / 4)).[ is V33() V34() V35() Element of K19(REAL)
{ b₁ where b₁ is V28() real ext-real Element of REAL : ( not b₁ <= O - (1 / 4) & not O + (1 / 4) <= b₁ ) } is set
S + (1 / 4) is V28() real ext-real Element of REAL
n is V28() real ext-real Element of REAL
f . z9 is V28() real ext-real Element of the carrier of R^1
z9 - (1 / 4) is V28() real ext-real Element of REAL
K103(z9,K105((1 / 4))) is V28() real ext-real set
z9 + (1 / 4) is V28() real ext-real non negative Element of REAL
].(z9 - (1 / 4)),(z9 + (1 / 4)).[ is V33() V34() V35() Element of K19(REAL)
{ b₁ where b₁ is V28() real ext-real Element of REAL : ( not b₁ <= z9 - (1 / 4) & not z9 + (1 / 4) <= b₁ ) } is set
r is V28() real ext-real Element of REAL
r - (1 / 4) is V28() real ext-real Element of REAL
K103(r,K105((1 / 4))) is V28() real ext-real set
n is V28() real ext-real Element of REAL
z9 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V28() real ext-real positive non negative V33() V34() V35() V36() V37() V38() Element of NAT
(r - (1 / 4)) + 1 is V28() real ext-real Element of REAL
- (1 / 4) is V28() real ext-real non positive Element of REAL
(- (1 / 4)) + 1 is V28() real ext-real Element of REAL
r + ((- (1 / 4)) + 1) is V28() real ext-real Element of REAL
(S + (1 / 4)) - ((- (1 / 4)) + 1) is V28() real ext-real Element of REAL
K105(((- (1 / 4)) + 1)) is V28() real ext-real set
K103((S + (1 / 4)),K105(((- (1 / 4)) + 1))) is V28() real ext-real set
Ball (x,(1 / 4)) is V33() V34() V35() Element of K19( the carrier of RealSpace)
{ b₁ where b₁ is V28() real ext-real Element of REAL : ( not b₁ <= a - (1 / 4) & not a + (1 / 4) <= b₁ ) } is set
r + (1 / 4) is V28() real ext-real Element of REAL
n is V28() real ext-real Element of REAL
(a + (1 / 4)) - (1 / 4) is V28() real ext-real Element of REAL
K103((a + (1 / 4)),K105((1 / 4))) is V28() real ext-real set
S - (1 / 4) is V28() real ext-real Element of REAL
K103(S,K105((1 / 4))) is V28() real ext-real set
n is V28() real ext-real Element of REAL
(r + (1 / 4)) + (- (1 / 4)) is V28() real ext-real Element of REAL
(S - (1 / 4)) + (- (1 / 4)) is V28() real ext-real Element of REAL
z9 is epsilon-transitive epsilon-connected ordinal natural V28() real ext-real non negative V33() V34() V35() V36() V37() V38() Element of NAT
O is epsilon-transitive epsilon-connected ordinal natural V28() real ext-real non negative V33() V34() V35() V36() V37() V38() Element of NAT
f . z9 is V28() real ext-real Element of the carrier of R^1
z9 - (1 / 4) is V28() real ext-real Element of REAL
K103(z9,K105((1 / 4))) is V28() real ext-real set
z9 + (1 / 4) is V28() real ext-real non negative Element of REAL
].(z9 - (1 / 4)),(z9 + (1 / 4)).[ is V33() V34() V35() Element of K19(REAL)
{ b₁ where b₁ is V28() real ext-real Element of REAL : ( not b₁ <= z9 - (1 / 4) & not z9 + (1 / 4) <= b₁ ) } is set
r is V28() real ext-real Element of REAL
r + (1 / 4) is V28() real ext-real Element of REAL
- (1 / 4) is V28() real ext-real non positive Element of REAL
z9 + (- (1 / 4)) is V28() real ext-real Element of REAL
(z9 + (- (1 / 4))) + (1 / 4) is V28() real ext-real Element of REAL
n is V28() real ext-real Element of REAL
f . O is V28() real ext-real Element of the carrier of R^1
O - (1 / 4) is V28() real ext-real Element of REAL
K103(O,K105((1 / 4))) is V28() real ext-real set
O + (1 / 4) is V28() real ext-real non negative Element of REAL
].(O - (1 / 4)),(O + (1 / 4)).[ is V33() V34() V35() Element of K19(REAL)
{ b₁ where b₁ is V28() real ext-real Element of REAL : ( not b₁ <= O - (1 / 4) & not O + (1 / 4) <= b₁ ) } is set
(O + (1 / 4)) - (1 / 4) is V28() real ext-real Element of REAL
K103((O + (1 / 4)),K105((1 / 4))) is V28() real ext-real set
S - (1 / 4) is V28() real ext-real Element of REAL
K103(S,K105((1 / 4))) is V28() real ext-real set
n is V28() real ext-real Element of REAL
O + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V28() real ext-real positive non negative V33() V34() V35() V36() V37() V38() Element of NAT
(S - (1 / 4)) + 1 is V28() real ext-real Element of REAL
S + (- (1 / 4)) is V28() real ext-real Element of REAL
(S + (- (1 / 4))) + 1 is V28() real ext-real Element of REAL
(- (1 / 4)) + 1 is V28() real ext-real Element of REAL
(r + (1 / 4)) - ((- (1 / 4)) + 1) is V28() real ext-real Element of REAL
K105(((- (1 / 4)) + 1)) is V28() real ext-real set
K103((r + (1 / 4)),K105(((- (1 / 4)) + 1))) is V28() real ext-real set
S + ((- (1 / 4)) + 1) is V28() real ext-real Element of REAL
(S + ((- (1 / 4)) + 1)) - ((- (1 / 4)) + 1) is V28() real ext-real Element of REAL
K103((S + ((- (1 / 4)) + 1)),K105(((- (1 / 4)) + 1))) is V28() real ext-real set
Ball (x,(1 / 4)) is V33() V34() V35() Element of K19( the carrier of RealSpace)
{ b₁ where b₁ is V28() real ext-real Element of REAL : ( not b₁ <= a - (1 / 4) & not a + (1 / 4) <= b₁ ) } is set
r - (1 / 4) is V28() real ext-real Element of REAL
K103(r,K105((1 / 4))) is V28() real ext-real set
n is V28() real ext-real Element of REAL
S + (1 / 4) is V28() real ext-real Element of REAL
a + (- (1 / 4)) is V28() real ext-real Element of REAL
(a + (- (1 / 4))) + (1 / 4) is V28() real ext-real Element of REAL
n is V28() real ext-real Element of REAL
(S + (1 / 4)) + (1 / 4) is V28() real ext-real Element of REAL
(r - (1 / 4)) + (1 / 4) is V28() real ext-real Element of REAL
1 / 2 is V28() real ext-real non negative Element of REAL
K106(2) is non empty V28() real ext-real positive non negative set
K104(1,K106(2)) is V28() real ext-real non negative set
S + (1 / 2) is V28() real ext-real Element of REAL
(S + (1 / 2)) - (1 / 2) is V28() real ext-real Element of REAL
K105((1 / 2)) is V28() real ext-real non positive set
K103((S + (1 / 2)),K105((1 / 2))) is V28() real ext-real set
r - (1 / 2) is V28() real ext-real Element of REAL
K103(r,K105((1 / 2))) is V28() real ext-real set
O is epsilon-transitive epsilon-connected ordinal natural V28() real ext-real non negative V33() V34() V35() V36() V37() V38() Element of NAT
z9 is epsilon-transitive epsilon-connected ordinal natural V28() real ext-real non negative V33() V34() V35() V36() V37() V38() Element of NAT
m is V33() V34() V35() Element of K19( the carrier of R^1)
(g `) ` is V33() V34() V35() Element of K19( the carrier of R^1)
the carrier of R^1 \ (g `) is V33() V34() V35() set
g /\ (g `) is V33() V34() V35() Element of K19( the carrier of R^1)
- S is V28() real ext-real Element of REAL
a + (- S) is V28() real ext-real Element of REAL
S + (- S) is V28() real ext-real Element of REAL
a is V28() real ext-real Element of REAL
a - (1 / 4) is V28() real ext-real Element of REAL
K105((1 / 4)) is V28() real ext-real non positive set
K103(a,K105((1 / 4))) is V28() real ext-real set
a + (1 / 4) is V28() real ext-real Element of REAL
].(a - (1 / 4)),(a + (1 / 4)).[ is V33() V34() V35() Element of K19(REAL)
].(a - (1 / 4)),(a + (1 / 4)).[ /\ g is V33() V34() V35() Element of K19( the carrier of R^1)
[#] R^1 is non empty non proper V33() V34() V35() closed Element of K19( the carrier of R^1)
([#] R^1) \ (rng f) is V33() V34() V35() Element of K19( the carrier of R^1)
f is V33() V34() V35() Element of K19( the carrier of R^1)
id NAT is Relation-like NAT -defined NAT -valued Function-like one-to-one non empty total Element of K19(K20(NAT,NAT))
K20(NAT,NAT) is Relation-like non empty set
K19(K20(NAT,NAT)) is non empty set
dom (id NAT) is non empty V33() V34() V35() V36() V37() V38() Element of K19(NAT)
K19(NAT) is non empty set
rng (id NAT) is non empty V33() V34() V35() V36() V37() V38() Element of K19(NAT)
g is set
g is Relation-like NAT -defined the carrier of R^1 -valued Function-like V18( NAT , the carrier of R^1) Element of K19(K20(NAT, the carrier of R^1))
x is epsilon-transitive epsilon-connected ordinal natural V28() real ext-real non negative V33() V34() V35() V36() V37() V38() Element of NAT
g . x is V28() real ext-real Element of the carrier of R^1
x - (1 / 4) is V28() real ext-real Element of REAL
K105((1 / 4)) is V28() real ext-real non positive set
K103(x,K105((1 / 4))) is V28() real ext-real set
x + (1 / 4) is V28() real ext-real non negative Element of REAL
].(x - (1 / 4)),(x + (1 / 4)).[ is V33() V34() V35() Element of K19(REAL)
0 + x is epsilon-transitive epsilon-connected ordinal natural V28() real ext-real non negative V33() V34() V35() V36() V37() V38() Element of NAT
- (1 / 4) is V28() real ext-real non positive Element of REAL
(- (1 / 4)) + x is V28() real ext-real Element of REAL
a is V28() real ext-real Element of REAL
{ b₁ where b₁ is V28() real ext-real Element of REAL : ( not b₁ <= x - (1 / 4) & not x + (1 / 4) <= b₁ ) } is set
f is non empty MetrStruct
TopSpaceMetr f is non empty strict TopSpace-like TopStruct
the carrier of (TopSpaceMetr f) is non empty set
K19( the carrier of (TopSpaceMetr f)) is non empty set
K19(K19( the carrier of (TopSpaceMetr f))) is non empty set
the carrier of f is non empty set
g is Element of the carrier of (TopSpaceMetr f)
x is Element of the carrier of f
{ (Ball (x,(1 / b₁))) where b₁ is epsilon-transitive epsilon-connected ordinal natural V28() real ext-real non negative V33() V34() V35() V36() V37() V38() Element of NAT : not b₁ = 0 } is set
bool the carrier of (TopSpaceMetr f) is non empty Element of K19(K19( the carrier of (TopSpaceMetr f)))
S9 is set
S is epsilon-transitive epsilon-connected ordinal natural V28() real ext-real non negative V33() V34() V35() V36() V37() V38() Element of NAT
1 / S is V28() real ext-real non negative Element of REAL
K106(S) is V28() real ext-real non negative set
K104(1,K106(S)) is V28() real ext-real non negative set
Ball (x,(1 / S)) is Element of K19( the carrier of f)
K19( the carrier of f) is non empty set
S9 is Element of the carrier of f
x is Element of K19(K19( the carrier of (TopSpaceMetr f)))
{ (Ball (S9,(1 / b₁))) where b₁ is epsilon-transitive epsilon-connected ordinal natural V28() real ext-real non negative V33() V34() V35() V36() V37() V38() Element of NAT : not b₁ = 0 } is set
S is Element of the carrier of f
a is Element of K19(K19( the carrier of (TopSpaceMetr f)))
{ (Ball (S,(1 / b₁))) where b₁ is epsilon-transitive epsilon-connected ordinal natural V28() real ext-real non negative V33() V34() V35() V36() V37() V38() Element of NAT : not b₁ = 0 } is set
f is non empty Reflexive discerning V88() triangle Discerning MetrStruct
TopSpaceMetr f is non empty strict TopSpace-like TopStruct
the carrier of (TopSpaceMetr f) is non empty set
g is Element of the carrier of (TopSpaceMetr f)
(f,g) is Element of K19(K19( the carrier of (TopSpaceMetr f)))
K19( the carrier of (TopSpaceMetr f)) is non empty set
K19(K19( the carrier of (TopSpaceMetr f))) is non empty set
the carrier of f is non empty set
a is Element of the carrier of f
{ (Ball (a,(1 / b₁))) where b₁ is epsilon-transitive epsilon-connected ordinal natural V28() real ext-real non negative V33() V34() V35() V36() V37() V38() Element of NAT : not b₁ = 0 } is set
the topology of (TopSpaceMetr f) is non empty Element of K19(K19( the carrier of (TopSpaceMetr f)))
S9 is set
S is epsilon-transitive epsilon-connected ordinal natural V28() real ext-real non negative V33() V34() V35() V36() V37() V38() Element of NAT
1 / S is V28() real ext-real non negative Element of REAL
K106(S) is V28() real ext-real non negative set
K104(1,K106(S)) is V28() real ext-real non negative set
Ball (a,(1 / S)) is Element of K19( the carrier of f)
K19( the carrier of f) is non empty set
Family_open_set f is Element of K19(K19( the carrier of f))
K19(K19( the carrier of f)) is non empty set
S9 is set
S is epsilon-transitive epsilon-connected ordinal natural V28() real ext-real non negative V33() V34() V35() V36() V37() V38() Element of NAT
1 / S is V28() real ext-real non negative Element of REAL
K106(S) is V28() real ext-real non negative set
K104(1,K106(S)) is V28() real ext-real non negative set
Ball (a,(1 / S)) is Element of K19( the carrier of f)
K19( the carrier of f) is non empty set
S9 is Element of K19( the carrier of (TopSpaceMetr f))
S is V28() real ext-real set
Ball (a,S) is Element of K19( the carrier of f)
K19( the carrier of f) is non empty set
U1 is V28() real ext-real Element of REAL
O is epsilon-transitive epsilon-connected ordinal natural V28() real ext-real non negative V33() V34() V35() V36() V37() V38() Element of NAT
1 / O is V28() real ext-real non negative Element of REAL
K106(O) is V28() real ext-real non negative set
K104(1,K106(O)) is V28() real ext-real non negative set
Ball (a,(1 / O)) is Element of K19( the carrier of f)
n is Element of K19( the carrier of (TopSpaceMetr f))
m is Element of K19( the carrier of (TopSpaceMetr f))
Ball (a,U1) is Element of K19( the carrier of f)
1 / 1 is V28() real ext-real non negative Element of REAL
K106(1) is non empty V28() real ext-real positive non negative set
K104(1,K106(1)) is V28() real ext-real non negative set
Ball (a,(1 / 1)) is Element of K19( the carrier of f)
K19( the carrier of f) is non empty set
Intersect (f,g) is Element of K19( the carrier of (TopSpaceMetr f))
meet (f,g) is Element of K19( the carrier of (TopSpaceMetr f))
f is non empty Reflexive discerning V88() triangle Discerning MetrStruct
TopSpaceMetr f is non empty strict TopSpace-like TopStruct
the carrier of (TopSpaceMetr f) is non empty set
g is Element of the carrier of (TopSpaceMetr f)
(f,g) is non empty open g -quasi_basis Element of K19(K19( the carrier of (TopSpaceMetr f)))
K19( the carrier of (TopSpaceMetr f)) is non empty set
K19(K19( the carrier of (TopSpaceMetr f))) is non empty set
the carrier of f is non empty set
a is Element of the carrier of f
{ (Ball (a,(1 / b₁))) where b₁ is epsilon-transitive epsilon-connected ordinal natural V28() real ext-real non negative V33() V34() V35() V36() V37() V38() Element of NAT : not b₁ = 0 } is set
K19( the carrier of f) is non empty set
{ H₁(b₁) where b₁ is epsilon-transitive epsilon-connected ordinal natural V28() real ext-real non negative V33() V34() V35() V36() V37() V38() Element of NAT : S₁[b₁] } is set
f is non empty Reflexive discerning V88() triangle Discerning MetrStruct
TopSpaceMetr f is non empty strict TopSpace-like TopStruct
the carrier of (TopSpaceMetr f) is non empty set
the carrier of f is non empty set
g is Element of the carrier of (TopSpaceMetr f)
(f,g) is non empty countable open g -quasi_basis Element of K19(K19( the carrier of (TopSpaceMetr f)))
K19( the carrier of (TopSpaceMetr f)) is non empty set
K19(K19( the carrier of (TopSpaceMetr f))) is non empty set
K20(NAT,(f,g)) is Relation-like non empty set
K19(K20(NAT,(f,g))) is non empty set
x is Element of the carrier of f
S9 is Element of the carrier of f
{ (Ball (S9,(1 / b₁))) where b₁ is epsilon-transitive epsilon-connected ordinal natural V28() real ext-real non negative V33() V34() V35() V36() V37() V38() Element of NAT : not b₁ = 0 } is set
S is set
U1 is epsilon-transitive epsilon-connected ordinal natural V28() real ext-real non negative V33() V34() V35() V36() V37() V38() Element of NAT
U1 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V28() real ext-real positive non negative V33() V34() V35() V36() V37() V38() Element of NAT
1 / (U1 + 1) is V28() real ext-real non negative Element of REAL
K106((U1 + 1)) is non empty V28() real ext-real positive non negative set
K104(1,K106((U1 + 1))) is V28() real ext-real non negative set
Ball (S9,(1 / (U1 + 1))) is Element of K19( the carrier of f)
K19( the carrier of f) is non empty set
S is Relation-like Function-like set
dom S is set
rng S is set
U1 is Relation-like NAT -defined (f,g) -valued Function-like V18( NAT ,(f,g)) Element of K19(K20(NAT,(f,g)))
O is epsilon-transitive epsilon-connected ordinal natural V28() real ext-real non negative V33() V34() V35() V36() V37() V38() Element of NAT
U1 . O is Element of (f,g)
O + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V28() real ext-real positive non negative V33() V34() V35() V36() V37() V38() Element of NAT
1 / (O + 1) is V28() real ext-real non negative Element of REAL
K106((O + 1)) is non empty V28() real ext-real positive non negative set
K104(1,K106((O + 1))) is V28() real ext-real non negative set
Ball (x,(1 / (O + 1))) is Element of K19( the carrier of f)
K19( the carrier of f) is non empty set
n is epsilon-transitive epsilon-connected ordinal natural V28() real ext-real non negative V33() V34() V35() V36() V37() V38() Element of NAT
n + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V28() real ext-real positive non negative V33() V34() V35() V36() V37() V38() Element of NAT
1 / (n + 1) is V28() real ext-real non negative Element of REAL
K106((n + 1)) is non empty V28() real ext-real positive non negative set
K104(1,K106((n + 1))) is V28() real ext-real non negative set
Ball (S9,(1 / (n + 1))) is Element of K19( the carrier of f)
f is Relation-like Function-like set
g is Relation-like Function-like set
f +* g is Relation-like Function-like set
rng (f +* g) is set
dom f is set
dom g is set
(dom f) \ (dom g) is Element of K19((dom f))
K19((dom f)) is non empty set
f .: ((dom f) \ (dom g)) is set
rng g is set
(f .: ((dom f) \ (dom g))) \/ (rng g) is set
x is set
dom (f +* g) is set
a is set
(f +* g) . a is set
g . a is set
(dom f) \/ (dom g) is set
f . a is set
x is set
a is set
f . a is set
(f +* g) . a is set
(dom f) \/ (dom g) is set
dom (f +* g) is set
g is set
f is set
id f is Relation-like f -defined f -valued Function-like one-to-one total Element of K19(K20(f,f))
K20(f,f) is Relation-like set
K19(K20(f,f)) is non empty set
(id f) .: g is Element of K19(f)
K19(f) is non empty set
x is set
dom (id f) is Element of K19(f)
a is set
(id f) . a is set
x is set
dom (id f) is Element of K19(f)
(id f) . x is set
f is set
id f is Relation-like f -defined f -valued Function-like one-to-one total Element of K19(K20(f,f))
K20(f,f) is Relation-like set
K19(K20(f,f)) is non empty set
g is set
x is set
g --> x is Relation-like g -defined {x} -valued Function-like V18(g,{x}) Element of K19(K20(g,{x}))
{x} is non empty set
K20(g,{x}) is Relation-like set
K19(K20(g,{x})) is non empty set
(id f) +* (g --> x) is Relation-like Function-like set
dom ((id f) +* (g --> x)) is set
f \/ g is set
dom (id f) is Element of K19(f)
K19(f) is non empty set
dom (g --> x) is Element of K19(g)
K19(g) is non empty set
(dom (id f)) \/ (dom (g --> x)) is set
f \/ (dom (g --> x)) is set
g is set
f is set
id f is Relation-like f -defined f -valued Function-like one-to-one total Element of K19(K20(f,f))
K20(f,f) is Relation-like set
K19(K20(f,f)) is non empty set
x is set
g --> x is Relation-like g -defined {x} -valued Function-like V18(g,{x}) Element of K19(K20(g,{x}))
{x} is non empty set
K20(g,{x}) is Relation-like set
K19(K20(g,{x})) is non empty set
(id f) +* (g --> x) is Relation-like Function-like set
rng ((id f) +* (g --> x)) is set
f \ g is Element of K19(f)
K19(f) is non empty set
(f \ g) \/ {x} is non empty set
rng (g --> x) is Element of K19({x})
K19({x}) is non empty set
S9 is set
dom ((id f) +* (g --> x)) is set
S is set
((id f) +* (g --> x)) . S is set
dom (id f) is Element of K19(f)
dom (g --> x) is Element of K19(g)
K19(g) is non empty set
(dom (id f)) \/ (dom (g --> x)) is set
(g --> x) . S is set
(id f) . S is set
S9 is set
(id f) .: (f \ g) is Element of K19(f)
dom (id f) is Element of K19(f)
(dom (id f)) \ g is Element of K19(f)
(id f) .: ((dom (id f)) \ g) is Element of K19(f)
dom (g --> x) is Element of K19(g)
K19(g) is non empty set
(dom (id f)) \ (dom (g --> x)) is Element of K19(f)
(id f) .: ((dom (id f)) \ (dom (g --> x))) is Element of K19(f)
x is set
f is set
id f is Relation-like f -defined f -valued Function-like one-to-one total Element of K19(K20(f,f))
K20(f,f) is Relation-like set
K19(K20(f,f)) is non empty set
g is set
a is set
g --> a is Relation-like g -defined {a} -valued Function-like V18(g,{a}) Element of K19(K20(g,{a}))
{a} is non empty set
K20(g,{a}) is Relation-like set
K19(K20(g,{a})) is non empty set
(id f) +* (g --> a) is Relation-like Function-like set
x \ {a} is Element of K19(x)
K19(x) is non empty set
((id f) +* (g --> a)) " (x \ {a}) is set
x \ g is Element of K19(x)
(x \ g) \ {a} is Element of K19(x)
S is set
((id f) +* (g --> a)) . S is set
dom (g --> a) is Element of K19(g)
K19(g) is non empty set
dom (id f) is Element of K19(f)
K19(f) is non empty set
(dom (id f)) \/ (dom (g --> a)) is set
(g --> a) . S is set
dom (g --> a) is Element of K19(g)
K19(g) is non empty set
dom ((id f) +* (g --> a)) is set
f \/ g is set
dom (id f) is Element of K19(f)
K19(f) is non empty set
(dom (id f)) \/ (dom (g --> a)) is set
(id f) . S is set
S is set
dom (id f) is Element of K19(f)
K19(f) is non empty set
dom (g --> a) is Element of K19(g)
K19(g) is non empty set
(dom (id f)) \/ (dom (g --> a)) is set
((id f) +* (g --> a)) . S is set
(id f) . S is set
dom ((id f) +* (g --> a)) is set
x is set
f is set
id f is Relation-like f -defined f -valued Function-like one-to-one total Element of K19(K20(f,f))
K20(f,f) is Relation-like set
K19(K20(f,f)) is non empty set
g is set
g --> x is Relation-like g -defined {x} -valued Function-like V18(g,{x}) Element of K19(K20(g,{x}))
{x} is non empty set
K20(g,{x}) is Relation-like set
K19(K20(g,{x})) is non empty set
(id f) +* (g --> x) is Relation-like Function-like set
((id f) +* (g --> x)) " {x} is set
S9 is set
dom ((id f) +* (g --> x)) is set
((id f) +* (g --> x)) . S9 is set
dom (g --> x) is Element of K19(g)
K19(g) is non empty set
dom (g --> x) is Element of K19(g)
K19(g) is non empty set
(id f) . S9 is set
dom (id f) is Element of K19(f)
K19(f) is non empty set
dom (g --> x) is Element of K19(g)
K19(g) is non empty set
S9 is set
dom (g --> x) is Element of K19(g)
K19(g) is non empty set
((id f) +* (g --> x)) . S9 is set
(g --> x) . S9 is set
dom ((id f) +* (g --> x)) is set
x is set
f is set
a is set
id f is Relation-like f -defined f -valued Function-like one-to-one total Element of K19(K20(f,f))
K20(f,f) is Relation-like set
K19(K20(f,f)) is non empty set
g is set
g --> a is Relation-like g -defined {a} -valued Function-like V18(g,{a}) Element of K19(K20(g,{a}))
{a} is non empty set
K20(g,{a}) is Relation-like set
K19(K20(g,{a})) is non empty set
(id f) +* (g --> a) is Relation-like Function-like set
x \/ {a} is non empty set
((id f) +* (g --> a)) " (x \/ {a}) is set
x \/ g is set
x \ {a} is Element of K19(x)
K19(x) is non empty set
S9 is set
x \ g is Element of K19(x)
(x \ g) \ {a} is Element of K19(x)
((x \ g) \ {a}) \/ g is set
S9 is set
S9 is set
(x \ g) \/ g is set
((id f) +* (g --> a)) " {a} is set
((id f) +* (g --> a)) " x is set
(((id f) +* (g --> a)) " x) \/ g is set
x is set
f is set
a is set
id f is Relation-like f -defined f -valued Function-like one-to-one total Element of K19(K20(f,f))
K20(f,f) is Relation-like set
K19(K20(f,f)) is non empty set
g is set
g --> a is Relation-like g -defined {a} -valued Function-like V18(g,{a}) Element of K19(K20(g,{a}))
{a} is non empty set
K20(g,{a}) is Relation-like set
K19(K20(g,{a})) is non empty set
(id f) +* (g --> a) is Relation-like Function-like set
x \ {a} is Element of K19(x)
K19(x) is non empty set
((id f) +* (g --> a)) " (x \ {a}) is set
x \ g is Element of K19(x)
(x \ g) \ {a} is Element of K19(x)
f is non empty Reflexive discerning V88() triangle Discerning MetrStruct
TopSpaceMetr f is non empty strict TopSpace-like TopStruct
the carrier of (TopSpaceMetr f) is non empty set
g is Element of the carrier of (TopSpaceMetr f)
K19( the carrier of (TopSpaceMetr f)) is non empty set
K19(K19( the carrier of (TopSpaceMetr f))) is non empty set
(f,g) is non empty countable open g -quasi_basis Element of K19(K19( the carrier of (TopSpaceMetr f)))
f is TopStruct
the carrier of f is set
K20(NAT, the carrier of f) is Relation-like set
K19(K20(NAT, the carrier of f)) is non empty set
f is non empty TopStruct
the carrier of f is non empty set
K20(NAT, the carrier of f) is Relation-like non empty set
K19(K20(NAT, the carrier of f)) is non empty set
g is Element of the carrier of f
NAT --> g is Relation-like NAT -defined the carrier of f -valued Function-like V18( NAT , the carrier of f) T-Sequence-like Element of K19(K20(NAT, the carrier of f))
x is Relation-like NAT -defined the carrier of f -valued Function-like V18( NAT , the carrier of f) Element of K19(K20(NAT, the carrier of f))
K19( the carrier of f) is non empty set
a is Element of K19( the carrier of f)
S9 is epsilon-transitive epsilon-connected ordinal natural V28() real ext-real non negative V33() V34() V35() V36() V37() V38() Element of NAT
x . S9 is Element of the carrier of f
f is TopStruct
the carrier of f is set
K20(NAT, the carrier of f) is Relation-like set
K19(K20(NAT, the carrier of f)) is non empty set
f is non empty TopStruct
the carrier of f is non empty set
K20(NAT, the carrier of f) is Relation-like non empty set
K19(K20(NAT, the carrier of f)) is non empty set
K19( the carrier of f) is non empty set
g is Relation-like NAT -defined the carrier of f -valued Function-like V18( NAT , the carrier of f) Element of K19(K20(NAT, the carrier of f))
{ b₁ where b₁ is Element of the carrier of f : S₁[b₁] } is set
x is Element of K19( the carrier of f)
a is Element of the carrier of f
S9 is Element of the carrier of f
S9 is Element of the carrier of f
x is Element of K19( the carrier of f)
a is Element of K19( the carrier of f)
S9 is Element of the carrier of f
f is non empty TopSpace-like TopStruct
the carrier of f is non empty set
K19( the carrier of f) is non empty set
g is Element of K19( the carrier of f)
Cl g is Element of K19( the carrier of f)
K20(NAT, the carrier of f) is Relation-like non empty set
K19(K20(NAT, the carrier of f)) is non empty set
x is Element of the carrier of f
K19(K19( the carrier of f)) is non empty set
a is non empty open x -quasi_basis Element of K19(K19( the carrier of f))
K20(NAT,a) is Relation-like non empty set
K19(K20(NAT,a)) is non empty set
S9 is Relation-like NAT -defined a -valued Function-like V18( NAT ,a) Element of K19(K20(NAT,a))
rng S9 is Element of K19(a)
K19(a) is non empty set
S is set
succ S is non empty set
S9 .: (succ S) is Element of K19(a)
meet (S9 .: (succ S)) is set
g /\ (meet (S9 .: (succ S))) is Element of K19( the carrier of f)
U1 is epsilon-transitive epsilon-connected ordinal natural V28() real ext-real non negative V33() V34() V35() V36() V37() V38() Element of NAT
succ U1 is non empty epsilon-transitive epsilon-connected ordinal natural V28() real ext-real positive non negative set
S9 .: (succ U1) is Element of K19(a)
meet (S9 .: (succ U1)) is set
U1 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V28() real ext-real positive non negative V33() V34() V35() V36() V37() V38() Element of NAT
succ (U1 + 1) is non empty epsilon-transitive epsilon-connected ordinal natural V28() real ext-real positive non negative set
S9 .: (succ (U1 + 1)) is Element of K19(a)
meet (S9 .: (succ (U1 + 1))) is set
O is Element of K19( the carrier of f)
dom S9 is V33() V34() V35() V36() V37() V38() Element of K19(NAT)
K19(NAT) is non empty set
S9 . U1 is Element of a
S9 . (U1 + 1) is Element of a
n is Element of K19( the carrier of f)
n /\ O is Element of K19( the carrier of f)
m is Element of K19( the carrier of f)
{(U1 + 1)} is non empty V33() V34() V35() V36() V37() V38() set
{(U1 + 1)} \/ (U1 + 1) is non empty V33() V34() V35() V36() V37() V38() set
S9 .: ({(U1 + 1)} \/ (U1 + 1)) is Element of K19(a)
meet (S9 .: ({(U1 + 1)} \/ (U1 + 1))) is set
{(U1 + 1)} \/ (succ U1) is non empty set
S9 .: ({(U1 + 1)} \/ (succ U1)) is Element of K19(a)
meet (S9 .: ({(U1 + 1)} \/ (succ U1))) is set
Im (S9,(U1 + 1)) is set
S9 .: {(U1 + 1)} is set
(Im (S9,(U1 + 1))) \/ (S9 .: (succ U1)) is set
meet ((Im (S9,(U1 + 1))) \/ (S9 .: (succ U1))) is set
{(S9 . (U1 + 1))} is non empty set
{(S9 . (U1 + 1))} \/ (S9 .: (succ U1)) is non empty set
meet ({(S9 . (U1 + 1))} \/ (S9 .: (succ U1))) is set
meet {(S9 . (U1 + 1))} is set
(meet {(S9 . (U1 + 1))}) /\ (meet (S9 .: (succ U1))) is set
succ 0 is non empty epsilon-transitive epsilon-connected ordinal natural V28() real ext-real positive non negative set
S9 .: (succ 0) is Element of K19(a)
meet (S9 .: (succ 0)) is set
S9 . 0 is Element of a
O is Element of K19( the carrier of f)
dom S9 is V33() V34() V35() V36() V37() V38() Element of K19(NAT)
K19(NAT) is non empty set
Im (S9,0) is set
{0} is functional non empty V33() V34() V35() V36() V37() V38() set
S9 .: {0} is set
meet (Im (S9,0)) is set
{(S9 . 0)} is non empty set
meet {(S9 . 0)} is set
U1 is epsilon-transitive epsilon-connected ordinal natural V28() real ext-real non negative V33() V34() V35() V36() V37() V38() Element of NAT
succ U1 is non empty epsilon-transitive epsilon-connected ordinal natural V28() real ext-real positive non negative set
S9 .: (succ U1) is Element of K19(a)
meet (S9 .: (succ U1)) is set
O is set
dom S9 is V33() V34() V35() V36() V37() V38() Element of K19(NAT)
K19(NAT) is non empty set
n is set
S9 . n is set
dom S9 is V33() V34() V35() V36() V37() V38() Element of K19(NAT)
K19(NAT) is non empty set
S9 . U1 is Element of a
O is Element of K19( the carrier of f)
g /\ (meet (S9 .: (succ U1))) is Element of K19( the carrier of f)
O is set
S is Relation-like Function-like set
dom S is set
rng S is set
U1 is set
O is set
S . O is set
succ O is non empty set
S9 .: (succ O) is Element of K19(a)
meet (S9 .: (succ O)) is set
g /\ (meet (S9 .: (succ O))) is Element of K19( the carrier of f)
n is epsilon-transitive epsilon-connected ordinal natural V28() real ext-real non negative V33() V34() V35() V36() V37() V38() Element of NAT
O is epsilon-transitive epsilon-connected ordinal natural V28() real ext-real non negative V33() V34() V35() V36() V37() V38() Element of NAT
succ O is non empty epsilon-transitive epsilon-connected ordinal natural V28() real ext-real positive non negative set
S9 .: (succ O) is Element of K19(a)
meet (S9 .: (succ O)) is set
g /\ (meet (S9 .: (succ O))) is Element of K19( the carrier of f)
succ n is non empty epsilon-transitive epsilon-connected ordinal natural V28() real ext-real positive non negative set
S9 .: (succ n) is Element of K19(a)
meet (S9 .: (succ n)) is set
g /\ (meet (S9 .: (succ n))) is Element of K19( the carrier of f)
n + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V28() real ext-real positive non negative V33() V34() V35() V36() V37() V38() Element of NAT
O + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V28() real ext-real positive non negative V33() V34() V35() V36() V37() V38() Element of NAT
dom S9 is V33() V34() V35() V36() V37() V38() Element of K19(NAT)
K19(NAT) is non empty set
S9 . n is Element of a
U1 is Relation-like NAT -defined the carrier of f -valued Function-like V18( NAT , the carrier of f) Element of K19(K20(NAT, the carrier of f))
O is Element of K19( the carrier of f)
n is Element of K19( the carrier of f)
m is Element of K19( the carrier of f)
dom S9 is V33() V34() V35() V36() V37() V38() Element of K19(NAT)
K19(NAT) is non empty set
S9 is set
S9 . S9 is set
z is epsilon-transitive epsilon-connected ordinal natural V28() real ext-real non negative V33() V34() V35() V36() V37() V38() Element of NAT
z9 is epsilon-transitive epsilon-connected ordinal natural V28() real ext-real non negative V33() V34() V35() V36() V37() V38() Element of NAT
U1 . z9 is Element of the carrier of f
succ z is non empty epsilon-transitive epsilon-connected ordinal natural V28() real ext-real positive non negative set
S9 . z is Element of a
S9 .: (succ z) is Element of K19(a)
succ z9 is non empty epsilon-transitive epsilon-connected ordinal natural V28() real ext-real positive non negative set
S9 .: (succ z9) is Element of K19(a)
meet (S9 .: (succ z9)) is set
g /\ (meet (S9 .: (succ z9))) is Element of K19( the carrier of f)
meet (S9 .: (succ z)) is set
g /\ (meet (S9 .: (succ z))) is Element of K19( the carrier of f)
(f,U1) is Element of K19( the carrier of f)
f is non empty TopSpace-like TopStruct
f is non empty TopSpace-like TopStruct
the carrier of f is non empty set
K19( the carrier of f) is non empty set
K20(NAT, the carrier of f) is Relation-like non empty set
K19(K20(NAT, the carrier of f)) is non empty set
g is Element of K19( the carrier of f)
x is Relation-like NAT -defined the carrier of f -valued Function-like V18( NAT , the carrier of f) Element of K19(K20(NAT, the carrier of f))
rng x is Element of K19( the carrier of f)
(f,x) is Element of K19( the carrier of f)
S9 is Element of K19( the carrier of f)
a is Element of K19( the carrier of f)
S is set
U1 is Element of the carrier of f
O is Element of K19( the carrier of f)
n is Element of K19( the carrier of f)
m is epsilon-transitive epsilon-connected ordinal natural V28() real ext-real non negative V33() V34() V35() V36() V37() V38() Element of NAT
dom x is V33() V34() V35() V36() V37() V38() Element of K19(NAT)
K19(NAT) is non empty set
x . m is Element of the carrier of f
a /\ O is Element of K19( the carrier of f)
Cl a is Element of K19( the carrier of f)
f is non empty TopSpace-like TopStruct
the carrier of f is non empty set
K19( the carrier of f) is non empty set
K20(NAT, the carrier of f) is Relation-like non empty set
K19(K20(NAT, the carrier of f)) is non empty set
g is Element of K19( the carrier of f)
x is Relation-like NAT -defined the carrier of f -valued Function-like V18( NAT , the carrier of f) Element of K19(K20(NAT, the carrier of f))
rng x is Element of K19( the carrier of f)
(f,x) is Element of K19( the carrier of f)
f is non empty TopSpace-like TopStruct
the carrier of f is non empty set
K19( the carrier of f) is non empty set
K20(NAT, the carrier of f) is Relation-like non empty set
K19(K20(NAT, the carrier of f)) is non empty set
g is Element of K19( the carrier of f)
Cl g is Element of K19( the carrier of f)
x is set
a is Element of the carrier of f
S9 is Relation-like NAT -defined the carrier of f -valued Function-like V18( NAT , the carrier of f) Element of K19(K20(NAT, the carrier of f))
rng S9 is Element of K19( the carrier of f)
(f,S9) is Element of K19( the carrier of f)
f is non empty TopSpace-like TopStruct
REAL \ NAT is V33() V34() V35() Element of K19(REAL)
{REAL} is non empty set
(REAL \ NAT) \/ {REAL} is non empty set
id REAL is Relation-like REAL -defined REAL -valued Function-like one-to-one non empty total Element of K19(K20(REAL,REAL))
K19(K20(REAL,REAL)) is non empty set
NAT --> REAL is Relation-like NAT -defined {REAL} -valued Function-like V18( NAT ,{REAL}) T-Sequence-like Element of K19(K20(NAT,{REAL}))
K20(NAT,{REAL}) is Relation-like non empty set
K19(K20(NAT,{REAL})) is non empty set
(id REAL) +* (NAT --> REAL) is Relation-like Function-like set
rng ((id REAL) +* (NAT --> REAL)) is set
REAL \/ NAT is non empty V33() V34() V35() set
dom ((id REAL) +* (NAT --> REAL)) is set
g is non empty set
K20( the carrier of R^1,g) is Relation-like non empty set
K19(K20( the carrier of R^1,g)) is non empty set
K19(g) is non empty set
x is Relation-like the carrier of R^1 -defined g -valued Function-like V18( the carrier of R^1,g) Element of K19(K20( the carrier of R^1,g))
{ (g \ b₁) where b₁ is Element of K19(g) : ex b₂ being V33() V34() V35() Element of K19( the carrier of R^1) st
( b₂ = x " b₁ & b₂ is closed ) } is set
bool g is non empty Element of K19(K19(g))
K19(K19(g)) is non empty set
S9 is set
S is Element of K19(g)
g \ S is Element of K19(g)
U1 is V33() V34() V35() Element of K19( the carrier of R^1)
x " S is V33() V34() V35() Element of K19( the carrier of R^1)
S9 is Element of K19(K19(g))
TopStruct(# g,S9 #) is non empty strict TopStruct
the carrier of TopStruct(# g,S9 #) is non empty set
K20( the carrier of R^1, the carrier of TopStruct(# g,S9 #)) is Relation-like non empty set
K19(K20( the carrier of R^1, the carrier of TopStruct(# g,S9 #))) is non empty set
K19( the carrier of TopStruct(# g,S9 #)) is non empty set
U1 is Relation-like the carrier of R^1 -defined the carrier of TopStruct(# g,S9 #) -valued Function-like V18( the carrier of R^1, the carrier of TopStruct(# g,S9 #)) Element of K19(K20( the carrier of R^1, the carrier of TopStruct(# g,S9 #)))
O is Element of K19( the carrier of TopStruct(# g,S9 #))
U1 " O is V33() V34() V35() Element of K19( the carrier of R^1)
[#] TopStruct(# g,S9 #) is non empty non proper Element of K19( the carrier of TopStruct(# g,S9 #))
([#] TopStruct(# g,S9 #)) \ O is Element of K19( the carrier of TopStruct(# g,S9 #))
the topology of TopStruct(# g,S9 #) is Element of K19(K19( the carrier of TopStruct(# g,S9 #)))
K19(K19( the carrier of TopStruct(# g,S9 #))) is non empty set
n is Element of K19(g)
g \ n is Element of K19(g)
U1 " n is V33() V34() V35() Element of K19( the carrier of R^1)
([#] TopStruct(# g,S9 #)) \ (([#] TopStruct(# g,S9 #)) \ O) is Element of K19( the carrier of TopStruct(# g,S9 #))
m is V33() V34() V35() Element of K19( the carrier of R^1)
g \ O is Element of K19(g)
[#] TopStruct(# g,S9 #) is non empty non proper Element of K19( the carrier of TopStruct(# g,S9 #))
([#] TopStruct(# g,S9 #)) \ O is Element of K19( the carrier of TopStruct(# g,S9 #))
O is non empty strict TopSpace-like TopStruct
the carrier of O is non empty set
K20( the carrier of R^1, the carrier of O) is Relation-like non empty set
K19(K20( the carrier of R^1, the carrier of O)) is non empty set
K19( the carrier of O) is non empty set
n is Relation-like the carrier of R^1 -defined the carrier of O -valued Function-like V18( the carrier of R^1, the carrier of O) Element of K19(K20( the carrier of R^1, the carrier of O))
m is Element of K19( the carrier of O)
n " m is V33() V34() V35() Element of K19( the carrier of R^1)
S9 is Element of K19( the carrier of O)
n " S9 is V33() V34() V35() Element of K19( the carrier of R^1)
f is non empty strict TopSpace-like TopStruct
the carrier of f is non empty set
K20( the carrier of R^1, the carrier of f) is Relation-like non empty set
K19(K20( the carrier of R^1, the carrier of f)) is non empty set
K19( the carrier of f) is non empty set
g is non empty strict TopSpace-like TopStruct
the carrier of g is non empty set
K20( the carrier of R^1, the carrier of g) is Relation-like non empty set
K19(K20( the carrier of R^1, the carrier of g)) is non empty set
K19( the carrier of g) is non empty set
x is Relation-like the carrier of R^1 -defined the carrier of g -valued Function-like V18( the carrier of R^1, the carrier of g) Element of K19(K20( the carrier of R^1, the carrier of g))
x is Relation-like the carrier of R^1 -defined the carrier of g -valued Function-like V18( the carrier of R^1, the carrier of g) Element of K19(K20( the carrier of R^1, the carrier of g))
a is Relation-like the carrier of R^1 -defined the carrier of f -valued Function-like V18( the carrier of R^1, the carrier of f) Element of K19(K20( the carrier of R^1, the carrier of f))
a is Relation-like the carrier of R^1 -defined the carrier of f -valued Function-like V18( the carrier of R^1, the carrier of f) Element of K19(K20( the carrier of R^1, the carrier of f))
the topology of g is non empty Element of K19(K19( the carrier of g))
K19(K19( the carrier of g)) is non empty set
the topology of f is non empty Element of K19(K19( the carrier of f))
K19(K19( the carrier of f)) is non empty set
S9 is set
S is Element of K19( the carrier of g)
U1 is Element of K19( the carrier of f)
O is Element of K19( the carrier of g)
[#] g is non empty non proper closed Element of K19( the carrier of g)
([#] g) \ O is Element of K19( the carrier of g)
a " (([#] g) \ O) is V33() V34() V35() Element of K19( the carrier of R^1)
[#] f is non empty non proper closed Element of K19( the carrier of f)
n is Element of K19( the carrier of f)
([#] f) \ n is Element of K19( the carrier of f)
S9 is set
S is Element of K19( the carrier of f)
U1 is Element of K19( the carrier of g)
O is Element of K19( the carrier of f)
[#] f is non empty non proper closed Element of K19( the carrier of f)
([#] f) \ O is Element of K19( the carrier of f)
x " (([#] f) \ O) is V33() V34() V35() Element of K19( the carrier of R^1)
[#] g is non empty non proper closed Element of K19( the carrier of g)
n is Element of K19( the carrier of g)
([#] g) \ n is Element of K19( the carrier of g)
() is non empty strict TopSpace-like TopStruct
the carrier of () is non empty set
f is set
K19( the carrier of ()) is non empty set
f is Element of K19( the carrier of ())
K20( the carrier of R^1, the carrier of ()) is Relation-like non empty set
K19(K20( the carrier of R^1, the carrier of ())) is non empty set
g is Relation-like the carrier of R^1 -defined the carrier of () -valued Function-like V18( the carrier of R^1, the carrier of ()) Element of K19(K20( the carrier of R^1, the carrier of ()))
f ` is Element of K19( the carrier of ())
the carrier of () \ f is set
g " (f `) is V33() V34() V35() Element of K19( the carrier of R^1)
(g " (f `)) ` is V33() V34() V35() Element of K19( the carrier of R^1)
the carrier of R^1 \ (g " (f `)) is V33() V34() V35() set
x is V33() V34() V35() Element of K19( the carrier of R^1)
[#] () is non empty non proper closed Element of K19( the carrier of ())
([#] ()) \ f is Element of K19( the carrier of ())
(f `) \ {REAL} is Element of K19( the carrier of ())
a is set
a is set
((id REAL) +* (NAT --> REAL)) " ((f `) \ {REAL}) is set
(f `) \ NAT is Element of K19( the carrier of ())
[#] R^1 is non empty non proper V33() V34() V35() closed Element of K19( the carrier of R^1)
([#] R^1) \ (f `) is V33() V34() V35() Element of K19( the carrier of R^1)
NAT /\ ([#] R^1) is V33() V34() V35() V36() V37() V38() Element of K19( the carrier of R^1)
(([#] R^1) \ (f `)) \/ (NAT /\ ([#] R^1)) is V33() V34() V35() Element of K19( the carrier of R^1)
(([#] R^1) \ (f `)) \/ NAT is non empty V33() V34() V35() set
(f `) ` is Element of K19( the carrier of ())
the carrier of () \ (f `) is set
the carrier of () \ (f `) is Element of K19( the carrier of ())
((REAL \ NAT) \/ {REAL}) \ (f `) is Element of K19(((REAL \ NAT) \/ {REAL}))
K19(((REAL \ NAT) \/ {REAL})) is non empty set
REAL \ (f `) is V33() V34() V35() Element of K19(REAL)
(REAL \ (f `)) \ NAT is V33() V34() V35() Element of K19(REAL)
((REAL \ (f `)) \ NAT) \/ {REAL} is non empty set
a is set
a is set
a is set
x is V33() V34() V35() Element of K19( the carrier of R^1)
x \ NAT is V33() V34() V35() Element of K19( the carrier of R^1)
(x \ NAT) \/ {REAL} is non empty set
[#] R^1 is non empty non proper V33() V34() V35() closed Element of K19( the carrier of R^1)
([#] R^1) \ x is V33() V34() V35() Element of K19( the carrier of R^1)
a is V33() V34() V35() Element of K19( the carrier of R^1)
REAL \ x is V33() V34() V35() Element of K19(REAL)
(REAL \ x) \ {REAL} is V33() V34() V35() Element of K19(REAL)
((id REAL) +* (NAT --> REAL)) " ((REAL \ x) \ {REAL}) is set
(REAL \ x) \ NAT is V33() V34() V35() Element of K19(REAL)
g " ((REAL \ x) \ {REAL}) is V33() V34() V35() Element of K19( the carrier of R^1)
x \/ NAT is non empty V33() V34() V35() set
REAL \ (x \/ NAT) is V33() V34() V35() Element of K19(REAL)
f ` is Element of K19( the carrier of ())
the carrier of () \ f is set
((REAL \ NAT) \/ {REAL}) \ ((x \ NAT) \/ {REAL}) is Element of K19(((REAL \ NAT) \/ {REAL}))
K19(((REAL \ NAT) \/ {REAL})) is non empty set
(REAL \ NAT) \ ((x \ NAT) \/ {REAL}) is V33() V34() V35() Element of K19(REAL)
{REAL} \/ (x \ NAT) is non empty set
{REAL} \ ({REAL} \/ (x \ NAT)) is Element of K19({REAL})
K19({REAL}) is non empty set
((REAL \ NAT) \ ((x \ NAT) \/ {REAL})) \/ ({REAL} \ ({REAL} \/ (x \ NAT))) is set
((REAL \ NAT) \ ((x \ NAT) \/ {REAL})) \/ {} is V33() V34() V35() set
(REAL \ NAT) \ (x \ NAT) is V33() V34() V35() Element of K19(REAL)
((REAL \ NAT) \ (x \ NAT)) \ {REAL} is V33() V34() V35() Element of K19(REAL)
NAT \/ (x \ NAT) is non empty V33() V34() V35() set
REAL \ (NAT \/ (x \ NAT)) is V33() V34() V35() Element of K19(REAL)
(REAL \ (NAT \/ (x \ NAT))) \ {REAL} is V33() V34() V35() Element of K19(REAL)
NAT \/ x is non empty V33() V34() V35() set
REAL \ (NAT \/ x) is V33() V34() V35() Element of K19(REAL)
(REAL \ (NAT \/ x)) \ {REAL} is V33() V34() V35() Element of K19(REAL)
g " (f `) is V33() V34() V35() Element of K19( the carrier of R^1)
[#] () is non empty non proper closed Element of K19( the carrier of ())
([#] ()) \ f is Element of K19( the carrier of ())
f is set
NAT /\ f is V33() V34() V35() V36() V37() V38() Element of K19(REAL)
g is set
the epsilon-transitive epsilon-connected ordinal natural V28() real ext-real non negative Element of NAT /\ f is epsilon-transitive epsilon-connected ordinal natural V28() real ext-real non negative Element of NAT /\ f
g is set
f is V33() V34() V35() Element of K19( the carrier of R^1)
NAT /\ f is V33() V34() V35() V36() V37() V38() Element of K19( the carrier of R^1)
g is Element of K19( the carrier of ())
K20( the carrier of R^1, the carrier of ()) is Relation-like non empty set
K19(K20( the carrier of R^1, the carrier of ())) is non empty set
x is Relation-like the carrier of R^1 -defined the carrier of () -valued Function-like V18( the carrier of R^1, the carrier of ()) Element of K19(K20( the carrier of R^1, the carrier of ()))
g ` is Element of K19( the carrier of ())
the carrier of () \ g is set
x " (g `) is V33() V34() V35() Element of K19( the carrier of R^1)
f ` is V33() V34() V35() Element of K19( the carrier of R^1)
the carrier of R^1 \ f is V33() V34() V35() set
REAL \ f is V33() V34() V35() Element of K19(REAL)
((REAL \ NAT) \/ {REAL}) \ f is Element of K19(((REAL \ NAT) \/ {REAL}))
K19(((REAL \ NAT) \/ {REAL})) is non empty set
(((REAL \ NAT) \/ {REAL}) \ f) \ {REAL} is Element of K19(((REAL \ NAT) \/ {REAL}))
((((REAL \ NAT) \/ {REAL}) \ f) \ {REAL}) \/ NAT is non empty set
a is set
a is set
(g `) \ {REAL} is Element of K19( the carrier of ())
a is set
[#] () is non empty non proper closed Element of K19( the carrier of ())
([#] ()) \ g is Element of K19( the carrier of ())
a is set
((g `) \ {REAL}) \/ {REAL} is non empty set
((id REAL) +* (NAT --> REAL)) " (g `) is set
(([#] ()) \ g) \ {REAL} is Element of K19( the carrier of ())
((([#] ()) \ g) \ {REAL}) \/ NAT is non empty set
g is Element of K19( the carrier of ())
f is V33() V34() V35() Element of K19( the carrier of R^1)
((REAL \ NAT) \/ {REAL}) \ {REAL} is Element of K19(((REAL \ NAT) \/ {REAL}))
K19(((REAL \ NAT) \/ {REAL})) is non empty set
a is set
a is set
x is V33() V34() V35() Element of K19( the carrier of R^1)
x /\ NAT is V33() V34() V35() V36() V37() V38() Element of K19(REAL)
a is Element of K19( the carrier of ())
g ` is Element of K19( the carrier of ())
the carrier of () \ g is set
S9 is V33() V34() V35() Element of K19( the carrier of R^1)
S is V33() V34() V35() Element of K19( the carrier of R^1)
S ` is V33() V34() V35() Element of K19( the carrier of R^1)
the carrier of R^1 \ S is V33() V34() V35() set
f is Element of the carrier of ()
K19(K19( the carrier of ())) is non empty set
g is non empty open f -quasi_basis Element of K19(K19( the carrier of ()))
K20(NAT,g) is Relation-like non empty set
K19(K20(NAT,g)) is non empty set
x is Relation-like NAT -defined g -valued Function-like V18( NAT ,g) Element of K19(K20(NAT,g))
rng x is Element of K19(g)
K19(g) is non empty set
a is set
x . a is set
dom x is V33() V34() V35() V36() V37() V38() Element of K19(NAT)
K19(NAT) is non empty set
S9 is epsilon-transitive epsilon-connected ordinal natural V28() real ext-real non negative V33() V34() V35() V36() V37() V38() Element of NAT
U1 is V28() real ext-real Element of the carrier of RealSpace
Ball (U1,(1 / 4)) is V33() V34() V35() Element of K19( the carrier of RealSpace)
K19( the carrier of RealSpace) is non empty set
S is Element of K19( the carrier of ())
n is Element of K19( the carrier of ())
m is V33() V34() V35() Element of K19( the carrier of R^1)
m \ NAT is V33() V34() V35() Element of K19( the carrier of R^1)
(m \ NAT) \/ {REAL} is non empty set
O is V33() V34() V35() Element of K19( the carrier of R^1)
S9 is V33() V34() V35() Element of K19( the carrier of R^1)
S9 /\ O is V33() V34() V35() Element of K19( the carrier of R^1)
dist (U1,U1) is V28() real ext-real Element of REAL
m /\ (Ball (U1,(1 / 4))) is V33() V34() V35() Element of K19( the carrier of RealSpace)
m /\ O is V33() V34() V35() Element of K19( the carrier of R^1)
z is V28() real ext-real set
Ball (U1,z) is V33() V34() V35() Element of K19( the carrier of RealSpace)
z9 is V28() real ext-real Element of REAL
S9 + z9 is V28() real ext-real Element of REAL
S9 - z9 is V28() real ext-real Element of REAL
K105(z9) is V28() real ext-real set
K103(S9,K105(z9)) is V28() real ext-real set
r is V28() real ext-real set
n is V28() real ext-real Element of REAL
1 / 2 is V28() real ext-real non negative Element of REAL
K106(2) is non empty V28() real ext-real positive non negative set
K104(1,K106(2)) is V28() real ext-real non negative set
- (1 / 2) is V28() real ext-real non positive Element of REAL
- z9 is V28() real ext-real Element of REAL
(- (1 / 2)) + S9 is V28() real ext-real Element of REAL
(- z9) + S9 is V28() real ext-real Element of REAL
z9 + S9 is V28() real ext-real Element of REAL
S9 - (1 / 2) is V28() real ext-real Element of REAL
K105((1 / 2)) is V28() real ext-real non positive set
K103(S9,K105((1 / 2))) is V28() real ext-real set
{ b₁ where b₁ is V28() real ext-real Element of REAL : ( not b₁ <= S9 - z9 & not S9 + z9 <= b₁ ) } is set
].(S9 - z9),(S9 + z9).[ is V33() V34() V35() Element of K19(REAL)
Ball (U1,z9) is V33() V34() V35() Element of K19( the carrier of RealSpace)
S9 - (1 / 4) is V28() real ext-real Element of REAL
K105((1 / 4)) is V28() real ext-real non positive set
K103(S9,K105((1 / 4))) is V28() real ext-real set
S9 + (1 / 4) is V28() real ext-real non negative Element of REAL
].(S9 - (1 / 4)),(S9 + (1 / 4)).[ is V33() V34() V35() Element of K19(REAL)
{ b₁ where b₁ is V28() real ext-real Element of REAL : ( not b₁ <= S9 - (1 / 4) & not S9 + (1 / 4) <= b₁ ) } is set
m is V28() real ext-real Element of REAL
m is epsilon-transitive epsilon-connected ordinal natural V28() real ext-real non negative V33() V34() V35() V36() V37() V38() Element of NAT
m is epsilon-transitive epsilon-connected ordinal natural V28() real ext-real non negative V33() V34() V35() V36() V37() V38() Element of NAT
m is epsilon-transitive epsilon-connected ordinal natural V28() real ext-real non negative V33() V34() V35() V36() V37() V38() Element of NAT
m + z9 is V28() real ext-real Element of REAL
S9 - m is V28() real ext-real Element of REAL
K105(m) is V28() real ext-real non positive set
K103(S9,K105(m)) is V28() real ext-real set
m + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V28() real ext-real positive non negative V33() V34() V35() V36() V37() V38() Element of NAT
m is epsilon-transitive epsilon-connected ordinal natural V28() real ext-real non negative V33() V34() V35() V36() V37() V38() Element of NAT
n + 0 is V28() real ext-real Element of REAL
{ b₁ where b₁ is V28() real ext-real Element of REAL : ( not b₁ <= S9 - z9 & not S9 + z9 <= b₁ ) } is set
].(S9 - z9),(S9 + z9).[ is V33() V34() V35() Element of K19(REAL)
Ball (U1,z9) is V33() V34() V35() Element of K19( the carrier of RealSpace)
S9 - (1 / 4) is V28() real ext-real Element of REAL
K105((1 / 4)) is V28() real ext-real non positive set
K103(S9,K105((1 / 4))) is V28() real ext-real set
S9 + (1 / 4) is V28() real ext-real non negative Element of REAL
].(S9 - (1 / 4)),(S9 + (1 / 4)).[ is V33() V34() V35() Element of K19(REAL)
(x . a) /\ ].(S9 - (1 / 4)),(S9 + (1 / 4)).[ is V33() V34() V35() Element of K19(REAL)
a is Relation-like Function-like set
dom a is set
rng a is set
S9 is Relation-like NAT -defined the carrier of R^1 -valued Function-like V18( NAT , the carrier of R^1) Element of K19(K20(NAT, the carrier of R^1))
rng S9 is V33() V34() V35() Element of K19( the carrier of R^1)
U1 is epsilon-transitive epsilon-connected ordinal natural V28() real ext-real non negative V33() V34() V35() V36() V37() V38() Element of NAT
S9 . U1 is V28() real ext-real Element of the carrier of R^1
U1 - (1 / 4) is V28() real ext-real Element of REAL
K105((1 / 4)) is V28() real ext-real non positive set
K103(U1,K105((1 / 4))) is V28() real ext-real set
U1 + (1 / 4) is V28() real ext-real non negative Element of REAL
].(U1 - (1 / 4)),(U1 + (1 / 4)).[ is V33() V34() V35() Element of K19(REAL)
x . U1 is Element of g
O is epsilon-transitive epsilon-connected ordinal natural V28() real ext-real non negative V33() V34() V35() V36() V37() V38() Element of NAT
O - (1 / 4) is V28() real ext-real Element of REAL
K103(O,K105((1 / 4))) is V28() real ext-real set
O + (1 / 4) is V28() real ext-real non negative Element of REAL
].(O - (1 / 4)),(O + (1 / 4)).[ is V33() V34() V35() Element of K19(REAL)
(x . U1) /\ ].(O - (1 / 4)),(O + (1 / 4)).[ is V33() V34() V35() Element of K19(REAL)
S is V33() V34() V35() Element of K19( the carrier of R^1)
[#] R^1 is non empty non proper V33() V34() V35() closed Element of K19( the carrier of R^1)
([#] R^1) \ S is V33() V34() V35() Element of K19( the carrier of R^1)
S ` is V33() V34() V35() Element of K19( the carrier of R^1)
the carrier of R^1 \ S is V33() V34() V35() set
(S `) \ NAT is V33() V34() V35() Element of K19( the carrier of R^1)
((S `) \ NAT) \/ {REAL} is non empty set
O is set
O is Element of K19( the carrier of ())
m is set
n is Element of K19( the carrier of ())
m is Element of K19( the carrier of ())
dom x is V33() V34() V35() V36() V37() V38() Element of K19(NAT)
K19(NAT) is non empty set
S9 is set
x . S9 is set
z9 is epsilon-transitive epsilon-connected ordinal natural V28() real ext-real non negative V33() V34() V35() V36() V37() V38() Element of NAT
x . z9 is Element of g
S9 . z9 is V28() real ext-real Element of the carrier of R^1
r is set
n is epsilon-transitive epsilon-connected ordinal natural V28() real ext-real non negative V33() V34() V35() V36() V37() V38() Element of NAT
n - (1 / 4) is V28() real ext-real Element of REAL
K105((1 / 4)) is V28() real ext-real non positive set
K103(n,K105((1 / 4))) is V28() real ext-real set
n + (1 / 4) is V28() real ext-real non negative Element of REAL
].(n - (1 / 4)),(n + (1 / 4)).[ is V33() V34() V35() Element of K19(REAL)
(x . z9) /\ ].(n - (1 / 4)),(n + (1 / 4)).[ is V33() V34() V35() Element of K19(REAL)
z is epsilon-transitive epsilon-connected ordinal natural V28() real ext-real non negative V33() V34() V35() V36() V37() V38() Element of NAT
x . z is Element of g
z9 is set
f is Element of K19( the carrier of ())
Cl f is Element of K19( the carrier of ())
K20(NAT, the carrier of ()) is Relation-like non empty set
K19(K20(NAT, the carrier of ())) is non empty set
g is Element of the carrier of ()
f \ {REAL} is Element of K19( the carrier of ())
x is set
x is V33() V34() V35() Element of K19( the carrier of R^1)
a is V28() real ext-real Element of the carrier of R^1
S9 is V33() V34() V35() Element of K19( the carrier of R^1)
U1 is V33() V34() V35() Element of K19( the carrier of R^1)
S is V33() V34() V35() Element of K19( the carrier of R^1)
U1 \ NAT is V33() V34() V35() Element of K19( the carrier of R^1)
(U1 \ NAT) /\ NAT is V33() V34() V35() V36() V37() V38() Element of K19(REAL)
O is V33() V34() V35() Element of K19( the carrier of R^1)
n is V33() V34() V35() Element of K19( the carrier of R^1)
O \ n is V33() V34() V35() Element of K19( the carrier of R^1)
m is Element of K19( the carrier of ())
S9 is Element of K19( the carrier of ())
f /\ S9 is Element of K19( the carrier of ())
S9 /\ U1 is V33() V34() V35() Element of K19( the carrier of R^1)
the Element of f /\ S9 is Element of f /\ S9
Cl S9 is V33() V34() V35() Element of K19( the carrier of R^1)
S is Relation-like NAT -defined the carrier of R^1 -valued Function-like V18( NAT , the carrier of R^1) Element of K19(K20(NAT, the carrier of R^1))
rng S is V33() V34() V35() Element of K19( the carrier of R^1)
(R^1,S) is V33() V34() V35() Element of K19( the carrier of R^1)
U1 is set
U1 is Relation-like NAT -defined the carrier of () -valued Function-like V18( NAT , the carrier of ()) Element of K19(K20(NAT, the carrier of ()))
rng U1 is Element of K19( the carrier of ())
((),U1) is Element of K19( the carrier of ())
n is Element of K19( the carrier of ())
O is Element of K19( the carrier of ())
n \ {REAL} is Element of K19( the carrier of ())
m is Element of K19( the carrier of ())
n \ m is Element of K19( the carrier of ())
S9 is V33() V34() V35() Element of K19( the carrier of R^1)
z is epsilon-transitive epsilon-connected ordinal natural V28() real ext-real non negative V33() V34() V35() V36() V37() V38() Element of NAT
z9 is epsilon-transitive epsilon-connected ordinal natural V28() real ext-real non negative V33() V34() V35() V36() V37() V38() Element of NAT
U1 . z9 is Element of the carrier of ()
S . z9 is V28() real ext-real Element of the carrier of R^1
NAT --> g is Relation-like NAT -defined the carrier of () -valued Function-like V18( NAT , the carrier of ()) T-Sequence-like Element of K19(K20(NAT, the carrier of ()))
x is Relation-like NAT -defined the carrier of () -valued Function-like V18( NAT , the carrier of ()) Element of K19(K20(NAT, the carrier of ()))
rng x is Element of K19( the carrier of ())
((),x) is Element of K19( the carrier of ())
{g} is non empty set
x is V33() V34() V35() Element of K19( the carrier of R^1)
the topology of R^1 is non empty Element of K19(K19( the carrier of R^1))
K19(K19( the carrier of R^1)) is non empty set
a is set
the carrier of (TopSpaceMetr RealSpace) is non empty set
S9 is V28() real ext-real Element of the carrier of R^1
S is Element of the carrier of (TopSpaceMetr RealSpace)
(RealSpace,S) is non empty countable open S -quasi_basis Element of K19(K19( the carrier of (TopSpaceMetr RealSpace)))
K19( the carrier of (TopSpaceMetr RealSpace)) is non empty set
K19(K19( the carrier of (TopSpaceMetr RealSpace))) is non empty set
K20(NAT,(RealSpace,S)) is Relation-like non empty set
K19(K20(NAT,(RealSpace,S))) is non empty set
U1 is V28() real ext-real Element of the carrier of RealSpace
n is Relation-like NAT -defined (RealSpace,S) -valued Function-like V18( NAT ,(RealSpace,S)) Element of K19(K20(NAT,(RealSpace,S)))
m is set
n . m is set
(n . m) /\ x is V33() V34() V35() Element of K19( the carrier of R^1)
S9 is epsilon-transitive epsilon-connected ordinal natural V28() real ext-real non negative V33() V34() V35() V36() V37() V38() Element of NAT
n . S9 is Element of (RealSpace,S)
z is V33() V34() V35() Element of K19( the carrier of R^1)
z /\ x is V33() V34() V35() Element of K19( the carrier of R^1)
the V28() real ext-real Element of z /\ x is V28() real ext-real Element of z /\ x
z9 is V28() real ext-real Element of z /\ x
m is Relation-like Function-like set
dom m is set
rng m is set
S9 is Relation-like NAT -defined the carrier of R^1 -valued Function-like V18( NAT , the carrier of R^1) Element of K19(K20(NAT, the carrier of R^1))
z is V33() V34() V35() Element of K19( the carrier of R^1)
z9 is V28() real ext-real set
Ball (U1,z9) is V33() V34() V35() Element of K19( the carrier of RealSpace)
K19( the carrier of RealSpace) is non empty set
r is V28() real ext-real Element of REAL
n is epsilon-transitive epsilon-connected ordinal natural V28() real ext-real non negative V33() V34() V35() V36() V37() V38() Element of NAT
1 / n is V28() real ext-real non negative Element of REAL
K106(n) is V28() real ext-real non negative set
K104(1,K106(n)) is V28() real ext-real non negative set
m is epsilon-transitive epsilon-connected ordinal natural V28() real ext-real non negative V33() V34() V35() V36() V37() V38() Element of NAT
S9 . m is V28() real ext-real Element of the carrier of R^1
n . m is Element of (RealSpace,S)
(n . m) /\ x is V33() V34() V35() Element of K19( the carrier of R^1)
m + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V28() real ext-real positive non negative V33() V34() V35() V36() V37() V38() Element of NAT
1 / (m + 1) is V28() real ext-real non negative Element of REAL
K106((m + 1)) is non empty V28() real ext-real positive non negative set
K104(1,K106((m + 1))) is V28() real ext-real non negative set
Ball (U1,(1 / (m + 1))) is V33() V34() V35() Element of K19( the carrier of RealSpace)
Ball (U1,r) is V33() V34() V35() Element of K19( the carrier of RealSpace)
rng S9 is V33() V34() V35() Element of K19( the carrier of R^1)
z is set
dom S9 is V33() V34() V35() V36() V37() V38() Element of K19(NAT)
K19(NAT) is non empty set
z9 is set
S9 . z9 is set
n . z9 is set
(n . z9) /\ x is V33() V34() V35() Element of K19( the carrier of R^1)
a is Relation-like Function-like set
dom a is set
rng a is set
bool the carrier of R^1 is non empty Element of K19(K19( the carrier of R^1))
S9 is set
S is set
a . S is set
S9 is Element of K19(K19( the carrier of R^1))
S is V33() V34() V35() Element of K19( the carrier of R^1)
U1 is set
a . U1 is set
union S9 is V33() V34() V35() Element of K19( the carrier of R^1)
(union S9) \ NAT is V33() V34() V35() Element of K19( the carrier of R^1)
((union S9) \ NAT) \/ {REAL} is non empty set
S is Element of K19( the carrier of ())
U1 is Element of K19( the carrier of ())
U1 /\ f is Element of K19( the carrier of ())
the Element of U1 /\ f is Element of U1 /\ f
n is set
m is set
a . m is set
(a . m) /\ f is Element of K19( the carrier of ())
O is set
a . O is set
a is V28() real ext-real Element of the carrier of R^1
S9 is Relation-like NAT -defined the carrier of R^1 -valued Function-like V18( NAT , the carrier of R^1) Element of K19(K20(NAT, the carrier of R^1))
rng S9 is V33() V34() V35() Element of K19( the carrier of R^1)
a is V28() real ext-real Element of the carrier of R^1
S9 is Relation-like NAT -defined the carrier of R^1 -valued Function-like V18( NAT , the carrier of R^1) Element of K19(K20(NAT, the carrier of R^1))
rng S9 is V33() V34() V35() Element of K19( the carrier of R^1)
S9 is Relation-like NAT -defined the carrier of R^1 -valued Function-like V18( NAT , the carrier of R^1) Element of K19(K20(NAT, the carrier of R^1))
rng S9 is V33() V34() V35() Element of K19( the carrier of R^1)
S is Relation-like NAT -defined the carrier of () -valued Function-like V18( NAT , the carrier of ()) Element of K19(K20(NAT, the carrier of ()))
rng S is Element of K19( the carrier of ())
((),S) is Element of K19( the carrier of ())
U1 is Element of K19( the carrier of ())
O is V33() V34() V35() Element of K19( the carrier of R^1)
O \ NAT is V33() V34() V35() Element of K19( the carrier of R^1)
(O \ NAT) \/ {REAL} is non empty set
n is epsilon-transitive epsilon-connected ordinal natural V28() real ext-real non negative V33() V34() V35() V36() V37() V38() Element of NAT
m is epsilon-transitive epsilon-connected ordinal natural V28() real ext-real non negative V33() V34() V35() V36() V37() V38() Element of NAT
S . m is Element of the carrier of ()
S9 . m is V28() real ext-real Element of the carrier of R^1
dom S9 is V33() V34() V35() V36() V37() V38() Element of K19(NAT)
K19(NAT) is non empty set
f is Relation-like Function-like set
g is Relation-like Function-like set
f +* g is Relation-like Function-like set
rng (f +* g) is set
rng f is set
rng g is set
(rng f) \/ (rng g) is set
x is set
dom f is set
dom g is set
(dom f) \ (dom g) is Element of K19((dom f))
K19((dom f)) is non empty set
f .: ((dom f) \ (dom g)) is set
(f .: ((dom f) \ (dom g))) \/ (rng g) is set
a is set
f . a is set
(f +* g) . a is set
g . a is set
f is V28() real ext-real Element of REAL