:: SIMPLEX0 semantic presentation

REAL is set

NAT is non empty non trivial non empty-membered epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal Element of bool REAL

bool REAL is non empty subset-closed V120() V252() d.union-closed set

NAT is non empty non trivial non empty-membered epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal set

bool NAT is non empty non trivial non empty-membered non finite subset-closed V120() V252() d.union-closed set

K215() is TopStruct

the carrier of K215() is set

COMPLEX is set

RAT is set

INT is set

[:COMPLEX,COMPLEX:] is Relation-like set

bool [:COMPLEX,COMPLEX:] is non empty subset-closed V120() V252() d.union-closed set

[:[:COMPLEX,COMPLEX:],COMPLEX:] is Relation-like set

bool [:[:COMPLEX,COMPLEX:],COMPLEX:] is non empty subset-closed V120() V252() d.union-closed set

[:REAL,REAL:] is Relation-like set

bool [:REAL,REAL:] is non empty subset-closed V120() V252() d.union-closed set

[:[:REAL,REAL:],REAL:] is Relation-like set

bool [:[:REAL,REAL:],REAL:] is non empty subset-closed V120() V252() d.union-closed set

[:RAT,RAT:] is Relation-like set

bool [:RAT,RAT:] is non empty subset-closed V120() V252() d.union-closed set

[:[:RAT,RAT:],RAT:] is Relation-like set

bool [:[:RAT,RAT:],RAT:] is non empty subset-closed V120() V252() d.union-closed set

[:INT,INT:] is Relation-like set

bool [:INT,INT:] is non empty subset-closed V120() V252() d.union-closed set

[:[:INT,INT:],INT:] is Relation-like set

bool [:[:INT,INT:],INT:] is non empty subset-closed V120() V252() d.union-closed set

[:NAT,NAT:] is non empty non trivial non empty-membered Relation-like non finite set

[:[:NAT,NAT:],NAT:] is non empty non trivial non empty-membered Relation-like non finite set

bool [:[:NAT,NAT:],NAT:] is non empty non trivial non empty-membered non finite subset-closed V120() V252() d.union-closed set

bool NAT is non empty non trivial non empty-membered non finite subset-closed V120() V252() d.union-closed set

K440() is set

{} is empty ext-real non positive non negative epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V17() real Relation-like non-empty empty-yielding Function-like one-to-one constant functional finite finite-yielding finite-membered cardinal {} -element integer Function-yielding V200() set

the empty ext-real non positive non negative epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V17() real Relation-like non-empty empty-yielding Function-like one-to-one constant functional finite finite-yielding finite-membered cardinal {} -element integer Function-yielding V200() set is empty ext-real non positive non negative epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V17() real Relation-like non-empty empty-yielding Function-like one-to-one constant functional finite finite-yielding finite-membered cardinal {} -element integer Function-yielding V200() set

{{}} is non empty trivial functional finite finite-membered 1 -element subset-closed V120() V252() d.union-closed set

1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V17() real finite cardinal integer Element of NAT

K387({{}}) is M22({{}})

[:K387({{}}),{{}}:] is Relation-like set

bool [:K387({{}}),{{}}:] is non empty subset-closed V120() V252() d.union-closed set

K89(K387({{}}),{{}}) is set

0 is empty ext-real non positive non negative epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V17() real Relation-like non-empty empty-yielding Function-like one-to-one constant functional finite finite-yielding finite-membered cardinal {} -element integer Function-yielding V200() Element of NAT

K63(1) is ext-real non positive V17() real integer Element of REAL

[:{{}},NAT:] is non empty non trivial non empty-membered Relation-like non finite set

NAT \/ [:{{}},NAT:] is non empty set

[{},{}] is set

{{},{}} is non empty functional finite finite-membered set

{{{},{}},{{}}} is non empty with_non-empty_elements non empty-membered finite finite-membered set

{[{},{}]} is non empty trivial Relation-like Function-like constant finite 1 -element set

(NAT \/ [:{{}},NAT:]) \ {[{},{}]} is Element of bool (NAT \/ [:{{}},NAT:])

bool (NAT \/ [:{{}},NAT:]) is non empty subset-closed V120() V252() d.union-closed set

+infty is non empty ext-real positive non negative non real set

-infty is non empty ext-real non positive negative non real set

bool {} is non empty finite finite-membered subset-closed V120() V252() d.union-closed set

union {} is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V17() real finite cardinal integer set

X is set

n is set

KX is set

X is set

X is set

n is set

X is set

Sub_of_Fin X is Element of bool X

bool X is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set

n is set

X is subset-closed V252() set

Sub_of_Fin X is finite-membered Element of bool X

bool X is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set

n is set

KX is set

X is set

n is set

bool n is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed Element of bool (bool n)

bool n is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set

bool (bool n) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set

KX is set

n is set

KX is set

bool n is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed Element of bool (bool n)

bool n is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set

bool (bool n) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set

X is subset-closed V252() set

n is subset-closed V252() set

X \/ n is set

KX is set

SX is set

X /\ n is set

KX is set

SX is set

X is set

