:: TOPGEN_2 semantic presentation

K190() is set

K32(K190()) is non empty set

K32(omega) is non empty non trivial non finite set

K33(1,1) is non empty finite set
K32(K33(1,1)) is non empty finite V32() set
K33(K33(1,1),1) is non empty finite set
K32(K33(K33(1,1),1)) is non empty finite V32() set
K33(K33(1,1),K190()) is set
K32(K33(K33(1,1),K190())) is non empty set
K33(K190(),K190()) is set
K33(K33(K190(),K190()),K190()) is set
K32(K33(K33(K190(),K190()),K190())) is non empty set

K33(2,2) is non empty finite set
K33(K33(2,2),K190()) is set
K32(K33(K33(2,2),K190())) is non empty set
K32(K194()) is non empty non trivial non finite set
{} is set

K32({}) is non empty set
is non empty trivial finite 1 -element set
e is non empty TopSpace-like TopStruct
the carrier of e is non empty set
K32( the carrier of e) is non empty set
K32(K32( the carrier of e)) is non empty set
tE is non empty open quasi_basis Element of K32(K32( the carrier of e))
E is Element of the carrier of e
{ b1 where b1 is Element of K32( the carrier of e) : ( E in b1 & b1 in tE ) } is set
O is set
B is Element of K32( the carrier of e)
O is Element of K32(K32( the carrier of e))
the topology of e is non empty open Element of K32(K32( the carrier of e))
B is set
dT is Element of K32( the carrier of e)
Intersect O is Element of K32( the carrier of e)
B is Element of K32( the carrier of e)
dT is Element of K32( the carrier of e)
e is non empty TopSpace-like TopStruct
the carrier of e is non empty set
K32( the carrier of e) is non empty set
K32(K32( the carrier of e)) is non empty set
tE is Relation-like the carrier of e -defined Function-like V36( the carrier of e) set
Union tE is set
proj2 tE is set
union (proj2 tE) is set
bool the carrier of e is non empty Element of K32(K32( the carrier of e))
E is set
dom tE is Element of K32( the carrier of e)
X is set
tE . X is set
O is Element of the carrier of e
tE . O is set
dom tE is Element of K32( the carrier of e)
X is Element of K32( the carrier of e)
O is Element of the carrier of e
tE . O is set
B is Element of K32( the carrier of e)
dT is Element of K32( the carrier of e)
E is Element of K32(K32( the carrier of e))
the topology of e is non empty open Element of K32(K32( the carrier of e))
X is set
O is set
tE . O is set
B is Element of the carrier of e
tE . B is set
e is non empty TopStruct
the carrier of e is non empty set
tE is Element of the carrier of e
K32( the carrier of e) is non empty set
K32(K32( the carrier of e)) is non empty set
the open tE -quasi_basis Element of K32(K32( the carrier of e)) is open tE -quasi_basis Element of K32(K32( the carrier of e))

O is open tE -quasi_basis Element of K32(K32( the carrier of e))

O is open tE -quasi_basis Element of K32(K32( the carrier of e))

B is open tE -quasi_basis Element of K32(K32( the carrier of e))

O is open tE -quasi_basis Element of K32(K32( the carrier of e))

B is open tE -quasi_basis Element of K32(K32( the carrier of e))

e is set
union e is set
tE is set
e is non empty TopStruct
the carrier of e is non empty set
{ (e,b1) where b1 is Element of the carrier of e : verum } is set
E is set
X is Element of the carrier of e

union { (e,b1) where b1 is Element of the carrier of e : verum } is set

X is Element of the carrier of e

O is set
B is Element of the carrier of e

e is non empty TopStruct
the carrier of e is non empty set
{ (e,b1) where b1 is Element of the carrier of e : verum } is set
union { (e,b1) where b1 is Element of the carrier of e : verum } is set

X is Element of the carrier of e

e is non empty TopStruct

the carrier of e is non empty set
{ (e,b1) where b1 is Element of the carrier of e : verum } is set
union { (e,b1) where b1 is Element of the carrier of e : verum } is set

X is Element of the carrier of e

e is non empty TopStruct
the carrier of e is non empty set

{ (e,b1) where b1 is Element of the carrier of e : verum } is set
E is Element of the carrier of e

union { (e,b1) where b1 is Element of the carrier of e : verum } is set
e is non empty TopSpace-like TopStruct

the carrier of e is non empty set
{ (e,b1) where b1 is Element of the carrier of e : verum } is set
union { (e,b1) where b1 is Element of the carrier of e : verum } is set
K32( the carrier of e) is non empty set
K32(K32( the carrier of e)) is non empty set
E is set
X is Element of the carrier of e

O is non empty open X -quasi_basis Element of K32(K32( the carrier of e))

E is Element of the carrier of e
K32( the carrier of e) is non empty set
K32(K32( the carrier of e)) is non empty set

X is non empty open E -quasi_basis Element of K32(K32( the carrier of e))

