:: TOPS_2 semantic presentation

K119() is V36() V37() V38() V42() set

K123() is V36() V37() V38() V39() V40() V41() V42() Element of bool K119()

bool K119() is non empty set

{} is empty Relation-like non-empty empty-yielding K123() -defined Function-like one-to-one constant functional V36() V37() V38() V39() V40() V41() V42() finite FinSequence-like FinSubsequence-like FinSequence-membered set

1 is non empty ext-real V27() V34() V35() V36() V37() V38() V39() V40() V41() Element of K123()

{{},1} is non empty set

K118() is V36() V37() V38() V39() V40() V41() V42() set

bool K118() is non empty set

bool K123() is non empty set

2 is non empty ext-real V27() V34() V35() V36() V37() V38() V39() V40() V41() Element of K123()

3 is non empty ext-real V27() V34() V35() V36() V37() V38() V39() V40() V41() Element of K123()

meet {} is set

0 is empty Relation-like non-empty empty-yielding K123() -defined Function-like one-to-one constant functional ext-real V27() V34() V35() V36() V37() V38() V39() V40() V41() V42() finite FinSequence-like FinSubsequence-like FinSequence-membered Element of K123()

Seg 1 is non empty V36() V37() V38() V39() V40() V41() finite V50(1) Element of bool K123()

{1} is non empty V36() V37() V38() V39() V40() V41() set

Seg 2 is non empty V36() V37() V38() V39() V40() V41() finite V50(2) Element of bool K123()

{1,2} is non empty V36() V37() V38() V39() V40() V41() set

union {} is set

X is 1-sorted

the carrier of X is set

bool the carrier of X is non empty set

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

c

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

