K190() is set
K194() is non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal Element of K32(K190())
K32(K190()) is non empty set
omega is non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal set
K32(omega) is non empty non trivial non finite set
1 is non empty epsilon-transitive epsilon-connected ordinal natural finite cardinal Element of K194()
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
2 is non empty epsilon-transitive epsilon-connected ordinal natural finite cardinal Element of K194()
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
the empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural finite V32() cardinal {} -element set is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural finite V32() cardinal {} -element 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))
card the open tE -quasi_basis Element of K32(K32( the carrier of e)) is epsilon-transitive epsilon-connected ordinal cardinal set
X is epsilon-transitive epsilon-connected ordinal set
O is open tE -quasi_basis Element of K32(K32( the carrier of e))
card O is epsilon-transitive epsilon-connected ordinal cardinal set
O is open tE -quasi_basis Element of K32(K32( the carrier of e))
card O is epsilon-transitive epsilon-connected ordinal cardinal set
B is open tE -quasi_basis Element of K32(K32( the carrier of e))
card B is epsilon-transitive epsilon-connected ordinal cardinal set
E is epsilon-transitive epsilon-connected ordinal cardinal set
X is epsilon-transitive epsilon-connected ordinal cardinal set
O is open tE -quasi_basis Element of K32(K32( the carrier of e))
card O is epsilon-transitive epsilon-connected ordinal cardinal set
B is open tE -quasi_basis Element of K32(K32( the carrier of e))
card B is epsilon-transitive epsilon-connected ordinal cardinal set
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
(e,X) is epsilon-transitive epsilon-connected ordinal cardinal set
union { (e,b1) where b1 is Element of the carrier of e : verum } is set
E is epsilon-transitive epsilon-connected ordinal cardinal set
X is Element of the carrier of e
(e,X) is epsilon-transitive epsilon-connected ordinal cardinal set
X is epsilon-transitive epsilon-connected ordinal cardinal set
O is set
B is Element of the carrier of e
(e,B) is epsilon-transitive epsilon-connected ordinal cardinal 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
union { (e,b1) where b1 is Element of the carrier of e : verum } is set
E is epsilon-transitive epsilon-connected ordinal cardinal set
X is Element of the carrier of e
(e,X) is epsilon-transitive epsilon-connected ordinal cardinal set
O is epsilon-transitive epsilon-connected ordinal cardinal set
tE is epsilon-transitive epsilon-connected ordinal cardinal set
E is epsilon-transitive epsilon-connected ordinal cardinal set
e is non empty TopStruct
(e) is epsilon-transitive epsilon-connected ordinal cardinal set
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
E is epsilon-transitive epsilon-connected ordinal cardinal set
X is epsilon-transitive epsilon-connected ordinal cardinal set
X is Element of the carrier of e
(e,X) is epsilon-transitive epsilon-connected ordinal cardinal set
e is non empty TopStruct
the carrier of e is non empty set
(e) is epsilon-transitive epsilon-connected ordinal cardinal set
{ (e,b1) where b1 is Element of the carrier of e : verum } is set
E is Element of the carrier of e
(e,E) is epsilon-transitive epsilon-connected ordinal cardinal set
union { (e,b1) where b1 is Element of the carrier of e : verum } is set
e is non empty TopSpace-like TopStruct
(e) is epsilon-transitive epsilon-connected ordinal cardinal set
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
(e,X) is epsilon-transitive epsilon-connected ordinal cardinal set
O is non empty open X -quasi_basis Element of K32(K32( the carrier of e))
card O is non empty epsilon-transitive epsilon-connected ordinal cardinal set
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
(e,E) is epsilon-transitive epsilon-connected ordinal cardinal set
X is non empty open E -quasi_basis Element of K32(K32( the carrier of e))
card X is non empty epsilon-transitive epsilon-connected ordinal cardinal 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
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))
e is TopSpace-like 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
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
weight e is epsilon-transitive epsilon-connected ordinal cardinal 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))
card E is non empty epsilon-transitive epsilon-connected ordinal cardinal set
{ 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
O is Relation-like Function-like 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)
card dT is epsilon-transitive epsilon-connected ordinal cardinal set
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
weight e is epsilon-transitive epsilon-connected ordinal cardinal set
tE is open quasi_basis Element of K32(K32( the carrier of e))
card tE is epsilon-transitive epsilon-connected ordinal cardinal set
e is TopStruct
e is set
SmallestPartition e is with_non-empty_elements a_partition of e
card (SmallestPartition e) is epsilon-transitive epsilon-connected ordinal cardinal set
card e is epsilon-transitive epsilon-connected ordinal cardinal 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,(SmallestPartition e)) is set
K32(K33(E,(SmallestPartition e))) is non empty set
X is Relation-like E -defined SmallestPartition e -valued Function-like V37(E, SmallestPartition e) Element of K32(K33(E,(SmallestPartition e)))
rng X is Element of K32((SmallestPartition e))
K32((SmallestPartition e)) 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
weight e is epsilon-transitive epsilon-connected ordinal cardinal set
the carrier of e is non empty set
card the carrier of e is non empty epsilon-transitive epsilon-connected ordinal cardinal 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))
card E is non empty epsilon-transitive epsilon-connected ordinal cardinal set
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))
card X is non empty epsilon-transitive epsilon-connected ordinal cardinal set
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
weight E is epsilon-transitive epsilon-connected ordinal cardinal set
the carrier of E is non empty set
card the carrier of E is non empty epsilon-transitive epsilon-connected ordinal cardinal 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
weight e is epsilon-transitive epsilon-connected ordinal cardinal 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))
card E is non empty epsilon-transitive epsilon-connected ordinal cardinal set
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)
card TT is epsilon-transitive epsilon-connected ordinal cardinal set
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
card a is epsilon-transitive epsilon-connected ordinal cardinal set
X is Relation-like Function-like set
proj1 X is set
proj2 X is set
Union X is set
union (proj2 X) 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
card (X . TT) is epsilon-transitive epsilon-connected ordinal cardinal set
T is set
card (proj2 X) is epsilon-transitive epsilon-connected ordinal cardinal set
dT is set
card dT is epsilon-transitive epsilon-connected ordinal cardinal set
TT is set
X . TT is set
B is non empty open quasi_basis Element of K32(K32( the carrier of e))
card B is non empty epsilon-transitive epsilon-connected ordinal cardinal set
(weight e) *` (weight e) is epsilon-transitive epsilon-connected ordinal cardinal 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
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
weight e is epsilon-transitive epsilon-connected ordinal cardinal set
tE is non empty open quasi_basis Element of K32(K32( the carrier of e))
card tE is non empty epsilon-transitive epsilon-connected ordinal cardinal set
{ 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)
e is TopSpace-like 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
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)
e is TopSpace-like 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
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
weight e is epsilon-transitive epsilon-connected ordinal cardinal set
tE is open quasi_basis Element of K32(K32( the carrier of e))
card tE is epsilon-transitive epsilon-connected ordinal cardinal 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
{ (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))
card O is epsilon-transitive epsilon-connected ordinal cardinal 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
weight e is epsilon-transitive epsilon-connected ordinal cardinal 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
card E is non empty epsilon-transitive epsilon-connected ordinal cardinal 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
weight e is epsilon-transitive epsilon-connected ordinal cardinal 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
E is strict TopStruct
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
X is strict TopStruct
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 empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural finite V32() cardinal {} -element Element of K32(e)
({} 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
SmallestPartition e is with_non-empty_elements a_partition of e
{tE} is non empty trivial finite 1 -element set
{{tE}} is non empty trivial finite V32() 1 -element set
(SmallestPartition e) \ {{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
((SmallestPartition e) \ {{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
Fin e is preBoolean set
card (Fin e) is epsilon-transitive epsilon-connected ordinal cardinal set
card e is non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal set
e * is set
E is Relation-like Function-like set
proj1 E is set
proj2 E is set
X is set
O is Relation-like Function-like FinSequence-like set
proj2 O is set
E . O is set
card (e *) is epsilon-transitive epsilon-connected ordinal cardinal set
SmallestPartition e is non empty with_non-empty_elements a_partition of e
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
card (SmallestPartition e) is non empty epsilon-transitive epsilon-connected ordinal cardinal 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
card e is non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal set
e * is set
E is Relation-like Function-like 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
B is Relation-like Function-like FinSequence-like set
proj2 B is set
E . B is set
card (e *) is epsilon-transitive epsilon-connected ordinal cardinal set
X is Relation-like Function-like 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
SmallestPartition e is non empty with_non-empty_elements a_partition of e
{ (b1 `) where b1 is Element of K32(e) : b1 is finite } is set
card e is non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal 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
(SmallestPartition e) \ {{tE}} is Element of K32(K32(e))
K32(K32(e)) is non empty non trivial non finite set
((SmallestPartition e) \ {{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 X is non empty epsilon-transitive epsilon-connected ordinal cardinal set
card (SmallestPartition e) is non empty epsilon-transitive epsilon-connected ordinal cardinal set
card {{tE}} is non empty epsilon-transitive epsilon-connected ordinal natural finite cardinal Element of omega
(card e) +` 1 is non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal set
card ((SmallestPartition e) \ {{tE}}) is epsilon-transitive epsilon-connected ordinal 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
card e is non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal 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
SmallestPartition e is non empty with_non-empty_elements a_partition of e
{tE} is non empty trivial finite 1 -element set
{{tE}} is non empty trivial finite V32() 1 -element set
card {{tE}} is non empty epsilon-transitive epsilon-connected ordinal natural finite cardinal Element of omega
card (SmallestPartition e) is non empty epsilon-transitive epsilon-connected ordinal cardinal set
O is non empty open quasi_basis Element of K32(K32( the carrier of (e,tE)))
card O is non empty epsilon-transitive epsilon-connected ordinal cardinal set
{ {b1} where b1 is Element of e : verum } is set
K32(e) is non empty non trivial non finite set
(SmallestPartition e) \ {{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
card ((SmallestPartition e) \ {{tE}}) is epsilon-transitive epsilon-connected ordinal cardinal set
e is non empty non trivial non finite set
card e is non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal set
tE is set
(e,tE) is non empty strict TopSpace-like TopStruct
weight (e,tE) is epsilon-transitive epsilon-connected ordinal cardinal set
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
SmallestPartition e is non empty with_non-empty_elements a_partition of e
{tE} is non empty trivial finite 1 -element set
{{tE}} is non empty trivial finite V32() 1 -element set
(SmallestPartition e) \ {{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
((SmallestPartition e) \ {{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 X is non empty epsilon-transitive epsilon-connected ordinal cardinal set
O is non empty open quasi_basis Element of K32(K32( the carrier of (e,tE)))
card O is non empty epsilon-transitive epsilon-connected ordinal cardinal set
e is non empty set
K32(e) is non empty set
SmallestPartition e is non empty with_non-empty_elements a_partition of e
{ ({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
(SmallestPartition e) \ {{tE}} is Element of K32(K32(e))
K32(K32(e)) is non empty set
((SmallestPartition e) \ {{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)))
((SmallestPartition e) \ {{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
SmallestPartition F is with_non-empty_elements a_partition of F
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 (COMPLEMENT SF) is Element of K32( the carrier of (e,tE))
Intersect (COMPLEMENT SF) 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)))
e is TopSpace-like 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 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 (union O) 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 (union o) 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 o) \/ (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 (union o)) \/ (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
e is TopSpace-like 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 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
B is TopSpace-like TopStruct
B is TopSpace-like 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
O is TopSpace-like TopStruct
K32(K32({})) is non empty set
bool {} is non empty Element of K32(K32({}))
{} (bool {}) is empty proper epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural finite V32() cardinal {} -element Element of K32((bool {}))
K32((bool {})) is non empty set
{} {} is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural finite V32() cardinal {} -element Element of K32({})
{({} {})} is non empty trivial finite V32() 1 -element Element of K32(K32({}))
K32(K32((bool {}))) is non empty set
bool (bool {}) is non empty Element of K32(K32((bool {})))
{} (bool (bool {})) is empty proper epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural finite V32() cardinal {} -element Element of K32((bool (bool {})))
K32((bool (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 (union O) is Element of K32(K32(X))
UniCl (FinMeetCl (union O)) 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({}))
{{},{}} is finite set
FinMeetCl tE is Element of K32(K32({}))
e is Element of K32(K32({}))
E is empty proper epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural finite V32() cardinal {} -element Element of K32(K32((bool {})))
union E is empty proper epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural finite V32() cardinal {} -element Element of K32((bool {}))
FinMeetCl (union E) is Element of K32(K32({}))
dT is TopSpace-like discrete V78() TopStruct
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
TT is TopSpace-like TopStruct
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
T is TopSpace-like TopStruct
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))