:: 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₁) where b₁ is Element of X : b₁ in X } is set
union { (bool b₁) where b₁ is Element of X : b₁ in X } is set
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₁) where b₁ is Element of X : b₁ in X } is set
union { (bool b₁) where b₁ is Element of X : b₁ in X } is set
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₁) where b₁ is Element of n : b₁ in n } is set
union { (bool b₁) where b₁ is Element of n : b₁ in n } is set
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₁ where b₁ is Element of bool X : ( b₁ in n & card b₁ c= card 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)
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₁ where b₁ is Element of bool X : ( KX in b₁ & b₁ in n ) } is set
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₁ where b₁ is Element of bool X : ( b₁ c< SX & b₁ in n ) } is set
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₁₁ 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 c₁₁ 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 c₁₁ is Element of bool ((KX . m) \ (SX . (KX . m)))
c₁₁ . m is set
(SX . (KX . m)) \/ (c₁₁ . m) is set
card (c₁₁ . m) is epsilon-transitive epsilon-connected ordinal cardinal set
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₁₁ . m)) \ (c₁₁ . m) is Element of bool ((SX . (KX . m)) \/ (c₁₁ . m))
bool ((SX . (KX . m)) \/ (c₁₁ . m)) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set
(SX . (KX . m)) \ (c₁₁ . m) is Element of bool (SX . (KX . m))
bool (SX . (KX . m)) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set
card (c₁₁ . m) is epsilon-transitive epsilon-connected ordinal cardinal set
TOP1 is set
{TOP1} is non empty trivial finite 1 -element set
(c₁₁ . m) \ {TOP1} is Element of bool (c₁₁ . m)
bool (c₁₁ . m) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed 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
K2 is set
c₁₁ . K2 is set
KX . K2 is set
Pn . K2 is set
(SX . (KX . m)) \/ ((c₁₁ . m) \ {TOP1}) is set
((SX . (KX . m)) \/ (c₁₁ . m)) \ {TOP1} is Element of bool ((SX . (KX . m)) \/ (c₁₁ . m))
bool ((SX . (KX . m)) \/ (c₁₁ . m)) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set
card (c₁₁ . m) is epsilon-transitive epsilon-connected ordinal cardinal set
Fm is set
m is set
SX is set
Pn . SX is set
c₁₁ is set
Pn . c₁₁ is set
KX . SX is set
KX . c₁₁ is set
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₁₁) is set
(KX . c₁₁) \ (SX . (KX . c₁₁)) is Element of bool (KX . c₁₁)
bool (KX . c₁₁) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set
bool ((KX . c₁₁) \ (SX . (KX . c₁₁))) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed Element of bool (bool ((KX . c₁₁) \ (SX . (KX . c₁₁))))
bool ((KX . c₁₁) \ (SX . (KX . c₁₁))) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set
bool (bool ((KX . c₁₁) \ (SX . (KX . c₁₁)))) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set
[:((KX . c₁₁) \ (SX . (KX . c₁₁))),(bool ((KX . c₁₁) \ (SX . (KX . c₁₁)))):] is Relation-like set
bool [:((KX . c₁₁) \ (SX . (KX . c₁₁))),(bool ((KX . c₁₁) \ (SX . (KX . c₁₁)))):] is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set
n . (KX . c₁₁) is Relation-like Function-like set
H2 is Relation-like (KX . c₁₁) \ (SX . (KX . c₁₁)) -defined bool ((KX . c₁₁) \ (SX . (KX . c₁₁))) -valued Function-like V33((KX . c₁₁) \ (SX . (KX . c₁₁)), bool ((KX . c₁₁) \ (SX . (KX . c₁₁)))) Element of bool [:((KX . c₁₁) \ (SX . (KX . c₁₁))),(bool ((KX . c₁₁) \ (SX . (KX . c₁₁)))):]
rng H2 is Element of bool (bool ((KX . c₁₁) \ (SX . (KX . c₁₁))))
bool (bool ((KX . c₁₁) \ (SX . (KX . c₁₁)))) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set
dom H2 is Element of bool ((KX . c₁₁) \ (SX . (KX . c₁₁)))
H2 . c₁₁ is set
(SX . (KX . c₁₁)) \/ (H2 . c₁₁) is set
TOP2 . c₁₁ is set
(SX . (KX . SX)) \/ ((KX . SX) \ (SX . (KX . SX))) is set
(SX . (KX . c₁₁)) \/ ((KX . c₁₁) \ (SX . (KX . c₁₁))) is set
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₁ where b₁ is Element of the carrier of X : b₁ is (X) } is set
[#] 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₁ where b₁ is Element of bool the carrier of X : ( b₁ is open & KX in b₁ ) } is 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
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₁ where b₁ is Element of bool the carrier of X : ( n in b₁ & b₁ c= KX ) } is set
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₁ where b₁ is Element of bool (KX \ {n}) : ex b₂ being Element of bool the carrier of X st
( S₁[b₂,b₁] & b₂ in { b₁ where b₃ is Element of bool the carrier of X : ( n in b₁ & b₁ c= KX ) } ) } is set
SX is set
c₁₁ is Element of bool the carrier of X
c₁₁ \/ {n} is non empty set
(c₁₁ \/ {n}) \ {n} is Element of bool (c₁₁ \/ {n})
bool (c₁₁ \/ {n}) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set
{ b₁ where b₁ is Element of bool the carrier of X : ( b₁ is open & n in b₁ ) } is set
c₁₁ is set
TOP1 is Element of bool the carrier of X
c₁₁ is Element of bool the carrier of X
c₁₁ \ {n} is Element of bool c₁₁
bool c₁₁ is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set
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 V17() real set
KX + 1 is ext-real V17() real set
K56(KX,1) is ext-real V17() real set
SX is finite Element of bool the carrier of X
card SX is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V17() real finite cardinal integer Element of NAT
SX is set
P is finite Element of bool the carrier of X
card P is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V17() real finite cardinal integer Element of NAT
SX is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V17() real finite cardinal integer Element of NAT
P is finite Element of bool the carrier of X
card P is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V17() real finite cardinal integer Element of NAT
SX + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V17() real finite cardinal integer Element of NAT
SX + 1 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 V17() real set
n + 1 is ext-real V17() real set
K56(n,1) is ext-real V17() real set
KX is Element of bool the carrier of X
card KX is epsilon-transitive epsilon-connected ordinal cardinal set
n is ext-real set
n + 1 is ext-real set
KX is ext-real set
KX + 1 is ext-real set
SX is Element of bool the carrier of X
card SX is epsilon-transitive epsilon-connected ordinal cardinal set
P is Element of bool the carrier of X
card P is epsilon-transitive epsilon-connected ordinal cardinal set
SX is Element of bool the carrier of X
card SX is epsilon-transitive epsilon-connected ordinal cardinal set
P is Element of bool the carrier of X
card P is epsilon-transitive epsilon-connected ordinal cardinal set
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
Pn is finite Element of bool the carrier of X
card Pn is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V17() real finite cardinal integer Element of NAT
n is ext-real set
n + 1 is ext-real set
KX is Element of bool the carrier of X
card KX is epsilon-transitive epsilon-connected ordinal cardinal set
SX is finite Element of bool the carrier of X
card SX is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V17() real finite cardinal integer Element of NAT
X is finite-membered finite-degree TopStruct
(X) is ext-real set
(X) + 1 is ext-real set
(- 1) + 1 is ext-real V17() real set
K56((- 1),1) is ext-real V17() real set
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
card n is epsilon-transitive epsilon-connected ordinal cardinal 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)
((X) + 1) - 1 is ext-real V17() real set
((X) + 1) + (- 1) is ext-real V17() real set
K56(((X) + 1),(- 1)) is ext-real V17() real set
K60(((X) + 1),1) is ext-real V17() real integer set
X is TopStruct
(X) is ext-real set
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 non empty set
KX is Element of bool the carrier of X
SX is finite Element of bool the carrier of X
card SX is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V17() real finite cardinal integer Element of NAT
(- 1) + 1 is ext-real V17() real set
K56((- 1),1) is ext-real V17() real set
(X) + 1 is ext-real set
n is Element of bool the carrier of X
card n is epsilon-transitive epsilon-connected ordinal cardinal set
X is TopStruct
(X) is ext-real set
(- 1) + 1 is ext-real V17() real set
K56((- 1),1) is ext-real V17() real set
n is ext-real V17() real integer set
n + 1 is ext-real V17() real set
K56(n,1) is ext-real V17() real integer 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 ext-real set
(X) + 1 is ext-real set
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
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
X is ext-real V17() real integer set
X + 1 is ext-real V17() real set
K56(X,1) is ext-real V17() real integer set
n is TopStruct
(n) is ext-real set
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
KX is finite Element of bool the carrier of n
the topology of n is Element of bool (bool the carrier of n)
bool (bool the carrier of n) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set
card KX 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 n
card KX is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V17() real finite cardinal integer Element of NAT
(n) + 1 is ext-real set
KX is finite Element of bool the carrier of n
card KX is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V17() real finite cardinal integer Element of NAT
the topology of n is Element of bool (bool the carrier of n)
bool (bool the carrier of n) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set
KX is set
SX is Element of bool the carrier of n
P is finite Element of bool the carrier of n
card P is ext-real 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 Element of NAT
Pn is finite Element of bool the carrier of n
card Pn is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V17() real finite cardinal integer Element of NAT
Pn is ext-real V17() real integer set
Pn + 1 is ext-real V17() real set
K56(Pn,1) is ext-real V17() real integer set
Fm is Element of bool the carrier of n
card Fm is epsilon-transitive epsilon-connected ordinal cardinal set
X is set
bool X is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set
n is finite Element of bool X
{n} is non empty trivial finite finite-membered 1 -element Element of bool (bool X)
bool (bool X) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set
(X,{n}) is strict non void subset-closed finite-membered finite-degree () () () (X) (X)
(X,{n}) is non empty non with_non-empty_elements finite-membered subset-closed V252() Element of bool (bool X)
TopStruct(# X,(X,{n}) #) is strict TopStruct
((X,{n})) is ext-real V17() real integer set
card n is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V17() real finite cardinal integer Element of NAT
(card n) - 1 is ext-real V17() real set
(card n) + (- 1) is ext-real V17() real set
K56((card n),(- 1)) is ext-real V17() real set
K60((card n),1) is ext-real V17() real integer set
the topology of (X,{n}) is non empty 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
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
SX is finite Element of bool the carrier of (X,{n})
card SX is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V17() real finite cardinal integer Element of NAT
((card n) - 1) + 1 is ext-real V17() real set
K56(((card n) - 1),1) is ext-real V17() real set
SX is finite open Element of bool the carrier of (X,{n})
card SX is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V17() real finite cardinal integer Element of NAT
((X,{n})) + 1 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V17() real finite cardinal integer set
K56(((X,{n})),1) is ext-real V17() real integer set
X is set
n is (X)
[#] n is non proper 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
the topology of n is Element of bool (bool the carrier of n)
bool (bool the carrier of n) 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
{} (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
the_family_of TopStruct(# {},({} (bool {})) #) is Element of bool (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
bool (bool the carrier of TopStruct(# {},({} (bool {})) #)) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set
the topology of TopStruct(# {},({} (bool {})) #) is Element of bool (bool the carrier of TopStruct(# {},({} (bool {})) #))
[#] TopStruct(# {},({} (bool {})) #) is non proper Element of bool the carrier of TopStruct(# {},({} (bool {})) #)
SX is subset-closed finite-membered (X)
[#] SX is non proper 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
the topology 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
X is set
n is (X)
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
({},({} (bool {}))) is strict subset-closed finite-membered finite-degree () () ( {} ) ( {} )
({},({} (bool {}))) is finite finite-membered subset-closed V252() Element of bool (bool {})
TopStruct(# {},({},({} (bool {}))) #) is strict TopStruct
the topology of ({},({} (bool {}))) is Element of bool (bool the carrier of ({},({} (bool {}))))
the carrier of ({},({} (bool {}))) is set
bool the carrier of ({},({} (bool {}))) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set
bool (bool the carrier of ({},({} (bool {})))) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set
[#] ({},({} (bool {}))) is non proper Element of bool the carrier of ({},({} (bool {})))
[#] n is non proper 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
the topology of n is Element of bool (bool the carrier of n)
bool (bool the carrier of n) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set
SX is subset-closed finite-membered (X,n)
X is set
n is void (X)
KX is subset-closed finite-membered (X,n)
the topology of KX is Element of bool (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
bool (bool the carrier of KX) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set
the topology of n is Element of bool (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
bool (bool the carrier of n) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set
X is non empty set
n is non void subset-closed () (X)
the_family_of n is subset-closed V252() Element of bool (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
bool (bool the carrier of n) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set
the topology of n is non empty Element of bool (bool the carrier of n)
KX is set
SX 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 n
{SX} is non empty trivial functional finite finite-membered 1 -element Element of bool (bool the carrier of n)
( the carrier of n,{SX}) is strict non void subset-closed finite-membered finite-degree () () () ( the carrier of n) ( the carrier of n)
( the carrier of n,{SX}) is non empty non with_non-empty_elements finite-membered subset-closed V252() Element of bool (bool the carrier of n)
TopStruct(# the carrier of n,( the carrier of n,{SX}) #) is strict TopStruct
[#] ( the carrier of n,{SX}) is non proper Element of bool the carrier of ( the carrier of n,{SX})
the carrier of ( the carrier of n,{SX}) is set
bool the carrier of ( the carrier of n,{SX}) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set
[#] n is non proper Element of bool the carrier of n
n is subset-closed finite-membered (X)
the Element of KX is Element of KX
{ the Element of KX} is non empty trivial finite 1 -element set
P is Element of bool the carrier of n
{P} is non empty trivial finite 1 -element Element of bool (bool the carrier of n)
( the carrier of n,{P}) is strict non void subset-closed () ( the carrier of n) ( the carrier of n)
( the carrier of n,{P}) is non empty non with_non-empty_elements subset-closed V252() Element of bool (bool the carrier of n)
TopStruct(# the carrier of n,( the carrier of n,{P}) #) is strict TopStruct
[#] ( the carrier of n,{P}) is non proper Element of bool the carrier of ( the carrier of n,{P})
the carrier of ( the carrier of n,{P}) is set
bool the carrier of ( the carrier of n,{P}) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set
[#] n is non proper Element of bool the carrier of n
Pn is subset-closed finite-membered (X)
the topology of Pn is Element of bool (bool the carrier of Pn)
the carrier of Pn is set
bool the carrier of Pn is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set
bool (bool the carrier of Pn) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set
X is set
n is finite-membered finite-degree () () (X)
KX is subset-closed finite-membered (X,n)
(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
the topology of KX is Element of bool (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
bool (bool the carrier of KX) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set
the topology of n is Element of bool (bool the carrier of n)
bool (bool the carrier of n) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set
union the topology of KX is Element of bool the carrier of KX
union the topology of n is Element of bool the carrier of n
(KX) is Element of bool the carrier of KX
X is set
n is finite-membered finite-degree (X)
KX is subset-closed finite-membered (X,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
SX is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V17() real finite cardinal integer set
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
P is finite Element of bool the carrier of KX
card P is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V17() real finite cardinal integer Element of NAT
the topology of KX is Element of bool (bool the carrier of KX)
bool (bool the carrier of KX) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set
[#] KX is non proper Element of bool the carrier of KX
[#] n is non proper Element of bool the carrier of n
the topology of n is Element of bool (bool the carrier of n)
bool (bool the carrier of n) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set
n is finite Element of bool the carrier of n
X is set
n is (X)
KX is subset-closed finite-membered (X,n)
SX is subset-closed finite-membered (X,KX)
[#] 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
[#] n is non proper 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
[#] SX is non proper 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
the topology of KX is Element of bool (bool the carrier of KX)
bool (bool the carrier of KX) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set
the topology of n is Element of bool (bool the carrier of n)
bool (bool the carrier of n) 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)
bool (bool the carrier of SX) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set
X is set
n is (X)
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
the topology of n is Element of bool (bool the carrier of n)
bool (bool the carrier of n) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set
KX is Element of bool the carrier of n
bool KX is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set
bool (bool KX) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set
SX is finite-membered Element of bool (bool KX)
(KX,SX) is finite-membered subset-closed V252() Element of bool (bool KX)
(KX,SX) is strict subset-closed finite-membered (KX) (KX)
TopStruct(# KX,(KX,SX) #) is strict TopStruct
[#] n is non proper Element of bool the carrier of n
[#] (KX,SX) is non proper Element of bool the carrier of (KX,SX)
the carrier of (KX,SX) is set
bool the carrier of (KX,SX) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set
X is set
n is subset-closed (X)
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
the topology of n is Element of bool (bool the carrier of n)
bool (bool the carrier of n) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set
KX is Element of bool the carrier of n
bool KX is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set
bool (bool KX) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set
SX is finite-membered Element of bool (bool KX)
(KX,SX) is strict subset-closed finite-membered (KX) (KX)
(KX,SX) is finite-membered subset-closed V252() Element of bool (bool KX)
TopStruct(# KX,(KX,SX) #) is strict TopStruct
the_family_of n is subset-closed V252() Element of bool (bool the carrier of 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 Element of bool (bool X)
KX is Element of bool (bool X)
(X,n) is strict subset-closed (X) (X)
(X,n) is subset-closed V252() Element of bool (bool X)
TopStruct(# X,(X,n) #) is strict TopStruct
(X,KX) is strict subset-closed (X) (X)
(X,KX) is subset-closed V252() Element of bool (bool X)
TopStruct(# X,(X,KX) #) 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
[#] (X,KX) is non proper Element of bool the carrier of (X,KX)
the carrier of (X,KX) is set
bool the carrier of (X,KX) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set
X is set
n is (X)
(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
KX is subset-closed finite-membered (X,n)
(KX) is 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
SX is set
P is Element of the carrier of KX
n is Element of bool the carrier of KX
the topology of KX is Element of bool (bool the carrier of KX)
bool (bool the carrier of KX) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set
the topology of n is Element of bool (bool the carrier of n)
bool (bool the carrier of n) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set
Pn is Element of bool the carrier of n
Fm is Element of the carrier of n
X is set
n is (X)
(n) is ext-real set
KX is subset-closed finite-membered (X,n)
(KX) is ext-real set
the topology of KX is Element of bool (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
bool (bool the carrier of KX) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set
the topology of n is Element of bool (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
bool (bool the carrier of n) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set
(KX) + 1 is ext-real set
SX is Element of bool the carrier of KX
card SX is epsilon-transitive epsilon-connected ordinal cardinal set
P is finite Element of bool the carrier of n
(n) + 1 is ext-real set
((KX) + 1) - 1 is ext-real set
((KX) + 1) + (- 1) is ext-real set
((n) + 1) - 1 is ext-real set
((n) + 1) + (- 1) is ext-real set
X is set
n is (X)
X is set
n is (X)
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
the topology of n is Element of bool (bool the carrier of n)
bool (bool the carrier of n) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set
KX is subset-closed finite-membered (X,n)
[#] 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
bool ([#] KX) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed Element of bool (bool ([#] KX))
bool ([#] KX) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set
bool (bool ([#] KX)) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set
(bool ([#] KX)) /\ the topology of n is Element of bool (bool the carrier of n)
the topology of KX is Element of bool (bool the carrier of KX)
bool (bool the carrier of KX) 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 KX
SX is Element of bool the carrier of KX
X is set
n is (X)
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
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
the topology of n is Element of bool (bool the carrier of n)
bool (bool the carrier of n) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set
(bool {}) /\ the topology of n is finite Element of bool (bool the carrier of n)
{} n 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 bool the carrier of 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
SX is finite finite-membered subset-closed V252() Element of bool (bool ({} n))
(({} n),SX) is finite finite-membered subset-closed V252() Element of bool (bool ({} n))
(({} n),SX) is strict subset-closed finite-membered finite-degree () () ( {} n) ( {} n)
TopStruct(# ({} n),(({} n),SX) #) is strict TopStruct
P is strict subset-closed finite-membered (X,n)
TopStruct(# ({} n),SX #) is strict TopStruct
[#] P is non proper Element of bool the carrier of P
the carrier of P is set
bool the carrier of P is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed 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
n is (X)
KX is subset-closed finite-membered (X,n)
SX is subset-closed finite-membered (X,KX)
[#] SX is non proper 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
[#] 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
P is subset-closed finite-membered (X,n)
the carrier of P is set
bool the carrier of P is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set
n is Element of bool the carrier of P
the topology of n is Element of bool (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
bool (bool the carrier of n) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set
Pn is Element of bool the carrier of KX
the topology of KX is Element of bool (bool the carrier of KX)
bool (bool the carrier of KX) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set
X is set
n is (X)
KX is subset-closed finite-membered (X,n)
SX is subset-closed finite-membered (X,KX)
the topology of KX is Element of bool (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
bool (bool the carrier of KX) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set
the topology of n is Element of bool (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
bool (bool the carrier of n) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set
P is subset-closed finite-membered (X,n) (X,n)
[#] P is non proper Element of bool the carrier of P
the carrier of P is set
bool the carrier of P is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed 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
(bool ([#] P)) /\ the topology of KX is Element of bool (bool the carrier of KX)
(bool ([#] P)) /\ the topology of n is Element of bool (bool the carrier of n)
the topology of P is Element of bool (bool the carrier of P)
bool (bool the carrier of P) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set
[#] SX is non proper 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
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
(bool ([#] SX)) /\ the topology of KX is Element of bool (bool the carrier of KX)
the topology 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
X is set
n is (X)
KX is subset-closed finite-membered (X,n) (X,n)
[#] 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
SX is subset-closed finite-membered (X,n) (X,n)
[#] SX is non proper 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
the topology of KX is Element of bool (bool the carrier of KX)
bool (bool the carrier of KX) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set
TopStruct(# the carrier of KX, the topology of KX #) is strict TopStruct
the topology 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
TopStruct(# the carrier of SX, the topology of SX #) is strict TopStruct
the topology of n is Element of bool (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
bool (bool the carrier of n) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set
bool ([#] SX) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set
bool ([#] SX) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed Element of bool (bool ([#] SX))
bool (bool ([#] SX)) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set
the topology of n /\ (bool ([#] SX)) is Element of bool (bool ([#] SX))
bool ([#] KX) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set
bool ([#] KX) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed Element of bool (bool ([#] KX))
bool (bool ([#] KX)) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set
the topology of n /\ (bool ([#] KX)) is Element of bool (bool ([#] KX))
X is set
n is subset-closed (X)
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
KX is Element of bool the carrier of n
bool KX is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed Element of bool (bool KX)
bool KX is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set
bool (bool KX) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set
the topology of n is Element of bool (bool the carrier of n)
bool (bool the carrier of n) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set
(bool KX) /\ the topology of n is Element of bool (bool the carrier of n)
the_family_of n is subset-closed V252() Element of bool (bool the carrier of n)
SX is finite-membered subset-closed V252() Element of bool (bool KX)
TopStruct(# KX,SX #) is strict TopStruct
[#] TopStruct(# KX,SX #) is non proper Element of bool the carrier of TopStruct(# KX,SX #)
the carrier of TopStruct(# KX,SX #) is set
bool the carrier of TopStruct(# KX,SX #) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set
[#] n is non proper Element of bool the carrier of n
the topology of TopStruct(# KX,SX #) is Element of bool (bool the carrier of TopStruct(# KX,SX #))
bool (bool the carrier of TopStruct(# KX,SX #)) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set
the_family_of TopStruct(# KX,SX #) is Element of bool (bool the carrier of TopStruct(# KX,SX #))
n is strict subset-closed finite-membered (X,n) (X,n)
[#] n is non proper 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
SX is strict subset-closed finite-membered (X,n) (X,n)
[#] SX is non proper 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 strict subset-closed finite-membered (X,n) (X,n)
[#] P is non proper Element of bool the carrier of P
the carrier of P is set
bool the carrier of P is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set
X is set
n is subset-closed finite-membered (X)
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
KX is Element of bool the carrier of n
(X,n,KX) is strict subset-closed finite-membered (X,n) (X,n)
SX is strict subset-closed finite-membered (X,n) (X,n)
[#] SX is non proper 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
the_family_of n is subset-closed V252() Element of bool (bool the carrier of n)
bool (bool the carrier of n) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set
the topology of n is Element of bool (bool the carrier of n)
bool KX is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed Element of bool (bool KX)
bool KX is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set
bool (bool KX) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set
(bool KX) /\ the topology of n is Element of bool (bool the carrier of n)
X is set
n is subset-closed finite-membered (X)
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
the topology of n is Element of bool (bool the carrier of n)
bool (bool the carrier of n) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set
KX is Element of bool the carrier of n
(X,n,KX) is strict subset-closed finite-membered (X,n) (X,n)
the topology of (X,n,KX) is Element of bool (bool the carrier of (X,n,KX))
the carrier of (X,n,KX) is set
bool the carrier of (X,n,KX) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set
bool (bool the carrier of (X,n,KX)) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set
bool KX is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed Element of bool (bool KX)
bool KX is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set
bool (bool KX) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set
(bool KX) /\ the topology of n is Element of bool (bool the carrier of n)
[#] (X,n,KX) is non proper Element of bool the carrier of (X,n,KX)
X is set
n is subset-closed finite-membered (X)
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
KX is Element of bool the carrier of n
(X,n,KX) is strict subset-closed finite-membered (X,n) (X,n)
the carrier of (X,n,KX) is set
bool the carrier of (X,n,KX) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set
SX is Element of bool the carrier of n
(X,n,SX) is strict subset-closed finite-membered (X,n) (X,n)
P is Element of bool the carrier of (X,n,KX)
(X,(X,n,KX),P) is strict subset-closed finite-membered (X,(X,n,KX)) (X,(X,n,KX))
n is strict subset-closed finite-membered (X,n) (X,n)
[#] n is non proper 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 set
n is subset-closed finite-membered (X)
[#] n is non proper 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,n,([#] n)) is strict subset-closed finite-membered (X,n) (X,n)
the topology of n is Element of bool (bool the carrier of n)
bool (bool the carrier of n) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set
TopStruct(# the carrier of n, the topology of n #) is strict TopStruct
[#] TopStruct(# the carrier of n, the topology of n #) is non proper Element of bool the carrier of TopStruct(# the carrier of n, the topology of n #)
the carrier of TopStruct(# the carrier of n, the topology of n #) is set
bool the carrier of TopStruct(# the carrier of n, the topology of n #) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set
bool ([#] TopStruct(# the carrier of n, the topology of n #)) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed Element of bool (bool ([#] TopStruct(# the carrier of n, the topology of n #)))
bool ([#] TopStruct(# the carrier of n, the topology of n #)) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set
bool (bool ([#] TopStruct(# the carrier of n, the topology of n #))) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set
(bool ([#] TopStruct(# the carrier of n, the topology of n #))) /\ the topology of n is Element of bool (bool the carrier of n)
the_family_of n is subset-closed V252() Element of bool (bool the carrier of n)
the_family_of TopStruct(# the carrier of n, the topology of n #) is Element of bool (bool the carrier of TopStruct(# the carrier of n, the topology of n #))
bool (bool the carrier of TopStruct(# the carrier of n, the topology of n #)) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set
the topology of TopStruct(# the carrier of n, the topology of n #) is Element of bool (bool the carrier of TopStruct(# the carrier of n, the topology of n #))
SX is subset-closed finite-membered (X,n) (X,n)
[#] SX is non proper 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
X is set
n is subset-closed finite-membered (X)
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
KX is Element of bool the carrier of n
SX is Element of bool the carrier of n
(X,n,KX) is strict subset-closed finite-membered (X,n) (X,n)
(X,n,SX) is strict subset-closed finite-membered (X,n) (X,n)
bool KX is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed Element of bool (bool KX)
bool KX is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set
bool (bool KX) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set
the topology of n is Element of bool (bool the carrier of n)
bool (bool the carrier of n) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set
(bool KX) /\ the topology of n is Element of bool (bool the carrier of n)
the topology of (X,n,KX) is Element of bool (bool the carrier of (X,n,KX))
the carrier of (X,n,KX) is set
bool the carrier of (X,n,KX) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set
bool (bool the carrier of (X,n,KX)) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed 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
(bool SX) /\ the topology of n is Element of bool (bool the carrier of n)
the topology of (X,n,SX) is Element of bool (bool the carrier of (X,n,SX))
the carrier of (X,n,SX) is set
bool the carrier of (X,n,SX) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set
bool (bool the carrier of (X,n,SX)) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set
[#] (X,n,KX) is non proper Element of bool the carrier of (X,n,KX)
[#] (X,n,SX) is non proper Element of bool the carrier of (X,n,SX)
X is ext-real V17() real integer set
[:{{}},NAT:] is non empty non trivial non empty-membered Relation-like non finite set
NAT \/ [:{{}},NAT:] is non empty set
(NAT \/ [:{{}},NAT:]) \ {[{},{}]} is Element of bool (NAT \/ [:{{}},NAT:])
bool (NAT \/ [:{{}},NAT:]) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set
n is set
KX is set
[n,KX] is set
{n,KX} is non empty finite set
{n} is non empty trivial finite 1 -element set
{{n,KX},{n}} is non empty with_non-empty_elements non empty-membered finite finite-membered set
X is set
n is (X)
the carrier of n is set
the topology of n is Element of bool (bool the carrier of n)
bool the carrier of n is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set
bool (bool the carrier of n) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set
KX is ext-real V17() real set
KX + 1 is ext-real V17() real set
K56(KX,1) is ext-real V17() real set
( the carrier of n, the topology of n,(KX + 1)) is Element of bool (bool the carrier of n)
( the carrier of n,( the carrier of n, the topology of n,(KX + 1))) is strict subset-closed ( the carrier of n) ( the carrier of n)
( the carrier of n,( the carrier of n, the topology of n,(KX + 1))) is subset-closed V252() Element of bool (bool the carrier of n)
TopStruct(# the carrier of n,( the carrier of n,( the carrier of n, the topology of n,(KX + 1))) #) is strict TopStruct
[#] n is non proper Element of bool the carrier of n
[#] ( the carrier of n,( the carrier of n, the topology of n,(KX + 1))) is non proper Element of bool the carrier of ( the carrier of n,( the carrier of n, the topology of n,(KX + 1)))
the carrier of ( the carrier of n,( the carrier of n, the topology of n,(KX + 1))) is set
bool the carrier of ( the carrier of n,( the carrier of n, the topology of n,(KX + 1))) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set
X is set
n is (X)
(X,n,(- 1)) is (X)
the carrier of n is set
the topology of n is Element of bool (bool the carrier of n)
bool the carrier of n is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set
bool (bool the carrier of n) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set
(- 1) + 1 is ext-real V17() real set
K56((- 1),1) is ext-real V17() real set
( the carrier of n, the topology of n,((- 1) + 1)) is Element of bool (bool the carrier of n)
( the carrier of n,( the carrier of n, the topology of n,((- 1) + 1))) is strict subset-closed ( the carrier of n) ( the carrier of n)
( the carrier of n,( the carrier of n, the topology of n,((- 1) + 1))) is subset-closed V252() Element of bool (bool the carrier of n)
TopStruct(# the carrier of n,( the carrier of n,( the carrier of n, the topology of n,((- 1) + 1))) #) is strict TopStruct
the topology of (X,n,(- 1)) is Element of bool (bool the carrier of (X,n,(- 1)))
the carrier of (X,n,(- 1)) is set
bool the carrier of (X,n,(- 1)) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set
bool (bool the carrier of (X,n,(- 1))) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set
KX is non empty set
SX is set
card SX is epsilon-transitive epsilon-connected ordinal cardinal set
card ((- 1) + 1) is epsilon-transitive epsilon-connected ordinal cardinal set
KX is ext-real V17() real finite integer set
(X,n,KX) is (X)
KX + 1 is ext-real V17() real set
K56(KX,1) is ext-real V17() real finite integer set
( the carrier of n, the topology of n,(KX + 1)) is Element of bool (bool the carrier of n)
( the carrier of n,( the carrier of n, the topology of n,(KX + 1))) is strict subset-closed ( the carrier of n) ( the carrier of n)
( the carrier of n,( the carrier of n, the topology of n,(KX + 1))) is subset-closed V252() Element of bool (bool the carrier of n)
TopStruct(# the carrier of n,( the carrier of n,( the carrier of n, the topology of n,(KX + 1))) #) is strict TopStruct
the carrier of ( the carrier of n,( the carrier of n, the topology of n,(KX + 1))) is set
bool the carrier of ( the carrier of n,( the carrier of n, the topology of n,(KX + 1))) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set
Pn is finite Element of bool the carrier of ( the carrier of n,( the carrier of n, the topology of n,(KX + 1)))
Fm is set
card Pn is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V17() real finite cardinal integer Element of NAT
card Fm is epsilon-transitive epsilon-connected ordinal cardinal set
SX is ext-real V17() real finite integer set
card SX 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 finite-membered finite-degree () () () (X)
KX is ext-real V17() real finite integer set
(X,n,KX) is finite-membered finite-degree (X)
the carrier of n is set
the topology of n is Element of bool (bool the carrier of n)
bool the carrier of n is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set
bool (bool the carrier of n) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set
KX + 1 is ext-real V17() real set
K56(KX,1) is ext-real V17() real finite integer set
( the carrier of n, the topology of n,(KX + 1)) is Element of bool (bool the carrier of n)
( the carrier of n,( the carrier of n, the topology of n,(KX + 1))) is strict subset-closed ( the carrier of n) ( the carrier of n)
( the carrier of n,( the carrier of n, the topology of n,(KX + 1))) is subset-closed V252() Element of bool (bool the carrier of n)
TopStruct(# the carrier of n,( the carrier of n,( the carrier of n, the topology of n,(KX + 1))) #) is strict TopStruct
the topology of (X,n,KX) is Element of bool (bool the carrier of (X,n,KX))
the carrier of (X,n,KX) is set
bool the carrier of (X,n,KX) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set
bool (bool the carrier of (X,n,KX)) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set
SX is non empty set
P is set
X is non empty set
n is non void subset-closed () (X)
KX is ext-real V17() real finite integer set
(X,n,KX) is finite-membered finite-degree (X)
the carrier of n is set
the topology of n is non empty Element of bool (bool the carrier of n)
bool the carrier of n is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set
bool (bool the carrier of n) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set
KX + 1 is ext-real V17() real set
K56(KX,1) is ext-real V17() real finite integer set
( the carrier of n, the topology of n,(KX + 1)) is Element of bool (bool the carrier of n)
( the carrier of n,( the carrier of n, the topology of n,(KX + 1))) is strict subset-closed ( the carrier of n) ( the carrier of n)
( the carrier of n,( the carrier of n, the topology of n,(KX + 1))) is subset-closed V252() Element of bool (bool the carrier of n)
TopStruct(# the carrier of n,( the carrier of n,( the carrier of n, the topology of n,(KX + 1))) #) is strict TopStruct
SX is Element of bool the carrier of n
card SX is epsilon-transitive epsilon-connected ordinal cardinal set
card (KX + 1) is epsilon-transitive epsilon-connected ordinal cardinal set
X is set
n is ext-real V17() real finite integer set
KX is ext-real V17() real finite integer set
SX is (X)
(X,SX,n) is finite-membered finite-degree (X)
the carrier of SX is set
the topology of SX is Element of bool (bool the carrier of SX)
bool the carrier of SX is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set
bool (bool the carrier of SX) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set
n + 1 is ext-real V17() real set
K56(n,1) is ext-real V17() real finite integer set
( the carrier of SX, the topology of SX,(n + 1)) is Element of bool (bool the carrier of SX)
( the carrier of SX,( the carrier of SX, the topology of SX,(n + 1))) is strict subset-closed ( the carrier of SX) ( the carrier of SX)
( the carrier of SX,( the carrier of SX, the topology of SX,(n + 1))) is subset-closed V252() Element of bool (bool the carrier of SX)
TopStruct(# the carrier of SX,( the carrier of SX,( the carrier of SX, the topology of SX,(n + 1))) #) is strict TopStruct
(X,SX,KX) is finite-membered finite-degree (X)
KX + 1 is ext-real V17() real set
K56(KX,1) is ext-real V17() real finite integer set
( the carrier of SX, the topology of SX,(KX + 1)) is Element of bool (bool the carrier of SX)
( the carrier of SX,( the carrier of SX, the topology of SX,(KX + 1))) is strict subset-closed ( the carrier of SX) ( the carrier of SX)
( the carrier of SX,( the carrier of SX, the topology of SX,(KX + 1))) is subset-closed V252() Element of bool (bool the carrier of SX)
TopStruct(# the carrier of SX,( the carrier of SX,( the carrier of SX, the topology of SX,(KX + 1))) #) is strict TopStruct
Pn is set
P is ext-real 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 Element of NAT
card P 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 Pn is epsilon-transitive epsilon-connected ordinal cardinal set
the topology of (X,SX,n) is Element of bool (bool the carrier of (X,SX,n))
the carrier of (X,SX,n) is set
bool the carrier of (X,SX,n) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set
bool (bool the carrier of (X,SX,n)) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set
the topology of (X,SX,KX) is Element of bool (bool the carrier of (X,SX,KX))
the carrier of (X,SX,KX) is set
bool the carrier of (X,SX,KX) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set
bool (bool the carrier of (X,SX,KX)) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set
[#] (X,SX,n) is non proper Element of bool the carrier of (X,SX,n)
[#] (X,SX,KX) is non proper Element of bool the carrier of (X,SX,KX)
X is set
n is subset-closed (X)
KX is ext-real V17() real finite integer set
(X,n,KX) is finite-membered finite-degree (X)
the carrier of n is set
the topology of n is Element of bool (bool the carrier of n)
bool the carrier of n is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set
bool (bool the carrier of n) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set
KX + 1 is ext-real V17() real set
K56(KX,1) is ext-real V17() real finite integer set
( the carrier of n, the topology of n,(KX + 1)) is Element of bool (bool the carrier of n)
( the carrier of n,( the carrier of n, the topology of n,(KX + 1))) is strict subset-closed ( the carrier of n) ( the carrier of n)
( the carrier of n,( the carrier of n, the topology of n,(KX + 1))) is subset-closed V252() Element of bool (bool the carrier of n)
TopStruct(# the carrier of n,( the carrier of n,( the carrier of n, the topology of n,(KX + 1))) #) is strict TopStruct
SX is set
the_family_of n is subset-closed V252() Element of bool (bool the carrier of n)
[#] (X,n,KX) is non proper Element of bool the carrier of (X,n,KX)
the carrier of (X,n,KX) is set
bool the carrier of (X,n,KX) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set
[#] n is non proper Element of bool the carrier of n
X is set
n is ext-real V17() real finite integer set
KX is (X)
(X,KX,n) is finite-membered finite-degree (X)
the carrier of KX is set
the topology of KX is Element of bool (bool the carrier of KX)
bool the carrier of KX is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set
bool (bool the carrier of KX) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set
n + 1 is ext-real V17() real set
K56(n,1) is ext-real V17() real finite integer set
( the carrier of KX, the topology of KX,(n + 1)) is Element of bool (bool the carrier of KX)
( the carrier of KX,( the carrier of KX, the topology of KX,(n + 1))) is strict subset-closed ( the carrier of KX) ( the carrier of KX)
( the carrier of KX,( the carrier of KX, the topology of KX,(n + 1))) is subset-closed V252() Element of bool (bool the carrier of KX)
TopStruct(# the carrier of KX,( the carrier of KX,( the carrier of KX, the topology of KX,(n + 1))) #) is strict TopStruct
the_family_of KX is Element of bool (bool the carrier of KX)
SX is non empty set
P is set
card (n + 1) is 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
the topology of (X,KX,n) is Element of bool (bool the carrier of (X,KX,n))
the carrier of (X,KX,n) is set
bool the carrier of (X,KX,n) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set
bool (bool the carrier of (X,KX,n)) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set
X is set
n is ext-real V17() real finite integer set
KX is (X)
(X,KX,n) is finite-membered finite-degree (X)
the carrier of KX is set
the topology of KX is Element of bool (bool the carrier of KX)
bool the carrier of KX is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set
bool (bool the carrier of KX) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set
n + 1 is ext-real V17() real set
K56(n,1) is ext-real V17() real finite integer set
( the carrier of KX, the topology of KX,(n + 1)) is Element of bool (bool the carrier of KX)
( the carrier of KX,( the carrier of KX, the topology of KX,(n + 1))) is strict subset-closed ( the carrier of KX) ( the carrier of KX)
( the carrier of KX,( the carrier of KX, the topology of KX,(n + 1))) is subset-closed V252() Element of bool (bool the carrier of KX)
TopStruct(# the carrier of KX,( the carrier of KX,( the carrier of KX, the topology of KX,(n + 1))) #) is strict TopStruct
((X,KX,n)) is ext-real V17() real finite integer set
(KX) is ext-real set
the carrier of (X,KX,n) is set
bool the carrier of (X,KX,n) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set
n is finite Element of bool the carrier of (X,KX,n)
Pn is set
card n is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V17() real finite cardinal integer Element of NAT
Fm is finite Element of bool the carrier of KX
card Fm is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V17() real finite cardinal integer Element of NAT
P is ext-real V17() real finite integer set
P + 1 is ext-real V17() real set
K56(P,1) is ext-real V17() real finite integer set
X is set
n is ext-real V17() real finite integer set
KX is (X)
(X,KX,n) is finite-membered finite-degree (X)
the carrier of KX is set
the topology of KX is Element of bool (bool the carrier of KX)
bool the carrier of KX is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set
bool (bool the carrier of KX) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set
n + 1 is ext-real V17() real set
K56(n,1) is ext-real V17() real finite integer set
( the carrier of KX, the topology of KX,(n + 1)) is Element of bool (bool the carrier of KX)
( the carrier of KX,( the carrier of KX, the topology of KX,(n + 1))) is strict subset-closed ( the carrier of KX) ( the carrier of KX)
( the carrier of KX,( the carrier of KX, the topology of KX,(n + 1))) is subset-closed V252() Element of bool (bool the carrier of KX)
TopStruct(# the carrier of KX,( the carrier of KX,( the carrier of KX, the topology of KX,(n + 1))) #) is strict TopStruct
((X,KX,n)) is ext-real V17() real finite integer set
the carrier of (X,KX,n) is set
bool the carrier of (X,KX,n) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set
Pn is finite Element of bool the carrier of (X,KX,n)
the topology of (X,KX,n) is Element of bool (bool the carrier of (X,KX,n))
bool (bool the carrier of (X,KX,n)) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set
Fm is set
card Fm is epsilon-transitive epsilon-connected ordinal cardinal set
card (n + 1) is epsilon-transitive epsilon-connected ordinal cardinal set
card Pn is ext-real 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 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 (card Pn) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V17() real finite cardinal integer Element of NAT
X is set
n is ext-real V17() real finite integer set
KX is (X)
(X,KX,n) is finite-membered finite-degree (X)
the carrier of KX is set
the topology of KX is Element of bool (bool the carrier of KX)
bool the carrier of KX is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set
bool (bool the carrier of KX) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set
n + 1 is ext-real V17() real set
K56(n,1) is ext-real V17() real finite integer set
( the carrier of KX, the topology of KX,(n + 1)) is Element of bool (bool the carrier of KX)
( the carrier of KX,( the carrier of KX, the topology of KX,(n + 1))) is strict subset-closed ( the carrier of KX) ( the carrier of KX)
( the carrier of KX,( the carrier of KX, the topology of KX,(n + 1))) is subset-closed V252() Element of bool (bool the carrier of KX)
TopStruct(# the carrier of KX,( the carrier of KX,( the carrier of KX, the topology of KX,(n + 1))) #) is strict TopStruct
TopStruct(# the carrier of KX, the topology of KX #) is strict TopStruct
(KX) is ext-real set
P is finite Element of bool the carrier of KX
SX is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V17() real finite cardinal integer Element of NAT
( the carrier of KX, the topology of KX,SX) is finite-membered Element of bool (bool the carrier of KX)
( the carrier of KX,( the carrier of KX, the topology of KX,SX)) is finite-membered subset-closed V252() Element of bool (bool the carrier of KX)
n is set
card P is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V17() real finite cardinal integer Element of NAT
card n 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
card (card P) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V17() real finite cardinal integer Element of NAT
P is set
the_family_of KX is Element of bool (bool the carrier of KX)
X is set
n is ext-real V17() real finite integer set
KX is (X)
(KX) is ext-real set
(X,KX,n) is finite-membered finite-degree (X)
the carrier of KX is set
the topology of KX is Element of bool (bool the carrier of KX)
bool the carrier of KX is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set
bool (bool the carrier of KX) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set
n + 1 is ext-real V17() real set
K56(n,1) is ext-real V17() real finite integer set
( the carrier of KX, the topology of KX,(n + 1)) is Element of bool (bool the carrier of KX)
( the carrier of KX,( the carrier of KX, the topology of KX,(n + 1))) is strict subset-closed ( the carrier of KX) ( the carrier of KX)
( the carrier of KX,( the carrier of KX, the topology of KX,(n + 1))) is subset-closed V252() Element of bool (bool the carrier of KX)
TopStruct(# the carrier of KX,( the carrier of KX,( the carrier of KX, the topology of KX,(n + 1))) #) is strict TopStruct
TopStruct(# the carrier of KX, the topology of KX #) is strict TopStruct
the_family_of KX is Element of bool (bool the carrier of KX)
the topology of (X,KX,n) is Element of bool (bool the carrier of (X,KX,n))
the carrier of (X,KX,n) is set
bool the carrier of (X,KX,n) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set
bool (bool the carrier of (X,KX,n)) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set
P is set
(KX) + 1 is ext-real set
n is finite Element of bool the carrier of KX
card n is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V17() real finite cardinal integer Element of NAT
card (card n) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V17() real finite cardinal integer Element of NAT
card (n + 1) is epsilon-transitive epsilon-connected ordinal cardinal set
P is set
X is ext-real V17() real finite integer set
X + 1 is ext-real V17() real set
K56(X,1) is ext-real V17() real finite integer set
n is non void subset-closed () TopStruct
(n) is ext-real set
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
the_family_of n is subset-closed V252() Element of bool (bool the carrier of n)
bool (bool the carrier of n) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set
the topology of n is non empty Element of bool (bool the carrier of n)
SX is set
KX is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V17() real finite cardinal integer Element of NAT
card KX is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V17() real finite cardinal integer Element of NAT
card SX is epsilon-transitive epsilon-connected ordinal cardinal set
P is Relation-like Function-like set
dom P is set
rng P is set
n is open Element of bool the carrier of n
card n is epsilon-transitive epsilon-connected ordinal cardinal set
KX is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V17() real finite cardinal integer Element of NAT
SX is finite Element of bool the carrier of n
card SX is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V17() real finite cardinal integer Element of NAT
card KX is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V17() real finite cardinal integer Element of NAT
card (card SX) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V17() real finite cardinal integer Element of NAT
P is Relation-like Function-like set
dom P is set
rng P is set
the_family_of n is subset-closed V252() Element of bool (bool the carrier of n)
bool (bool the carrier of n) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set
the topology of n is non empty Element of bool (bool the carrier of n)
n is open Element of bool the carrier of n
card n is epsilon-transitive epsilon-connected ordinal cardinal set
SX is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V17() real finite cardinal integer set
(n) + 1 is ext-real set
P is Element of bool the carrier of n
card P is epsilon-transitive epsilon-connected ordinal cardinal set
SX is ext-real V17() real finite integer set
SX + 1 is ext-real V17() real set
K56(SX,1) is ext-real V17() real finite integer set
KX is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V17() real finite cardinal integer Element of NAT
n is finite Element of bool the carrier of n
card n is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V17() real finite cardinal integer Element of NAT
card KX is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V17() real finite cardinal integer Element of NAT
card (card n) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V17() real finite cardinal integer Element of NAT
Pn is Relation-like Function-like set
dom Pn is set
rng Pn is set
the_family_of n is subset-closed V252() Element of bool (bool the carrier of n)
bool (bool the carrier of n) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set
the topology of n is non empty Element of bool (bool the carrier of n)
Fm is open Element of bool the carrier of n
card Fm is epsilon-transitive epsilon-connected ordinal cardinal set
n is ext-real V17() real set
X is non void subset-closed () TopStruct
(X) is ext-real set
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 + 1 is ext-real V17() real set
K56(n,1) is ext-real V17() real 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
KX is open Element of bool the carrier of X
SX is open Element of bool the carrier of X
KX is open Element of bool the carrier of X
card KX is epsilon-transitive epsilon-connected ordinal cardinal set
SX is open Element of bool the carrier of X
SX is finite open Element of bool the carrier of X
card SX is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V17() real finite cardinal integer Element of NAT
P is finite open Element of bool the carrier of X
Pn is finite open Element of bool the carrier of X
card Pn is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V17() real finite cardinal integer Element of NAT
Fm is finite open Element of bool the carrier of X
X is non void subset-closed () TopStruct
n is finite open (X, - 1)
(X) is ext-real set
card n is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V17() real finite cardinal integer Element of NAT
X is ext-real V17() real finite integer set
n is non void subset-closed () TopStruct
KX is finite open (n,X)
X is non void subset-closed () 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 finite open 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
(card n) - 1 is ext-real V17() real set
(card n) + (- 1) is ext-real V17() real set
K56((card n),(- 1)) is ext-real V17() real set
K60((card n),1) is ext-real V17() real finite integer set
(X) is ext-real set
(X) + 1 is ext-real set
((X) + 1) - 1 is ext-real set
((X) + 1) + (- 1) is ext-real set
{} - 1 is non empty ext-real non positive negative V17() real set
{} + (- 1) is non empty ext-real non positive negative V17() real set
K56({},(- 1)) is non empty ext-real non positive negative V17() real set
K60({},1) is non empty ext-real non positive negative V17() real finite integer set
((card n) - 1) + 1 is ext-real V17() real set
K56(((card n) - 1),1) is ext-real V17() real set
X is non empty set
n is non void subset-closed () (X)
(n) is ext-real set
KX is non void subset-closed finite-membered () (X,n)
(KX) is ext-real set
SX is ext-real V17() real finite integer set
P is finite open (KX,SX)
the topology of KX is non empty Element of bool (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
bool (bool the carrier of KX) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set
the topology of n is non empty Element of bool (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
bool (bool the carrier of n) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set
n is open Element of bool the carrier of n
card n is epsilon-transitive epsilon-connected ordinal cardinal set
SX + 1 is ext-real V17() real set
K56(SX,1) is ext-real V17() real finite integer set
n is open Element of bool the carrier of n
card n is epsilon-transitive epsilon-connected ordinal cardinal set
SX + 1 is ext-real V17() real set
K56(SX,1) is ext-real V17() real finite integer set
n is open Element of bool the carrier of n
n is open Element of bool the carrier of n
card n is epsilon-transitive epsilon-connected ordinal cardinal set
SX + 1 is ext-real V17() real set
K56(SX,1) is ext-real V17() real finite integer set
n is open Element of bool the carrier of n
n is ext-real V17() real set
X is non void subset-closed () TopStruct
(X) is ext-real 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 set
max ((n - 1),(- 1)) is ext-real V17() real set
KX is finite open (X,n)
{} - 1 is non empty ext-real non positive negative V17() real set
{} + (- 1) is non empty ext-real non positive negative V17() real set
K56({},(- 1)) is non empty ext-real non positive negative V17() real set
K60({},1) is non empty ext-real non positive negative V17() real finite integer 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 open integer subset-closed Function-yielding V200() V252() (X, - 1) 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() (X, - 1)
SX is finite open (X, max ((n - 1),(- 1)))
card KX is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V17() real finite cardinal integer Element of NAT
n + 1 is ext-real V17() real set
K56(n,1) is ext-real V17() real set
SX is set
(X) - {} is ext-real 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 subset-closed Function-yielding V200() V252() set
K58({}) 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() set
(X) + (- {}) is ext-real set
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
{SX} is non empty trivial finite 1 -element set
KX \ {SX} is finite open Element of bool the carrier of X
n is open Element of bool the carrier of X
card n is epsilon-transitive epsilon-connected ordinal cardinal set
P is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V17() real finite cardinal integer Element of NAT
P - 1 is ext-real V17() real set
P + (- 1) is ext-real V17() real set
K56(P,(- 1)) is ext-real V17() real set
K60(P,1) is ext-real V17() real finite integer set
(P - 1) + 1 is ext-real V17() real set
K56((P - 1),1) is ext-real V17() real set
{} - 1 is non empty ext-real non positive negative V17() real set
{} + (- 1) is non empty ext-real non positive negative V17() real set
K56({},(- 1)) is non empty ext-real non positive negative V17() real set
K60({},1) is non empty ext-real non positive negative V17() real finite integer set
Pn is finite open (X, max ((n - 1),(- 1)))
X is set
n is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V17() real finite cardinal integer set
KX is non void subset-closed () TopStruct
(KX) is ext-real set
the carrier of KX is set
SX is finite open (KX,n)
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 finite integer set
n - {} is ext-real non negative V17() real 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 subset-closed Function-yielding V200() V252() set
K58({}) 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() set
n + (- {}) is ext-real non negative V17() real set
K56(n,(- {})) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V17() real finite cardinal integer set
K60(n,{}) is ext-real non negative V17() real finite integer set
{} - 1 is non empty ext-real non positive negative V17() real set
{} + (- 1) is non empty ext-real non positive negative V17() real set
K56({},(- 1)) is non empty ext-real non positive negative V17() real set
K60({},1) is non empty ext-real non positive negative V17() real finite integer set
max ((n - 1),(- 1)) is ext-real V17() real set
card SX is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V17() real finite cardinal integer Element of NAT
P is ext-real V17() real finite integer set
P + 1 is ext-real V17() real set
K56(P,1) is ext-real V17() real finite integer set
n is finite open (KX,n,SX)
card n is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V17() real finite cardinal integer Element of NAT
(n - 1) + 1 is ext-real V17() real set
K56((n - 1),1) is ext-real V17() real set
SX \ n is finite open Element of bool the carrier of KX
bool the carrier of KX is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set
card (SX \ n) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V17() real finite cardinal integer Element of NAT
n + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V17() real finite cardinal integer Element of NAT
(n + 1) - n is ext-real V17() real set
- n is ext-real non positive V17() real set
K58(n) is ext-real non positive V17() real finite integer set
(n + 1) + (- n) is ext-real V17() real set
K56((n + 1),(- n)) is ext-real V17() real set
K60((n + 1),n) is ext-real V17() real finite integer set
Pn is set
{Pn} is non empty trivial finite 1 -element set
Fm is set
{Fm} is non empty trivial finite 1 -element set
SX \ {Fm} is finite open Element of bool the carrier of KX
n /\ SX is finite open Element of bool the carrier of KX
n is set
{n} is non empty trivial finite 1 -element set
SX \ {n} is finite open Element of bool the carrier of KX
Pn is finite open Element of bool the carrier of KX
card Pn is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V17() real finite cardinal integer Element of NAT
X is set
n is (X)
[#] n is non proper 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
bool (bool the carrier of n) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set
KX is Relation-like Function-like set
{ b₁ where b₁ is Element of bool the carrier of n : S₁[b₁] } is set
bool the carrier of n is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed Element of bool (bool the carrier of n)
P is set
n is Element of bool the carrier of n
Pn is c=-linear finite open Element of bool (bool the carrier of n)
KX .: Pn is finite set
P is Element of bool (bool the carrier of n)
TopStruct(# the carrier of n,P #) is strict TopStruct
[#] TopStruct(# the carrier of n,P #) is non proper Element of bool the carrier of TopStruct(# the carrier of n,P #)
the carrier of TopStruct(# the carrier of n,P #) is set
bool the carrier of TopStruct(# the carrier of n,P #) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set
Pn is strict (X)
[#] Pn is non proper Element of bool the carrier of Pn
the carrier of Pn is set
bool the carrier of Pn is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set
Fm is Element of bool the carrier of Pn
m is Element of bool the carrier of n
SX is c=-linear finite open Element of bool (bool the carrier of n)
KX .: SX is finite set
m is c=-linear finite open Element of bool (bool the carrier of n)
KX .: m is finite set
SX is strict (X)
[#] SX is non proper 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 strict (X)
[#] P is non proper Element of bool the carrier of P
the carrier of P is set
bool the carrier of P is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set
n is set
the topology 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
Pn is Element of bool the carrier of SX
Fm is Element of bool the carrier of P
m is c=-linear finite open Element of bool (bool the carrier of n)
KX .: m is finite set
the topology of P is Element of bool (bool the carrier of P)
bool (bool the carrier of P) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set
Pn is Element of bool the carrier of P
Fm is Element of bool the carrier of SX
m is c=-linear finite open Element of bool (bool the carrier of n)
KX .: m is finite set
X is set
n is (X)
KX is Relation-like Function-like set
(X,n,KX) is strict (X)
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
bool (bool the carrier of n) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set
the 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 open integer subset-closed Function-yielding V200() V252() Element of bool (bool the carrier of 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 open integer subset-closed Function-yielding V200() V252() Element of bool (bool the carrier of n)
KX .: the 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 open integer subset-closed Function-yielding V200() V252() Element of bool (bool the carrier of n) 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() set
{} n 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 bool the carrier of n
{} (X,n,KX) 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 bool the carrier of (X,n,KX)
the carrier of (X,n,KX) is set
bool the carrier of (X,n,KX) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set
the topology of (X,n,KX) is Element of bool (bool the carrier of (X,n,KX))
bool (bool the carrier of (X,n,KX)) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set
n is set
the_family_of (X,n,KX) is Element of bool (bool the carrier of (X,n,KX))
Pn is set
Fm is Element of bool the carrier of (X,n,KX)
SX is c=-linear finite open Element of bool (bool the carrier of n)
KX .: SX is finite set
m is Element of bool the carrier of (X,n,KX)
{ b₁ where b₁ is Element of bool the carrier of n : ( b₁ in SX & KX . b₁ in m ) } is set
TOP1 is set
K2 is Element of bool the carrier of n
KX . K2 is set
TOP1 is c=-linear finite open Element of bool (bool the carrier of n)
KX .: TOP1 is finite set
K2 is set
dom KX is set
TOP2 is set
KX . TOP2 is set
H2 is Element of bool the carrier of n
KX . H2 is set
K2 is set
dom KX is set
TOP2 is set
KX . TOP2 is set
n is set
the_family_of (X,n,KX) is Element of bool (bool the carrier of (X,n,KX))
Pn is Element of bool the carrier of (X,n,KX)
Fm is c=-linear finite open Element of bool (bool the carrier of n)
KX .: Fm is finite set
X is set
n is void (X)
KX is Relation-like Function-like set
(X,n,KX) is strict non void subset-closed finite-membered () (X)
the topology of (X,n,KX) is non empty Element of bool (bool the carrier of (X,n,KX))
the carrier of (X,n,KX) is set
bool the carrier of (X,n,KX) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set
bool (bool the carrier of (X,n,KX)) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set
P is non empty set
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
bool (bool the carrier of n) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set
n is finite open Element of bool the carrier of (X,n,KX)
Pn is c=-linear finite open Element of bool (bool the carrier of n)
KX .: Pn is finite set
dom KX is set
Pn /\ (dom KX) is finite Element of bool (bool the carrier of n)
KX .: (Pn /\ (dom KX)) is finite set
Fm is set
m is Element of bool the carrier of n
the topology of n is Element of bool (bool the carrier of n)
X is set
n is (X)
(n) is ext-real set
(n) + 1 is ext-real set
KX is Relation-like Function-like set
(X,n,KX) is strict non void subset-closed finite-membered () (X)
((X,n,KX)) is ext-real set
(n) + {} is ext-real set
P is ext-real V17() real finite integer set
P + 1 is ext-real V17() real set
K56(P,1) is ext-real V17() real finite integer set
the carrier of (X,n,KX) is set
bool the carrier of (X,n,KX) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set
(P + 1) + 1 is ext-real V17() real set
K56((P + 1),1) is ext-real V17() real set
Pn is finite Element of bool the carrier of (X,n,KX)
card Pn is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V17() real finite cardinal integer Element of NAT
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
bool (bool the carrier of n) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set
Fm is c=-linear finite open Element of bool (bool the carrier of n)
KX .: Fm is finite set
dom KX is set
Fm /\ (dom KX) is finite Element of bool (bool the carrier of n)
KX .: (Fm /\ (dom KX)) is finite set
card (Fm /\ (dom KX)) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V17() real finite cardinal integer Element of NAT
(Fm /\ (dom KX)) \ {{}} is finite Element of bool (bool the carrier of n)
SX is c=-linear finite open Element of bool (bool the carrier of n)
SX \/ {{}} is non empty finite set
(Fm /\ (dom KX)) \/ {{}} is non empty finite set
card {{}} is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V17() real finite cardinal integer Element of NAT
card (SX \/ {{}}) is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V17() real finite cardinal integer Element of NAT
card SX is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V17() real finite cardinal integer Element of NAT
(card SX) + (card {{}}) is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V17() real finite cardinal integer Element of NAT
(card SX) + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V17() real finite cardinal integer Element of NAT
{} + 1 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
n + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V17() real finite cardinal integer Element of NAT
union SX is Element of bool the carrier of n
c₁₁ is Element of bool the carrier of n
card (union SX) is epsilon-transitive epsilon-connected ordinal cardinal set
TOP1 is finite Element of bool the carrier of n
card TOP1 is ext-real 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
n + 1 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
n is (X)
(n) is ext-real set
KX is Relation-like Function-like set
dom KX is set
(X,n,KX) is strict non void subset-closed finite-membered () (X)
((X,n,KX)) is ext-real set
P is ext-real V17() real finite integer set
P + 1 is ext-real V17() real set
K56(P,1) is ext-real V17() real finite integer set
the carrier of (X,n,KX) is set
bool the carrier of (X,n,KX) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set
Pn is finite Element of bool the carrier of (X,n,KX)
card Pn is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V17() real finite cardinal integer Element of NAT
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
bool (bool the carrier of n) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set
Fm is c=-linear finite open Element of bool (bool the carrier of n)
KX .: Fm is finite set
Fm /\ (dom KX) is finite Element of bool (bool the carrier of n)
KX .: (Fm /\ (dom KX)) is finite set
n is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V17() real finite cardinal integer set
union (Fm /\ (dom KX)) is Element of bool the carrier of n
m is Element of bool the carrier of n
the topology of n is Element of bool (bool the carrier of n)
the_family_of n is Element of bool (bool the carrier of n)
SX is finite Element of bool the carrier of n
card SX is ext-real 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
card (Fm /\ (dom KX)) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V17() real finite cardinal integer Element of NAT
card (union (Fm /\ (dom KX))) is epsilon-transitive epsilon-connected ordinal cardinal set
X is set
n is finite-membered finite-degree (X)
KX is Relation-like Function-like set
(X,n,KX) is strict non void subset-closed finite-membered () (X)
(n) is ext-real V17() real finite integer set
(n) + 1 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V17() real finite cardinal integer set
K56((n),1) is ext-real V17() real finite integer set
((X,n,KX)) is ext-real set
X is set
n is finite-membered finite-degree () () (X)
KX is Relation-like Function-like set
(X,n,KX) is strict non void subset-closed finite-membered finite-degree () (X)
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
the topology of (X,n,KX) is non empty Element of bool (bool the carrier of (X,n,KX))
the carrier of (X,n,KX) is set
bool the carrier of (X,n,KX) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set
bool (bool the carrier of (X,n,KX)) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set
SX is finite Element of bool the carrier of n
bool SX is non empty non with_non-empty_elements finite finite-membered subset-closed V120() V252() d.union-closed Element of bool (bool SX)
bool SX is non empty non with_non-empty_elements finite finite-membered subset-closed V120() V252() d.union-closed set
bool (bool SX) is non empty non with_non-empty_elements finite finite-membered subset-closed V120() V252() d.union-closed set
the topology of n is Element of bool (bool the carrier of n)
bool (bool the carrier of n) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set
union the topology of n is Element of bool the carrier of n
bool (union the topology of n) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed Element of bool (bool (union the topology of n))
bool (union the topology of n) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set
bool (bool (union the topology of n)) 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 finite finite-membered subset-closed V120() V252() d.union-closed Element of bool (bool (bool SX))
bool (bool SX) is non empty non with_non-empty_elements finite finite-membered subset-closed V120() V252() d.union-closed set
bool (bool (bool SX)) is non empty non with_non-empty_elements finite finite-membered subset-closed V120() V252() d.union-closed set
Pn is set
Fm is Element of bool the carrier of (X,n,KX)
m is c=-linear finite finite-membered open Element of bool (bool the carrier of n)
KX .: m is finite set
SX is set
c₁₁ is Element of bool the carrier of n
[: the topology of (X,n,KX),(bool (bool SX)):] is non empty Relation-like set
bool [: the topology of (X,n,KX),(bool (bool SX)):] is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set
Pn is Relation-like the topology of (X,n,KX) -defined bool (bool SX) -valued Function-like V33( the topology of (X,n,KX), bool (bool SX)) Element of bool [: the topology of (X,n,KX),(bool (bool SX)):]
Fm is set
dom Pn is Element of bool the topology of (X,n,KX)
bool the topology of (X,n,KX) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set
m is set
Pn . Fm is set
Pn . m is set
KX .: (Pn . Fm) is set
rng Pn is finite finite-membered Element of bool (bool (bool SX))
bool (bool (bool SX)) is non empty non with_non-empty_elements finite finite-membered subset-closed V120() V252() d.union-closed set
card the topology of (X,n,KX) is non empty epsilon-transitive epsilon-connected ordinal cardinal set
card (bool (bool SX)) 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
n is subset-closed (X)
(n) is ext-real set
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
KX is Relation-like Function-like set
dom KX is set
(X,n,KX) is strict non void subset-closed finite-membered () (X)
((X,n,KX)) is ext-real set
the carrier of (X,n,KX) is set
bool the carrier of (X,n,KX) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set
P is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V17() real finite cardinal integer set
P + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V17() real finite cardinal integer Element of NAT
[#] n is non proper Element of bool the carrier of n
[#] (X,n,KX) is non proper Element of bool the carrier of (X,n,KX)
n is Element of bool the carrier of n
card n is epsilon-transitive epsilon-connected ordinal cardinal set
BOOL n is set
KX .: (BOOL n) is set
KX | (BOOL n) is Relation-like Function-like set
dom (KX | (BOOL n)) is set
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 Element of bool (bool n)
card Pn is epsilon-transitive epsilon-connected ordinal cardinal set
bool n is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed Element of bool (bool n)
bool the carrier of n is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed Element of bool (bool the carrier of n)
bool (bool the carrier of n) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set
m is set
(bool n) \ {{}} is Element of bool (bool n)
KX .: Pn is set
Fm is Element of bool (bool the carrier of n)
KX .: Fm is set
the_family_of n is subset-closed V252() Element of bool (bool the carrier of n)
the topology of n is Element of bool (bool the carrier of n)
SX is Element of bool the carrier of n
m is Element of bool the carrier of (X,n,KX)
(KX | (BOOL n)) .: Pn is set
SX is finite open Element of bool the carrier of (X,n,KX)
card SX is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V17() real finite cardinal integer Element of NAT
P is ext-real V17() real finite integer set
Pn is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V17() real finite cardinal integer Element of NAT
Pn + 1 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 V17() real finite integer set
n + 1 is ext-real V17() real set
K56(n,1) is ext-real V17() real finite integer set
Fm is finite open Element of bool the carrier of (X,n,KX)
card Fm is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V17() real finite cardinal integer Element of NAT
((X,n,KX)) + 1 is ext-real set
P is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V17() real finite cardinal integer set
n is Element of bool the carrier of (X,n,KX)
card n is epsilon-transitive epsilon-connected ordinal cardinal set
Pn is finite Element of bool the carrier of (X,n,KX)
card Pn is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V17() real finite cardinal integer Element of NAT
(card Pn) + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V17() real finite cardinal integer Element of NAT
P + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V17() real finite cardinal integer Element of NAT
Fm is finite open Element of bool the carrier of (X,n,KX)
card Fm is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V17() real finite cardinal integer Element of NAT
X is set
n is set
KX is set
SX is (X)
P is Relation-like Function-like set
P | n is Relation-like Function-like set
(X,SX,(P | n)) is strict non void subset-closed finite-membered () (X)
P | KX is Relation-like Function-like set
(X,SX,(P | KX)) is strict non void subset-closed finite-membered () (X)
dom (P | KX) is set
dom P is set
KX /\ (dom P) is set
n /\ KX is set
dom (P | n) is set
KX /\ n is set
(KX /\ n) /\ (dom P) is set
n /\ (dom (P | KX)) is set
[#] (X,SX,(P | n)) is non proper Element of bool the carrier of (X,SX,(P | n))
the carrier of (X,SX,(P | n)) is set
bool the carrier of (X,SX,(P | n)) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set
[#] SX is non proper 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
[#] (X,SX,(P | KX)) is non proper Element of bool the carrier of (X,SX,(P | KX))
the carrier of (X,SX,(P | KX)) is set
bool the carrier of (X,SX,(P | KX)) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set
the topology of (X,SX,(P | n)) is non empty Element of bool (bool the carrier of (X,SX,(P | n)))
bool (bool the carrier of (X,SX,(P | n))) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set
the topology of (X,SX,(P | KX)) is non empty Element of bool (bool the carrier of (X,SX,(P | KX)))
bool (bool the carrier of (X,SX,(P | KX))) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set
Fm is set
m is finite open Element of bool the carrier of (X,SX,(P | n))
bool (bool the carrier of SX) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set
c₁₁ is c=-linear finite open Element of bool (bool the carrier of SX)
(P | n) .: c₁₁ is finite set
c₁₁ /\ n is finite Element of bool (bool the carrier of SX)
(dom (P | n)) /\ c₁₁ is finite Element of bool (bool the carrier of SX)
SX is Element of bool the carrier of (X,SX,(P | KX))
(P | n) .: ((dom (P | n)) /\ c₁₁) is finite set
P .: ((dom (P | n)) /\ c₁₁) is finite set
(P | KX) .: ((dom (P | n)) /\ c₁₁) is finite set
TOP1 is c=-linear finite open Element of bool (bool the carrier of SX)
(dom (P | KX)) /\ TOP1 is finite Element of bool (bool the carrier of SX)
(P | KX) .: ((dom (P | KX)) /\ TOP1) is finite set
(P | KX) .: TOP1 is finite set
X is set
n is set
KX is (X)
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 topology of KX is Element of bool (bool the carrier of KX)
bool (bool the carrier of KX) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set
SX is Relation-like Function-like set
dom SX is set
(dom SX) /\ the topology of KX is Element of bool (bool the carrier of KX)
SX | n is Relation-like Function-like set
(X,KX,(SX | n)) is strict non void subset-closed finite-membered () (X)
(X,KX,SX) is strict non void subset-closed finite-membered () (X)
dom (SX | n) is set
(SX | n) | (dom (SX | n)) is Relation-like Function-like set
SX | (dom (SX | n)) is Relation-like Function-like set
[#] (X,KX,(SX | n)) is non proper Element of bool the carrier of (X,KX,(SX | n))
the carrier of (X,KX,(SX | n)) is set
bool the carrier of (X,KX,(SX | n)) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set
[#] KX is non proper Element of bool the carrier of KX
[#] (X,KX,SX) is non proper Element of bool the carrier of (X,KX,SX)
the carrier of (X,KX,SX) is set
bool the carrier of (X,KX,SX) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set
the topology of (X,KX,SX) is non empty Element of bool (bool the carrier of (X,KX,SX))
bool (bool the carrier of (X,KX,SX)) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set
the topology of (X,KX,(SX | n)) is non empty Element of bool (bool the carrier of (X,KX,(SX | n)))
bool (bool the carrier of (X,KX,(SX | n))) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set
Pn is set
Fm is finite open Element of bool the carrier of (X,KX,SX)
SX is c=-linear finite open Element of bool (bool the carrier of KX)
SX .: SX is finite set
SX /\ (dom SX) is finite Element of bool (bool the carrier of KX)
c₁₁ is set
TOP1 is Element of bool the carrier of KX
the topology of KX /\ (dom SX) is Element of bool (bool the carrier of KX)
(SX /\ (dom SX)) /\ n is finite Element of bool (bool the carrier of KX)
m is Element of bool the carrier of (X,KX,(SX | n))
SX .: (SX /\ (dom SX)) is finite set
(SX | n) .: ((SX /\ (dom SX)) /\ n) is finite set
(dom SX) /\ n is set
SX /\ ((dom SX) /\ n) is finite Element of bool (bool the carrier of KX)
(SX | n) .: (SX /\ ((dom SX) /\ n)) is finite set
SX /\ (dom (SX | n)) is finite Element of bool (bool the carrier of KX)
(SX | n) .: (SX /\ (dom (SX | n))) is finite set
(SX | n) .: SX is finite set
SX | (dom SX) is Relation-like Function-like set
X is set
n is set
KX is set
SX is (X)
P is Relation-like Function-like set
n |` P is Relation-like Function-like set
(X,SX,(n |` P)) is strict non void subset-closed finite-membered () (X)
KX |` P is Relation-like Function-like set
(X,SX,(KX |` P)) is strict non void subset-closed finite-membered () (X)
[#] (X,SX,(n |` P)) is non proper Element of bool the carrier of (X,SX,(n |` P))
the carrier of (X,SX,(n |` P)) is set
bool the carrier of (X,SX,(n |` P)) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set
[#] SX is non proper 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
[#] (X,SX,(KX |` P)) is non proper Element of bool the carrier of (X,SX,(KX |` P))
the carrier of (X,SX,(KX |` P)) is set
bool the carrier of (X,SX,(KX |` P)) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set
the topology of (X,SX,(n |` P)) is non empty Element of bool (bool the carrier of (X,SX,(n |` P)))
bool (bool the carrier of (X,SX,(n |` P))) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set
the topology of (X,SX,(KX |` P)) is non empty Element of bool (bool the carrier of (X,SX,(KX |` P)))
bool (bool the carrier of (X,SX,(KX |` P))) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set
Fm is set
bool (bool the carrier of SX) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set
m is finite open Element of bool the carrier of (X,SX,(n |` P))
SX is c=-linear finite open Element of bool (bool the carrier of SX)
(n |` P) .: SX is finite set
dom (n |` P) is set
SX /\ (dom (n |` P)) is finite Element of bool (bool the carrier of SX)
n |` (KX |` P) is Relation-like Function-like set
c₁₁ is c=-linear finite open Element of bool (bool the carrier of SX)
(n |` P) .: c<sub>11</sub> is finite set
(KX |` P) .: c₁₁ is finite set
K2 is set
dom (KX |` P) is set
TOP2 is set
(KX |` P) . TOP2 is set
P . TOP2 is set
(n |` P) . TOP2 is set
TOP1 is Element of bool the carrier of (X,SX,(KX |` P))
X is set
n is set
KX is (X)
the topology of KX is Element of bool (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
bool (bool the carrier of KX) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set
SX is Relation-like Function-like set
SX .: the topology of KX is set
n |` SX is Relation-like Function-like set
(X,KX,(n |` SX)) is strict non void subset-closed finite-membered () (X)
(X,KX,SX) is strict non void subset-closed finite-membered () (X)
rng SX is set
(rng SX) |` SX is Relation-like Function-like set
n |` ((rng SX) |` SX) is Relation-like Function-like set
n /\ (rng SX) is set
(n /\ (rng SX)) |` SX is Relation-like Function-like set
n is subset-closed finite-membered (X,(X,KX,SX))
[#] n is non proper 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
[#] KX is non proper Element of bool the carrier of KX
[#] (X,KX,SX) is non proper Element of bool the carrier of (X,KX,SX)
the carrier of (X,KX,SX) is set
bool the carrier of (X,KX,SX) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set
the topology of (X,KX,SX) is non empty Element of bool (bool the carrier of (X,KX,SX))
bool (bool the carrier of (X,KX,SX)) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set
the topology of n is Element of bool (bool the carrier of n)
bool (bool the carrier of n) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set
Pn is set
Fm is finite open Element of bool the carrier of (X,KX,SX)
m is c=-linear finite open Element of bool (bool the carrier of KX)
SX .: m is finite set
c₁₁ is set
TOP1 is Element of bool the carrier of KX
SX is Element of bool the carrier of n
SX /\ n is Element of bool the carrier of n
(n |` SX) .: m is finite set
X is set
n is (X)
KX is subset-closed finite-membered (X,n)
SX is Relation-like Function-like set
(X,KX,SX) is strict non void subset-closed finite-membered () (X)
(X,n,SX) is strict non void subset-closed finite-membered () (X)
[#] 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
[#] n is non proper 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,n,SX) is non proper Element of bool the carrier of (X,n,SX)
the carrier of (X,n,SX) is set
bool the carrier of (X,n,SX) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set
[#] (X,KX,SX) is non proper Element of bool the carrier of (X,KX,SX)
the carrier of (X,KX,SX) is set
bool the carrier of (X,KX,SX) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set
the topology of (X,KX,SX) is non empty Element of bool (bool the carrier of (X,KX,SX))
bool (bool the carrier of (X,KX,SX)) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set
the topology of (X,n,SX) is non empty Element of bool (bool the carrier of (X,n,SX))
bool (bool the carrier of (X,n,SX)) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set
Pn is set
Fm is finite open Element of bool the carrier of (X,KX,SX)
bool (bool the carrier of KX) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set
SX is c=-linear finite finite-membered open Element of bool (bool the carrier of KX)
SX .: SX is finite set
bool ([#] KX) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed Element of bool (bool ([#] KX))
bool ([#] KX) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set
bool (bool ([#] KX)) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed 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
bool (bool the carrier of n) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set
c₁₁ is c=-linear finite Element of bool (bool the carrier of n)
TOP1 is Element of bool the carrier of n
K2 is Element of bool the carrier of KX
the topology of KX is Element of bool (bool the carrier of KX)
the topology of n is Element of bool (bool the carrier of n)
m is Element of bool the carrier of (X,n,SX)
X is set
n is (X)
KX is subset-closed finite-membered (X,n)
the topology of KX is Element of bool (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
bool (bool the carrier of KX) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set
[#] KX is non proper Element of bool the carrier of KX
SX is Relation-like Function-like set
(X,n,SX) is strict non void subset-closed finite-membered () (X)
the carrier of (X,n,SX) is set
bool the carrier of (X,n,SX) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set
dom SX is set
(X,KX,SX) is strict non void subset-closed finite-membered () (X)
Pn is Element of bool the carrier of (X,n,SX)
(X,(X,n,SX),Pn) is strict subset-closed finite-membered (X,(X,n,SX)) (X,(X,n,SX))
n is strict subset-closed finite-membered (X,(X,n,SX))
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
Fm is Element of bool the carrier of n
the topology of (X,n,SX) is non empty Element of bool (bool the carrier of (X,n,SX))
bool (bool the carrier of (X,n,SX)) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set
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
bool (bool the carrier of n) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set
m is finite open Element of bool the carrier of (X,n,SX)
SX is c=-linear finite open Element of bool (bool the carrier of n)
SX .: SX is finite set
SX /\ (dom SX) is finite Element of bool (bool the carrier of n)
c₁₁ is c=-linear finite Element of bool (bool the carrier of KX)
TOP1 is Element of bool the carrier of KX
SX .: c₁₁ is finite set
[#] n is non proper Element of bool the carrier of n
X is set
n is Relation-like Function-like set
KX is (X)
the carrier of KX is set
the topology of KX is Element of bool (bool the carrier of KX)
bool the carrier of KX is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set
bool (bool the carrier of KX) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set
TopStruct(# the carrier of KX, the topology of KX #) is strict TopStruct
SX is (X)
the carrier of SX is set
the topology of SX is Element of bool (bool the carrier of SX)
bool the carrier of SX is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set
bool (bool the carrier of SX) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set
TopStruct(# the carrier of SX, the topology of SX #) is strict TopStruct
(X,KX,n) is strict non void subset-closed finite-membered () (X)
(X,SX,n) is strict non void subset-closed finite-membered () (X)
[#] KX is non proper Element of bool the carrier of KX
[#] (X,KX,n) is non proper Element of bool the carrier of (X,KX,n)
the carrier of (X,KX,n) is set
bool the carrier of (X,KX,n) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set
[#] SX is non proper Element of bool the carrier of SX
[#] (X,SX,n) is non proper Element of bool the carrier of (X,SX,n)
the carrier of (X,SX,n) is set
bool the carrier of (X,SX,n) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set
the topology of (X,KX,n) is non empty Element of bool (bool the carrier of (X,KX,n))
bool (bool the carrier of (X,KX,n)) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set
the topology of (X,SX,n) is non empty Element of bool (bool the carrier of (X,SX,n))
bool (bool the carrier of (X,SX,n)) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set
Pn is set
Fm is Element of bool the carrier of (X,KX,n)
SX is c=-linear finite open Element of bool (bool the carrier of KX)
n .: SX is finite set
c₁₁ is Element of bool (bool the carrier of SX)
m is Element of bool the carrier of (X,SX,n)
Pn is set
Fm is Element of bool the carrier of (X,SX,n)
SX is c=-linear finite open Element of bool (bool the carrier of SX)
n .: SX is finite set
c₁₁ is Element of bool (bool the carrier of KX)
m is Element of bool the carrier of (X,KX,n)
X is set
n is (X)
SX is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V17() real finite cardinal integer set
KX is Relation-like Function-like set
[#] n is non proper 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
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
bool (bool ([#] n)) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed Element of bool (bool (bool ([#] n)))
bool (bool ([#] n)) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set
bool (bool (bool ([#] n))) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set
n is set
Pn is (X)
the topology of Pn is Element of bool (bool the carrier of Pn)
the carrier of Pn is set
bool the carrier of Pn is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set
bool (bool the carrier of Pn) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set
[#] Pn is non proper Element of bool the carrier of Pn
Pn is (X)
the topology of Pn is Element of bool (bool the carrier of Pn)
the carrier of Pn is set
bool the carrier of Pn is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set
bool (bool the carrier of Pn) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set
[#] Pn is non proper Element of bool the carrier of Pn
(X,Pn,KX) is strict non void subset-closed finite-membered () (X)
the carrier of (X,Pn,KX) is set
bool the carrier of (X,Pn,KX) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set
bool (bool the carrier of (X,Pn,KX)) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set
the topology of (X,Pn,KX) is non empty Element of bool (bool the carrier of (X,Pn,KX))
Fm is non empty Element of bool (bool the carrier of (X,Pn,KX))
[#] (X,Pn,KX) is non proper Element of bool the carrier of (X,Pn,KX)
m is (X)
the topology of m is Element of bool (bool the carrier of m)
the carrier of m is set
bool the carrier of m is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set
bool (bool the carrier of m) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set
[#] m is non proper Element of bool the carrier of m
(X,m,KX) is strict non void subset-closed finite-membered () (X)
the topology of (X,m,KX) is non empty Element of bool (bool the carrier of (X,m,KX))
the carrier of (X,m,KX) is set
bool the carrier of (X,m,KX) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set
bool (bool the carrier of (X,m,KX)) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set
TopStruct(# the carrier of Pn, the topology of Pn #) is strict TopStruct
TopStruct(# the carrier of m, the topology of m #) is strict TopStruct
Pn is (X)
the topology of Pn is Element of bool (bool the carrier of Pn)
the carrier of Pn is set
bool the carrier of Pn is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set
bool (bool the carrier of Pn) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set
[#] Pn is non proper Element of bool the carrier of Pn
(X,Pn,KX) is strict non void subset-closed finite-membered () (X)
the topology of (X,Pn,KX) is non empty Element of bool (bool the carrier of (X,Pn,KX))
the carrier of (X,Pn,KX) is set
bool the carrier of (X,Pn,KX) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set
bool (bool the carrier of (X,Pn,KX)) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set
Pn is (X)
the topology of Pn is Element of bool (bool the carrier of Pn)
the carrier of Pn is set
bool the carrier of Pn is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set
bool (bool the carrier of Pn) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set
[#] Pn is non proper Element of bool the carrier of Pn
[:(bool (bool ([#] n))),(bool (bool ([#] n))):] is non empty Relation-like set
bool [:(bool (bool ([#] n))),(bool (bool ([#] n))):] is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set
n is Relation-like bool (bool ([#] n)) -defined bool (bool ([#] n)) -valued Function-like V33( bool (bool ([#] n)), bool (bool ([#] n))) Element of bool [:(bool (bool ([#] n))),(bool (bool ([#] n))):]
the topology of n is Element of bool (bool the carrier of n)
bool (bool the carrier of n) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set
Pn is Relation-like Function-like set
dom Pn is set
Pn . {} is set
{} + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V17() real finite cardinal integer Element of NAT
Pn . ({} + 1) is set
n . the topology of n is set
Pn . 1 is set
(X,n,KX) is strict non void subset-closed finite-membered () (X)
the topology of (X,n,KX) is non empty Element of bool (bool the carrier of (X,n,KX))
the carrier of (X,n,KX) is set
bool the carrier of (X,n,KX) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set
bool (bool the carrier of (X,n,KX)) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set
Fm is (X)
the topology of Fm is Element of bool (bool the carrier of Fm)
the carrier of Fm is set
bool the carrier of Fm is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set
bool (bool the carrier of Fm) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set
[#] Fm is non proper Element of bool the carrier of Fm
(X,Fm,KX) is strict non void subset-closed finite-membered () (X)
the topology of (X,Fm,KX) is non empty Element of bool (bool the carrier of (X,Fm,KX))
the carrier of (X,Fm,KX) is set
bool the carrier of (X,Fm,KX) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set
bool (bool the carrier of (X,Fm,KX)) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set
TopStruct(# the carrier of Fm, the topology of Fm #) is strict TopStruct
TopStruct(# the carrier of n, the topology of n #) is strict TopStruct
Fm is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V17() real finite cardinal integer set
Pn . Fm is set
Fm + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V17() real finite cardinal integer Element of NAT
Pn . (Fm + 1) is set
(Fm + 1) + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V17() real finite cardinal integer Element of NAT
Pn . ((Fm + 1) + 1) is set
SX is (X)
the topology of SX is Element of bool (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
bool (bool the carrier of SX) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set
[#] SX is non proper Element of bool the carrier of SX
(X,SX,KX) is strict non void subset-closed finite-membered () (X)
the topology of (X,SX,KX) is non empty Element of bool (bool the carrier of (X,SX,KX))
the carrier of (X,SX,KX) is set
bool the carrier of (X,SX,KX) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set
bool (bool the carrier of (X,SX,KX)) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set
[#] (X,SX,KX) is non proper Element of bool the carrier of (X,SX,KX)
c₁₁ is (X)
the topology of c₁₁ is Element of bool (bool the carrier of c₁₁)
the carrier of c₁₁ is set
bool the carrier of c₁₁ is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set
bool (bool the carrier of c₁₁) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set
[#] c₁₁ is non proper Element of bool the carrier of c₁₁
(X,c₁₁,KX) is strict non void subset-closed finite-membered () (X)
the topology of (X,c₁₁,KX) is non empty Element of bool (bool the carrier of (X,c₁₁,KX))
the carrier of (X,c₁₁,KX) is set
bool the carrier of (X,c₁₁,KX) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set
bool (bool the carrier of (X,c₁₁,KX)) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set
(Fm + 1) + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V17() real finite cardinal integer Element of NAT
Pn . ((Fm + 1) + 1) is set
n . (Pn . (Fm + 1)) is set
Fm is set
m is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V17() real finite cardinal integer set
SX is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V17() real finite cardinal integer set
c₁₁ is Element of bool (bool the carrier of n)
Pn . SX is set
TopStruct(# the carrier of n,c₁₁ #) is strict TopStruct
m is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V17() real finite cardinal integer set
Pn . m is set
SX is (X)
the topology of SX is Element of bool (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
bool (bool the carrier of SX) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set
[#] SX is non proper Element of bool the carrier of SX
c₁₁ is Element of bool (bool the carrier of n)
TopStruct(# the carrier of n,c₁₁ #) is strict TopStruct
TOP1 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V17() real finite cardinal integer set
K2 is Element of bool (bool the carrier of n)
Pn . TOP1 is set
TopStruct(# the carrier of n,K2 #) is strict TopStruct
m is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V17() real finite cardinal integer set
Fm is Relation-like Function-like set
dom Fm is set
Fm . {} is set
m is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V17() real finite cardinal integer set
Fm . m is set
m + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V17() real finite cardinal integer Element of NAT
Fm . (m + 1) is set
SX is (X)
(X,SX,KX) is strict non void subset-closed finite-membered () (X)
Pn . (m + 1) is set
(m + 1) + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V17() real finite cardinal integer Element of NAT
Pn . ((m + 1) + 1) is set
c₁₁ is (X)
the topology of c₁₁ is Element of bool (bool the carrier of c₁₁)
the carrier of c₁₁ is set
bool the carrier of c₁₁ is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set
bool (bool the carrier of c₁₁) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set
[#] c₁₁ is non proper Element of bool the carrier of c₁₁
(X,c₁₁,KX) is strict non void subset-closed finite-membered () (X)
the topology of (X,c₁₁,KX) is non empty Element of bool (bool the carrier of (X,c₁₁,KX))
the carrier of (X,c₁₁,KX) is set
bool the carrier of (X,c₁₁,KX) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set
bool (bool the carrier of (X,c₁₁,KX)) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set
c₁₁ is (X)
the topology of c₁₁ is Element of bool (bool the carrier of c₁₁)
the carrier of c₁₁ is set
bool the carrier of c₁₁ is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set
bool (bool the carrier of c₁₁) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set
[#] c₁₁ is non proper Element of bool the carrier of c₁₁
c₁₁ is (X)
the topology of c₁₁ is Element of bool (bool the carrier of c₁₁)
the carrier of c₁₁ is set
bool the carrier of c₁₁ is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set
bool (bool the carrier of c₁₁) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set
[#] c₁₁ is non proper Element of bool the carrier of c₁₁
Pn . m is set
K2 is (X)
the topology of K2 is Element of bool (bool the carrier of K2)
the carrier of K2 is set
bool the carrier of K2 is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set
bool (bool the carrier of K2) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set
[#] K2 is non proper Element of bool the carrier of K2
(X,K2,KX) is strict non void subset-closed finite-membered () (X)
the topology of (X,K2,KX) is non empty Element of bool (bool the carrier of (X,K2,KX))
the carrier of (X,K2,KX) is set
bool the carrier of (X,K2,KX) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set
bool (bool the carrier of (X,K2,KX)) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set
K2 is (X)
the topology of K2 is Element of bool (bool the carrier of K2)
the carrier of K2 is set
bool the carrier of K2 is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set
bool (bool the carrier of K2) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set
[#] K2 is non proper Element of bool the carrier of K2
K2 is (X)
the topology of K2 is Element of bool (bool the carrier of K2)
the carrier of K2 is set
bool the carrier of K2 is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set
bool (bool the carrier of K2) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set
[#] K2 is non proper Element of bool the carrier of K2
[#] (X,SX,KX) is non proper Element of bool the carrier of (X,SX,KX)
the carrier of (X,SX,KX) is set
bool the carrier of (X,SX,KX) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set
[#] SX is non proper 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
TOP1 is Element of bool (bool the carrier of n)
the topology of (X,SX,KX) is non empty Element of bool (bool the carrier of (X,SX,KX))
bool (bool the carrier of (X,SX,KX)) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set
H2 is (X)
the topology of H2 is Element of bool (bool the carrier of H2)
the carrier of H2 is set
bool the carrier of H2 is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set
bool (bool the carrier of H2) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set
[#] H2 is non proper Element of bool the carrier of H2
TOP2 is Element of bool (bool the carrier of n)
TopStruct(# the carrier of n,TOP2 #) is strict TopStruct
the topology of (X,SX,KX) is non empty Element of bool (bool the carrier of (X,SX,KX))
bool (bool the carrier of (X,SX,KX)) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set
Pn . SX is set
m is (X)
the topology of m is Element of bool (bool the carrier of m)
the carrier of m is set
bool the carrier of m is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set
bool (bool the carrier of m) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set
[#] m is non proper Element of bool the carrier of m
SX is strict (X)
Fm . SX is set
TOP1 is (X)
c₁₁ is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V17() real finite cardinal integer set
Fm . c₁₁ is set
c₁₁ + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V17() real finite cardinal integer Element of NAT
Fm . (c₁₁ + 1) is set
(X,TOP1,KX) is strict non void subset-closed finite-membered () (X)
P is (X)
n is (X)
Pn is Relation-like Function-like set
Pn . {} is set
Pn . SX is set
dom Pn is set
Fm is Relation-like Function-like set
Fm . {} is set
Fm . SX is set
dom Fm is set
m is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V17() real finite cardinal integer set
Pn . m is set
Fm . m is set
m + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V17() real finite cardinal integer Element of NAT
Pn . (m + 1) is set
Fm . (m + 1) is set
SX is (X)
SX is (X)
(X,SX,KX) is strict non void subset-closed finite-membered () (X)
c₁₁ is (X)
X is set
n is (X)
KX is Relation-like Function-like set
(X,n,KX,{}) is (X)
SX is Relation-like Function-like set
SX . {} is set
dom SX is set
X is set
n is (X)
KX is Relation-like Function-like set
(X,n,KX,1) is (X)
(X,n,KX) is strict non void subset-closed finite-membered () (X)
SX is Relation-like Function-like set
SX . {} is set
SX . 1 is set
dom SX is set
{} + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V17() real finite cardinal integer Element of NAT
SX . ({} + 1) is set
X is set
n is (X)
KX is Relation-like Function-like set
SX is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V17() real finite cardinal integer Element of NAT
P is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V17() real finite cardinal integer Element of NAT
SX + P is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V17() real finite cardinal integer Element of NAT
(X,n,KX,(SX + P)) is (X)
(X,n,KX,P) is (X)
(X,(X,n,KX,P),KX,SX) is (X)
n is Relation-like Function-like set
n . {} is set
n . SX is set
dom n is set
Pn is Relation-like Function-like set
Pn . {} is set
Pn . (SX + P) is set
dom Pn is set
Fm is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V17() real finite cardinal integer set
n . Fm is set
Fm + P is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V17() real finite cardinal integer Element of NAT
Pn . (Fm + P) is set
Fm + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V17() real finite cardinal integer Element of NAT
n . (Fm + 1) is set
(Fm + 1) + P is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V17() real finite cardinal integer Element of NAT
Pn . ((Fm + 1) + P) is set
m is (X)
m is (X)
(X,m,KX) is strict non void subset-closed finite-membered () (X)
(Fm + P) + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V17() real finite cardinal integer Element of NAT
Pn . ((Fm + P) + 1) is set
SX is (X)
Fm is Relation-like Function-like set
Fm . {} is set
Fm . P is set
dom Fm is set
m is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V17() real finite cardinal integer set
Fm . m is set
Pn . m is set
m + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V17() real finite cardinal integer Element of NAT
Fm . (m + 1) is set
Pn . (m + 1) is set
SX is (X)
SX is (X)
(X,SX,KX) is strict non void subset-closed finite-membered () (X)
c₁₁ is (X)
{} + P is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V17() real finite cardinal integer Element of NAT
Pn . ({} + P) is set
X is set
n is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V17() real finite cardinal integer set
KX is (X)
[#] 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
SX is Relation-like Function-like set
(X,KX,SX,n) is (X)
[#] (X,KX,SX,n) is non proper Element of bool the carrier of (X,KX,SX,n)
the carrier of (X,KX,SX,n) is set
bool the carrier of (X,KX,SX,n) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set
P is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V17() real finite cardinal integer set
(X,KX,SX,P) is (X)
[#] (X,KX,SX,P) is non proper Element of bool the carrier of (X,KX,SX,P)
the carrier of (X,KX,SX,P) is set
bool the carrier of (X,KX,SX,P) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set
P + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V17() real finite cardinal integer Element of NAT
(X,KX,SX,(P + 1)) is (X)
[#] (X,KX,SX,(P + 1)) is non proper Element of bool the carrier of (X,KX,SX,(P + 1))
the carrier of (X,KX,SX,(P + 1)) is set
bool the carrier of (X,KX,SX,(P + 1)) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set
(X,(X,KX,SX,P),SX,1) is (X)
(X,(X,KX,SX,P),SX) is strict non void subset-closed finite-membered () (X)
(X,KX,SX,{}) is (X)
[#] (X,KX,SX,{}) is non proper Element of bool the carrier of (X,KX,SX,{})
the carrier of (X,KX,SX,{}) is set
bool the carrier of (X,KX,SX,{}) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set
X is set
n is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V17() real finite cardinal integer set
KX is (X)
SX is subset-closed finite-membered (X,KX)
P is Relation-like Function-like set
(X,SX,P,n) is (X)
(X,KX,P,n) is (X)
n is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V17() real finite cardinal integer set
(X,SX,P,n) is (X)
(X,KX,P,n) is (X)
n + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V17() real finite cardinal integer Element of NAT
(X,SX,P,(n + 1)) is (X)
(X,KX,P,(n + 1)) is (X)
Pn is subset-closed finite-membered (X,(X,KX,P,n))
(X,Pn,P,1) is (X)
(X,Pn,P) is strict non void subset-closed finite-membered () (X)
(X,(X,KX,P,n),P,1) is (X)
(X,(X,KX,P,n),P) is strict non void subset-closed finite-membered () (X)
(X,SX,P,{}) is (X)
(X,KX,P,{}) is (X)