bool ([#] X) is non empty Element of bool (bool ([#] X))

bool ([#] X) is non empty set

bool (bool ([#] X)) is non empty set

X is 1-sorted

the carrier of X is set

bool the carrier of X is non empty set

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

c

A is set

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

A is set

X is non empty 1-sorted

the carrier of X is non empty set

bool the carrier of X is non empty set

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

c

union c

the Element of union c

A is set

X is 1-sorted

the carrier of X is set

bool the carrier of X is non empty set

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

c

union c

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

union A is Element of bool the carrier of X

(union c

c

union (c

A is set

u is set

X is set

bool X is non empty set

bool (bool X) is non empty set

c

COMPLEMENT c

COMPLEMENT (COMPLEMENT c

X is set

bool X is non empty set

bool (bool X) is non empty set

c

COMPLEMENT c

meet (COMPLEMENT c

union c

(union c

X \ (union c

[#] X is non proper Element of bool X

([#] X) \ (union c

X is set

bool X is non empty set

bool (bool X) is non empty set

c

COMPLEMENT c

union (COMPLEMENT c

meet c

(meet c

X \ (meet c

[#] X is non proper Element of bool X

([#] X) \ (meet c

X \ (meet c

X is 1-sorted

the carrier of X is set

bool the carrier of X is non empty set

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

c

COMPLEMENT c

A is set

A is Element of bool the carrier of X

A ` is Element of bool the carrier of X

the carrier of X \ A is set

u is set

y is Element of bool the carrier of X

y ` is Element of bool the carrier of X

the carrier of X \ y is set

A is Relation-like Function-like set

dom A is set

rng A is set

A is set

u is set

A . u is set

y is Element of bool the carrier of X

y ` is Element of bool the carrier of X

the carrier of X \ y is set

u is Element of bool the carrier of X

u ` is Element of bool the carrier of X

the carrier of X \ u is set

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

the carrier of X \ (u `) is set

A . (u `) is set

A .: (COMPLEMENT c

X is 1-sorted

the carrier of X is set

bool the carrier of X is non empty set

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

c

COMPLEMENT c

COMPLEMENT (COMPLEMENT c

X is TopStruct

the carrier of X is set

bool the carrier of X is non empty set

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

X is TopStruct

the carrier of X is set

bool the carrier of X is non empty set

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

c

COMPLEMENT c

A is Element of bool the carrier of X

A ` is Element of bool the carrier of X

the carrier of X \ A is set

A is Element of bool the carrier of X

A ` is Element of bool the carrier of X

the carrier of X \ A is set

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

the carrier of X \ (A `) is set

X is TopStruct

the carrier of X is set

bool the carrier of X is non empty set

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

c

COMPLEMENT c

COMPLEMENT (COMPLEMENT c

X is TopStruct

the carrier of X is set

bool the carrier of X is non empty set

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

c

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

A is Element of bool the carrier of X

X is TopStruct

the carrier of X is set

bool the carrier of X is non empty set

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

c

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

A is Element of bool the carrier of X

X is TopStruct

the carrier of X is set

bool the carrier of X is non empty set

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

c

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

c

A is Element of bool the carrier of X

X is TopStruct

the carrier of X is set

bool the carrier of X is non empty set

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

c

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

c

A is Element of bool the carrier of X

X is TopStruct

the carrier of X is set

bool the carrier of X is non empty set

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

c

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

c

A is Element of bool the carrier of X

X is TopStruct

the carrier of X is set

bool the carrier of X is non empty set

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

c

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

c

A is Element of bool the carrier of X

X is TopStruct

the carrier of X is set

bool the carrier of X is non empty set

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

c

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

c

A is Element of bool the carrier of X

X is TopStruct

the carrier of X is set

bool the carrier of X is non empty set

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

c

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

c

A is Element of bool the carrier of X

X is TopSpace-like TopStruct

the carrier of X is set

bool the carrier of X is non empty set

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

c

union c

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

A is set

A is Element of bool the carrier of X

X is TopSpace-like TopStruct

the carrier of X is set

bool the carrier of X is non empty set

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

c

meet c

A is Relation-like K123() -defined Function-like finite FinSequence-like FinSubsequence-like set

rng A is set

dom A is V36() V37() V38() V39() V40() V41() Element of bool K123()

A is ext-real V27() V34() V35() set

Seg A is V36() V37() V38() V39() V40() V41() finite V50(A) Element of bool K123()

u is ext-real V27() V34() V35() set

Seg u is V36() V37() V38() V39() V40() V41() finite V50(u) Element of bool K123()

A .: (Seg u) is set

u + 1 is ext-real V27() V34() V35() V36() V37() V38() V39() V40() V41() Element of K123()

Seg (u + 1) is V36() V37() V38() V39() V40() V41() finite V50(u + 1) Element of bool K123()

A .: (Seg (u + 1)) is set

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

meet y is Element of bool the carrier of X

Im (A,(u + 1)) is set

{(u + 1)} is non empty V36() V37() V38() V39() V40() V41() set

A .: {(u + 1)} is set

A + 1 is ext-real V27() V34() V35() V36() V37() V38() V39() V40() V41() Element of K123()

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

meet GY is Element of bool the carrier of X

0 + 1 is ext-real V27() V34() V35() V36() V37() V38() V39() V40() V41() Element of K123()

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

A . (u + 1) is set

{(A . (u + 1))} is non empty set

meet x is Element of bool the carrier of X

(Seg u) \/ {(u + 1)} is non empty V36() V37() V38() V39() V40() V41() set

A .: ((Seg u) \/ {(u + 1)}) is set

(A .: (Seg u)) \/ (A .: {(u + 1)}) is set

(meet GY) /\ (meet x) is Element of bool the carrier of X

Im (A,1) is set

A .: {1} is set

A . 1 is set

{(A . 1)} is non empty set

Seg 0 is empty Relation-like non-empty empty-yielding K123() -defined Function-like one-to-one constant functional V36() V37() V38() V39() V40() V41() V42() finite V50( 0 ) FinSequence-like FinSubsequence-like FinSequence-membered Element of bool K123()

A .: (Seg 0) is empty Relation-like non-empty empty-yielding K123() -defined Function-like one-to-one constant functional V36() V37() V38() V39() V40() V41() V42() finite FinSequence-like FinSubsequence-like FinSequence-membered set

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

meet u is Element of bool the carrier of X

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

A .: (Seg A) is set

A .: {} is empty Relation-like non-empty empty-yielding K123() -defined Function-like one-to-one constant functional V36() V37() V38() V39() V40() V41() V42() finite FinSequence-like FinSubsequence-like FinSequence-membered set

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

0 + 1 is ext-real V27() V34() V35() V36() V37() V38() V39() V40() V41() Element of K123()

X is TopSpace-like TopStruct

the carrier of X is set

bool the carrier of X is non empty set

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

c

union c

COMPLEMENT c

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

meet A is Element of bool the carrier of X

meet (COMPLEMENT c

(union c

the carrier of X \ (union c

X is TopSpace-like TopStruct

the carrier of X is set

bool the carrier of X is non empty set

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

c

meet c

COMPLEMENT c

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

union A is Element of bool the carrier of X

union (COMPLEMENT c

(meet c

the carrier of X \ (meet c

{} X is empty Relation-like non-empty empty-yielding K123() -defined Function-like one-to-one constant functional V36() V37() V38() V39() V40() V41() V42() finite FinSequence-like FinSubsequence-like FinSequence-membered closed Element of bool the carrier of X

X is TopStruct

the carrier of X is set

bool the carrier of X is non empty set

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

c

the carrier of c

bool the carrier of c

bool (bool the carrier of c

A is Element of bool (bool the carrier of c

[#] c

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

bool the carrier of c

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

X is TopStruct

the carrier of X is set

bool the carrier of X is non empty set

c

the carrier of c

bool the carrier of c

[#] c

A is Element of bool the carrier of c

the topology of c

bool (bool the carrier of c

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

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

A is Element of bool the carrier of X

A /\ ([#] c

u is Element of bool the carrier of X

y is Element of bool the carrier of X

y /\ ([#] c

A is Element of bool the carrier of X

A /\ ([#] c

X is TopStruct

the carrier of X is set

bool the carrier of X is non empty set

c

A is SubSpace of X

the carrier of A is set

bool the carrier of A is non empty set

A is Element of bool the carrier of A

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

c

X is TopStruct

the carrier of X is set

bool the carrier of X is non empty set

c

A is SubSpace of X

the carrier of A is set

bool the carrier of A is non empty set

A is Element of bool the carrier of A

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

c

X is TopStruct

the carrier of X is set

bool the carrier of X is non empty set

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

c

A is SubSpace of X

the carrier of A is set

bool the carrier of A is non empty set

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

A is Element of bool (bool the carrier of A)

u is Element of bool the carrier of A

y is Element of bool the carrier of X

X is TopStruct

the carrier of X is set

bool the carrier of X is non empty set

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

c

A is SubSpace of X

the carrier of A is set

bool the carrier of A is non empty set

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

A is Element of bool (bool the carrier of A)

u is Element of bool the carrier of A

y is Element of bool the carrier of X

X is TopStruct

the carrier of X is set

bool the carrier of X is non empty set

c

A is Element of bool the carrier of X

c

X | A is strict SubSpace of X

the carrier of (X | A) is set

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

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

X is TopStruct

the carrier of X is set

bool the carrier of X is non empty set

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

c

X | c

the carrier of (X | c

bool the carrier of (X | c

bool (bool the carrier of (X | c

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

A is Element of bool (bool the carrier of (X | c

A is Element of bool (bool the carrier of (X | c

u is Element of bool (bool the carrier of (X | c

y is set

x is Element of bool the carrier of (X | c

GY is Element of bool the carrier of X

GY /\ c

x is Element of bool the carrier of (X | c

GY is Element of bool the carrier of X

GY /\ c

X is TopStruct

the carrier of X is set

bool the carrier of X is non empty set

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

c

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

(X,c

X | c

the carrier of (X | c

bool the carrier of (X | c

bool (bool the carrier of (X | c

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

(X,c

u is set

y is Element of bool the carrier of (X | c

x is Element of bool the carrier of X

x /\ c

X is TopStruct

the carrier of X is set

bool the carrier of X is non empty set

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

c

A is Element of bool the carrier of X

c

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

(X,A,A) is Element of bool (bool the carrier of (X | A))

X | A is strict SubSpace of X

the carrier of (X | A) is set

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

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

u is Element of bool the carrier of (X | A)

X is TopStruct

the carrier of X is set

bool the carrier of X is non empty set

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

c

A is Element of bool the carrier of X

c

X | A is strict SubSpace of X

the carrier of (X | A) is set

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

union A is Element of bool the carrier of X

(X,A,A) is Element of bool (bool the carrier of (X | A))

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

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

union (X,A,A) is Element of bool the carrier of (X | A)

u is set

y is set

x is Element of bool the carrier of X

x /\ A is Element of bool the carrier of X

GY is Element of bool the carrier of (X | A)

X is TopStruct

the carrier of X is set

bool the carrier of X is non empty set

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

c

X | c

the carrier of (X | c

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

union A is Element of bool the carrier of X

(X,c

bool the carrier of (X | c

bool (bool the carrier of (X | c

union (X,c

A is set

u is set

u /\ c

[#] (X | c

y is Element of bool the carrier of X

y /\ c

x is Element of bool the carrier of (X | c

u is set

y is Element of bool the carrier of (X | c

x is Element of bool the carrier of X

x /\ c

X is TopStruct

the carrier of X is set

bool the carrier of X is non empty set

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

c

X | c

the carrier of (X | c

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

(X,c

bool the carrier of (X | c

bool (bool the carrier of (X | c

union (X,c

union A is Element of bool the carrier of X

A is set

u is set

y is Element of bool the carrier of (X | c

x is Element of bool the carrier of X

x /\ c

X is TopStruct

the carrier of X is set

bool the carrier of X is non empty set

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

c

X | c

the carrier of (X | c

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

(X,c

bool the carrier of (X | c

bool (bool the carrier of (X | c

union (X,c

union A is Element of bool the carrier of X

X is TopStruct

the carrier of X is set

bool the carrier of X is non empty set

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

c

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

(X,c

X | c

the carrier of (X | c

bool the carrier of (X | c

bool (bool the carrier of (X | c

A is set

u is Element of bool the carrier of X

u /\ c

y is set

x is Element of bool the carrier of X

x /\ c

A is Relation-like Function-like set

dom A is set

rng A is set

u is set

y is set

A . y is set

x is Element of bool the carrier of X

x /\ c

[#] (X | c

GY is Element of bool the carrier of (X | c

y is Element of bool the carrier of (X | c

x is Element of bool the carrier of X

x /\ c

A . x is set

A .: A is set

X is TopStruct

the carrier of X is set

bool the carrier of X is non empty set

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

c

X | c

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

(X,c

the carrier of (X | c

bool the carrier of (X | c

bool (bool the carrier of (X | c

A is Element of bool the carrier of (X | c

u is Element of bool the carrier of X

u /\ c

y is Element of bool the carrier of X

[#] (X | c

y /\ ([#] (X | c

X is TopStruct

the carrier of X is set

bool the carrier of X is non empty set

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

c

X | c

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

(X,c

the carrier of (X | c

bool the carrier of (X | c

bool (bool the carrier of (X | c

A is Element of bool the carrier of (X | c

u is Element of bool the carrier of X

u /\ c

y is Element of bool the carrier of X

[#] (X | c

y /\ ([#] (X | c

X is TopStruct

the carrier of X is set

bool the carrier of X is non empty set

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

c

the carrier of c

bool the carrier of c

bool (bool the carrier of c

[#] c

A is Element of bool (bool the carrier of c

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

A is Element of bool the carrier of X

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

y is Element of bool the carrier of X

y /\ A is Element of bool the carrier of X

x is Element of bool the carrier of X

y is Element of bool the carrier of X

(X,y,u) is Element of bool (bool the carrier of (X | y))

X | y is strict SubSpace of X

the carrier of (X | y) is set

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

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

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

bool y is non empty set

bool (bool y) is non empty set

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

bool ([#] (X | y)) is non empty Element of bool (bool ([#] (X | y)))

bool ([#] (X | y)) is non empty set

bool (bool ([#] (X | y))) is non empty set

x is Element of bool (bool the carrier of (X | y))

GY is Element of bool the carrier of (X | y)

f is Element of bool the carrier of c

Q2 is Element of bool the carrier of X

Q2 /\ ([#] c

Q2 /\ y is Element of bool the carrier of X

f is Element of bool the carrier of X

f /\ y is Element of bool the carrier of X

f /\ A is Element of bool the carrier of X

Q2 is Element of bool the carrier of X

X is TopStruct

the carrier of X is set

bool the carrier of X is non empty set

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

c

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

(X,c

X | c

the carrier of (X | c

bool the carrier of (X | c

bool (bool the carrier of (X | c

A is set

u is Element of bool the carrier of X

u /\ c

y is set

x is Element of bool the carrier of X

x /\ c

A is Relation-like Function-like set

dom A is set

rng A is set

u is set

y is set

A . y is set

x is Element of bool the carrier of X

x /\ c

[#] (X | c

GY is Element of bool the carrier of (X | c

y is Element of bool the carrier of (X | c

x is Element of bool the carrier of X

x /\ c

GY is set

A . GY is set

u is set

y is Element of bool the carrier of X

A . u is set

y /\ c

X is 1-sorted

the carrier of X is set

c

the carrier of c

[: the carrier of X, the carrier of c

bool [: the carrier of X, the carrier of c

[#] c

bool the carrier of c

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

bool the carrier of X is non empty set

A is Relation-like the carrier of X -defined the carrier of c

A " ([#] c

rng A is Element of bool the carrier of c

A " (rng A) is Element of bool the carrier of X

dom A is Element of bool the carrier of X

X is 1-sorted

the carrier of X is set

bool the carrier of X is non empty set

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

c

the carrier of c

[: the carrier of X, the carrier of c

bool [: the carrier of X, the carrier of c

bool the carrier of c

bool (bool the carrier of c

A is Relation-like the carrier of X -defined the carrier of c

" A is Relation-like Function-like set

A is Element of bool (bool the carrier of c

(" A) .: A is set

rng (" A) is set

dom A is Element of bool the carrier of X

bool (dom A) is non empty Element of bool (bool (dom A))

bool (dom A) is non empty set

bool (bool (dom A)) is non empty set

X is TopStruct

the carrier of X is set

c

the carrier of c

[: the carrier of X, the carrier of c

bool [: the carrier of X, the carrier of c

[#] c

bool the carrier of c

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

bool the carrier of X is non empty set

A is Relation-like the carrier of X -defined the carrier of c

A is Element of bool the carrier of c

A ` is Element of bool the carrier of c

the carrier of c

A " (A `) is Element of bool the carrier of X

A " ([#] c

A " A is Element of bool the carrier of X

(A " ([#] c

([#] X) \ (A " A) is Element of bool the carrier of X

(A " A) ` is Element of bool the carrier of X

the carrier of X \ (A " A) is set

A is Element of bool the carrier of c

A " A is Element of bool the carrier of X

A ` is Element of bool the carrier of c

the carrier of c

A " (A `) is Element of bool the carrier of X

(A " ([#] c

([#] X) \ (A " A) is Element of bool the carrier of X

(A " A) ` is Element of bool the carrier of X

the carrier of X \ (A " A) is set

X is TopSpace-like TopStruct

the carrier of X is set

c

the carrier of c

[: the carrier of X, the carrier of c

bool [: the carrier of X, the carrier of c

bool the carrier of c

A is Relation-like the carrier of X -defined the carrier of c

A is Element of bool the carrier of c

Cl A is Element of bool the carrier of c

Cl (Cl A) is Element of bool the carrier of c

A " (Cl A) is Element of bool the carrier of X

bool the carrier of X is non empty set

A " A is Element of bool the carrier of X

Cl (A " A) is Element of bool the carrier of X

Cl (A " (Cl A)) is Element of bool the carrier of X

A is Element of bool the carrier of c

A " A is Element of bool the carrier of X

Cl A is Element of bool the carrier of c

Cl (A " A) is Element of bool the carrier of X

X is TopSpace-like TopStruct

the carrier of X is set

bool the carrier of X is non empty set

c

the carrier of c

[: the carrier of X, the carrier of c

bool [: the carrier of X, the carrier of c

A is Relation-like the carrier of X -defined the carrier of c

A is Element of bool the carrier of X

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

dom A is Element of bool the carrier of X

Cl A is Element of bool the carrier of X

A .: A is Element of bool the carrier of c

bool the carrier of c

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

Cl (A " (A .: A)) is Element of bool the carrier of X

Cl (A .: A) is Element of bool the carrier of c

A " (Cl (A .: A)) is Element of bool the carrier of X

A .: (Cl A) is Element of bool the carrier of c

A .: (A " (Cl (A .: A))) is Element of bool the carrier of c

A is Element of bool the carrier of c

A " A is Element of bool the carrier of X

Cl (A " A) is Element of bool the carrier of X

A .: (Cl (A " A)) is Element of bool the carrier of c

A " (A .: (Cl (A " A))) is Element of bool the carrier of X

A .: (A " A) is Element of bool the carrier of c

Cl (A .: (A " A)) is Element of bool the carrier of c

Cl A is Element of bool the carrier of c

A " (Cl A) is Element of bool the carrier of X

X is TopStruct

the carrier of X is set

c

the carrier of c

A is non empty TopStruct

the carrier of A is non empty set

[: the carrier of X, the carrier of A:] is Relation-like set

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

[: the carrier of A, the carrier of c

bool [: the carrier of A, the carrier of c

A is Relation-like the carrier of X -defined the carrier of A -valued Function-like V17( the carrier of X) quasi_total Element of bool [: the carrier of X, the carrier of A:]

u is Relation-like the carrier of A -defined the carrier of c

u * A is Relation-like the carrier of X -defined the carrier of c

[: the carrier of X, the carrier of c

bool [: the carrier of X, the carrier of c

bool the carrier of c

y is Element of bool the carrier of c

(u * A) " y is Element of bool the carrier of X

bool the carrier of X is non empty set

u " y is Element of bool the carrier of A

bool the carrier of A is non empty set

A " (u " y) is Element of bool the carrier of X

X is TopStruct

the carrier of X is set

bool the carrier of X is non empty set

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

c

the carrier of c

[: the carrier of X, the carrier of c

bool [: the carrier of X, the carrier of c

bool the carrier of c

bool (bool the carrier of c

A is Relation-like the carrier of X -defined the carrier of c

" A is Relation-like Function-like set

A is Element of bool (bool the carrier of c

(" A) .: A is set

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

y is Element of bool the carrier of X

dom (" A) is set

x is set

(" A) . x is set

GY is Element of bool the carrier of c

A " GY is Element of bool the carrier of X

[#] c

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

X is TopStruct

the carrier of X is set

c

the carrier of c

[: the carrier of X, the carrier of c

bool [: the carrier of X, the carrier of c

bool the carrier of c

bool (bool the carrier of c

bool the carrier of X is non empty set

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

A is Relation-like the carrier of X -defined the carrier of c

" A is Relation-like Function-like set

A is Element of bool (bool the carrier of c

(" A) .: A is set

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

y is Element of bool the carrier of X

dom (" A) is set

x is set

(" A) . x is set

GY is Element of bool the carrier of c

A " GY is Element of bool the carrier of X

X is set

c

[:X,c

bool [:X,c

A is Relation-like X -defined c

A " is Relation-like Function-like set

[:c

bool [:c

rng A is Element of bool c

bool c

[#] c

X is set

c

[:X,c

bool [:X,c

X is 1-sorted

the carrier of X is set

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

bool the carrier of X is non empty set

c

the carrier of c

[: the carrier of X, the carrier of c

bool [: the carrier of X, the carrier of c

[#] c

bool the carrier of c

A is Relation-like the carrier of X -defined the carrier of c

rng A is Element of bool the carrier of c

( the carrier of X, the carrier of c

[: the carrier of c

bool [: the carrier of c

dom ( the carrier of X, the carrier of c

rng ( the carrier of X, the carrier of c

A " is Relation-like Function-like set

dom (A ") is set

rng (A ") is set

dom A is Element of bool the carrier of X

X is 1-sorted

the carrier of X is set

c

the carrier of c

[: the carrier of X, the carrier of c

bool [: the carrier of X, the carrier of c

[#] c

bool the carrier of c

A is Relation-like the carrier of X -defined the carrier of c

rng A is Element of bool the carrier of c

( the carrier of X, the carrier of c

[: the carrier of c

bool [: the carrier of c

A " is Relation-like Function-like set

X is 1-sorted

the carrier of X is set

c

the carrier of c

[: the carrier of X, the carrier of c

bool [: the carrier of X, the carrier of c

[#] c

bool the carrier of c

A is Relation-like the carrier of X -defined the carrier of c

rng A is Element of bool the carrier of c

( the carrier of X, the carrier of c

[: the carrier of c

bool [: the carrier of c

( the carrier of c

A " is Relation-like Function-like set

(A ") " is Relation-like Function-like set

( the carrier of X, the carrier of c

rng ( the carrier of X, the carrier of c

bool the carrier of X is non empty set

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

X is 1-sorted

the carrier of X is set

c

the carrier of c

[: the carrier of X, the carrier of c

bool [: the carrier of X, the carrier of c

[#] c

bool the carrier of c

A is Relation-like the carrier of X -defined the carrier of c

rng A is Element of bool the carrier of c

( the carrier of X, the carrier of c

[: the carrier of c

bool [: the carrier of c

( the carrier of X, the carrier of c

[: the carrier of X, the carrier of X:] is Relation-like set

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

dom A is Element of bool the carrier of X

bool the carrier of X is non empty set

id (dom A) is Relation-like dom A -defined dom A -valued Function-like one-to-one V17( dom A) quasi_total Element of bool [:(dom A),(dom A):]

[:(dom A),(dom A):] is Relation-like set

bool [:(dom A),(dom A):] is non empty set

A * ( the carrier of X, the carrier of c

[: the carrier of c

bool [: the carrier of c

id (rng A) is Relation-like rng A -defined rng A -valued Function-like one-to-one V17( rng A) quasi_total Element of bool [:(rng A),(rng A):]

[:(rng A),(rng A):] is Relation-like set

bool [:(rng A),(rng A):] is non empty set

A " is Relation-like Function-like set

A (#) (A ") is Relation-like the carrier of X -defined Function-like set

(A ") (#) A is Relation-like the carrier of c

X is 1-sorted

the carrier of X is set

c

the carrier of c

[: the carrier of X, the carrier of c

bool [: the carrier of X, the carrier of c

A is non empty 1-sorted

the carrier of A is non empty set

[: the carrier of c

bool [: the carrier of c

[#] c

bool the carrier of c

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

bool the carrier of A is non empty set

A is Relation-like the carrier of X -defined the carrier of c

rng A is Element of bool the carrier of c

( the carrier of X, the carrier of c

[: the carrier of c

bool [: the carrier of c

u is non empty Relation-like the carrier of c

dom u is non empty Element of bool the carrier of c

rng u is non empty Element of bool the carrier of A

u * A is Relation-like the carrier of X -defined the carrier of A -valued Function-like V17( the carrier of X) quasi_total Element of bool [: the carrier of X, the carrier of A:]

[: the carrier of X, the carrier of A:] is Relation-like set

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

( the carrier of X, the carrier of A,(u * A)) is Relation-like the carrier of A -defined the carrier of X -valued Function-like quasi_total Element of bool [: the carrier of A, the carrier of X:]

[: the carrier of A, the carrier of X:] is Relation-like set

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

( the carrier of c

[: the carrier of A, the carrier of c

bool [: the carrier of A, the carrier of c

( the carrier of X, the carrier of c

rng (u * A) is Element of bool the carrier of A

(u * A) " is Relation-like Function-like set

A " is Relation-like Function-like set

u " is Relation-like Function-like set

X is 1-sorted

the carrier of X is set

c

the carrier of c

[: the carrier of X, the carrier of c

bool [: the carrier of X, the carrier of c

bool the carrier of X is non empty set

[#] c

bool the carrier of c

A is Relation-like the carrier of X -defined the carrier of c

rng A is Element of bool the carrier of c

( the carrier of X, the carrier of c

[: the carrier of c

bool [: the carrier of c

A is Element of bool the carrier of X

A .: A is Element of bool the carrier of c

( the carrier of X, the carrier of c

A " is Relation-like Function-like set

(A ") " A is set

X is 1-sorted

the carrier of X is set

c

the carrier of c

[: the carrier of X, the carrier of c

bool [: the carrier of X, the carrier of c

bool the carrier of c

[#] c

A is Relation-like the carrier of X -defined the carrier of c

rng A is Element of bool the carrier of c

( the carrier of X, the carrier of c

[: the carrier of c

bool [: the carrier of c

A is Element of bool the carrier of c

A " A is Element of bool the carrier of X

bool the carrier of X is non empty set

( the carrier of X, the carrier of c

A " is Relation-like Function-like set

(A ") .: A is set

X is TopStruct

the carrier of X is set

c

the carrier of c

[: the carrier of X, the carrier of c

bool [: the carrier of X, the carrier of c

X is TopStruct

the carrier of X is set

c

the carrier of c

[: the carrier of X, the carrier of c

bool [: the carrier of X, the carrier of c

A is Relation-like the carrier of X -defined the carrier of c

( the carrier of X, the carrier of c

[: the carrier of c

bool [: the carrier of c

rng A is Element of bool the carrier of c

bool the carrier of c

[#] c

dom ( the carrier of X, the carrier of c

rng ( the carrier of X, the carrier of c

bool the carrier of X is non empty set

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

( the carrier of c

X is non empty TopStruct

the carrier of X is non empty set

c

the carrier of c

[: the carrier of X, the carrier of c

bool [: the carrier of X, the carrier of c

A is non empty TopStruct

the carrier of A is non empty set

[: the carrier of c

bool [: the carrier of c

A is non empty Relation-like the carrier of X -defined the carrier of c

u is non empty Relation-like the carrier of c

u * A is non empty Relation-like the carrier of X -defined the carrier of A -valued Function-like V17( the carrier of X) quasi_total Element of bool [: the carrier of X, the carrier of A:]

[: the carrier of X, the carrier of A:] is non empty Relation-like set

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

rng A is non empty Element of bool the carrier of c

bool the carrier of c

[#] c

dom u is non empty Element of bool the carrier of c

rng u is non empty Element of bool the carrier of A

bool the carrier of A is non empty set

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

dom A is non empty Element of bool the carrier of X

bool the carrier of X is non empty set

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

dom (u * A) is non empty Element of bool the carrier of X

rng (u * A) is non empty Element of bool the carrier of A

( the carrier of X, the carrier of A,(u * A)) is non empty Relation-like the carrier of A -defined the carrier of X -valued Function-like V17( the carrier of A) quasi_total Element of bool [: the carrier of A, the carrier of X:]

[: the carrier of A, the carrier of X:] is non empty Relation-like set

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

( the carrier of X, the carrier of c

[: the carrier of c

bool [: the carrier of c

( the carrier of c

[: the carrier of A, the carrier of c

bool [: the carrier of A, the carrier of c

( the carrier of X, the carrier of c

X is TopStruct

the carrier of X is set

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

bool the carrier of X is non empty set

c

the carrier of c

[: the carrier of X, the carrier of c

bool [: the carrier of X, the carrier of c

[#] c

bool the carrier of c

A is Relation-like the carrier of X -defined the carrier of c

dom A is Element of bool the carrier of X

rng A is Element of bool the carrier of c

( the carrier of X, the carrier of c

[: the carrier of c

bool [: the carrier of c

A is Element of bool the carrier of X

( the carrier of X, the carrier of c

A " is Relation-like Function-like set

(A ") " A is set

A .: A is Element of bool the carrier of c

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

A is Element of bool the carrier of c

A " A is Element of bool the carrier of X

A .: (A " A) is Element of bool the carrier of c

A is Element of bool the carrier of X

( the carrier of X, the carrier of c

(A ") " A is set

A .: A is Element of bool the carrier of c

X is non empty TopSpace-like TopStruct

the carrier of X is non empty set

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

bool the carrier of X is non empty set

c

the carrier of c

[: the carrier of X, the carrier of c

bool [: the carrier of X, the carrier of c

[#] c

bool the carrier of c

A is Relation-like the carrier of X -defined the carrier of c

dom A is Element of bool the carrier of X

rng A is Element of bool the carrier of c

A is Element of bool the carrier of c

A " A is Element of bool the carrier of X

Cl (A " A) is Element of bool the carrier of X

Cl A is Element of bool the carrier of c

A " (Cl A) is Element of bool the carrier of X

( the carrier of X, the carrier of c

[: the carrier of c

bool [: the carrier of c

( the carrier of X, the carrier of c

( the carrier of X, the carrier of c

Cl (( the carrier of X, the carrier of c

A is Element of bool the carrier of c

A " A is Element of bool the carrier of X

Cl (A " A) is Element of bool the carrier of X

Cl A is Element of bool the carrier of c

A " (Cl A) is Element of bool the carrier of X

A is Element of bool the carrier of c

Cl A is Element of bool the carrier of c

( the carrier of X, the carrier of c

A " (Cl A) is Element of bool the carrier of X

( the carrier of X, the carrier of c

A " A is Element of bool the carrier of X

Cl (( the carrier of X, the carrier of c

X is TopSpace-like TopStruct

the carrier of X is set

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

bool the carrier of X is non empty set

c

the carrier of c

[: the carrier of X, the carrier of c

bool [: the carrier of X, the carrier of c

[#] c

bool the carrier of c

A is Relation-like the carrier of X -defined the carrier of c

dom A is Element of bool the carrier of X

rng A is Element of bool the carrier of c

A is Element of bool the carrier of X

Cl A is Element of bool the carrier of X

A .: (Cl A) is Element of bool the carrier of c

A .: A is Element of bool the carrier of c

Cl (A .: A) is Element of bool the carrier of c

( the carrier of X, the carrier of c

[: the carrier of c

bool [: the carrier of c

( the carrier of X, the carrier of c

Cl (( the carrier of X, the carrier of c

( the carrier of X, the carrier of c

A is Element of bool the carrier of X

Cl A is Element of bool the carrier of X

A .: (Cl A) is Element of bool the carrier of c

A .: A is Element of bool the carrier of c

Cl (A .: A) is Element of bool the carrier of c

A is Element of bool the carrier of X

( the carrier of X, the carrier of c

A .: A is Element of bool the carrier of c

Cl A is Element of bool the carrier of X

( the carrier of X, the carrier of c

A .: (Cl A) is Element of bool the carrier of c

Cl (( the carrier of X, the carrier of c

X is non empty TopSpace-like TopStruct

the carrier of X is non empty set

c

the carrier of c

[: the carrier of X, the carrier of c

bool [: the carrier of X, the carrier of c

bool the carrier of X is non empty set

A is non empty Relation-like the carrier of X -defined the carrier of c

A is Element of bool the carrier of X

A .: A is Element of bool the carrier of c

bool the carrier of c

{} c

u is Element of bool the carrier of c

y is Element of bool the carrier of c

u \/ y is Element of bool the carrier of c

A " u is Element of bool the carrier of X

A " y is Element of bool the carrier of X

x is Element of bool the carrier of X

x /\ A is Element of bool the carrier of X

GY is Element of bool the carrier of X

GY /\ A is Element of bool the carrier of X

the Element of u is Element of u

dom A is non empty Element of bool the carrier of X

x is set

A . x is set

Cl y is Element of bool the carrier of c

A " (Cl y) is Element of bool the carrier of X

(A " u) /\ (A " (Cl y)) is Element of bool the carrier of X

u /\ (Cl y) is Element of bool the carrier of c

A " (u /\ (Cl y)) is Element of bool the carrier of X

A " ({} c

Cl GY is Element of bool the carrier of X

x /\ (Cl GY) is Element of bool the carrier of X

Cl u is Element of bool the carrier of c

A " (Cl u) is Element of bool the carrier of X

(A " (Cl u)) /\ (A " y) is Element of bool the carrier of X

(Cl u) /\ y is Element of bool the carrier of c

A " ((Cl u) /\ y) is Element of bool the carrier of X

Cl x is Element of bool the carrier of X

(Cl x) /\ GY is Element of bool the carrier of X

{} X is empty proper Relation-like non-empty empty-yielding K123() -defined Function-like one-to-one constant functional V36() V37() V38() V39() V40() V41() V42() finite FinSequence-like FinSubsequence-like FinSequence-membered closed Element of bool the carrier of X

the Element of y is Element of y

x1 is set

A . x1 is set

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

(A " u) \/ (A " y) is Element of bool the carrier of X

x \/ GY is Element of bool the carrier of X

(x \/ GY) /\ A is Element of bool the carrier of X

(x /\ A) \/ (GY /\ A) is Element of bool the carrier of X

c

c

c

X is non empty TopSpace-like TopStruct

the carrier of X is non empty set

c

the carrier of c

[: the carrier of X, the carrier of c

bool [: the carrier of X, the carrier of c

bool the carrier of c

A is non empty Relation-like the carrier of X -defined the carrier of c

A is Element of bool the carrier of c

A " A is Element of bool the carrier of X

bool the carrier of X is non empty set

( the carrier of X, the carrier of c

[: the carrier of c

bool [: the carrier of c

( the carrier of X, the carrier of c

rng A is non empty Element of bool the carrier of c

[#] c

X is non empty TopSpace-like TopStruct

the carrier of X is non empty set

bool the carrier of X is non empty set

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

{} X is empty proper Relation-like non-empty empty-yielding K123() -defined Function-like one-to-one constant functional V36() V37() V38() V39() V40() V41() V42() finite FinSequence-like FinSubsequence-like FinSequence-membered closed Element of bool the carrier of X

c

A is Element of bool the carrier of X

c

the Element of A is Element of A

the Element of c

x is Element of the carrier of X

y is Element of the carrier of X

GY is non empty TopSpace-like TopStruct

the carrier of GY is non empty set

[: the carrier of GY, the carrier of X:] is non empty Relation-like set

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

f is non empty Relation-like the carrier of GY -defined the carrier of X -valued Function-like V17( the carrier of GY) quasi_total Element of bool [: the carrier of GY, the carrier of X:]

rng f is non empty Element of bool the carrier of X

f is non empty Relation-like the carrier of GY -defined the carrier of X -valued Function-like V17( the carrier of GY) quasi_total Element of bool [: the carrier of GY, the carrier of X:]

rng f is non empty Element of bool the carrier of X

f " ([#] X) is Element of bool the carrier of GY

bool the carrier of GY is non empty set

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

f " c

f " A is Element of bool the carrier of GY

(f " c

(rng f) /\ A is Element of bool the carrier of X

{} GY is empty proper Relation-like non-empty empty-yielding K123() -defined Function-like one-to-one constant functional V36() V37() V38() V39() V40() V41() V42() finite FinSequence-like FinSubsequence-like FinSequence-membered closed Element of bool the carrier of GY

(rng f) /\ c

(f " c

c

f " (c

Q2 is set

X is TopStruct

the carrier of X is set

bool the carrier of X is non empty set

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

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

c

A is set

A is Element of bool the carrier of X

A is Element of bool the carrier of X

X is TopStruct

the carrier of X is set

bool the carrier of X is non empty set

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

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

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

c

A is set

A is Element of bool the carrier of X

A ` is Element of bool the carrier of X

the carrier of X \ A is set

A is Element of bool the carrier of X

A ` is Element of bool the carrier of X

the carrier of X \ A is set

X is TopStruct

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

the carrier of X is set

bool the carrier of X is non empty set

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