e is non empty TopSpace-like TopStruct
the carrier of e is non empty set
K32( the carrier of e) is non empty set
K32(K32( the carrier of e)) is non empty set
the non empty open quasi_basis Element of K32(K32( the carrier of e)) is non empty open quasi_basis Element of K32(K32( the carrier of e))
{ b1 where b1 is Element of K32( the carrier of e) : ( a1 in b1 & b1 in the non empty open quasi_basis Element of K32(K32( the carrier of e)) ) } is set
E is Relation-like the carrier of e -defined Function-like V36( the carrier of e) set
X is Element of the carrier of e
E . X is set
{ b1 where b1 is Element of K32( the carrier of e) : ( X in b1 & b1 in the non empty open quasi_basis Element of K32(K32( the carrier of e)) ) } is set
e is non empty TopSpace-like TopStruct
the carrier of e is non empty set
tE is Relation-like the carrier of e -defined Function-like V36( the carrier of e) (e)
Union tE is set
proj2 tE is set
union (proj2 tE) is set
K32( the carrier of e) is non empty set
K32(K32( the carrier of e)) is non empty set
E is Element of the carrier of e
tE . E is set
E is Element of the carrier of e
tE . E is set
e is non empty TopSpace-like TopStruct
the carrier of e is non empty set
K32( the carrier of e) is non empty set
K32(K32( the carrier of e)) is non empty set
tE is Element of the carrier of e
E is Element of the carrier of e
X is non empty open tE -quasi_basis Element of K32(K32( the carrier of e))
O is non empty open E -quasi_basis Element of K32(K32( the carrier of e))
B is set
dT is Element of K32( the carrier of e)
e is non empty TopSpace-like TopStruct
the carrier of e is non empty set
K32( the carrier of e) is non empty set
K32(K32( the carrier of e)) is non empty set
tE is Element of the carrier of e
E is non empty open tE -quasi_basis Element of K32(K32( the carrier of e))
X is set
O is set
X /\ O is set
dT is open Element of K32( the carrier of e)
B is open Element of K32( the carrier of e)
B /\ dT is open Element of K32( the carrier of e)
TT is Element of K32( the carrier of e)
e is non empty TopSpace-like TopStruct
the carrier of e is non empty set
K32( the carrier of e) is non empty set
E is Element of the carrier of e
tE is Element of K32( the carrier of e)
Cl tE is closed Element of K32( the carrier of e)
K32(K32( the carrier of e)) is non empty set
O is set
X is non empty open E -quasi_basis Element of K32(K32( the carrier of e))
e is non empty TopSpace-like TopStruct
the carrier of e is non empty set
K32( the carrier of e) is non empty set
E is Element of the carrier of e
K32(K32( the carrier of e)) is non empty set
tE is Element of K32( the carrier of e)
X is non empty open E -quasi_basis Element of K32(K32( the carrier of e))
O is Element of K32( the carrier of e)
B is Element of K32( the carrier of e)
Cl tE is closed Element of K32( the carrier of e)
e is non empty TopSpace-like TopStruct
the carrier of e is non empty set
K32( the carrier of e) is non empty set
K32(K32( the carrier of e)) is non empty set
tE is Element of K32( the carrier of e)
Cl tE is closed Element of K32( the carrier of e)
E is Element of the carrier of e
the non empty open E -quasi_basis Element of K32(K32( the carrier of e)) is non empty open E -quasi_basis Element of K32(K32( the carrier of e))
B is set
O is non empty open E -quasi_basis Element of K32(K32( the carrier of e))
O is set
e is non empty TopSpace-like TopStruct
the carrier of e is non empty set
K32( the carrier of e) is non empty set
K32(K32( the carrier of e)) is non empty set
tE is Element of K32( the carrier of e)
Cl tE is closed Element of K32( the carrier of e)
E is Element of the carrier of e
the non empty open E -quasi_basis Element of K32(K32( the carrier of e)) is non empty open E -quasi_basis Element of K32(K32( the carrier of e))
O is set
O is non empty open E -quasi_basis Element of K32(K32( the carrier of e))

the carrier of e is set
K32( the carrier of e) is non empty set
K32(K32( the carrier of e)) is non empty set
the topology of e is non empty open Element of K32(K32( the carrier of e))
e is non empty TopSpace-like TopStruct
the carrier of e is non empty set
K32( the carrier of e) is non empty set
K32(K32( the carrier of e)) is non empty set

tE is open Element of K32(K32( the carrier of e))
union tE is Element of K32( the carrier of e)
E is non empty open quasi_basis Element of K32(K32( the carrier of e))

{ b1 where b1 is Element of K32( the carrier of e) : ( b1 in E & ex b2 being set st
( b2 in tE & b1 c= b2 ) )
}
is set

O is set
B is Element of K32( the carrier of e)
dT is set
card { b1 where b1 is Element of K32( the carrier of e) : ( b1 in E & ex b2 being set st
( b2 in tE & b1 c= b2 ) )
}
is epsilon-transitive epsilon-connected ordinal cardinal set

O is set
B is Element of K32( the carrier of e)
dT is set

proj1 O is set
proj2 O is set
dT is open Element of K32(K32( the carrier of e))
union dT is Element of K32( the carrier of e)

TT is set
T is set
o is Element of the carrier of e
a is open Element of K32( the carrier of e)
F is Element of K32( the carrier of e)
O . F is set
e is TopStruct
the carrier of e is set
K32( the carrier of e) is non empty set
K32(K32( the carrier of e)) is non empty set

tE is open quasi_basis Element of K32(K32( the carrier of e))

e is TopStruct
e is set

E is non empty set
{ {b1} where b1 is Element of E : verum } is set
X is set
{X} is non empty trivial finite 1 -element set
K33(E,) is set
K32(K33(E,)) is non empty set

rng X is Element of K32()
K32() is non empty set
O is set
B is Element of E
{B} is non empty trivial finite 1 -element Element of K32(E)
K32(E) is non empty set
X . B is Element of SmallestPartition e
O is set
proj1 X is set
X . O is set
B is set
X . B is set
dom X is Element of K32(E)
K32(E) is non empty set
{O} is non empty trivial finite 1 -element set
{B} is non empty trivial finite 1 -element set
dom X is Element of K32(E)
K32(E) is non empty set
e is non empty TopSpace-like discrete V78() V79() V80() TopStruct
the carrier of e is non empty set
SmallestPartition the carrier of e is non empty with_non-empty_elements a_partition of the carrier of e
K32( the carrier of e) is non empty set
K32(K32( the carrier of e)) is non empty set
the topology of e is non empty open Element of K32(K32( the carrier of e))
E is set
X is Element of K32( the carrier of e)
{ {b1} where b1 is Element of the carrier of e : verum } is set
E is Element of K32( the carrier of e)
X is Element of the carrier of e
{X} is non empty trivial finite 1 -element Element of K32( the carrier of e)
O is Element of K32( the carrier of e)
B is Element of K32( the carrier of e)
E is non empty open quasi_basis Element of K32(K32( the carrier of e))
X is set
O is Element of the carrier of e
{O} is non empty trivial finite 1 -element Element of K32( the carrier of e)
B is Element of K32( the carrier of e)
dT is Element of K32( the carrier of e)
e is non empty TopSpace-like discrete V78() V79() V80() TopStruct