{ (bool b

union { (bool b

KX is set

SX is set

P is set

n is Element of X

bool n is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed Element of bool (bool n)

bool n is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set

bool (bool n) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set

KX is subset-closed V252() set

SX is set

bool SX is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed Element of bool (bool SX)

bool SX is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set

bool (bool SX) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set

SX is set

P is set

n is set

Pn is Element of X

bool Pn is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed Element of bool (bool Pn)

bool Pn is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set

bool (bool Pn) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set

X is set

{ (bool b

union { (bool b

n is subset-closed V252() set

n is subset-closed V252() set

KX is subset-closed V252() set

X is set

n is set

(n) is subset-closed V252() set

{ (bool b

union { (bool b

SX is subset-closed V252() set

P is set

n is Element of n

bool n is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed Element of bool (bool n)

bool n is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set

bool (bool n) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set

Pn is set

Fm is set

P is set

bool P is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed Element of bool (bool P)

bool P is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set

bool (bool P) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set

X is set

bool X is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set

bool (bool X) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set

n is Element of bool (bool X)

(n) is subset-closed V252() set

bool X is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed Element of bool (bool X)

SX is set

P is set

({}) is subset-closed V252() set

X is set

n is set

X is non empty set

(X) is subset-closed V252() set

n is set

X is non empty non empty-membered set

(X) is non empty non with_non-empty_elements subset-closed V252() set

n is non empty set

X is finite-membered set

(X) is subset-closed V252() set

n is set

KX is set

X is set

(X) is subset-closed V252() set

n is set

KX is set

SX is set

X is set

{X} is non empty trivial finite 1 -element set

({X}) is non empty non with_non-empty_elements subset-closed V252() set

bool X is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed Element of bool (bool X)

bool X is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set

bool (bool X) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set

KX is set

SX is set

KX is set

X is set

(X) is subset-closed V252() set

n is set

X \/ n is set

((X \/ n)) is subset-closed V252() set

(n) is subset-closed V252() set

(X) \/ (n) is subset-closed V252() set

n is set

Pn is set

n is set

Pn is set

Pn is set

X is set

(X) is subset-closed V252() set

n is set

(n) is subset-closed V252() set

P is set

n is set

Pn is set

P is set

n is set

X is set

(X) is subset-closed V252() set

KX is set

SX is set

X is set

(X) is subset-closed V252() set

KX is set

SX is set

X is set

bool X is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set

bool (bool X) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set

n is set

KX is set

card KX is epsilon-transitive epsilon-connected ordinal cardinal set

{ b

bool X is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed Element of bool (bool X)

P is set

n is Element of bool X

card n is epsilon-transitive epsilon-connected ordinal cardinal set

P is Element of bool (bool X)

n is Element of bool X

card n is epsilon-transitive epsilon-connected ordinal cardinal set

Pn is Element of bool X

card Pn is epsilon-transitive epsilon-connected ordinal cardinal set

SX is Element of bool (bool X)

P is Element of bool (bool X)

n is set

card n is epsilon-transitive epsilon-connected ordinal cardinal set

n is set

card n is epsilon-transitive epsilon-connected ordinal cardinal set

X is non empty set

bool X is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set

bool (bool X) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set

n is set

{n} is non empty trivial finite 1 -element set

bool {n} is non empty non with_non-empty_elements finite finite-membered subset-closed V120() V252() d.union-closed Element of bool (bool {n})

bool {n} is non empty non with_non-empty_elements finite finite-membered subset-closed V120() V252() d.union-closed set

bool (bool {n}) is non empty non with_non-empty_elements finite finite-membered subset-closed V120() V252() d.union-closed set

KX is Element of bool (bool X)

X is set

n is set

KX is finite set

(X,n,KX) is Element of bool (bool X)

bool X is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set

bool (bool X) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set

SX is set

card SX is epsilon-transitive epsilon-connected ordinal cardinal set

card KX is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V17() real finite cardinal integer Element of NAT

X is set

n is subset-closed V252() set

KX is set

(X,n,KX) is Element of bool (bool X)

bool X is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set

bool (bool X) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set

SX is set

P is set

card SX is epsilon-transitive epsilon-connected ordinal cardinal set

card KX is epsilon-transitive epsilon-connected ordinal cardinal set

card P is epsilon-transitive epsilon-connected ordinal cardinal set

X is set

n is non empty non with_non-empty_elements set

KX is set

(X,n,KX) is Element of bool (bool X)

bool X is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set

bool (bool X) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set

card {} is empty ext-real non positive non negative epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V17() real Relation-like non-empty empty-yielding Function-like one-to-one constant functional finite finite-yielding finite-membered cardinal {} -element integer subset-closed Function-yielding V200() V252() Element of NAT

card KX is epsilon-transitive epsilon-connected ordinal cardinal set

X is non empty set

bool X is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set

bool (bool X) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set

n is non empty non with_non-empty_elements non empty-membered subset-closed V252() Element of bool (bool X)

KX is non empty set

(X,n,KX) is non empty non with_non-empty_elements subset-closed V252() Element of bool (bool X)

SX is non empty set

P is set

card KX is non empty epsilon-transitive epsilon-connected ordinal cardinal set

{P} is non empty trivial finite 1 -element set

card {P} is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V17() real finite cardinal integer Element of NAT

X is set

bool X is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set

bool (bool X) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set

X is set

union X is set

n is set

KX is set

SX is set

X is c=-linear finite set

card X is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V17() real finite cardinal integer Element of NAT

union X is set

card (union X) is epsilon-transitive epsilon-connected ordinal cardinal set

n is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V17() real finite cardinal integer set

n + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V17() real finite cardinal integer Element of NAT

KX is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V17() real finite cardinal integer set

SX is c=-linear finite set

union SX is set

card (union SX) is epsilon-transitive epsilon-connected ordinal cardinal set

card SX is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V17() real finite cardinal integer Element of NAT

P is finite set

{P} is non empty trivial finite finite-membered 1 -element set

SX \ {P} is c=-linear finite Element of bool SX

bool SX is non empty non with_non-empty_elements finite finite-membered subset-closed V120() V252() d.union-closed set

n is c=-linear finite set

n \/ {P} is non empty finite set

union n is set

union {P} is finite set

(union n) \/ (union {P}) is set

(union n) \/ P is set

Pn is finite set

card Pn is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V17() real finite cardinal integer Element of NAT

card n is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V17() real finite cardinal integer Element of NAT

card P is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V17() real finite cardinal integer Element of NAT

1 + (card n) is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V17() real finite cardinal integer Element of NAT

n is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V17() real finite cardinal integer set

KX is c=-linear finite set

union KX is set

card (union KX) is epsilon-transitive epsilon-connected ordinal cardinal set

card KX is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V17() real finite cardinal integer Element of NAT

X is set

union X is set

n is set

(union X) \/ n is set

{((union X) \/ n)} is non empty trivial finite 1 -element set

X \/ {((union X) \/ n)} is non empty set

P is set

n is set

X is non empty set

bool X is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set

bool (bool X) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set

card X is non empty epsilon-transitive epsilon-connected ordinal cardinal set

n is Relation-like set

n |_2 X is Relation-like set

bool X is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed Element of bool (bool X)

SX is set

(n |_2 X) -Seg SX is set

X \ ((n |_2 X) -Seg SX) is Element of bool X

[:X,(bool X):] is non empty Relation-like set

bool [:X,(bool X):] is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set

SX is Relation-like X -defined bool X -valued Function-like V33(X, bool X) Element of bool [:X,(bool X):]

bool (bool X) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set

rng SX is Element of bool (bool X)

P is Element of bool (bool X)

card P is epsilon-transitive epsilon-connected ordinal cardinal set

dom SX is Element of bool X

n is set

SX . n is set

(n |_2 X) -Seg n is set

X \ ((n |_2 X) -Seg n) is Element of bool X

n is set

Pn is set

Fm is set

SX . Fm is set

m is set

SX . m is set

(n |_2 X) -Seg Fm is set

(n |_2 X) -Seg m is set

X \ ((n |_2 X) -Seg m) is Element of bool X

X \ ((n |_2 X) -Seg Fm) is Element of bool X

field (n |_2 X) is set

n is set

(n |_2 X) -Seg n is set

Pn is set

[Pn,n] is set

{Pn,n} is non empty finite set

{Pn} is non empty trivial finite 1 -element set

{{Pn,n},{Pn}} is non empty with_non-empty_elements non empty-membered finite finite-membered set

[n,Pn] is set

{n,Pn} is non empty finite set

{n} is non empty trivial finite 1 -element set

{{n,Pn},{n}} is non empty with_non-empty_elements non empty-membered finite finite-membered set

SX . n is set

X \ ((n |_2 X) -Seg n) is Element of bool X

Pn is set

(n |_2 X) -Seg Pn is set

Fm is set

(n |_2 X) -Seg Fm is set

SX . Pn is set

SX . Fm is set

m is Element of bool X

m ` is Element of bool X

X \ m is set

SX is Element of bool X

SX ` is Element of bool X

X \ SX is set

[Pn,Fm] is set

{Pn,Fm} is non empty finite set

{Pn} is non empty trivial finite 1 -element set

{{Pn,Fm},{Pn}} is non empty with_non-empty_elements non empty-membered finite finite-membered set

[Fm,Pn] is set

{Fm,Pn} is non empty finite set

{Fm} is non empty trivial finite 1 -element set

{{Fm,Pn},{Fm}} is non empty with_non-empty_elements non empty-membered finite finite-membered set

Pn is set

card Pn is epsilon-transitive epsilon-connected ordinal cardinal set

Fm is set

SX . Fm is set

{Fm} is non empty trivial finite 1 -element set

Pn \ {Fm} is Element of bool Pn

bool Pn is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set

(n |_2 X) -Seg Fm is set

X \ ((n |_2 X) -Seg Fm) is Element of bool X

((n |_2 X) -Seg Fm) \/ {Fm} is non empty set

m is Element of bool X

X \ m is Element of bool X

m \ ((n |_2 X) -Seg Fm) is Element of bool X

{Fm} \ ((n |_2 X) -Seg Fm) is trivial finite Element of bool {Fm}

bool {Fm} is non empty non with_non-empty_elements finite finite-membered subset-closed V120() V252() d.union-closed set

m ` is Element of bool X

X \ m is set

SX is set

(n |_2 X) -Seg SX is set

[Fm,SX] is set

{Fm,SX} is non empty finite set

{{Fm,SX},{Fm}} is non empty with_non-empty_elements non empty-membered finite finite-membered set

[SX,Fm] is set

{SX,Fm} is non empty finite set

{SX} is non empty trivial finite 1 -element set

{{SX,Fm},{SX}} is non empty with_non-empty_elements non empty-membered finite finite-membered set

SX . SX is set

(X \ ((n |_2 X) -Seg Fm)) \ {Fm} is Element of bool X

X is set

bool X is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set

bool (bool X) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set

card X is epsilon-transitive epsilon-connected ordinal cardinal set

n is Element of bool (bool X)

KX is set

{ b

P is set

n is Element of bool X

P is Element of bool (bool X)

n is set

Pn is Element of bool X

Pn is set

KX is Relation-like Function-like set

dom KX is set

bool X is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed Element of bool (bool X)

SX is set

{ b

n is set

Pn is Element of bool X

n is Element of bool (bool X)

union n is Element of bool X

Pn is Element of bool X

Fm is set

Fm is set

Fm is set

Fm is set

m is Element of bool X

Fm is set

[:n,(bool X):] is Relation-like set

bool [:n,(bool X):] is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set

SX is Relation-like n -defined bool X -valued Function-like V33(n, bool X) Element of bool [:n,(bool X):]

P is set

SX . P is set

P \ (SX . P) is Element of bool P

bool P is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set

bool (P \ (SX . P)) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed Element of bool (bool (P \ (SX . P)))

bool (P \ (SX . P)) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set

bool (bool (P \ (SX . P))) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set

[:(P \ (SX . P)),(bool (P \ (SX . P))):] is Relation-like set

bool [:(P \ (SX . P)),(bool (P \ (SX . P))):] is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set

card (P \ (SX . P)) is epsilon-transitive epsilon-connected ordinal cardinal set

n is Element of bool (bool (P \ (SX . P)))

card n is epsilon-transitive epsilon-connected ordinal cardinal set

Pn is Relation-like Function-like set

dom Pn is set

rng Pn is set

Fm is Relation-like P \ (SX . P) -defined bool (P \ (SX . P)) -valued Function-like V33(P \ (SX . P), bool (P \ (SX . P))) Element of bool [:(P \ (SX . P)),(bool (P \ (SX . P))):]

P is Relation-like Function-like set

dom P is set

n is set

SX . n is set

n \ (SX . n) is Element of bool n

bool n is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set

bool (n \ (SX . n)) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed Element of bool (bool (n \ (SX . n)))

bool (n \ (SX . n)) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set

bool (bool (n \ (SX . n))) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set

[:(n \ (SX . n)),(bool (n \ (SX . n))):] is Relation-like set

bool [:(n \ (SX . n)),(bool (n \ (SX . n))):] is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set

P . n is set

Pn is Relation-like n \ (SX . n) -defined bool (n \ (SX . n)) -valued Function-like V33(n \ (SX . n), bool (n \ (SX . n))) Element of bool [:(n \ (SX . n)),(bool (n \ (SX . n))):]

rng Pn is Element of bool (bool (n \ (SX . n)))

bool (bool (n \ (SX . n))) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set

dom Pn is Element of bool (n \ (SX . n))

n is Relation-like Function-like Function-yielding V200() set

Pn is set

KX . Pn is set

SX . (KX . Pn) is set

(KX . Pn) \ (SX . (KX . Pn)) is Element of bool (KX . Pn)

bool (KX . Pn) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set

Pn is set

KX . Pn is set

SX . (KX . Pn) is set

n . (KX . Pn) is Relation-like Function-like set

(n . (KX . Pn)) . Pn is set

(SX . (KX . Pn)) \/ ((n . (KX . Pn)) . Pn) is set

(KX . Pn) \ (SX . (KX . Pn)) is Element of bool (KX . Pn)

bool (KX . Pn) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set

bool ((KX . Pn) \ (SX . (KX . Pn))) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed Element of bool (bool ((KX . Pn) \ (SX . (KX . Pn))))

bool ((KX . Pn) \ (SX . (KX . Pn))) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set

bool (bool ((KX . Pn) \ (SX . (KX . Pn)))) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set

[:((KX . Pn) \ (SX . (KX . Pn))),(bool ((KX . Pn) \ (SX . (KX . Pn)))):] is Relation-like set

bool [:((KX . Pn) \ (SX . (KX . Pn))),(bool ((KX . Pn) \ (SX . (KX . Pn)))):] is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set

m is Relation-like (KX . Pn) \ (SX . (KX . Pn)) -defined bool ((KX . Pn) \ (SX . (KX . Pn))) -valued Function-like V33((KX . Pn) \ (SX . (KX . Pn)), bool ((KX . Pn) \ (SX . (KX . Pn)))) Element of bool [:((KX . Pn) \ (SX . (KX . Pn))),(bool ((KX . Pn) \ (SX . (KX . Pn)))):]

rng m is Element of bool (bool ((KX . Pn) \ (SX . (KX . Pn))))

bool (bool ((KX . Pn) \ (SX . (KX . Pn)))) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set

dom m is Element of bool ((KX . Pn) \ (SX . (KX . Pn)))

m . Pn is set

[:X,(bool X):] is Relation-like set

bool [:X,(bool X):] is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set

Pn is Relation-like X -defined bool X -valued Function-like V33(X, bool X) Element of bool [:X,(bool X):]

dom Pn is Element of bool X

rng Pn is Element of bool (bool X)

bool (bool X) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set

Fm is set

SX . Fm is set

Fm \ (SX . Fm) is Element of bool Fm

bool Fm is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set

bool (Fm \ (SX . Fm)) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed Element of bool (bool (Fm \ (SX . Fm)))

bool (Fm \ (SX . Fm)) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set

bool (bool (Fm \ (SX . Fm))) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set

[:(Fm \ (SX . Fm)),(bool (Fm \ (SX . Fm))):] is Relation-like set

bool [:(Fm \ (SX . Fm)),(bool (Fm \ (SX . Fm))):] is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set

n . Fm is Relation-like Function-like set

m is Relation-like Fm \ (SX . Fm) -defined bool (Fm \ (SX . Fm)) -valued Function-like V33(Fm \ (SX . Fm), bool (Fm \ (SX . Fm))) Element of bool [:(Fm \ (SX . Fm)),(bool (Fm \ (SX . Fm))):]

rng m is Element of bool (bool (Fm \ (SX . Fm)))

bool (bool (Fm \ (SX . Fm))) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set

dom m is Element of bool (Fm \ (SX . Fm))

SX is set

m . SX is set

KX . SX is set

Pn . SX is set

(SX . Fm) \/ (Fm \ (SX . Fm)) is set

Fm is set

card Fm is epsilon-transitive epsilon-connected ordinal cardinal set

m is set

Pn . m is set

KX . m is set

SX . (KX . m) is set

(KX . m) \ (SX . (KX . m)) is Element of bool (KX . m)

bool (KX . m) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set

bool ((KX . m) \ (SX . (KX . m))) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed Element of bool (bool ((KX . m) \ (SX . (KX . m))))

bool ((KX . m) \ (SX . (KX . m))) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set

bool (bool ((KX . m) \ (SX . (KX . m)))) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set

[:((KX . m) \ (SX . (KX . m))),(bool ((KX . m) \ (SX . (KX . m)))):] is Relation-like set

bool [:((KX . m) \ (SX . (KX . m))),(bool ((KX . m) \ (SX . (KX . m)))):] is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set

n . (KX . m) is Relation-like Function-like set

c

rng c

bool (bool ((KX . m) \ (SX . (KX . m)))) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set

dom c

c

(SX . (KX . m)) \/ (c

card (c

TOP1 is set

{TOP1} is non empty trivial finite 1 -element set

Fm \ {TOP1} is Element of bool Fm

bool Fm is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set

((SX . (KX . m)) \/ (c

bool ((SX . (KX . m)) \/ (c

(SX . (KX . m)) \ (c

bool (SX . (KX . m)) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set

card (c

TOP1 is set

{TOP1} is non empty trivial finite 1 -element set

(c

bool (c

Fm \ {TOP1} is Element of bool Fm

bool Fm is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set

K2 is set

c

KX . K2 is set

Pn . K2 is set

(SX . (KX . m)) \/ ((c

((SX . (KX . m)) \/ (c

bool ((SX . (KX . m)) \/ (c

card (c

Fm is set

m is set

SX is set

Pn . SX is set

c

Pn . c

KX . SX is set

KX . c

SX . (KX . SX) is set

(KX . SX) \ (SX . (KX . SX)) is Element of bool (KX . SX)

bool (KX . SX) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set

bool ((KX . SX) \ (SX . (KX . SX))) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed Element of bool (bool ((KX . SX) \ (SX . (KX . SX))))

bool ((KX . SX) \ (SX . (KX . SX))) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set

bool (bool ((KX . SX) \ (SX . (KX . SX)))) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set

[:((KX . SX) \ (SX . (KX . SX))),(bool ((KX . SX) \ (SX . (KX . SX)))):] is Relation-like set

bool [:((KX . SX) \ (SX . (KX . SX))),(bool ((KX . SX) \ (SX . (KX . SX)))):] is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set

n . (KX . SX) is Relation-like Function-like set

TOP2 is Relation-like (KX . SX) \ (SX . (KX . SX)) -defined bool ((KX . SX) \ (SX . (KX . SX))) -valued Function-like V33((KX . SX) \ (SX . (KX . SX)), bool ((KX . SX) \ (SX . (KX . SX)))) Element of bool [:((KX . SX) \ (SX . (KX . SX))),(bool ((KX . SX) \ (SX . (KX . SX)))):]

rng TOP2 is Element of bool (bool ((KX . SX) \ (SX . (KX . SX))))

bool (bool ((KX . SX) \ (SX . (KX . SX)))) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set

dom TOP2 is Element of bool ((KX . SX) \ (SX . (KX . SX)))

TOP2 . SX is set

(SX . (KX . SX)) \/ (TOP2 . SX) is set

SX . (KX . c

(KX . c

bool (KX . c

bool ((KX . c

bool ((KX . c

bool (bool ((KX . c

[:((KX . c

bool [:((KX . c

n . (KX . c

H2 is Relation-like (KX . c

rng H2 is Element of bool (bool ((KX . c

bool (bool ((KX . c

dom H2 is Element of bool ((KX . c

H2 . c

(SX . (KX . c

TOP2 . c

(SX . (KX . SX)) \/ ((KX . SX) \ (SX . (KX . SX))) is set

(SX . (KX . c

Fm is set

Pn . Fm is set

KX . Fm is set

SX . (KX . Fm) is set

(KX . Fm) \ (SX . (KX . Fm)) is Element of bool (KX . Fm)

bool (KX . Fm) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set

bool ((KX . Fm) \ (SX . (KX . Fm))) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed Element of bool (bool ((KX . Fm) \ (SX . (KX . Fm))))

bool ((KX . Fm) \ (SX . (KX . Fm))) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set

bool (bool ((KX . Fm) \ (SX . (KX . Fm)))) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set

[:((KX . Fm) \ (SX . (KX . Fm))),(bool ((KX . Fm) \ (SX . (KX . Fm)))):] is Relation-like set

bool [:((KX . Fm) \ (SX . (KX . Fm))),(bool ((KX . Fm) \ (SX . (KX . Fm)))):] is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set

n . (KX . Fm) is Relation-like Function-like set

SX is Relation-like (KX . Fm) \ (SX . (KX . Fm)) -defined bool ((KX . Fm) \ (SX . (KX . Fm))) -valued Function-like V33((KX . Fm) \ (SX . (KX . Fm)), bool ((KX . Fm) \ (SX . (KX . Fm)))) Element of bool [:((KX . Fm) \ (SX . (KX . Fm))),(bool ((KX . Fm) \ (SX . (KX . Fm)))):]

rng SX is Element of bool (bool ((KX . Fm) \ (SX . (KX . Fm))))

bool (bool ((KX . Fm) \ (SX . (KX . Fm)))) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set

dom SX is Element of bool ((KX . Fm) \ (SX . (KX . Fm)))

SX . Fm is set

(SX . (KX . Fm)) \/ (SX . Fm) is set

card (rng Pn) is epsilon-transitive epsilon-connected ordinal cardinal set

Fm is set

m is set

Pn . Fm is set

Pn . m is set

KX . Fm is set

KX . m is set

SX . (KX . Fm) is set

n . (KX . Fm) is Relation-like Function-like set

(n . (KX . Fm)) . Fm is set

(SX . (KX . Fm)) \/ ((n . (KX . Fm)) . Fm) is set

SX . (KX . m) is set

n . (KX . m) is Relation-like Function-like set

(n . (KX . m)) . m is set

(SX . (KX . m)) \/ ((n . (KX . m)) . m) is set

(KX . m) \ (SX . (KX . m)) is Element of bool (KX . m)

bool (KX . m) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set

bool ((KX . m) \ (SX . (KX . m))) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed Element of bool (bool ((KX . m) \ (SX . (KX . m))))

bool ((KX . m) \ (SX . (KX . m))) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set

bool (bool ((KX . m) \ (SX . (KX . m)))) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set

[:((KX . m) \ (SX . (KX . m))),(bool ((KX . m) \ (SX . (KX . m)))):] is Relation-like set

bool [:((KX . m) \ (SX . (KX . m))),(bool ((KX . m) \ (SX . (KX . m)))):] is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set

TOP1 is Relation-like (KX . m) \ (SX . (KX . m)) -defined bool ((KX . m) \ (SX . (KX . m))) -valued Function-like V33((KX . m) \ (SX . (KX . m)), bool ((KX . m) \ (SX . (KX . m)))) Element of bool [:((KX . m) \ (SX . (KX . m))),(bool ((KX . m) \ (SX . (KX . m)))):]

rng TOP1 is Element of bool (bool ((KX . m) \ (SX . (KX . m))))

bool (bool ((KX . m) \ (SX . (KX . m)))) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set

dom TOP1 is Element of bool ((KX . m) \ (SX . (KX . m)))

TOP1 . m is set

(KX . Fm) \ (SX . (KX . Fm)) is Element of bool (KX . Fm)

bool (KX . Fm) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set

bool ((KX . Fm) \ (SX . (KX . Fm))) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed Element of bool (bool ((KX . Fm) \ (SX . (KX . Fm))))

bool ((KX . Fm) \ (SX . (KX . Fm))) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set

bool (bool ((KX . Fm) \ (SX . (KX . Fm)))) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set

[:((KX . Fm) \ (SX . (KX . Fm))),(bool ((KX . Fm) \ (SX . (KX . Fm)))):] is Relation-like set

bool [:((KX . Fm) \ (SX . (KX . Fm))),(bool ((KX . Fm) \ (SX . (KX . Fm)))):] is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set

K2 is Relation-like (KX . Fm) \ (SX . (KX . Fm)) -defined bool ((KX . Fm) \ (SX . (KX . Fm))) -valued Function-like V33((KX . Fm) \ (SX . (KX . Fm)), bool ((KX . Fm) \ (SX . (KX . Fm)))) Element of bool [:((KX . Fm) \ (SX . (KX . Fm))),(bool ((KX . Fm) \ (SX . (KX . Fm)))):]

rng K2 is Element of bool (bool ((KX . Fm) \ (SX . (KX . Fm))))

bool (bool ((KX . Fm) \ (SX . (KX . Fm)))) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set

dom K2 is Element of bool ((KX . Fm) \ (SX . (KX . Fm)))

K2 . Fm is set

K2 . m is set

(SX . (KX . Fm)) \/ ((KX . Fm) \ (SX . (KX . Fm))) is set

(SX . (KX . m)) \/ ((KX . m) \ (SX . (KX . m))) is set

Fm is set

card Fm is epsilon-transitive epsilon-connected ordinal cardinal set

X is TopStruct

the carrier of X is set

bool the carrier of X is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set

X is TopStruct

the carrier of X is set

bool the carrier of X is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set

bool (bool the carrier of X) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set

X is TopStruct

the carrier of X is set

bool the carrier of X is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set

bool (bool the carrier of X) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set

bool the carrier of X is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed Element of bool (bool the carrier of X)

bool (bool the carrier of X) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set

{} (bool the carrier of X) is empty proper ext-real non positive non negative epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V17() real Relation-like non-empty empty-yielding Function-like one-to-one constant functional finite finite-yielding finite-membered cardinal {} -element integer subset-closed Function-yielding V200() V252() Element of bool (bool the carrier of X)

n is empty proper ext-real non positive non negative epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V17() real Relation-like non-empty empty-yielding Function-like one-to-one constant functional finite finite-yielding finite-membered cardinal {} -element integer subset-closed Function-yielding V200() V252() Element of bool (bool the carrier of X)

KX is Element of bool the carrier of X

X is TopStruct

the carrier of X is set

bool the carrier of X is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set

bool (bool the carrier of X) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set

the topology of X is Element of bool (bool the carrier of X)

n is Element of bool (bool the carrier of X)

KX is set

SX is Element of bool the carrier of X

KX is Element of bool the carrier of X

X is TopStruct

the carrier of X is set

X is TopStruct

the carrier of X is set

bool the carrier of X is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set

{ b

[#] X is non proper Element of bool the carrier of X

KX is set

SX is Element of the carrier of X

P is Element of bool the carrier of X

KX is Element of bool the carrier of X

SX is Element of the carrier of X

P is Element of the carrier of X

n is Element of bool the carrier of X

KX is Element of bool the carrier of X

SX is set

P is Element of the carrier of X

SX is set

P is Element of the carrier of X

X is set

the empty trivial finite {} -element T_0 finite-membered finite-degree TopStruct is empty trivial finite {} -element T_0 finite-membered finite-degree TopStruct

[#] the empty trivial finite {} -element T_0 finite-membered finite-degree TopStruct is empty trivial non proper ext-real non positive non negative epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V17() real Relation-like non-empty empty-yielding Function-like one-to-one constant functional finite finite-yielding finite-membered cardinal {} -element integer subset-closed Function-yielding V200() V252() Element of bool the carrier of the empty trivial finite {} -element T_0 finite-membered finite-degree TopStruct

the carrier of the empty trivial finite {} -element T_0 finite-membered finite-degree TopStruct is empty trivial ext-real non positive non negative epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V17() real Relation-like non-empty empty-yielding Function-like one-to-one constant functional finite finite-yielding finite-membered cardinal {} -element integer subset-closed Function-yielding V200() V252() set

bool the carrier of the empty trivial finite {} -element T_0 finite-membered finite-degree TopStruct is non empty non with_non-empty_elements finite finite-membered subset-closed V120() V252() d.union-closed set

X is set

X is TopStruct

(X) is Element of bool the carrier of X

the carrier of X is set

bool the carrier of X is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set

the topology of X is Element of bool (bool the carrier of X)

bool (bool the carrier of X) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set

n is non empty set

the Element of n is Element of n

KX is Element of bool the carrier of X

SX is Element of the carrier of X

n is set

KX is Element of the carrier of X

SX is Element of bool the carrier of X

X is set

n is TopStruct

the carrier of n is set

bool the carrier of n is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set

(n) is Element of bool the carrier of n

KX is Element of bool the carrier of n

SX is Element of the carrier of n

X is TopStruct

the carrier of X is set

bool the carrier of X is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set

(X) is Element of bool the carrier of X

n is Element of bool the carrier of X

KX is set

X is TopStruct

(X) is Element of bool the carrier of X

the carrier of X is set

bool the carrier of X is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set

the topology of X is Element of bool (bool the carrier of X)

bool (bool the carrier of X) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set

union the topology of X is Element of bool the carrier of X

n is set

KX is Element of the carrier of X

SX is Element of bool the carrier of X

n is set

KX is set

SX is Element of bool the carrier of X

X is TopStruct

the topology of X is Element of bool (bool the carrier of X)

the carrier of X is set

bool the carrier of X is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set

bool (bool the carrier of X) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set

(X) is Element of bool the carrier of X

union the topology of X is Element of bool the carrier of X

bool (X) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed Element of bool (bool (X))

bool (X) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set

bool (bool (X)) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set

X is TopStruct

the topology of X is Element of bool (bool the carrier of X)

the carrier of X is set

bool the carrier of X is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set

bool (bool the carrier of X) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set

X is TopStruct

the topology of X is Element of bool (bool the carrier of X)

the carrier of X is set

bool the carrier of X is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set

bool (bool the carrier of X) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set

X is TopStruct

the topology of X is Element of bool (bool the carrier of X)

the carrier of X is set

bool the carrier of X is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set

bool (bool the carrier of X) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set

X is TopStruct

the_family_of X is Element of bool (bool the carrier of X)

the carrier of X is set

bool the carrier of X is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set

bool (bool the carrier of X) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set

the topology of X is Element of bool (bool the carrier of X)

n is set

X is TopStruct

the topology of X is Element of bool (bool the carrier of X)

the carrier of X is set

bool the carrier of X is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set

bool (bool the carrier of X) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set

n is set

the_family_of X is Element of bool (bool the carrier of X)

KX is set

(X) is Element of bool the carrier of X

X is TopStruct

the carrier of X is set

bool the carrier of X is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set

(X) is Element of bool the carrier of X

KX is Element of (X)

{ b

the topology of X is Element of bool (bool the carrier of X)

bool (bool the carrier of X) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set

SX is set

P is Element of bool the carrier of X

KX is set

the_family_of X is Element of bool (bool the carrier of X)

bool (bool the carrier of X) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set

the topology of X is Element of bool (bool the carrier of X)

SX is Element of bool the carrier of X

n is finite Element of bool the carrier of X

n is finite Element of bool the carrier of X

card n is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V17() real finite cardinal integer Element of NAT

KX is finite Element of bool the carrier of X

card KX is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V17() real finite cardinal integer Element of NAT

X is TopStruct

the_family_of X is Element of bool (bool the carrier of X)

the carrier of X is set

bool the carrier of X is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set

bool (bool the carrier of X) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set

the topology of X is Element of bool (bool the carrier of X)

n is set

KX is Element of bool the carrier of X

SX is set

P is Element of the carrier of X

(X) is Element of bool the carrier of X

n is Element of (X)

{n} is non empty trivial finite 1 -element set

KX \ {n} is Element of bool the carrier of X

{ b

bool (KX \ {n}) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set

bool (KX \ {n}) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed Element of bool (bool (KX \ {n}))

bool (bool (KX \ {n})) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set

{ b

( S

SX is set

c

c

(c

bool (c

{ b

c

TOP1 is Element of bool the carrier of X

c

c

bool c

TOP1 is Element of bool (KX \ {n})

K2 is Element of bool (KX \ {n})

(KX \ {n}) \/ {n} is non empty set

X is set

bool {} is non empty non with_non-empty_elements finite finite-membered subset-closed V120() V252() d.union-closed Element of bool (bool {})

bool (bool {}) is non empty non with_non-empty_elements finite finite-membered subset-closed V120() V252() d.union-closed set

{} (bool {}) is empty proper ext-real non positive non negative epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V17() real Relation-like non-empty empty-yielding Function-like one-to-one constant functional finite finite-yielding finite-membered cardinal {} -element integer subset-closed Function-yielding V200() V252() Element of bool (bool {})

bool (bool {}) is non empty non with_non-empty_elements finite finite-membered subset-closed V120() V252() d.union-closed set

TopStruct(# {},({} (bool {})) #) is strict TopStruct

[#] TopStruct(# {},({} (bool {})) #) is non proper Element of bool the carrier of TopStruct(# {},({} (bool {})) #)

the carrier of TopStruct(# {},({} (bool {})) #) is set

bool the carrier of TopStruct(# {},({} (bool {})) #) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set

n is (X)

X is non empty set

bool X is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set

bool (bool X) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set

bool {} is non empty non with_non-empty_elements finite finite-membered subset-closed V120() V252() d.union-closed Element of bool (bool {})

bool (bool {}) is non empty non with_non-empty_elements finite finite-membered subset-closed V120() V252() d.union-closed set

n is Element of bool (bool X)

TopStruct(# X,n #) is non empty strict TopStruct

[#] TopStruct(# X,n #) is non empty non proper Element of bool the carrier of TopStruct(# X,n #)

the carrier of TopStruct(# X,n #) is non empty set

bool the carrier of TopStruct(# X,n #) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set

KX is (X)

SX is non empty set

[#] KX is non proper Element of bool the carrier of KX

the carrier of KX is set

bool the carrier of KX is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set

the Element of X is Element of X

bool X is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set

bool (bool X) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set

{ the Element of X} is non empty trivial finite 1 -element Element of bool X

bool { the Element of X} is non empty non with_non-empty_elements finite finite-membered subset-closed V120() V252() d.union-closed Element of bool (bool { the Element of X})

bool { the Element of X} is non empty non with_non-empty_elements finite finite-membered subset-closed V120() V252() d.union-closed set

bool (bool { the Element of X}) is non empty non with_non-empty_elements finite finite-membered subset-closed V120() V252() d.union-closed set

KX is Element of bool (bool X)

TopStruct(# X,KX #) is non empty strict TopStruct

[#] TopStruct(# X,KX #) is non empty non proper Element of bool the carrier of TopStruct(# X,KX #)

the carrier of TopStruct(# X,KX #) is non empty set

bool the carrier of TopStruct(# X,KX #) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set

[#] X is non empty non proper Element of bool X

SX is (X)

(SX) is Element of bool the carrier of SX

the carrier of SX is set

bool the carrier of SX is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set

P is set

n is Element of the carrier of SX

Pn is Element of bool the carrier of SX

[#] SX is non proper Element of bool the carrier of SX

the_family_of SX is Element of bool (bool the carrier of SX)

bool (bool the carrier of SX) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set

the topology of SX is Element of bool (bool the carrier of SX)

the non empty set is non empty set

the non empty strict non void subset-closed finite-membered finite-degree () () () () ( the non empty set ) is non empty strict non void subset-closed finite-membered finite-degree () () () () ( the non empty set )

X is non void () TopStruct

(X) is Element of bool the carrier of X

the carrier of X is set

bool the carrier of X is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set

X is finite-membered finite-degree () () TopStruct

the carrier of X is set

bool the carrier of X is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set

bool (bool the carrier of X) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set

n is Element of bool (bool the carrier of X)

the topology of X is Element of bool (bool the carrier of X)

(X) is Element of bool the carrier of X

union the topology of X is Element of bool the carrier of X

bool (X) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed Element of bool (bool (X))

bool (X) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set

bool (bool (X)) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set

X is finite-membered TopStruct

the carrier of X is set

bool the carrier of X is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set

bool (bool the carrier of X) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set

n is Element of bool (bool the carrier of X)

KX is set

SX is Element of bool the carrier of X

the topology of X is Element of bool (bool the carrier of X)

the_family_of X is Element of bool (bool the carrier of X)

X is TopStruct

(X) is Element of bool the carrier of X

the carrier of X is set

bool the carrier of X is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set

n is TopStruct

(n) is Element of bool the carrier of n

the carrier of n is set

bool the carrier of n is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set

X is TopStruct

(X) is Element of bool the carrier of X

the carrier of X is set

bool the carrier of X is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set

the topology of X is Element of bool (bool the carrier of X)

bool (bool the carrier of X) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set

union the topology of X is Element of bool the carrier of X

X is TopStruct

the carrier of X is set

bool the carrier of X is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set

n is Element of bool the carrier of X

(X) is Element of bool the carrier of X

X is TopStruct

the topology of X is Element of bool (bool the carrier of X)

the carrier of X is set

bool the carrier of X is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set

bool (bool the carrier of X) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set

X is TopStruct

the topology of X is Element of bool (bool the carrier of X)

the carrier of X is set

bool the carrier of X is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set

bool (bool the carrier of X) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set

(X) is Element of bool the carrier of X

union the topology of X is Element of bool the carrier of X

KX is set

SX is set

[:(X), the topology of X:] is Relation-like set

bool [:(X), the topology of X:] is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set

KX is Relation-like (X) -defined the topology of X -valued Function-like V33((X), the topology of X) Element of bool [:(X), the topology of X:]

dom KX is Element of bool (X)

bool (X) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set

rng KX is Element of bool the topology of X

bool the topology of X is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set

SX is set

{SX} is non empty trivial finite 1 -element set

KX " {SX} is Element of bool (X)

P is Element of bool the carrier of X

{P} is non empty trivial finite 1 -element Element of bool (bool the carrier of X)

KX " {P} is Element of bool (X)

n is set

KX . n is set

the_family_of X is Element of bool (bool the carrier of X)

X is TopStruct

the topology of X is Element of bool (bool the carrier of X)

the carrier of X is set

bool the carrier of X is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set

bool (bool the carrier of X) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set

the_family_of X is Element of bool (bool the carrier of X)

n is set

{n} is non empty trivial finite 1 -element set

({n}) is non empty non with_non-empty_elements subset-closed V252() set

bool n is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed Element of bool (bool n)

bool n is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set

bool (bool n) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set

X is set

bool X is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set

bool (bool X) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set

n is Element of bool (bool X)

(X,n) is subset-closed V252() Element of bool (bool X)

TopStruct(# X,(X,n) #) is strict TopStruct

[#] TopStruct(# X,(X,n) #) is non proper Element of bool the carrier of TopStruct(# X,(X,n) #)

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

bool the carrier of TopStruct(# X,(X,n) #) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set

X is set

bool X is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set

bool (bool X) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set

n is Element of bool (bool X)

(X,n) is strict (X)

(X,n) is subset-closed V252() Element of bool (bool X)

TopStruct(# X,(X,n) #) is strict TopStruct

[#] (X,n) is non proper Element of bool the carrier of (X,n)

the carrier of (X,n) is set

bool the carrier of (X,n) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set

the_family_of TopStruct(# X,(X,n) #) is Element of bool (bool the carrier of TopStruct(# X,(X,n) #))

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

bool the carrier of TopStruct(# X,(X,n) #) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set

bool (bool the carrier of TopStruct(# X,(X,n) #)) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set

the topology of TopStruct(# X,(X,n) #) is Element of bool (bool the carrier of TopStruct(# X,(X,n) #))

X is set

bool X is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set

bool (bool X) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set

n is non empty Element of bool (bool X)

(X,n) is strict subset-closed (X) (X)

(X,n) is non empty non with_non-empty_elements subset-closed V252() Element of bool (bool X)

TopStruct(# X,(X,n) #) is strict TopStruct

X is set

bool X is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set

bool (bool X) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set

n is finite-membered Element of bool (bool X)

(X,n) is strict subset-closed (X) (X)

(X,n) is finite-membered subset-closed V252() Element of bool (bool X)

TopStruct(# X,(X,n) #) is strict TopStruct

the_family_of (X,n) is subset-closed V252() Element of bool (bool the carrier of (X,n))

the carrier of (X,n) is set

bool the carrier of (X,n) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set

bool (bool the carrier of (X,n)) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set

the topology of (X,n) is Element of bool (bool the carrier of (X,n))

X is set

bool X is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set

bool (bool X) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set

n is finite finite-membered Element of bool (bool X)

(X,n) is strict subset-closed finite-membered (X) (X)

(X,n) is finite-membered subset-closed V252() Element of bool (bool X)

TopStruct(# X,(X,n) #) is strict TopStruct

union n is finite Element of bool X

bool (union n) is non empty non with_non-empty_elements finite finite-membered subset-closed V120() V252() d.union-closed set

bool (bool (union n)) is non empty non with_non-empty_elements finite finite-membered subset-closed V120() V252() d.union-closed set

SX is finite finite-membered Element of bool (bool (union n))

((union n),SX) is finite finite-membered subset-closed V252() Element of bool (bool (union n))

bool (union n) is non empty non with_non-empty_elements finite finite-membered subset-closed V120() V252() d.union-closed Element of bool (bool (union n))

the carrier of (X,n) is set

the topology of (X,n) is Element of bool (bool the carrier of (X,n))

bool the carrier of (X,n) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set

bool (bool the carrier of (X,n)) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set

union the topology of (X,n) is Element of bool the carrier of (X,n)

union (bool (union n)) is finite Element of bool (union n)

((X,n)) is Element of bool the carrier of (X,n)

X is TopStruct

the carrier of X is set

the topology of X is Element of bool (bool the carrier of X)

bool the carrier of X is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set

bool (bool the carrier of X) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set

TopStruct(# the carrier of X, the topology of X #) is strict TopStruct

( the carrier of X, the topology of X) is strict subset-closed ( the carrier of X) ( the carrier of X)

( the carrier of X, the topology of X) is subset-closed V252() Element of bool (bool the carrier of X)

TopStruct(# the carrier of X,( the carrier of X, the topology of X) #) is strict TopStruct

the_family_of X is Element of bool (bool the carrier of X)

X is non void () TopStruct

the carrier of X is set

bool the carrier of X is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set

n is Element of bool the carrier of X

the topology of X is non empty Element of bool (bool the carrier of X)

bool (bool the carrier of X) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set

{} X is empty ext-real non positive non negative epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V17() real Relation-like non-empty empty-yielding Function-like one-to-one constant functional finite finite-yielding finite-membered cardinal {} -element open integer subset-closed Function-yielding V200() V252() Element of bool the carrier of X

X is non void finite-membered TopStruct

the carrier of X is set

bool the carrier of X is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set

the topology of X is non empty Element of bool (bool the carrier of X)

bool (bool the carrier of X) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set

n is set

KX is finite open Element of bool the carrier of X

X is TopStruct

the carrier of X is set

bool the carrier of X is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set

- 1 is non empty ext-real non positive negative V17() real set

K58(1) is ext-real non positive V17() real integer set

the_family_of X is Element of bool (bool the carrier of X)

bool (bool the carrier of X) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set

the topology of X is Element of bool (bool the carrier of X)

n is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V17() real finite cardinal integer set

n - 1 is ext-real V17() real set

n + (- 1) is ext-real V17() real set

K56(n,(- 1)) is ext-real V17() real set

K60(n,1) is ext-real V17() real integer set

KX is ext-real