:: 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

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

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

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

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

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

(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

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

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

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

S is Element of the carrier of f

a is Element of K19(K19( the carrier of (TopSpaceMetr f)))

{ (Ball (S,(1 / b

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

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

K19( the carrier of f) is non empty set

{ H

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

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

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

( b

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 `))