the carrier of e is non empty set

K32( the carrier of e) is non empty set
K32(K32( the carrier of e)) is non empty set
{ (card b1) where b1 is non empty open quasi_basis Element of K32(K32( the carrier of e)) : verum } is set
SmallestPartition the carrier of e is non empty with_non-empty_elements a_partition of the carrier of e
E is non empty open quasi_basis Element of K32(K32( the carrier of e))

meet { (card b1) where b1 is non empty open quasi_basis Element of K32(K32( the carrier of e)) : verum } is set
X is non empty open quasi_basis Element of K32(K32( the carrier of e))

the non empty non trivial non finite set is non empty non trivial non finite set
K32( the non empty non trivial non finite set ) is non empty non trivial non finite set
K32(K32( the non empty non trivial non finite set )) is non empty non trivial non finite set
bool the non empty non trivial non finite set is non empty non trivial non finite Element of K32(K32( the non empty non trivial non finite set ))
tE is Element of K32(K32( the non empty non trivial non finite set ))
TopStruct(# the non empty non trivial non finite set ,tE #) is non empty strict TopStruct
E is non empty TopSpace-like discrete V78() V79() V80() TopStruct

the carrier of E is non empty set

e is non empty non trivial non finite TopSpace-like () TopStruct
the carrier of e is non empty non trivial non finite set
K32( the carrier of e) is non empty non trivial non finite set
K32(K32( the carrier of e)) is non empty non trivial non finite set

tE is non empty open quasi_basis Element of K32(K32( the carrier of e))
E is non empty open quasi_basis Element of K32(K32( the carrier of e))

X is set
{ b1 where b1 is Element of K32( the carrier of e) : ( b1 in tE & b1 c= X ) } is set
B is set
dT is Element of K32( the carrier of e)
union { b1 where b1 is Element of K32( the carrier of e) : ( b1 in tE & b1 c= X ) } is set
B is open Element of K32( the carrier of e)
dT is open Element of K32(K32( the carrier of e))
union dT is Element of K32( the carrier of e)
TT is open Element of K32(K32( the carrier of e))
union TT is Element of K32( the carrier of e)

T is set
a is set
bool tE is non empty Element of K32(K32(tE))
K32(tE) is non empty set
K32(K32(tE)) is non empty set
union a is set

proj1 X is set
proj2 X is set
Union X is set
union () is set
union (bool tE) is Element of K32(tE)
the topology of e is non empty open Element of K32(K32( the carrier of e))
O is Element of K32(K32( the carrier of e))
B is Element of K32( the carrier of e)
dT is Element of the carrier of e
TT is Element of K32( the carrier of e)
X . TT is set
union (X . TT) is set

T is set

dT is set

TT is set
X . TT is set
B is non empty open quasi_basis Element of K32(K32( the carrier of e))

e is non empty TopSpace-like () TopStruct
the carrier of e is non empty set
K32( the carrier of e) is non empty set
K32(K32( the carrier of e)) is non empty set
the topology of e is non empty open Element of K32(K32( the carrier of e))
K33( the carrier of e, the topology of e) is non empty set
K32(K33( the carrier of e, the topology of e)) is non empty set

tE is non empty open quasi_basis Element of K32(K32( the carrier of e))

{ b1 where b1 is Element of K32( the carrier of e) : ( a1 in b1 & b1 in tE ) } is set
meet { b1 where b1 is Element of K32( the carrier of e) : ( a1 in b1 & b1 in tE ) } is set
FinMeetCl tE is Element of K32(K32( the carrier of e))
FinMeetCl the topology of e is Element of K32(K32( the carrier of e))
E is set
X is Element of the carrier of e
{ b1 where b1 is Element of K32( the carrier of e) : ( X in b1 & b1 in tE ) } is set
[#] e is non empty non proper open closed dense non boundary Element of K32( the carrier of e)
B is Element of K32( the carrier of e)
dT is set
TT is Element of K32( the carrier of e)
dT is Element of K32(K32( the carrier of e))
Intersect dT is Element of K32( the carrier of e)
{ b1 where b1 is Element of K32( the carrier of e) : ( E in b1 & b1 in tE ) } is set
meet { b1 where b1 is Element of K32( the carrier of e) : ( E in b1 & b1 in tE ) } is set
E is Relation-like the carrier of e -defined the topology of e -valued Function-like V37( the carrier of e, the topology of e) Element of K32(K33( the carrier of e, the topology of e))
rng E is Element of K32( the topology of e)
K32( the topology of e) is non empty set
B is set
dT is Element of the carrier of e
{ b1 where b1 is Element of K32( the carrier of e) : ( dT in b1 & b1 in tE ) } is set
T is Element of K32( the carrier of e)
a is set
o is Element of K32( the carrier of e)
E . B is set
meet { b1 where b1 is Element of K32( the carrier of e) : ( dT in b1 & b1 in tE ) } is set
B is Element of the carrier of e
{ b1 where b1 is Element of K32( the carrier of e) : ( B in b1 & b1 in tE ) } is set
dT is Element of K32( the carrier of e)
T is Element of K32( the carrier of e)
E . B is Element of the topology of e
meet { b1 where b1 is Element of K32( the carrier of e) : ( B in b1 & b1 in tE ) } is set
B is Element of K32( the carrier of e)
dT is Element of the carrier of e
E . dT is Element of the topology of e
TT is Element of K32( the carrier of e)
T is Element of K32( the carrier of e)
O is Element of K32(K32( the carrier of e))
B is non empty open quasi_basis Element of K32(K32( the carrier of e))
dT is Element of the carrier of e
E . dT is Element of the topology of e
TT is open Element of K32( the carrier of e)

the carrier of e is set
K32( the carrier of e) is non empty set
K32(K32( the carrier of e)) is non empty set
the topology of e is non empty open Element of K32(K32( the carrier of e))
K33( the carrier of e, the topology of e) is set
K32(K33( the carrier of e, the topology of e)) is non empty set
tE is open quasi_basis Element of K32(K32( the carrier of e))
E is open quasi_basis Element of K32(K32( the carrier of e))
X is Relation-like the carrier of e -defined the topology of e -valued Function-like V37( the carrier of e, the topology of e) Element of K32(K33( the carrier of e, the topology of e))
rng X is Element of K32( the topology of e)
K32( the topology of e) is non empty set
O is set
dom X is Element of K32( the carrier of e)
dT is set
X . dT is set
B is Element of K32( the carrier of e)
TT is Element of the carrier of e
T is Element of K32( the carrier of e)

the carrier of e is set
K32( the carrier of e) is non empty set
K32(K32( the carrier of e)) is non empty set
the topology of e is non empty open Element of K32(K32( the carrier of e))
K33( the carrier of e, the topology of e) is set
K32(K33( the carrier of e, the topology of e)) is non empty set

tE is open quasi_basis Element of K32(K32( the carrier of e))

E is Relation-like the carrier of e -defined the topology of e -valued Function-like V37( the carrier of e, the topology of e) Element of K32(K33( the carrier of e, the topology of e))
rng E is Element of K32( the topology of e)
K32( the topology of e) is non empty set
{ (card b1) where b1 is open quasi_basis Element of K32(K32( the carrier of e)) : verum } is set
meet { (card b1) where b1 is open quasi_basis Element of K32(K32( the carrier of e)) : verum } is set
O is open quasi_basis Element of K32(K32( the carrier of e))

e is non empty TopSpace-like () TopStruct
the carrier of e is non empty set
K32( the carrier of e) is non empty set
K32(K32( the carrier of e)) is non empty set

tE is non empty open quasi_basis Element of K32(K32( the carrier of e))
the topology of e is non empty open Element of K32(K32( the carrier of e))
K33( the carrier of e, the topology of e) is non empty set
K32(K33( the carrier of e, the topology of e)) is non empty set
E is non empty open quasi_basis Element of K32(K32( the carrier of e))
X is Relation-like the carrier of e -defined the topology of e -valued Function-like V37( the carrier of e, the topology of e) Element of K32(K33( the carrier of e, the topology of e))
rng X is Element of K32( the topology of e)
K32( the topology of e) is non empty set

e is non empty TopSpace-like TopStruct
the carrier of e is non empty set
K32( the carrier of e) is non empty set
K32(K32( the carrier of e)) is non empty set

tE is non empty open quasi_basis Element of K32(K32( the carrier of e))
e is set
K32(e) is non empty set
tE is set
{ b1 where b1 is Element of K32(e) : not tE in b1 } is set
{ (b1 `) where b1 is Element of K32(e) : b1 is finite } is set
{ b1 where b1 is Element of K32(e) : not tE in b1 } \/ { (b1 `) where b1 is Element of K32(e) : b1 is finite } is set

the carrier of E is set
the topology of E is open Element of K32(K32( the carrier of E))
K32( the carrier of E) is non empty set
K32(K32( the carrier of E)) is non empty set

the carrier of X is set
the topology of X is open Element of K32(K32( the carrier of X))
K32( the carrier of X) is non empty set
K32(K32( the carrier of X)) is non empty set
bool e is non empty Element of K32(K32(e))
K32(K32(e)) is non empty set
B is set
dT is Element of K32(e)
TT is Element of K32(e)
TT ` is Element of K32(e)
e \ TT is set
B is Element of K32(K32(e))
TopStruct(# e,B #) is strict TopStruct
the carrier of TopStruct(# e,B #) is set
the topology of TopStruct(# e,B #) is open Element of K32(K32( the carrier of TopStruct(# e,B #)))
K32( the carrier of TopStruct(# e,B #)) is non empty set
K32(K32( the carrier of TopStruct(# e,B #))) is non empty set
e is set
tE is set
(e,tE) is strict TopStruct
K32(e) is non empty set
{ b1 where b1 is Element of K32(e) : not tE in b1 } is set
{ (b1 `) where b1 is Element of K32(e) : b1 is finite } is set
{ b1 where b1 is Element of K32(e) : not tE in b1 } \/ { (b1 `) where b1 is Element of K32(e) : b1 is finite } is set
the carrier of (e,tE) is set
the topology of (e,tE) is open Element of K32(K32( the carrier of (e,tE)))
K32( the carrier of (e,tE)) is non empty set
K32(K32( the carrier of (e,tE))) is non empty set

({} e) ` is Element of K32(e)
e \ ({} e) is set
dT is Element of K32(K32( the carrier of (e,tE)))
TT is set
union dT is Element of K32( the carrier of (e,tE))
(union dT) ` is Element of K32( the carrier of (e,tE))
the carrier of (e,tE) \ (union dT) is set
((union dT) `) ` is Element of K32( the carrier of (e,tE))
the carrier of (e,tE) \ ((union dT) `) is set
T is Element of K32(e)
T ` is Element of K32(e)
e \ T is set
union dT is Element of K32( the carrier of (e,tE))
TT is set
T is Element of K32(e)
dT is Element of K32( the carrier of (e,tE))
TT is Element of K32( the carrier of (e,tE))
dT /\ TT is Element of K32( the carrier of (e,tE))
T is Element of K32(e)
T ` is Element of K32(e)
e \ T is set
a is Element of K32(e)
a ` is Element of K32(e)
e \ a is set
a \/ T is Element of K32(e)
(a \/ T) ` is Element of K32(e)
e \ (a \/ T) is set
T is Element of K32(e)
a is Element of K32(e)
e is non empty set
tE is set
(e,tE) is strict TopSpace-like TopStruct
e is set
tE is set
(e,tE) is strict TopSpace-like TopStruct
the carrier of (e,tE) is set
K32( the carrier of (e,tE)) is non empty set
K32(e) is non empty set
{ b1 where b1 is Element of K32(e) : not tE in b1 } is set
{ (b1 `) where b1 is Element of K32(e) : b1 is finite } is set
B is Element of K32( the carrier of (e,tE))
B ` is Element of K32( the carrier of (e,tE))
the carrier of (e,tE) \ B is set
the topology of (e,tE) is non empty open Element of K32(K32( the carrier of (e,tE)))
K32(K32( the carrier of (e,tE))) is non empty set
{ b1 where b1 is Element of K32(e) : not tE in b1 } \/ { (b1 `) where b1 is Element of K32(e) : b1 is finite } is set
dT is Element of K32(e)
TT is Element of K32(e)
TT ` is Element of K32(e)
e \ TT is set
(B `) ` is Element of K32( the carrier of (e,tE))
the carrier of (e,tE) \ (B `) is set
e is set
tE is set
(e,tE) is strict TopSpace-like TopStruct
the carrier of (e,tE) is set
K32( the carrier of (e,tE)) is non empty set
X is Element of K32( the carrier of (e,tE))
X ` is Element of K32( the carrier of (e,tE))
the carrier of (e,tE) \ X is set
(X `) ` is Element of K32( the carrier of (e,tE))
the carrier of (e,tE) \ (X `) is set
E is set
e is set
{E} is non empty trivial finite 1 -element set
tE is set
(e,tE) is strict TopSpace-like TopStruct
the carrier of (e,tE) is set
K32( the carrier of (e,tE)) is non empty set
E is set
e is set
tE is set
{E} is non empty trivial finite 1 -element set
(e,tE) is strict TopSpace-like TopStruct
the carrier of (e,tE) is set
K32( the carrier of (e,tE)) is non empty set
e is set
tE is set
(e,tE) is strict TopSpace-like TopStruct
the carrier of (e,tE) is set
K32( the carrier of (e,tE)) is non empty set
{tE} is non empty trivial finite 1 -element set
X is Element of K32( the carrier of (e,tE))
X ` is Element of K32( the carrier of (e,tE))
the carrier of (e,tE) \ X is set
(X `) \/ {tE} is set
e is set
tE is set
(e,tE) is strict TopSpace-like TopStruct
the carrier of (e,tE) is set
K32( the carrier of (e,tE)) is non empty set
E is Element of K32( the carrier of (e,tE))
Cl E is closed Element of K32( the carrier of (e,tE))
e is non empty TopSpace-like TopStruct
the carrier of e is non empty set
K32( the carrier of e) is non empty set
tE is Element of K32( the carrier of e)
Cl tE is closed Element of K32( the carrier of e)
E is Element of the carrier of e
{E} is non empty trivial finite 1 -element Element of K32( the carrier of e)
tE \/ {E} is Element of K32( the carrier of e)
Cl (tE \/ {E}) is closed Element of K32( the carrier of e)
tE is set
e is set
(e,tE) is strict TopSpace-like TopStruct
the carrier of (e,tE) is set
K32( the carrier of (e,tE)) is non empty set
{tE} is non empty trivial finite 1 -element set
X is non empty TopSpace-like TopStruct
the carrier of X is non empty set
B is Element of K32( the carrier of (e,tE))
Cl B is closed Element of K32( the carrier of (e,tE))
B \/ {tE} is set
K32( the carrier of X) is non empty set
O is Element of the carrier of X
{O} is non empty trivial finite 1 -element Element of K32( the carrier of X)
TT is Element of K32( the carrier of X)
dT is Element of K32( the carrier of X)
TT \/ dT is Element of K32( the carrier of X)
Cl (TT \/ dT) is closed Element of K32( the carrier of X)
e is set
tE is set
(e,tE) is strict TopSpace-like TopStruct
the carrier of (e,tE) is set
K32( the carrier of (e,tE)) is non empty set
E is Element of K32( the carrier of (e,tE))
E ` is Element of K32( the carrier of (e,tE))
the carrier of (e,tE) \ E is set
Int E is open Element of K32( the carrier of (e,tE))
Cl (E `) is closed Element of K32( the carrier of (e,tE))
(E `) ` is Element of K32( the carrier of (e,tE))
the carrier of (e,tE) \ (E `) is set
tE is set
e is set
(e,tE) is strict TopSpace-like TopStruct
the carrier of (e,tE) is set
K32( the carrier of (e,tE)) is non empty set
{tE} is non empty trivial finite 1 -element set
X is non empty TopSpace-like TopStruct
the carrier of X is non empty set
B is Element of K32( the carrier of (e,tE))
B ` is Element of K32( the carrier of (e,tE))
the carrier of (e,tE) \ B is set
Int B is open Element of K32( the carrier of (e,tE))
B \ {tE} is Element of K32( the carrier of (e,tE))
K32( the carrier of X) is non empty set
Cl (B `) is closed Element of K32( the carrier of (e,tE))
dT is Element of K32( the carrier of X)
dT ` is Element of K32( the carrier of X)
the carrier of X \ dT is set
O is Element of the carrier of X
{O} is non empty trivial finite 1 -element Element of K32( the carrier of X)
(dT `) \/ {O} is Element of K32( the carrier of X)
((dT `) \/ {O}) ` is Element of K32( the carrier of X)
the carrier of X \ ((dT `) \/ {O}) is set
dT \ {O} is Element of K32( the carrier of X)
(dT \ {O}) ` is Element of K32( the carrier of X)
the carrier of X \ (dT \ {O}) is set
((dT \ {O}) `) ` is Element of K32( the carrier of X)
the carrier of X \ ((dT \ {O}) `) is set
e is set
tE is set
(e,tE) is strict TopSpace-like TopStruct
the carrier of (e,tE) is set
K32( the carrier of (e,tE)) is non empty set
K32(K32( the carrier of (e,tE))) is non empty set
K32(e) is non empty set

{tE} is non empty trivial finite 1 -element set
{{tE}} is non empty trivial finite V32() 1 -element set
\ {{tE}} is Element of K32(K32(e))
K32(K32(e)) is non empty set
{ (b1 `) where b1 is Element of K32(e) : b1 is finite } is set
( \ {{tE}}) \/ { (b1 `) where b1 is Element of K32(e) : b1 is finite } is set
the topology of (e,tE) is non empty open Element of K32(K32( the carrier of (e,tE)))
B is set
dT is non empty set
SmallestPartition dT is non empty with_non-empty_elements a_partition of dT
{ {b1} where b1 is Element of dT : verum } is set
TT is Element of dT
{TT} is non empty trivial finite 1 -element Element of K32(dT)
K32(dT) is non empty set
bool the carrier of (e,tE) is non empty Element of K32(K32( the carrier of (e,tE)))
B is set
dT is Element of K32(e)
dT ` is Element of K32(e)
e \ dT is set
dT is Element of K32( the carrier of (e,tE))
dT ` is Element of K32( the carrier of (e,tE))
the carrier of (e,tE) \ dT is set
TT is Element of the carrier of (e,tE)
T is non empty set
{ {b1} where b1 is Element of T : verum } is set
a is Element of T
{a} is non empty trivial finite 1 -element Element of K32(T)
K32(T) is non empty set
{TT} is non empty trivial finite 1 -element set
(dT `) ` is Element of K32( the carrier of (e,tE))
the carrier of (e,tE) \ (dT `) is set
B is Element of K32(K32( the carrier of (e,tE)))
dT is set
TT is Element of K32(e)
TT ` is Element of K32(e)
e \ TT is set
(TT `) ` is Element of K32(e)
e \ (TT `) is set
dT is open quasi_basis Element of K32(K32( the carrier of (e,tE)))
e is non empty non trivial non finite set

e * is set

proj1 E is set
proj2 E is set
X is set

proj2 O is set
E . O is set

O is set
{ {b1} where b1 is Element of e : verum } is set
B is Element of e
{B} is non empty trivial finite 1 -element Element of K32(e)
K32(e) is non empty non trivial non finite set

e is non empty non trivial non finite set
K32(e) is non empty non trivial non finite set
{ (b1 `) where b1 is Element of K32(e) : b1 is finite } is set
card { (b1 `) where b1 is Element of K32(e) : b1 is finite } is epsilon-transitive epsilon-connected ordinal cardinal set

e * is set

proj1 E is set
proj2 E is set
X is set
O is Element of K32(e)
O ` is Element of K32(e)
e \ O is set

proj2 B is set
E . B is set

proj1 X is set
proj2 X is set
O is set
B is set
X . B is set
dT is Element of e
{dT} is non empty trivial finite 1 -element Element of K32(e)
{dT} ` is Element of K32(e)
e \ {dT} is set
O is set
X . O is set
B is set
X . B is set
dT is Element of e
{dT} is non empty trivial finite 1 -element Element of K32(e)
{dT} ` is Element of K32(e)
e \ {dT} is set
TT is Element of e
X . TT is set
{TT} is non empty trivial finite 1 -element Element of K32(e)
{TT} ` is Element of K32(e)
e \ {TT} is set
e is non empty non trivial non finite set
K32(e) is non empty non trivial non finite set

{ (b1 `) where b1 is Element of K32(e) : b1 is finite } is set

tE is set
(e,tE) is non empty strict TopSpace-like TopStruct
the carrier of (e,tE) is non empty set
K32( the carrier of (e,tE)) is non empty set
K32(K32( the carrier of (e,tE))) is non empty set
{tE} is non empty trivial finite 1 -element set
{{tE}} is non empty trivial finite V32() 1 -element set
\ {{tE}} is Element of K32(K32(e))
K32(K32(e)) is non empty non trivial non finite set
( \ {{tE}}) \/ { (b1 `) where b1 is Element of K32(e) : b1 is finite } is set
X is non empty open quasi_basis Element of K32(K32( the carrier of (e,tE)))

(card e) +` 1 is non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal set

card { (b1 `) where b1 is Element of K32(e) : b1 is finite } is epsilon-transitive epsilon-connected ordinal cardinal set
(card e) +` (card e) is non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal set
e is non empty non trivial non finite set

tE is set
(e,tE) is non empty strict TopSpace-like TopStruct
the carrier of (e,tE) is non empty set
K32( the carrier of (e,tE)) is non empty set
K32(K32( the carrier of (e,tE))) is non empty set

{tE} is non empty trivial finite 1 -element set
{{tE}} is non empty trivial finite V32() 1 -element set

O is non empty open quasi_basis Element of K32(K32( the carrier of (e,tE)))

{ {b1} where b1 is Element of e : verum } is set
K32(e) is non empty non trivial non finite set
\ {{tE}} is Element of K32(K32(e))
K32(K32(e)) is non empty non trivial non finite set
B is set
dT is Element of e
{dT} is non empty trivial finite 1 -element Element of K32(e)
dT is Element of the carrier of (e,tE)
{dT} is non empty trivial finite 1 -element Element of K32( the carrier of (e,tE))
TT is Element of K32( the carrier of (e,tE))
(card e) +` 1 is non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal set

e is non empty non trivial non finite set

tE is set
(e,tE) is non empty strict TopSpace-like TopStruct

the carrier of (e,tE) is non empty set
K32( the carrier of (e,tE)) is non empty set
K32(K32( the carrier of (e,tE))) is non empty set
K32(e) is non empty non trivial non finite set

{tE} is non empty trivial finite 1 -element set
{{tE}} is non empty trivial finite V32() 1 -element set
\ {{tE}} is Element of K32(K32(e))
K32(K32(e)) is non empty non trivial non finite set
{ (b1 `) where b1 is Element of K32(e) : b1 is finite } is set
( \ {{tE}}) \/ { (b1 `) where b1 is Element of K32(e) : b1 is finite } is set
X is non empty open quasi_basis Element of K32(K32( the carrier of (e,tE)))

O is non empty open quasi_basis Element of K32(K32( the carrier of (e,tE)))

e is non empty set
K32(e) is non empty set

{ ({b1} `) where b1 is Element of e : verum } is set
tE is set
(e,tE) is non empty strict TopSpace-like TopStruct
the carrier of (e,tE) is non empty set
K32( the carrier of (e,tE)) is non empty set
K32(K32( the carrier of (e,tE))) is non empty set
{tE} is non empty trivial finite 1 -element set
{{tE}} is non empty trivial finite V32() 1 -element set
\ {{tE}} is Element of K32(K32(e))
K32(K32(e)) is non empty set
( \ {{tE}}) \/ { ({b1} `) where b1 is Element of e : verum } is set
{ (b1 `) where b1 is Element of K32(e) : b1 is finite } is set
bool e is non empty Element of K32(K32(e))
TT is set
T is Element of e
{T} is non empty trivial finite 1 -element Element of K32(e)
{T} ` is Element of K32(e)
e \ {T} is set
dT is Element of K32(K32( the carrier of (e,tE)))
dT \ {{tE}} is Element of K32(K32( the carrier of (e,tE)))
TT is Element of K32(K32( the carrier of (e,tE)))
(dT \ {{tE}}) \/ TT is Element of K32(K32( the carrier of (e,tE)))
( \ {{tE}}) \/ { (b1 `) where b1 is Element of K32(e) : b1 is finite } is set
a is non empty open quasi_basis Element of K32(K32( the carrier of (e,tE)))
T is Element of K32(K32( the carrier of (e,tE)))
FinMeetCl T is Element of K32(K32( the carrier of (e,tE)))
o is set
F is Element of K32( the carrier of (e,tE))
F ` is Element of K32( the carrier of (e,tE))
the carrier of (e,tE) \ F is set

bool F is non empty Element of K32(K32(F))
K32(F) is non empty set
K32(K32(F)) is non empty set
SF is Element of K32(K32( the carrier of (e,tE)))
F is non empty Element of K32( the carrier of (e,tE))
SF is non empty Element of K32(K32( the carrier of (e,tE)))
COMPLEMENT SF is non empty Element of K32(K32( the carrier of (e,tE)))
a is set
a is Element of K32( the carrier of (e,tE))
a ` is Element of K32( the carrier of (e,tE))
the carrier of (e,tE) \ a is set
{ {b1} where b1 is Element of F : verum } is set
b is Element of F
{b} is non empty trivial finite 1 -element Element of K32(F)
K32(F) is non empty set
b is Element of e
{b} is non empty trivial finite 1 -element Element of K32(e)
{b} ` is Element of K32(e)
e \ {b} is set
union SF is Element of K32( the carrier of (e,tE))
meet () is Element of K32( the carrier of (e,tE))
Intersect () is Element of K32( the carrier of (e,tE))
o is set
the topology of (e,tE) is non empty open Element of K32(K32( the carrier of (e,tE)))
o is set
F is Element of e
{F} is non empty trivial finite 1 -element Element of K32(e)
{F} ` is Element of K32(e)
e \ {F} is set
FinMeetCl the topology of (e,tE) is Element of K32(K32( the carrier of (e,tE)))

the carrier of e is set
K32( the carrier of e) is non empty set
K32(K32( the carrier of e)) is non empty set
tE is Element of K32(K32( the carrier of e))
K32(tE) is non empty set
K32(K32(tE)) is non empty set
union tE is Element of K32( the carrier of e)
Cl (union tE) is closed Element of K32( the carrier of e)
clf tE is Element of K32(K32( the carrier of e))
union (clf tE) is Element of K32( the carrier of e)
E is non empty Element of K32(K32(tE))
{ (Cl (union b1)) where b1 is Element of K32(K32( the carrier of e)) : b1 in E } is set
meet { (Cl (union b1)) where b1 is Element of K32(K32( the carrier of e)) : b1 in E } is set
(union (clf tE)) \/ (meet { (Cl (union b1)) where b1 is Element of K32(K32( the carrier of e)) : b1 in E } ) is set
the Element of E is Element of E
O is Element of K32(K32( the carrier of e))
union O is Element of K32( the carrier of e)
Cl () is closed Element of K32( the carrier of e)
TT is set
T is Element of the carrier of e
dT is non empty set
meet dT is set
a is set
o is Element of K32(K32( the carrier of e))
union o is Element of K32( the carrier of e)
Cl () is closed Element of K32( the carrier of e)
tE \ o is Element of K32(K32( the carrier of e))
clf (tE \ o) is Element of K32(K32( the carrier of e))
union (clf (tE \ o)) is Element of K32( the carrier of e)
o \/ (tE \ o) is Element of K32(K32( the carrier of e))
union (tE \ o) is Element of K32( the carrier of e)
() \/ (union (tE \ o)) is Element of K32( the carrier of e)
Cl (union (tE \ o)) is closed Element of K32( the carrier of e)
(Cl ()) \/ (Cl (union (tE \ o))) is closed Element of K32( the carrier of e)
TT is set
T is set
a is Element of K32( the carrier of e)
Cl a is closed Element of K32( the carrier of e)
dT is non empty set
meet dT is set
dT is non empty set
meet dT is set

the carrier of e is set
K32( the carrier of e) is non empty set
K32(K32( the carrier of e)) is non empty set
tE is Element of K32(K32( the carrier of e))
union tE is Element of K32( the carrier of e)
Cl (union tE) is closed Element of K32( the carrier of e)
clf tE is Element of K32(K32( the carrier of e))
union (clf tE) is Element of K32( the carrier of e)
{ (Cl (union b1)) where b1 is Element of K32(K32( the carrier of e)) : ( b1 c= tE & tE \ b1 is finite ) } is set
meet { (Cl (union b1)) where b1 is Element of K32(K32( the carrier of e)) : ( b1 c= tE & tE \ b1 is finite ) } is set
(union (clf tE)) \/ (meet { (Cl (union b1)) where b1 is Element of K32(K32( the carrier of e)) : ( b1 c= tE & tE \ b1 is finite ) } ) is set
tE \ tE is Element of K32(K32( the carrier of e))
O is set
B is Element of the carrier of e
X is non empty set
meet X is set
dT is set
TT is Element of K32(K32( the carrier of e))
union TT is Element of K32( the carrier of e)
Cl (union TT) is closed Element of K32( the carrier of e)
tE \ TT is Element of K32(K32( the carrier of e))
clf (tE \ TT) is Element of K32(K32( the carrier of e))
union (clf (tE \ TT)) is Element of K32( the carrier of e)
TT \/ (tE \ TT) is Element of K32(K32( the carrier of e))
union (tE \ TT) is Element of K32( the carrier of e)
(union TT) \/ (union (tE \ TT)) is Element of K32( the carrier of e)
Cl (union (tE \ TT)) is closed Element of K32( the carrier of e)
(Cl (union TT)) \/ (Cl (union (tE \ TT))) is closed Element of K32( the carrier of e)
O is set
B is set
dT is Element of K32( the carrier of e)
Cl dT is closed Element of K32( the carrier of e)
X is non empty set
meet X is set
X is non empty set
meet X is set
e is set
bool e is non empty Element of K32(K32(e))
K32(e) is non empty set
K32(K32(e)) is non empty set
K32((bool e)) is non empty set
K32(K32((bool e))) is non empty set
tE is Element of K32(K32((bool e)))
Intersect tE is Element of K32((bool e))
E is Element of K32(K32(e))
TopStruct(# e,E #) is strict TopStruct
the carrier of TopStruct(# e,E #) is set
bool the carrier of TopStruct(# e,E #) is non empty Element of K32(K32( the carrier of TopStruct(# e,E #)))
K32( the carrier of TopStruct(# e,E #)) is non empty set
K32(K32( the carrier of TopStruct(# e,E #))) is non empty set
O is set
B is Element of K32(K32(e))
TopStruct(# e,B #) is strict TopStruct
the topology of TopStruct(# e,E #) is open Element of K32(K32( the carrier of TopStruct(# e,E #)))
O is Element of K32(K32( the carrier of TopStruct(# e,E #)))
B is set
dT is Element of K32(K32(e))
TopStruct(# e,dT #) is strict TopStruct
union O is Element of K32( the carrier of TopStruct(# e,E #))
O is Element of K32( the carrier of TopStruct(# e,E #))
B is Element of K32( the carrier of TopStruct(# e,E #))
O /\ B is Element of K32( the carrier of TopStruct(# e,E #))
dT is set
TT is Element of K32(K32(e))
TopStruct(# e,TT #) is strict TopStruct
O is Element of K32(K32(e))
TopStruct(# e,O #) is strict TopStruct

the carrier of B is set
dT is set
TT is Element of K32(K32(e))
TopStruct(# e,TT #) is strict TopStruct
the topology of B is non empty open Element of K32(K32( the carrier of B))
K32( the carrier of B) is non empty set
K32(K32( the carrier of B)) is non empty set

K32(K32({})) is non empty set
bool {} is non empty Element of K32(K32({}))

K32(()) is non empty set

{()} is non empty trivial finite V32() 1 -element Element of K32(K32({}))
K32(K32(())) is non empty set
bool () is non empty Element of K32(K32(()))

K32((bool ())) is non empty set
X is set
bool X is non empty Element of K32(K32(X))
K32(X) is non empty set
K32(K32(X)) is non empty set
K32((bool X)) is non empty set
K32(K32((bool X))) is non empty set
O is Element of K32(K32((bool X)))
union O is Element of K32((bool X))
FinMeetCl () is Element of K32(K32(X))
UniCl (FinMeetCl ()) is Element of K32(K32(X))
B is Element of K32(K32(X))
TopStruct(# X,B #) is strict TopStruct
tE is Element of K32(K32({}))
TopStruct(# {},tE #) is strict TopStruct
UniCl tE is Element of K32(K32({}))

FinMeetCl tE is Element of K32(K32({}))
e is Element of K32(K32({}))

FinMeetCl () is Element of K32(K32({}))

the topology of dT is non empty open Element of K32(K32( the carrier of dT))
the carrier of dT is set
K32( the carrier of dT) is non empty set
K32(K32( the carrier of dT)) is non empty set
T is Element of K32(K32(X))
TopStruct(# X,T #) is strict TopStruct
the topology of TopStruct(# X,T #) is open Element of K32(K32( the carrier of TopStruct(# X,T #)))
the carrier of TopStruct(# X,T #) is set
K32( the carrier of TopStruct(# X,T #)) is non empty set
K32(K32( the carrier of TopStruct(# X,T #))) is non empty set

the topology of TT is non empty open Element of K32(K32( the carrier of TT))
the carrier of TT is set
K32( the carrier of TT) is non empty set
K32(K32( the carrier of TT)) is non empty set

the carrier of T is set
the carrier of TopStruct(# X,B #) is set
the topology of TopStruct(# X,B #) is open Element of K32(K32( the carrier of TopStruct(# X,B #)))
K32( the carrier of TopStruct(# X,B #)) is non empty set
K32(K32( the carrier of TopStruct(# X,B #))) is non empty set
the topology of T is non empty open Element of K32(K32( the carrier of T))
K32( the carrier of T) is non empty set
K32(K32( the carrier of T)) is non empty set
a is set
o is Element of K32(K32(X))
TopStruct(# X,o #) is strict TopStruct
FinMeetCl the topology of T is Element of K32(K32( the carrier of T))
UniCl (FinMeetCl the topology of T) is Element of K32(K32( the carrier of T))