:: SIMPLEX0 semantic presentation

REAL is 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

RAT is set
INT is set

is non empty non trivial non empty-membered Relation-like non finite set
is non empty non trivial non empty-membered Relation-like non finite set
bool 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

K387() is M22()

K89(K387(),) is set

K63(1) is ext-real non positive V17() real integer Element of REAL
is non empty non trivial non empty-membered Relation-like non finite set
NAT \/ is non empty set
is set

() \ is Element of bool ()
bool () 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

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

n is set
X is subset-closed V252() 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 (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 (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 b1) where b1 is Element of X : b1 in X } is set
union { (bool b1) where b1 is Element of X : b1 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 (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 (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 (bool Pn) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set
X is set
{ (bool b1) where b1 is Element of X : b1 in X } is set
union { (bool b1) where b1 is Element of X : b1 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 b1) where b1 is Element of n : b1 in n } is set
union { (bool b1) where b1 is Element of n : b1 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 (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 (bool P) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set
X is 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 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 (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 (bool X) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set
n is set
KX is set

{ b1 where b1 is Element of bool X : ( b1 in n & card b1 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

P is Element of bool (bool X)
n is Element of bool X

Pn is Element of bool X

SX is Element of bool (bool X)
P is Element of bool (bool X)
n is set

n is set

X is non empty 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

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 (bool X) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set
SX is set

X is set
n is subset-closed V252() set
KX is set
(X,n,KX) 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
SX is set
P is 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 (bool X) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set

X is non empty 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

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

X is 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

union X is set

union SX is set

P is finite set

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

n \/ {P} is non empty finite set
union n is set

() \/ () is set
() \/ P is set
Pn is finite set

union KX is set

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

bool (bool X) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed 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)

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

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

Fm is set
SX . Fm is set
{Fm} is non empty trivial finite 1 -element set
Pn \ {Fm} is Element of bool Pn

(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}

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 (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 set
{ b1 where b1 is Element of bool X : ( KX in b1 & b1 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

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
{ b1 where b1 is Element of bool X : ( b1 c< SX & b1 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 \ (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

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

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

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

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

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 \ (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

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

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
c11 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 c11 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 c11 is Element of bool ((KX . m) \ (SX . (KX . m)))
c11 . m is set
(SX . (KX . m)) \/ (c11 . m) is set

TOP1 is set
{TOP1} is non empty trivial finite 1 -element set
Fm \ {TOP1} is Element of bool Fm

((SX . (KX . m)) \/ (c11 . m)) \ (c11 . m) is Element of bool ((SX . (KX . m)) \/ (c11 . m))
bool ((SX . (KX . m)) \/ (c11 . m)) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set
(SX . (KX . m)) \ (c11 . 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

TOP1 is set
{TOP1} is non empty trivial finite 1 -element set
(c11 . m) \ {TOP1} is Element of bool (c11 . m)
bool (c11 . m) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set
Fm \ {TOP1} is Element of bool Fm

K2 is set
c11 . K2 is set
KX . K2 is set
Pn . K2 is set
(SX . (KX . m)) \/ ((c11 . m) \ {TOP1}) is set
((SX . (KX . m)) \/ (c11 . m)) \ {TOP1} is Element of bool ((SX . (KX . m)) \/ (c11 . m))
bool ((SX . (KX . m)) \/ (c11 . m)) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set

Fm is set
m is set
SX is set
Pn . SX is set
c11 is set
Pn . c11 is set
KX . SX is set
KX . c11 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 . c11) is set
(KX . c11) \ (SX . (KX . c11)) is Element of bool (KX . c11)
bool (KX . c11) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set
bool ((KX . c11) \ (SX . (KX . c11))) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed Element of bool (bool ((KX . c11) \ (SX . (KX . c11))))
bool ((KX . c11) \ (SX . (KX . c11))) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set
bool (bool ((KX . c11) \ (SX . (KX . c11)))) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set
[:((KX . c11) \ (SX . (KX . c11))),(bool ((KX . c11) \ (SX . (KX . c11)))):] is Relation-like set
bool [:((KX . c11) \ (SX . (KX . c11))),(bool ((KX . c11) \ (SX . (KX . c11)))):] is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set
n . (KX . c11) is Relation-like Function-like set
H2 is Relation-like (KX . c11) \ (SX . (KX . c11)) -defined bool ((KX . c11) \ (SX . (KX . c11))) -valued Function-like V33((KX . c11) \ (SX . (KX . c11)), bool ((KX . c11) \ (SX . (KX . c11)))) Element of bool [:((KX . c11) \ (SX . (KX . c11))),(bool ((KX . c11) \ (SX . (KX . c11)))):]
rng H2 is Element of bool (bool ((KX . c11) \ (SX . (KX . c11))))
bool (bool ((KX . c11) \ (SX . (KX . c11)))) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set
dom H2 is Element of bool ((KX . c11) \ (SX . (KX . c11)))
H2 . c11 is set
(SX . (KX . c11)) \/ (H2 . c11) is set
TOP2 . c11 is set
(SX . (KX . SX)) \/ ((KX . SX) \ (SX . (KX . SX))) is set
(SX . (KX . c11)) \/ ((KX . c11) \ (SX . (KX . c11))) 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

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

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

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
{ b1 where b1 is Element of the carrier of X : b1 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

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)
{ b1 where b1 is Element of bool the carrier of X : ( b1 is open & KX in b1 ) } 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

KX is finite Element of bool the carrier of X

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
{ b1 where b1 is Element of bool the carrier of X : ( n in b1 & b1 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
{ b1 where b1 is Element of bool (KX \ {n}) : ex b2 being Element of bool the carrier of X st
( S1[b2,b1] & b2 in { b1 where b3 is Element of bool the carrier of X : ( n in b1 & b1 c= KX ) } )
}
is set

SX is set
c11 is Element of bool the carrier of X
c11 \/ {n} is non empty set
(c11 \/ {n}) \ {n} is Element of bool (c11 \/ {n})
bool (c11 \/ {n}) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set
{ b1 where b1 is Element of bool the carrier of X : ( b1 is open & n in b1 ) } is set
c11 is set
TOP1 is Element of bool the carrier of X
c11 is Element of bool the carrier of X
c11 \ {n} is Element of bool c11
bool c11 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

TopStruct(# {},({} ()) #) is strict TopStruct
[#] TopStruct(# {},({} ()) #) is non proper Element of bool the carrier of TopStruct(# {},({} ()) #)
the carrier of TopStruct(# {},({} ()) #) is set
bool the carrier of TopStruct(# {},({} ()) #) 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 (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)
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 (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

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

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 (bool n) is non empty non with_non-empty_elements subset-closed V120() V252() d.union-closed set
X is 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 (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 (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 (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 (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

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

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 ()) is finite Element of bool ()
((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 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 - 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