:: COMPTS_1 semantic presentation

{} is empty finite V28() set

the empty finite V28() set is empty finite V28() set

1 is non empty set

{{},1} is non empty finite set

K137() is set

bool K137() is non empty set

T is non empty TopSpace-like TopStruct

the carrier of T is non empty set

bool the carrier of T is non empty set

Z is Element of bool the carrier of T

X is Element of the carrier of T

Z ` is Element of bool the carrier of T

the carrier of T \ Z is set

X is Element of the carrier of T

Z is Element of bool the carrier of T

Z ` is Element of bool the carrier of T

the carrier of T \ Z is set

[#] T is non empty non proper open closed Element of bool the carrier of T

F is non empty non proper open closed Element of bool the carrier of T

{} T is empty proper finite V28() open closed Element of bool the carrier of T

FF is empty proper finite V28() open closed Element of bool the carrier of T

X is Element of bool the carrier of T

Z is Element of bool the carrier of T

X is Element of bool the carrier of T

Z is Element of bool the carrier of T

{} T is empty proper finite V28() open closed Element of bool the carrier of T

F is empty proper finite V28() open closed Element of bool the carrier of T

[#] T is non empty non proper open closed Element of bool the carrier of T

FF is non empty non proper open closed Element of bool the carrier of T

[#] T is non empty non proper open closed Element of bool the carrier of T

F is non empty non proper open closed Element of bool the carrier of T

{} T is empty proper finite V28() open closed Element of bool the carrier of T

FF is empty proper finite V28() open closed Element of bool the carrier of T

T is TopStruct

the carrier of T is set

bool the carrier of T is non empty set

T is TopStruct

the carrier of T is set

bool the carrier of T is non empty set

bool (bool the carrier of T) is non empty set

Z is Element of bool the carrier of T

X is Element of bool (bool the carrier of T)

union X is Element of bool the carrier of T

F is Element of bool (bool the carrier of T)

T is TopStruct

[#] T is non proper Element of bool the carrier of T

the carrier of T is set

bool the carrier of T is non empty set

bool (bool the carrier of T) is non empty set

X is Element of bool (bool the carrier of T)

Z is Element of bool (bool the carrier of T)

bool (bool the carrier of T) is non empty set

X is Element of bool (bool the carrier of T)

Z is Element of bool (bool the carrier of T)

T is TopStruct

the carrier of T is set

bool the carrier of T is non empty set

X is SubSpace of T

[#] X is non proper Element of bool the carrier of X

the carrier of X is set

bool the carrier of X is non empty set

Z is Element of bool the carrier of T

[#] T is non proper Element of bool the carrier of T

F is Element of bool the carrier of T

Z /\ F is Element of bool the carrier of T

FF is Element of bool the carrier of X

bool (bool the carrier of X) is non empty set

G is Element of bool (bool the carrier of X)

bool (bool the carrier of T) is non empty set

g is Element of bool (bool the carrier of T)

union G is Element of bool the carrier of X

T | F is strict SubSpace of T

the carrier of (T | F) is set

g | F is Element of bool (bool the carrier of (T | F))

bool the carrier of (T | F) is non empty set

bool (bool the carrier of (T | F)) is non empty set

union (g | F) is Element of bool the carrier of (T | F)

union g is Element of bool the carrier of T

h is Element of bool (bool the carrier of T)

h | F is Element of bool (bool the carrier of (T | F))

[#] (T | F) is non proper Element of bool the carrier of (T | F)

bool ([#] (T | F)) is non empty Element of bool (bool ([#] (T | F)))

bool ([#] (T | F)) is non empty set

bool (bool ([#] (T | F))) is non empty set

h is Element of bool (bool the carrier of X)

union h is Element of bool the carrier of T

union h is Element of bool the carrier of X

FF is Element of bool the carrier of X

bool (bool the carrier of T) is non empty set

G is Element of bool (bool the carrier of T)

G | F is Element of bool (bool the carrier of (T | F))

T | F is strict SubSpace of T

the carrier of (T | F) is set

bool the carrier of (T | F) is non empty set

bool (bool the carrier of (T | F)) is non empty set

g is Relation-like Function-like set

dom g is set

rng g is set

[#] (T | F) is non proper Element of bool the carrier of (T | F)

bool ([#] (T | F)) is non empty Element of bool (bool ([#] (T | F)))

bool ([#] (T | F)) is non empty set

bool (bool ([#] (T | F))) is non empty set

bool (bool the carrier of X) is non empty set

h is Element of bool (bool the carrier of X)

h is Element of bool the carrier of X

P is Element of bool the carrier of (T | F)

P1 is Element of bool the carrier of T

P1 /\ F is Element of bool the carrier of T

the topology of T is Element of bool (bool the carrier of T)

the topology of X is Element of bool (bool the carrier of X)

union G is Element of bool the carrier of T

union h is Element of bool the carrier of X

h is Element of bool (bool the carrier of X)

P is set

g .: P is set

P1 is Element of bool (bool the carrier of T)

union P1 is Element of bool the carrier of T

P2 is set

union h is Element of bool the carrier of X

x is set

x is set

g . x is set

D is Element of bool the carrier of T

D /\ F is Element of bool the carrier of T

T is TopStruct

the carrier of T is set

bool the carrier of T is non empty set

X is Element of bool the carrier of T

T | X is strict SubSpace of T

[#] (T | X) is non proper Element of bool the carrier of (T | X)

the carrier of (T | X) is set

bool the carrier of (T | X) is non empty set

Z is non empty TopSpace-like TopStruct

the carrier of Z is non empty set

bool the carrier of Z is non empty set

F is non empty Element of bool the carrier of Z

Z | F is non empty strict TopSpace-like SubSpace of Z

[#] (Z | F) is non empty non proper open closed Element of bool the carrier of (Z | F)

the carrier of (Z | F) is non empty set

bool the carrier of (Z | F) is non empty set

FF is Element of bool the carrier of (T | X)

T is non empty TopSpace-like TopStruct

the carrier of T is non empty set

bool the carrier of T is non empty set

bool (bool the carrier of T) is non empty set

X is Element of bool (bool the carrier of T)

meet X is Element of bool the carrier of T

COMPLEMENT X is Element of bool (bool the carrier of T)

union (COMPLEMENT X) is Element of bool the carrier of T

(meet X) ` is Element of bool the carrier of T

the carrier of T \ (meet X) is set

[#] T is non empty non proper open closed Element of bool the carrier of T

Z is Element of bool (bool the carrier of T)

F is Element of bool (bool the carrier of T)

COMPLEMENT F is Element of bool (bool the carrier of T)

G is set

c

c

the carrier of T \ c

(c

the carrier of T \ (c

meet (COMPLEMENT F) is Element of bool the carrier of T

union F is Element of bool the carrier of T

(union F) ` is Element of bool the carrier of T

the carrier of T \ (union F) is set

([#] T) \ ([#] T) is Element of bool the carrier of T

X is Element of bool (bool the carrier of T)

COMPLEMENT X is Element of bool (bool the carrier of T)

Z is Element of bool (bool the carrier of T)

meet Z is Element of bool the carrier of T

union X is Element of bool the carrier of T

(union X) ` is Element of bool the carrier of T

the carrier of T \ (union X) is set

[#] T is non empty non proper open closed Element of bool the carrier of T

([#] T) \ ([#] T) is Element of bool the carrier of T

F is set

meet F is set

FF is Element of bool (bool the carrier of T)

COMPLEMENT FF is Element of bool (bool the carrier of T)

G is Element of bool (bool the carrier of T)

c

g is Element of bool the carrier of T

g ` is Element of bool the carrier of T

the carrier of T \ g is set

(g `) ` is Element of bool the carrier of T

the carrier of T \ (g `) is set

union G is Element of bool the carrier of T

meet FF is Element of bool the carrier of T

(meet FF) ` is Element of bool the carrier of T

the carrier of T \ (meet FF) is set

T is non empty TopSpace-like TopStruct

the carrier of T is non empty set

bool the carrier of T is non empty set

bool (bool the carrier of T) is non empty set

X is Element of bool (bool the carrier of T)

meet X is Element of bool the carrier of T

Z is set

meet Z is set

F is Element of bool (bool the carrier of T)

meet F is Element of bool the carrier of T

X is Element of bool (bool the carrier of T)

meet X is Element of bool the carrier of T

Z is Element of bool (bool the carrier of T)

meet Z is Element of bool the carrier of T

T is TopSpace-like TopStruct

the carrier of T is set

bool the carrier of T is non empty set

X is Element of bool the carrier of T

X ` is Element of bool the carrier of T

the carrier of T \ X is set

the Element of X is Element of X

F is Element of the carrier of T

the topology of T is non empty Element of bool (bool the carrier of T)

bool (bool the carrier of T) is non empty set

FF is set

G is Element of the carrier of T

c

g is Element of bool the carrier of T

h is set

h is set

c

FF is Relation-like Function-like set

dom FF is set

G is Relation-like Function-like set

dom G is set

G .: X is set

bool the carrier of T is non empty Element of bool (bool the carrier of T)

c

g is set

G . g is set

FF . g is set

h is Element of bool the carrier of T

h is Element of bool the carrier of T

h /\ h is Element of bool the carrier of T

c

g is Element of bool the carrier of T

h is set

G . h is set

FF . h is set

h is Element of bool the carrier of T

P is Element of bool the carrier of T

h /\ P is Element of bool the carrier of T

union c

g is set

FF . g is set

G . g is set

h is Element of bool the carrier of T

h is Element of bool the carrier of T

h /\ h is Element of bool the carrier of T

g is Element of bool (bool the carrier of T)

rng G is set

h is set

G .: h is set

FF .: h is set

h is set

P is set

FF . P is set

G . P is set

P1 is Element of bool the carrier of T

P2 is Element of bool the carrier of T

P1 /\ P2 is Element of bool the carrier of T

h is Element of bool (bool the carrier of T)

meet h is Element of bool the carrier of T

P is Element of bool the carrier of T

union g is Element of bool the carrier of T

P1 is Element of bool the carrier of T

P2 is Element of bool the carrier of T

x is set

FF . x is set

G . x is set

x is Element of bool the carrier of T

D is Element of bool the carrier of T

x /\ D is Element of bool the carrier of T

P2 is set

x is Element of bool the carrier of T

x is set

FF . x is set

G . x is set

D is Element of bool the carrier of T

z is Element of bool the carrier of T

D /\ z is Element of bool the carrier of T

P2 is set

x is Element of bool the carrier of T

x is set

G . x is set

FF . x is set

D is Element of bool the carrier of T

z is Element of bool the carrier of T

D /\ z is Element of bool the carrier of T

P /\ P1 is Element of bool the carrier of T

(meet h) /\ (union g) is Element of bool the carrier of T

the Element of (meet h) /\ (union g) is Element of (meet h) /\ (union g)

z is set

P is set

G . P is set

FF . P is set

Q is Element of bool the carrier of T

QS is Element of bool the carrier of T

Q /\ QS is Element of bool the carrier of T

T is TopSpace-like TopStruct

the carrier of T is set

bool the carrier of T is non empty set

X is Element of bool the carrier of T

Z is set

X ` is Element of bool the carrier of T

the carrier of T \ X is set

F is Element of the carrier of T

FF is Element of bool the carrier of T

G is Element of bool the carrier of T

c

G ` is Element of bool the carrier of T

the carrier of T \ G is set

(G `) ` is Element of bool the carrier of T

the carrier of T \ (G `) is set

F is Element of bool the carrier of T

T is TopStruct

the carrier of T is set

bool the carrier of T is non empty set

X is Element of bool the carrier of T

bool (bool the carrier of T) is non empty set

X ` is Element of bool the carrier of T

the carrier of T \ X is set

{(X `)} is non empty finite Element of bool (bool the carrier of T)

F is Element of bool (bool the carrier of T)

Z is Element of bool (bool the carrier of T)

F \/ Z is Element of bool (bool the carrier of T)

G is Element of bool the carrier of T

F \/ {(X `)} is non empty Element of bool (bool the carrier of T)

(F \/ {(X `)}) \ {(X `)} is Element of bool (bool the carrier of T)

F \ {(X `)} is Element of bool (bool the carrier of T)

union F is Element of bool the carrier of T

X \/ (X `) is Element of bool the carrier of T

(union F) \/ (X `) is Element of bool the carrier of T

[#] T is non proper Element of bool the carrier of T

union {(X `)} is Element of bool the carrier of T

(union F) \/ (union {(X `)}) is Element of bool the carrier of T

union (F \/ {(X `)}) is Element of bool the carrier of T

c

c

g is Element of bool (bool the carrier of T)

union c

G is Element of bool (bool the carrier of T)

union G is Element of bool the carrier of T

(union c

([#] T) \ (union {(X `)}) is Element of bool the carrier of T

(X `) ` is Element of bool the carrier of T

the carrier of T \ (X `) is set

union g is Element of bool the carrier of T

T is TopSpace-like TopStruct

the carrier of T is set

bool the carrier of T is non empty set

X is Element of bool the carrier of T

Z is Element of bool the carrier of T

T | X is strict TopSpace-like SubSpace of T

the carrier of (T | X) is set

bool the carrier of (T | X) is non empty set

F is Element of bool the carrier of (T | X)

[#] (T | X) is non proper open closed Element of bool the carrier of (T | X)

T is TopStruct

the carrier of T is set

bool the carrier of T is non empty set

X is Element of bool the carrier of T

Z is Element of bool the carrier of T

X \/ Z is Element of bool the carrier of T

bool (bool the carrier of T) is non empty set

F is Element of bool (bool the carrier of T)

union F is Element of bool the carrier of T

FF is Element of bool (bool the carrier of T)

union FF is Element of bool the carrier of T

G is Element of bool (bool the carrier of T)

G \/ FF is Element of bool (bool the carrier of T)

c

union G is Element of bool the carrier of T

(union G) \/ (union FF) is Element of bool the carrier of T

union (G \/ FF) is Element of bool the carrier of T

T is TopSpace-like TopStruct

the carrier of T is set

bool the carrier of T is non empty set

X is Element of bool the carrier of T

Z is Element of bool the carrier of T

X /\ Z is Element of bool the carrier of T

T is non empty TopSpace-like TopStruct

the carrier of T is non empty set

bool the carrier of T is non empty set

X is Element of the carrier of T

Z is Element of bool the carrier of T

Z ` is Element of bool the carrier of T

the carrier of T \ Z is set

T is non empty TopSpace-like TopStruct

the carrier of T is non empty set

bool the carrier of T is non empty set

X is Element of bool the carrier of T

Z is Element of bool the carrier of T

X /\ Z is Element of bool the carrier of T

the topology of T is non empty Element of bool (bool the carrier of T)

bool (bool the carrier of T) is non empty set

F is set

FF is Element of the carrier of T

Z ` is Element of bool the carrier of T

the carrier of T \ Z is set

G is Element of bool the carrier of T

c

g is set

h is set

G /\ c

F is Relation-like Function-like set

dom F is set

FF is Relation-like Function-like set

dom FF is set

F .: X is set

bool the carrier of T is non empty Element of bool (bool the carrier of T)

G is set

c

F . c

FF . c

g is Element of bool the carrier of T

h is Element of bool the carrier of T

g /\ h is Element of bool the carrier of T

G is Element of bool (bool the carrier of T)

union G is Element of bool the carrier of T

c

F . c

FF . c

g is Element of bool the carrier of T

h is Element of bool the carrier of T

g /\ h is Element of bool the carrier of T

c

g is set

F . g is set

FF . g is set

h is Element of bool the carrier of T

h is Element of bool the carrier of T

h /\ h is Element of bool the carrier of T

c

the Element of X is Element of X

union c

h is set

rng F is set

h is set

F .: h is set

FF .: h is set

P is set

P1 is set

FF . P1 is set

F . P1 is set

P2 is Element of bool the carrier of T

x is Element of bool the carrier of T

P2 /\ x is Element of bool the carrier of T

P1 is set

F . P1 is set

P is Element of bool (bool the carrier of T)

P2 is set

x is Element of bool the carrier of T

x is set

FF . x is set

F . x is set

D is Element of bool the carrier of T

z is Element of bool the carrier of T

D /\ z is Element of bool the carrier of T

P2 is Element of bool the carrier of T

meet P is Element of bool the carrier of T

x is Element of bool the carrier of T

x is Element of bool the carrier of T

D is set

FF . D is set

F . D is set

z is Element of bool the carrier of T

P is Element of bool the carrier of T

z /\ P is Element of bool the carrier of T

FF . P1 is set

x is Element of bool the carrier of T

D is Element of bool the carrier of T

x /\ D is Element of bool the carrier of T

P2 /\ x is Element of bool the carrier of T

(union c

the Element of (union c

D is set

z is set

F . z is set

FF . z is set

P is Element of bool the carrier of T

Q is Element of bool the carrier of T

P /\ Q is Element of bool the carrier of T

T is TopStruct

the carrier of T is set

X is non empty TopStruct

the carrier of X is non empty set

[: the carrier of T, the carrier of X:] is set

bool [: the carrier of T, the carrier of X:] is non empty set

[#] X is non empty non proper Element of bool the carrier of X

bool the carrier of X is non empty set

Z is Relation-like the carrier of T -defined the carrier of X -valued Function-like V21( the carrier of T, the carrier of X) Element of bool [: the carrier of T, the carrier of X:]

rng Z is Element of bool the carrier of X

[#] T is non proper Element of bool the carrier of T

bool the carrier of T is non empty set

dom Z is Element of bool the carrier of T

Z .: ([#] T) is Element of bool the carrier of X

Z " (Z .: ([#] T)) is Element of bool the carrier of T

bool (bool the carrier of X) is non empty set

F is Element of bool (bool the carrier of X)

bool (bool the carrier of T) is non empty set

" Z is Relation-like Function-like set

(" Z) .: F is set

G is Element of bool (bool the carrier of T)

union G is Element of bool the carrier of T

union F is Element of bool the carrier of X

Z " (union F) is Element of bool the carrier of T

Z " (rng Z) is Element of bool the carrier of T

Z .: (dom Z) is Element of bool the carrier of X

Z " (Z .: (dom Z)) is Element of bool the carrier of T

.: Z is Relation-like bool the carrier of T -defined bool the carrier of X -valued Function-like V21( bool the carrier of T, bool the carrier of X) Element of bool [:(bool the carrier of T),(bool the carrier of X):]

[:(bool the carrier of T),(bool the carrier of X):] is non empty set

bool [:(bool the carrier of T),(bool the carrier of X):] is non empty set

(.: Z) " F is Element of bool (bool the carrier of T)

(.: Z) .: ((.: Z) " F) is Element of bool (bool the carrier of X)

(.: Z) .: ((" Z) .: F) is Element of bool (bool the carrier of X)

(.: Z) .: G is Element of bool (bool the carrier of X)

c

(.: Z) .: c

g is Element of bool (bool the carrier of X)

union g is Element of bool the carrier of X

union c

Z .: (union c

T is TopStruct

the carrier of T is set

bool the carrier of T is non empty set

X is Element of bool the carrier of T

Z is non empty TopStruct

the carrier of Z is non empty set

[: the carrier of T, the carrier of Z:] is set

bool [: the carrier of T, the carrier of Z:] is non empty set

[#] Z is non empty non proper Element of bool the carrier of Z

bool the carrier of Z is non empty set

F is Relation-like the carrier of T -defined the carrier of Z -valued Function-like V21( the carrier of T, the carrier of Z) Element of bool [: the carrier of T, the carrier of Z:]

rng F is Element of bool the carrier of Z

F .: X is Element of bool the carrier of Z

bool (bool the carrier of Z) is non empty set

FF is Element of bool (bool the carrier of Z)

bool (bool the carrier of T) is non empty set

" F is Relation-like Function-like set

(" F) .: FF is set

union FF is Element of bool the carrier of Z

F " (F .: X) is Element of bool the carrier of T

F " (union FF) is Element of bool the carrier of T

[#] T is non proper Element of bool the carrier of T

dom F is Element of bool the carrier of T

G is Element of bool (bool the carrier of T)

union G is Element of bool the carrier of T

c

.: F is Relation-like bool the carrier of T -defined bool the carrier of Z -valued Function-like V21( bool the carrier of T, bool the carrier of Z) Element of bool [:(bool the carrier of T),(bool the carrier of Z):]

[:(bool the carrier of T),(bool the carrier of Z):] is non empty set

bool [:(bool the carrier of T),(bool the carrier of Z):] is non empty set

(.: F) .: c

g is Element of bool (bool the carrier of Z)

(.: F) " FF is Element of bool (bool the carrier of T)

(.: F) .: ((.: F) " FF) is Element of bool (bool the carrier of Z)

(.: F) .: ((" F) .: FF) is Element of bool (bool the carrier of Z)

(.: F) .: G is Element of bool (bool the carrier of Z)

union c

union g is Element of bool the carrier of Z

F .: (union c

T is TopSpace-like TopStruct

the carrier of T is set

bool the carrier of T is non empty set

X is non empty TopSpace-like TopStruct

the carrier of X is non empty set

[: the carrier of T, the carrier of X:] is set

bool [: the carrier of T, the carrier of X:] is non empty set

[#] X is non empty non proper open closed Element of bool the carrier of X

bool the carrier of X is non empty set

Z is Relation-like the carrier of T -defined the carrier of X -valued Function-like V21( the carrier of T, the carrier of X) Element of bool [: the carrier of T, the carrier of X:]

rng Z is Element of bool the carrier of X

F is Element of bool the carrier of T

Z .: F is Element of bool the carrier of X

T is TopSpace-like TopStruct

the carrier of T is set

[#] T is non proper open closed Element of bool the carrier of T

bool the carrier of T is non empty set

X is non empty TopSpace-like TopStruct

the carrier of X is non empty set

[: the carrier of T, the carrier of X:] is set

bool [: the carrier of T, the carrier of X:] is non empty set

[#] X is non empty non proper open closed Element of bool the carrier of X

bool the carrier of X is non empty set

Z is Relation-like the carrier of T -defined the carrier of X -valued Function-like V21( the carrier of T, the carrier of X) Element of bool [: the carrier of T, the carrier of X:]

dom Z is Element of bool the carrier of T

rng Z is Element of bool the carrier of X

F is Element of bool the carrier of T

Z .: F is Element of bool the carrier of X

Z " (Z .: F) is Element of bool the carrier of T

T is set

bool T is non empty Element of bool (bool T)

bool T is non empty set

bool (bool T) is non empty set

[#] (bool T) is non empty non proper Element of bool (bool T)

bool (bool T) is non empty set

TopStruct(# T,([#] (bool T)) #) is strict TopStruct

T is set

(T) is TopStruct

bool T is non empty Element of bool (bool T)

bool T is non empty set

bool (bool T) is non empty set

[#] (bool T) is non empty non proper Element of bool (bool T)

bool (bool T) is non empty set

TopStruct(# T,([#] (bool T)) #) is strict TopStruct

the carrier of (T) is set

bool the carrier of (T) is non empty set

bool (bool the carrier of (T)) is non empty set

the topology of (T) is Element of bool (bool the carrier of (T))

Z is Element of bool (bool the carrier of (T))

union Z is Element of bool the carrier of (T)

Z is Element of bool the carrier of (T)

F is Element of bool the carrier of (T)

Z /\ F is Element of bool the carrier of (T)

T is non empty set

(T) is strict TopSpace-like TopStruct

bool T is non empty Element of bool (bool T)

bool T is non empty set

bool (bool T) is non empty set

[#] (bool T) is non empty non proper Element of bool (bool T)

bool (bool T) is non empty set

TopStruct(# T,([#] (bool T)) #) is non empty strict TopStruct

T is set

{T} is non empty finite set

({T}) is non empty strict TopSpace-like TopStruct

bool {T} is non empty finite V28() Element of bool (bool {T})

bool {T} is non empty finite V28() set

bool (bool {T}) is non empty finite V28() set

[#] (bool {T}) is non empty non proper finite V28() Element of bool (bool {T})

bool (bool {T}) is non empty finite V28() set

TopStruct(# {T},([#] (bool {T})) #) is non empty strict TopStruct

the carrier of ({T}) is non empty set

X is Element of the carrier of ({T})

Z is Element of the carrier of ({T})

bool the carrier of ({T}) is non empty set

{{}} is non empty finite V28() set

({{}}) is non empty strict TopSpace-like T_0 T_1 T_2 TopStruct

bool {{}} is non empty finite V28() Element of bool (bool {{}})

bool {{}} is non empty finite V28() set

bool (bool {{}}) is non empty finite V28() set

[#] (bool {{}}) is non empty non proper finite V28() Element of bool (bool {{}})

bool (bool {{}}) is non empty finite V28() set

TopStruct(# {{}},([#] (bool {{}})) #) is non empty strict TopStruct

T is non empty TopSpace-like T_0 T_1 T_2 TopStruct

the carrier of T is non empty set

bool the carrier of T is non empty set

X is Element of bool the carrier of T

T is finite set

(T) is strict TopSpace-like TopStruct

bool T is non empty finite V28() Element of bool (bool T)

bool T is non empty finite V28() set

bool (bool T) is non empty finite V28() set

[#] (bool T) is non empty non proper finite V28() Element of bool (bool T)

bool (bool T) is non empty finite V28() set

TopStruct(# T,([#] (bool T)) #) is strict TopStruct

{{}} is non empty finite V28() set

({{}}) is non empty finite strict TopSpace-like T_0 T_1 T_2 TopStruct

bool {{}} is non empty finite V28() Element of bool (bool {{}})

bool {{}} is non empty finite V28() set

bool (bool {{}}) is non empty finite V28() set

[#] (bool {{}}) is non empty non proper finite V28() Element of bool (bool {{}})

bool (bool {{}}) is non empty finite V28() set

TopStruct(# {{}},([#] (bool {{}})) #) is non empty strict TopStruct

T is TopSpace-like TopStruct

the carrier of T is set

bool the carrier of T is non empty set

bool (bool the carrier of T) is non empty set

X is Element of bool (bool the carrier of T)

T is TopSpace-like TopStruct

the carrier of T is set

T is TopSpace-like TopStruct

the carrier of T is set

bool the carrier of T is non empty set

X is Element of bool the carrier of T

Z is finite Element of bool the carrier of T

T | Z is strict TopSpace-like SubSpace of T

[#] (T | Z) is non proper open closed Element of bool the carrier of (T | Z)

the carrier of (T | Z) is set

bool the carrier of (T | Z) is non empty set

T is non empty TopSpace-like TopStruct

the carrier of T is non empty set

bool the carrier of T is non empty set

the non empty finite (T) Element of bool the carrier of T is non empty finite (T) Element of bool the carrier of T

T is TopStruct

the carrier of T is set

X is Element of the carrier of T

Z is Element of the carrier of T

bool the carrier of T is non empty set

T is T_0 T_1 T_2 TopStruct

X is SubSpace of T

the carrier of X is set

Z is Element of the carrier of X

F is Element of the carrier of X

bool the carrier of X is non empty set

[#] X is non proper Element of bool the carrier of X

[#] T is non proper Element of bool the carrier of T

the carrier of T is set

bool the carrier of T is non empty set

FF is Element of the carrier of T

G is Element of the carrier of T

c

g is Element of bool the carrier of T

c

g /\ ([#] X) is Element of bool the carrier of X

the topology of T is Element of bool (bool the carrier of T)

bool (bool the carrier of T) is non empty set

h is Element of bool the carrier of X

the topology of X is Element of bool (bool the carrier of X)

bool (bool the carrier of X) is non empty set

h is Element of bool the carrier of X

c

h /\ h is Element of bool the carrier of X

c

(c

{} /\ ([#] X) is finite Element of bool the carrier of X

T is TopStruct

the carrier of T is set

bool the carrier of T is non empty set

X is SubSpace of T

the carrier of X is set

bool the carrier of X is non empty set

Z is Element of bool the carrier of T

F is Element of bool the carrier of X

[#] X is non proper Element of bool the carrier of X

FF is Element of bool the carrier of X

T is non empty TopSpace-like TopStruct

the carrier of T is non empty set

[#] T is non empty non proper open closed Element of bool the carrier of T

bool the carrier of T is non empty set

X is non empty TopSpace-like TopStruct

the carrier of X is non empty set

[: the carrier of T, the carrier of X:] is non empty set

bool [: the carrier of T, the carrier of X:] is non empty set

Z is Element of the carrier of T

{Z} is non empty finite (T) Element of bool the carrier of T

F is TopSpace-like SubSpace of T

the carrier of F is set

[: the carrier of F, the carrier of X:] is set

bool [: the carrier of F, the carrier of X:] is non empty set

FF is TopSpace-like SubSpace of T

the carrier of FF is set

[: the carrier of FF, the carrier of X:] is set

bool [: the carrier of FF, the carrier of X:] is non empty set

[#] F is non proper open closed Element of bool the carrier of F

bool the carrier of F is non empty set

[#] FF is non proper open closed Element of bool the carrier of FF

bool the carrier of FF is non empty set

([#] F) \/ ([#] FF) is set

([#] F) /\ ([#] FF) is Element of bool the carrier of FF

G is Relation-like the carrier of F -defined the carrier of X -valued Function-like V21( the carrier of F, the carrier of X) Element of bool [: the carrier of F, the carrier of X:]

G . Z is set

c

c

G +* c

dom c

rng (G +* c

rng G is Element of bool the carrier of X

bool the carrier of X is non empty set

rng c

(rng G) \/ (rng c

dom G is Element of bool the carrier of F

dom (G +* c

h is Relation-like the carrier of T -defined the carrier of X -valued Function-like V21( the carrier of T, the carrier of X) Element of bool [: the carrier of T, the carrier of X:]

h is Element of bool the carrier of X

h " h is Element of bool the carrier of T

G " h is Element of bool the carrier of F

c

dom h is Element of bool the carrier of T

(dom G) \/ (dom c

P2 is set

(h " h) /\ ([#] FF) is Element of bool the carrier of FF

h . P2 is set

c

c

h . P2 is set

P2 is set

h . P2 is set

G . P2 is set

P2 is set

(h " h) /\ ([#] F) is Element of bool the carrier of F

h . P2 is set

G . P2 is set

G . P2 is set

h . P2 is set

P is Element of bool the carrier of T

P1 is Element of bool the carrier of T

(h " h) /\ (([#] F) \/ ([#] FF)) is Element of bool the carrier of T

((h " h) /\ ([#] F)) \/ ((h " h) /\ ([#] FF)) is set

(G " h) \/ (c

T is non empty TopSpace-like TopStruct

the carrier of T is non empty set

X is non empty TopSpace-like TopStruct

the carrier of X is non empty set

[#] X is non empty non proper open closed Element of bool the carrier of X

bool the carrier of X is non empty set

[: the carrier of X, the carrier of T:] is non empty set

bool [: the carrier of X, the carrier of T:] is non empty set

Z is TopSpace-like SubSpace of X

the carrier of Z is set

[: the carrier of Z, the carrier of T:] is set

bool [: the carrier of Z, the carrier of T:] is non empty set

F is TopSpace-like SubSpace of X

the carrier of F is set

[: the carrier of F, the carrier of T:] is set

bool [: the carrier of F, the carrier of T:] is non empty set

[#] Z is non proper open closed Element of bool the carrier of Z

bool the carrier of Z is non empty set

[#] F is non proper open closed Element of bool the carrier of F

bool the carrier of F is non empty set

([#] Z) \/ ([#] F) is set

([#] Z) /\ ([#] F) is Element of bool the carrier of F

FF is Element of the carrier of X

G is Element of the carrier of X

{FF,G} is non empty finite (X) Element of bool the carrier of X

c

c

c

g is Relation-like the carrier of F -defined the carrier of T -valued Function-like V21( the carrier of F, the carrier of T) Element of bool [: the carrier of F, the carrier of T:]

g . FF is set

g . G is set

c

dom g is Element of bool the carrier of F

rng (c

rng c

bool the carrier of T is non empty set

rng g is Element of bool the carrier of T

(rng c

dom c

dom (c

h is Relation-like the carrier of X -defined the carrier of T -valued Function-like V21( the carrier of X, the carrier of T) Element of bool [: the carrier of X, the carrier of T:]

P is Element of bool the carrier of T

h " P is Element of bool the carrier of X

c

g " P is Element of bool the carrier of F

dom h is Element of bool the carrier of X

(dom c

x is set

(h " P) /\ ([#] F) is Element of bool the carrier of F

h . x is set

g . x is set

g . x is set

h . x is set

x is set

h . x is set

c

x is set

(h " P) /\ ([#] Z) is Element of bool the carrier of Z

h . x is set

c

c

h . x is set

P1 is Element of bool the carrier of X

P2 is Element of bool the carrier of X

(h " P) /\ (([#] Z) \/ ([#] F)) is Element of bool the carrier of X

((h " P) /\ ([#] Z)) \/ ((h " P) /\ ([#] F)) is set

(c

T is TopStruct

the topology of T is Element of bool (bool the carrier of T)

the carrier of T is set

bool the carrier of T is non empty set

bool (bool the carrier of T) is non empty set

X is Element of bool the carrier of T

T is TopSpace-like TopStruct

the carrier of T is set

bool the carrier of T is non empty set

bool (bool the carrier of T) is non empty set

the topology of T is non empty open Element of bool (bool the carrier of T)

T is non empty TopSpace-like TopStruct

the carrier of T is non empty set

bool the carrier of T is non empty set

bool (bool the carrier of T) is non empty set

the topology of T is non empty open Element of bool (bool the carrier of T)

TopStruct(# the carrier of T, the topology of T #) is non empty strict TopSpace-like TopStruct

the carrier of TopStruct(# the carrier of T, the topology of T #) is non empty set

bool the carrier of TopStruct(# the carrier of T, the topology of T #) is non empty set

bool (bool the carrier of TopStruct(# the carrier of T, the topology of T #)) is non empty set

X is set

Z is Element of bool (bool the carrier of TopStruct(# the carrier of T, the topology of T #))

F is Element of bool the carrier of TopStruct(# the carrier of T, the topology of T #)

Z is Element of bool (bool the carrier of T)

F is Element of bool the carrier of T

T is non empty TopSpace-like TopStruct

the carrier of T is non empty set

bool the carrier of T is non empty set

the topology of T is non empty open Element of bool (bool the carrier of T)

bool (bool the carrier of T) is non empty set

TopStruct(# the carrier of T, the topology of T #) is non empty strict TopSpace-like TopStruct

the carrier of TopStruct(# the carrier of T, the topology of T #) is non empty set

bool the carrier of TopStruct(# the carrier of T, the topology of T #) is non empty set

X is set

Z is Element of bool the carrier of TopStruct(# the carrier of T, the topology of T #)

bool (bool the carrier of TopStruct(# the carrier of T, the topology of T #)) is non empty set

F is Element of bool (bool the carrier of TopStruct(# the carrier of T, the topology of T #))

FF is Element of bool (bool the carrier of T)

G is Element of bool (bool the carrier of TopStruct(# the carrier of T, the topology of T #))

Z is Element of bool the carrier of T

F is Element of bool (bool the carrier of T)

bool (bool the carrier of TopStruct(# the carrier of T, the topology of T #)) is non empty set

FF is Element of bool (bool the carrier of TopStruct(# the carrier of T, the topology of T #))

G is Element of bool (bool the carrier of T)