:: TOPGEN_2 semantic presentation

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

{ b

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,b

E is set

X is Element of the carrier of e

(e,X) is epsilon-transitive epsilon-connected ordinal cardinal set

union { (e,b

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,b

union { (e,b

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,b

union { (e,b

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,b

E is Element of the carrier of e

(e,E) is epsilon-transitive epsilon-connected ordinal cardinal set

union { (e,b

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,b

union { (e,b

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

{ b

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

{ b

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

{ b

( b

O is set

B is Element of K32( the carrier of e)

dT is set

card { b

( b

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

{ {b

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)

{ {b

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 b

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 b

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

{ b

B is set

dT is Element of K32( the carrier of e)

union { b

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

{ b

meet { b

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

{ b

[#] 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)

{ b

meet { b

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

{ b

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 { b

B is Element of the carrier of e

{ b

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 { b

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 b

meet { (card b

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

{ b

{ (b

{ b

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

{ b

{ (b

{ b

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

{ b

{ (b

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

{ b

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

{ (b

((SmallestPartition e) \ {{tE}}) \/ { (b

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

{ {b

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

{ {b

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

{ {b

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

{ (b

card { (b

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

{ (b

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}}) \/ { (b

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 { (b

(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

{ {b

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

{ (b

((SmallestPartition e) \ {{tE}}) \/ { (b

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

{ ({b

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}}) \/ { ({b

{ (b

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}}) \/ { (b

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

{ {b

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 b

meet { (Cl (union b

(union (clf tE)) \/ (meet { (Cl (union b

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 b

meet { (Cl (union b

(union (clf tE)) \/ (meet { (Cl (union b

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