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

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

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

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
c2 is Element of bool (bool the carrier of X)
[#] 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
c2 is Element of bool (bool the carrier of X)
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
c2 is Element of bool (bool the carrier of X)
union c2 is Element of bool the carrier of X
the Element of union c2 is Element of union c2
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
c2 is Element of bool (bool the carrier of X)
union c2 is Element of bool the carrier of X
A is Element of bool (bool the carrier of X)
union A is Element of bool the carrier of X
(union c2) \ () is Element of bool the carrier of X
c2 \ A is Element of bool (bool the carrier of X)
union (c2 \ A) is Element of bool the carrier of X
A is set
u is set
X is set
bool X is non empty set
bool (bool X) is non empty set
c2 is Element of bool (bool X)
COMPLEMENT c2 is Element of bool (bool X)
COMPLEMENT () is Element of bool (bool X)
X is set
bool X is non empty set
bool (bool X) is non empty set
c2 is Element of bool (bool X)
COMPLEMENT c2 is Element of bool (bool X)
meet () is Element of bool X
union c2 is Element of bool X
(union c2) ` is Element of bool X
X \ (union c2) is set
[#] X is non proper Element of bool X
([#] X) \ (union c2) is Element of bool X
X is set
bool X is non empty set
bool (bool X) is non empty set
c2 is Element of bool (bool X)
COMPLEMENT c2 is Element of bool (bool X)
union () is Element of bool X
meet c2 is Element of bool X
(meet c2) ` is Element of bool X
X \ (meet c2) is set
[#] X is non proper Element of bool X
([#] X) \ (meet c2) is Element of bool X
X \ (meet c2) is Element of bool 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
c2 is Element of bool (bool the carrier of X)
COMPLEMENT c2 is Element of bool (bool 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
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

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 .: () 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
c2 is Element of bool (bool the carrier of X)
COMPLEMENT c2 is Element of bool (bool the carrier of X)
COMPLEMENT () is 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
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
c2 is Element of bool (bool the carrier of X)
COMPLEMENT c2 is Element of bool (bool the carrier of X)
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
c2 is Element of bool (bool the carrier of X)
COMPLEMENT c2 is Element of bool (bool the carrier of X)
COMPLEMENT () is 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
bool (bool the carrier of X) is non empty set
c2 is Element of bool (bool the carrier of X)
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
c2 is Element of bool (bool the carrier of X)
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
c2 is Element of bool (bool the carrier of X)
A is Element of bool (bool the carrier of X)
c2 \/ 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
c2 is Element of bool (bool the carrier of X)
A is Element of bool (bool the carrier of X)
c2 /\ 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
c2 is Element of bool (bool the carrier of X)
A is Element of bool (bool the carrier of X)
c2 \ 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
c2 is Element of bool (bool the carrier of X)
A is Element of bool (bool the carrier of X)
c2 \/ 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
c2 is Element of bool (bool the carrier of X)
A is Element of bool (bool the carrier of X)
c2 /\ 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
c2 is Element of bool (bool the carrier of X)
A is Element of bool (bool the carrier of X)
c2 \ A is Element of bool (bool the carrier of X)
A is Element of 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
c2 is Element of bool (bool the carrier of X)
union c2 is Element of bool the carrier of X
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

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
c2 is Element of bool (bool the carrier of X)
meet c2 is Element of bool the carrier of X

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

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

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

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
c2 is Element of bool (bool the carrier of X)
union c2 is Element of bool the carrier of X
COMPLEMENT c2 is Element of bool (bool the carrier of X)
A is Element of bool (bool the carrier of X)
meet A is Element of bool the carrier of X
meet () is Element of bool the carrier of X
(union c2) ` is Element of bool the carrier of X
the carrier of X \ (union c2) is set

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
c2 is Element of bool (bool the carrier of X)
meet c2 is Element of bool the carrier of X
COMPLEMENT c2 is Element of bool (bool the carrier of X)
A is Element of bool (bool the carrier of X)
union A is Element of bool the carrier of X
union () is Element of bool the carrier of X
(meet c2) ` is Element of bool the carrier of X
the carrier of X \ (meet c2) 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
c2 is SubSpace of X
the carrier of c2 is set
bool the carrier of c2 is non empty set
bool (bool the carrier of c2) is non empty set
A is Element of bool (bool the carrier of c2)
[#] c2 is non proper Element of bool the carrier of c2
[#] X is non proper Element of bool the carrier of X
bool the carrier of c2 is non empty Element of bool (bool the carrier of c2)
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
c2 is SubSpace of X
the carrier of c2 is set
bool the carrier of c2 is non empty set
[#] c2 is non proper Element of bool the carrier of c2
A is Element of bool the carrier of c2
the topology of c2 is Element of bool (bool the carrier of c2)
bool (bool the carrier of c2) is non empty set
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 /\ ([#] c2) is Element of bool the carrier of c2
u is Element of bool the carrier of X
y is Element of bool the carrier of X
y /\ ([#] c2) is Element of bool the carrier of c2
A is Element of bool the carrier of X
A /\ ([#] c2) is Element of bool the carrier of c2
X is TopStruct
the carrier of X is set
bool the carrier of X is non empty set
c2 is Element of bool the carrier of X
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
c2 /\ ([#] A) is Element of bool the carrier of A
X is TopStruct
the carrier of X is set
bool the carrier of X is non empty set
c2 is Element of bool the carrier of X
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
c2 /\ ([#] A) is Element of bool the carrier of 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
c2 is Element of bool (bool the carrier of X)
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
c2 is Element of bool (bool the carrier of X)
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
c2 is Element of bool the carrier of X
A is Element of bool the carrier of X
c2 /\ A is Element of bool the carrier of X
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
c2 is Element of bool the carrier of X
X | c2 is strict SubSpace of X
the carrier of (X | c2) is set
bool the carrier of (X | c2) is non empty set
bool (bool the carrier of (X | c2)) is non empty set
A is Element of bool (bool the carrier of X)
A is Element of bool (bool the carrier of (X | c2))
A is Element of bool (bool the carrier of (X | c2))
u is Element of bool (bool the carrier of (X | c2))
y is set
x is Element of bool the carrier of (X | c2)
GY is Element of bool the carrier of X
GY /\ c2 is Element of bool the carrier of X
x is Element of bool the carrier of (X | c2)
GY is Element of bool the carrier of X
GY /\ c2 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
c2 is Element of bool the carrier of X
A is Element of bool (bool the carrier of X)
(X,c2,A) is Element of bool (bool the carrier of (X | c2))
X | c2 is strict SubSpace of X
the carrier of (X | c2) is set
bool the carrier of (X | c2) is non empty set
bool (bool the carrier of (X | c2)) is non empty set
A is Element of bool (bool the carrier of X)
(X,c2,A) is Element of bool (bool the carrier of (X | c2))
u is set
y is Element of bool the carrier of (X | c2)
x is Element of bool the carrier of X
x /\ c2 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
c2 is Element of bool the carrier of X
A is Element of bool the carrier of X
c2 /\ A is Element of bool the carrier of X
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
c2 is Element of bool the carrier of X
A is Element of bool the carrier of X
c2 /\ A is Element of bool the carrier of X
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
c2 is Element of bool the carrier of X
X | c2 is strict SubSpace of X
the carrier of (X | c2) is set
A is Element of bool (bool the carrier of X)
union A is Element of bool the carrier of X
(X,c2,A) is Element of bool (bool the carrier of (X | c2))
bool the carrier of (X | c2) is non empty set
bool (bool the carrier of (X | c2)) is non empty set
union (X,c2,A) is Element of bool the carrier of (X | c2)
A is set
u is set
u /\ c2 is Element of bool the carrier of X
[#] (X | c2) is non proper Element of bool the carrier of (X | c2)
y is Element of bool the carrier of X
y /\ c2 is Element of bool the carrier of X
x is Element of bool the carrier of (X | c2)
u is set
y is Element of bool the carrier of (X | c2)
x is Element of bool the carrier of X
x /\ c2 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
c2 is Element of bool the carrier of X
X | c2 is strict SubSpace of X
the carrier of (X | c2) is set
A is Element of bool (bool the carrier of X)
(X,c2,A) is Element of bool (bool the carrier of (X | c2))
bool the carrier of (X | c2) is non empty set
bool (bool the carrier of (X | c2)) is non empty set
union (X,c2,A) is Element of bool the carrier of (X | c2)
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 | c2)
x is Element of bool the carrier of X
x /\ c2 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
c2 is Element of bool the carrier of X
X | c2 is strict SubSpace of X
the carrier of (X | c2) is set
A is Element of bool (bool the carrier of X)
(X,c2,A) is Element of bool (bool the carrier of (X | c2))
bool the carrier of (X | c2) is non empty set
bool (bool the carrier of (X | c2)) is non empty set
union (X,c2,A) is Element of bool the carrier of (X | c2)
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
c2 is Element of bool the carrier of X
A is Element of bool (bool the carrier of X)
(X,c2,A) is Element of bool (bool the carrier of (X | c2))
X | c2 is strict SubSpace of X
the carrier of (X | c2) is set
bool the carrier of (X | c2) is non empty set
bool (bool the carrier of (X | c2)) is non empty set
A is set
u is Element of bool the carrier of X
u /\ c2 is Element of bool the carrier of X
y is set
x is Element of bool the carrier of X
x /\ c2 is Element of bool the carrier of X

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 /\ c2 is Element of bool the carrier of X
[#] (X | c2) is non proper Element of bool the carrier of (X | c2)
GY is Element of bool the carrier of (X | c2)
y is Element of bool the carrier of (X | c2)
x is Element of bool the carrier of X
x /\ c2 is Element of bool the carrier of X
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
c2 is Element of bool the carrier of X
X | c2 is strict SubSpace of X
A is Element of bool (bool the carrier of X)
(X,c2,A) is Element of bool (bool the carrier of (X | c2))
the carrier of (X | c2) is set
bool the carrier of (X | c2) is non empty set
bool (bool the carrier of (X | c2)) is non empty set
A is Element of bool the carrier of (X | c2)
u is Element of bool the carrier of X
u /\ c2 is Element of bool the carrier of X
y is Element of bool the carrier of X
[#] (X | c2) is non proper Element of bool the carrier of (X | c2)
y /\ ([#] (X | c2)) is Element of bool the carrier of (X | c2)
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
c2 is Element of bool the carrier of X
X | c2 is strict SubSpace of X
A is Element of bool (bool the carrier of X)
(X,c2,A) is Element of bool (bool the carrier of (X | c2))
the carrier of (X | c2) is set
bool the carrier of (X | c2) is non empty set
bool (bool the carrier of (X | c2)) is non empty set
A is Element of bool the carrier of (X | c2)
u is Element of bool the carrier of X
u /\ c2 is Element of bool the carrier of X
y is Element of bool the carrier of X
[#] (X | c2) is non proper Element of bool the carrier of (X | c2)
y /\ ([#] (X | c2)) is Element of bool the carrier of (X | c2)
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
c2 is SubSpace of X
the carrier of c2 is set
bool the carrier of c2 is non empty set
bool (bool the carrier of c2) is non empty set
[#] c2 is non proper Element of bool the carrier of c2
A is Element of bool (bool the carrier of c2)
[#] 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 c2
Q2 is Element of bool the carrier of X
Q2 /\ ([#] c2) is Element of bool the carrier of c2
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
c2 is Element of bool the carrier of X
A is Element of bool (bool the carrier of X)
(X,c2,A) is Element of bool (bool the carrier of (X | c2))
X | c2 is strict SubSpace of X
the carrier of (X | c2) is set
bool the carrier of (X | c2) is non empty set
bool (bool the carrier of (X | c2)) is non empty set
A is set
u is Element of bool the carrier of X
u /\ c2 is Element of bool the carrier of X
y is set
x is Element of bool the carrier of X
x /\ c2 is Element of bool the carrier of X

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 /\ c2 is Element of bool the carrier of X
[#] (X | c2) is non proper Element of bool the carrier of (X | c2)
GY is Element of bool the carrier of (X | c2)
y is Element of bool the carrier of (X | c2)
x is Element of bool the carrier of X
x /\ c2 is Element of bool the carrier of X
GY is set
A . GY is set
u is set
y is Element of bool the carrier of X
A . u is set
y /\ c2 is Element of bool the carrier of X
X is 1-sorted
the carrier of X is set
c2 is 1-sorted
the carrier of c2 is set
[: the carrier of X, the carrier of c2:] is Relation-like set
bool [: the carrier of X, the carrier of c2:] is non empty set
[#] c2 is non proper Element of bool the carrier of c2
bool the carrier of c2 is non empty set
[#] 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 c2 -valued Function-like quasi_total Element of bool [: the carrier of X, the carrier of c2:]
A " ([#] c2) is Element of bool the carrier of X
rng A is Element of bool the carrier of c2
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
c2 is non empty 1-sorted
the carrier of c2 is non empty set
[: the carrier of X, the carrier of c2:] is Relation-like set
bool [: the carrier of X, the carrier of c2:] is non empty set
bool the carrier of c2 is non empty set
bool (bool the carrier of c2) is non empty set
A is Relation-like the carrier of X -defined the carrier of c2 -valued Function-like V17( the carrier of X) quasi_total Element of bool [: the carrier of X, the carrier of c2:]

A is Element of bool (bool the carrier of c2)
(" 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
c2 is TopStruct
the carrier of c2 is set
[: the carrier of X, the carrier of c2:] is Relation-like set
bool [: the carrier of X, the carrier of c2:] is non empty set
[#] c2 is non proper Element of bool the carrier of c2
bool the carrier of c2 is non empty set
[#] 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 c2 -valued Function-like quasi_total Element of bool [: the carrier of X, the carrier of c2:]
A is Element of bool the carrier of c2
A ` is Element of bool the carrier of c2
the carrier of c2 \ A is set
A " (A `) is Element of bool the carrier of X
A " ([#] c2) is Element of bool the carrier of X
A " A is Element of bool the carrier of X
(A " ([#] c2)) \ (A " A) is Element of bool the carrier of X
([#] 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 c2
A " A is Element of bool the carrier of X
A ` is Element of bool the carrier of c2
the carrier of c2 \ A is set
A " (A `) is Element of bool the carrier of X
(A " ([#] c2)) \ (A " A) is Element of bool the carrier of X
([#] 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

the carrier of X is set

the carrier of c2 is set
[: the carrier of X, the carrier of c2:] is Relation-like set
bool [: the carrier of X, the carrier of c2:] is non empty set
bool the carrier of c2 is non empty set
A is Relation-like the carrier of X -defined the carrier of c2 -valued Function-like quasi_total Element of bool [: the carrier of X, the carrier of c2:]
A is Element of bool the carrier of c2
Cl A is Element of bool the carrier of c2
Cl (Cl A) is Element of bool the carrier of c2
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 c2
A " A is Element of bool the carrier of X
Cl A is Element of bool the carrier of c2
Cl (A " A) is Element of bool the carrier of X

the carrier of X is set
bool the carrier of X is non empty set
c2 is non empty TopSpace-like TopStruct
the carrier of c2 is non empty set
[: the carrier of X, the carrier of c2:] is Relation-like set
bool [: the carrier of X, the carrier of c2:] is non empty set
A is Relation-like the carrier of X -defined the carrier of c2 -valued Function-like V17( the carrier of X) quasi_total Element of bool [: the carrier of X, the carrier of c2:]
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 c2
bool the carrier of c2 is non empty set
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 c2
A " (Cl (A .: A)) is Element of bool the carrier of X
A .: (Cl A) is Element of bool the carrier of c2
A .: (A " (Cl (A .: A))) is Element of bool the carrier of c2
A is Element of bool the carrier of c2
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 c2
A " (A .: (Cl (A " A))) is Element of bool the carrier of X
A .: (A " A) is Element of bool the carrier of c2
Cl (A .: (A " A)) is Element of bool the carrier of c2
Cl A is Element of bool the carrier of c2
A " (Cl A) is Element of bool the carrier of X
X is TopStruct
the carrier of X is set
c2 is TopStruct
the carrier of c2 is set
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 c2:] is Relation-like set
bool [: the carrier of A, the carrier of c2:] is non empty set
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 c2 -valued Function-like quasi_total Element of bool [: the carrier of A, the carrier of c2:]
u * A is Relation-like the carrier of X -defined the carrier of c2 -valued Function-like quasi_total Element of bool [: the carrier of X, the carrier of c2:]
[: the carrier of X, the carrier of c2:] is Relation-like set
bool [: the carrier of X, the carrier of c2:] is non empty set
bool the carrier of c2 is non empty set
y is Element of bool the carrier of c2
(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
c2 is non empty TopStruct
the carrier of c2 is non empty set
[: the carrier of X, the carrier of c2:] is Relation-like set
bool [: the carrier of X, the carrier of c2:] is non empty set
bool the carrier of c2 is non empty set
bool (bool the carrier of c2) is non empty set
A is Relation-like the carrier of X -defined the carrier of c2 -valued Function-like V17( the carrier of X) quasi_total Element of bool [: the carrier of X, the carrier of c2:]

A is Element of bool (bool the carrier of c2)
(" 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 c2
A " GY is Element of bool the carrier of X
[#] c2 is non empty non proper Element of bool the carrier of c2
[#] X is non proper Element of bool the carrier of X
X is TopStruct
the carrier of X is set
c2 is TopStruct
the carrier of c2 is set
[: the carrier of X, the carrier of c2:] is Relation-like set
bool [: the carrier of X, the carrier of c2:] is non empty set
bool the carrier of c2 is non empty set
bool (bool the carrier of c2) is non empty set
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 c2 -valued Function-like quasi_total Element of bool [: the carrier of X, the carrier of c2:]

A is Element of bool (bool the carrier of c2)
(" 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 c2
A " GY is Element of bool the carrier of X
X is set
c2 is set
[:X,c2:] is Relation-like set
bool [:X,c2:] is non empty set

[:c2,X:] is Relation-like set
bool [:c2,X:] is non empty set
rng A is Element of bool c2
bool c2 is non empty set
[#] c2 is non proper Element of bool c2
X is set
c2 is set
[:X,c2:] is Relation-like set
bool [:X,c2:] is non empty set
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
c2 is non empty 1-sorted
the carrier of c2 is non empty set
[: the carrier of X, the carrier of c2:] is Relation-like set
bool [: the carrier of X, the carrier of c2:] is non empty set
[#] c2 is non empty non proper Element of bool the carrier of c2
bool the carrier of c2 is non empty set
A is Relation-like the carrier of X -defined the carrier of c2 -valued Function-like V17( the carrier of X) quasi_total Element of bool [: the carrier of X, the carrier of c2:]
rng A is Element of bool the carrier of c2
( the carrier of X, the carrier of c2,A) is Relation-like the carrier of c2 -defined the carrier of X -valued Function-like quasi_total Element of bool [: the carrier of c2, the carrier of X:]
[: the carrier of c2, the carrier of X:] is Relation-like set
bool [: the carrier of c2, the carrier of X:] is non empty set
dom ( the carrier of X, the carrier of c2,A) is Element of bool the carrier of c2
rng ( the carrier of X, the carrier of c2,A) is Element of bool the carrier of X

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
c2 is 1-sorted
the carrier of c2 is set
[: the carrier of X, the carrier of c2:] is Relation-like set
bool [: the carrier of X, the carrier of c2:] is non empty set
[#] c2 is non proper Element of bool the carrier of c2
bool the carrier of c2 is non empty set
A is Relation-like the carrier of X -defined the carrier of c2 -valued Function-like quasi_total Element of bool [: the carrier of X, the carrier of c2:]
rng A is Element of bool the carrier of c2
( the carrier of X, the carrier of c2,A) is Relation-like the carrier of c2 -defined the carrier of X -valued Function-like quasi_total Element of bool [: the carrier of c2, the carrier of X:]
[: the carrier of c2, the carrier of X:] is Relation-like set
bool [: the carrier of c2, the carrier of X:] is non empty set

X is 1-sorted
the carrier of X is set
c2 is non empty 1-sorted
the carrier of c2 is non empty set
[: the carrier of X, the carrier of c2:] is Relation-like set
bool [: the carrier of X, the carrier of c2:] is non empty set
[#] c2 is non empty non proper Element of bool the carrier of c2
bool the carrier of c2 is non empty set
A is Relation-like the carrier of X -defined the carrier of c2 -valued Function-like V17( the carrier of X) quasi_total Element of bool [: the carrier of X, the carrier of c2:]
rng A is Element of bool the carrier of c2
( the carrier of X, the carrier of c2,A) is Relation-like the carrier of c2 -defined the carrier of X -valued Function-like quasi_total Element of bool [: the carrier of c2, the carrier of X:]
[: the carrier of c2, the carrier of X:] is Relation-like set
bool [: the carrier of c2, the carrier of X:] is non empty set
( the carrier of c2, the carrier of X,( the carrier of X, the carrier of c2,A)) is Relation-like the carrier of X -defined the carrier of c2 -valued Function-like V17( the carrier of X) quasi_total Element of bool [: the carrier of X, the carrier of c2:]

( the carrier of X, the carrier of c2,A) " is Relation-like Function-like set
rng ( the carrier of X, the carrier of c2,A) is Element of bool the carrier of X
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
c2 is 1-sorted
the carrier of c2 is set
[: the carrier of X, the carrier of c2:] is Relation-like set
bool [: the carrier of X, the carrier of c2:] is non empty set
[#] c2 is non proper Element of bool the carrier of c2
bool the carrier of c2 is non empty set
A is Relation-like the carrier of X -defined the carrier of c2 -valued Function-like quasi_total Element of bool [: the carrier of X, the carrier of c2:]
rng A is Element of bool the carrier of c2
( the carrier of X, the carrier of c2,A) is Relation-like the carrier of c2 -defined the carrier of X -valued Function-like quasi_total Element of bool [: the carrier of c2, the carrier of X:]
[: the carrier of c2, the carrier of X:] is Relation-like set
bool [: the carrier of c2, the carrier of X:] is non empty set
( the carrier of X, the carrier of c2,A) * A is Relation-like the carrier of X -defined the carrier of X -valued Function-like Element of bool [: the carrier of X, the carrier of X:]
[: 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

[:(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 c2,A) is Relation-like the carrier of c2 -defined the carrier of c2 -valued Function-like Element of bool [: the carrier of c2, the carrier of c2:]
[: the carrier of c2, the carrier of c2:] is Relation-like set
bool [: the carrier of c2, the carrier of c2:] is non empty set

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

A (#) (A ") is Relation-like the carrier of X -defined Function-like set
(A ") (#) A is Relation-like the carrier of c2 -valued Function-like set
X is 1-sorted
the carrier of X is set
c2 is non empty 1-sorted
the carrier of c2 is non empty set
[: the carrier of X, the carrier of c2:] is Relation-like set
bool [: the carrier of X, the carrier of c2:] is non empty set
A is non empty 1-sorted
the carrier of A is non empty set
[: the carrier of c2, the carrier of A:] is non empty Relation-like set
bool [: the carrier of c2, the carrier of A:] is non empty set
[#] c2 is non empty non proper Element of bool the carrier of c2
bool the carrier of c2 is non empty set
[#] 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 c2 -valued Function-like V17( the carrier of X) quasi_total Element of bool [: the carrier of X, the carrier of c2:]
rng A is Element of bool the carrier of c2
( the carrier of X, the carrier of c2,A) is Relation-like the carrier of c2 -defined the carrier of X -valued Function-like quasi_total Element of bool [: the carrier of c2, the carrier of X:]
[: the carrier of c2, the carrier of X:] is Relation-like set
bool [: the carrier of c2, the carrier of X:] is non empty set
u is non empty Relation-like the carrier of c2 -defined the carrier of A -valued Function-like V17( the carrier of c2) quasi_total Element of bool [: the carrier of c2, the carrier of A:]
dom u is non empty Element of bool the carrier of c2
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 c2, the carrier of A,u) is non empty Relation-like the carrier of A -defined the carrier of c2 -valued Function-like V17( the carrier of A) quasi_total Element of bool [: the carrier of A, the carrier of c2:]
[: the carrier of A, the carrier of c2:] is non empty Relation-like set
bool [: the carrier of A, the carrier of c2:] is non empty set
( the carrier of X, the carrier of c2,A) * ( the carrier of c2, the carrier of A,u) 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:]
rng (u * A) is Element of bool the carrier of A
(u * A) " is Relation-like Function-like set

X is 1-sorted
the carrier of X is set
c2 is 1-sorted
the carrier of c2 is set
[: the carrier of X, the carrier of c2:] is Relation-like set
bool [: the carrier of X, the carrier of c2:] is non empty set
bool the carrier of X is non empty set
[#] c2 is non proper Element of bool the carrier of c2
bool the carrier of c2 is non empty set
A is Relation-like the carrier of X -defined the carrier of c2 -valued Function-like quasi_total Element of bool [: the carrier of X, the carrier of c2:]
rng A is Element of bool the carrier of c2
( the carrier of X, the carrier of c2,A) is Relation-like the carrier of c2 -defined the carrier of X -valued Function-like quasi_total Element of bool [: the carrier of c2, the carrier of X:]
[: the carrier of c2, the carrier of X:] is Relation-like set
bool [: the carrier of c2, the carrier of X:] is non empty set
A is Element of bool the carrier of X
A .: A is Element of bool the carrier of c2
( the carrier of X, the carrier of c2,A) " A is Element of bool the carrier of c2

(A ") " A is set
X is 1-sorted
the carrier of X is set
c2 is 1-sorted
the carrier of c2 is set
[: the carrier of X, the carrier of c2:] is Relation-like set
bool [: the carrier of X, the carrier of c2:] is non empty set
bool the carrier of c2 is non empty set
[#] c2 is non proper Element of bool the carrier of c2
A is Relation-like the carrier of X -defined the carrier of c2 -valued Function-like quasi_total Element of bool [: the carrier of X, the carrier of c2:]
rng A is Element of bool the carrier of c2
( the carrier of X, the carrier of c2,A) is Relation-like the carrier of c2 -defined the carrier of X -valued Function-like quasi_total Element of bool [: the carrier of c2, the carrier of X:]
[: the carrier of c2, the carrier of X:] is Relation-like set
bool [: the carrier of c2, the carrier of X:] is non empty set
A is Element of bool the carrier of c2
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 c2,A) .: A is Element of bool the carrier of X

(A ") .: A is set
X is TopStruct
the carrier of X is set
c2 is TopStruct
the carrier of c2 is set
[: the carrier of X, the carrier of c2:] is Relation-like set
bool [: the carrier of X, the carrier of c2:] is non empty set
X is TopStruct
the carrier of X is set
c2 is non empty TopStruct
the carrier of c2 is non empty set
[: the carrier of X, the carrier of c2:] is Relation-like set
bool [: the carrier of X, the carrier of c2:] is non empty set
A is Relation-like the carrier of X -defined the carrier of c2 -valued Function-like V17( the carrier of X) quasi_total Element of bool [: the carrier of X, the carrier of c2:]
( the carrier of X, the carrier of c2,A) is Relation-like the carrier of c2 -defined the carrier of X -valued Function-like quasi_total Element of bool [: the carrier of c2, the carrier of X:]
[: the carrier of c2, the carrier of X:] is Relation-like set
bool [: the carrier of c2, the carrier of X:] is non empty set
rng A is Element of bool the carrier of c2
bool the carrier of c2 is non empty set
[#] c2 is non empty non proper Element of bool the carrier of c2
dom ( the carrier of X, the carrier of c2,A) is Element of bool the carrier of c2
rng ( the carrier of X, the carrier of c2,A) is Element of bool the carrier of X
bool the carrier of X is non empty set
[#] X is non proper Element of bool the carrier of X
( the carrier of c2, the carrier of X,( the carrier of X, the carrier of c2,A)) is Relation-like the carrier of X -defined the carrier of c2 -valued Function-like V17( the carrier of X) quasi_total Element of bool [: the carrier of X, the carrier of c2:]
X is non empty TopStruct
the carrier of X is non empty set
c2 is non empty TopStruct
the carrier of c2 is non empty set
[: the carrier of X, the carrier of c2:] is non empty Relation-like set
bool [: the carrier of X, the carrier of c2:] is non empty set
A is non empty TopStruct
the carrier of A is non empty set
[: the carrier of c2, the carrier of A:] is non empty Relation-like set
bool [: the carrier of c2, the carrier of A:] is non empty set
A is non empty Relation-like the carrier of X -defined the carrier of c2 -valued Function-like V17( the carrier of X) quasi_total Element of bool [: the carrier of X, the carrier of c2:]
u is non empty Relation-like the carrier of c2 -defined the carrier of A -valued Function-like V17( the carrier of c2) quasi_total Element of bool [: the carrier of c2, the carrier of A:]
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 c2
bool the carrier of c2 is non empty set
[#] c2 is non empty non proper Element of bool the carrier of c2
dom u is non empty Element of bool the carrier of c2
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 c2,A) is non empty Relation-like the carrier of c2 -defined the carrier of X -valued Function-like V17( the carrier of c2) quasi_total Element of bool [: the carrier of c2, the carrier of X:]
[: the carrier of c2, the carrier of X:] is non empty Relation-like set
bool [: the carrier of c2, the carrier of X:] is non empty set
( the carrier of c2, the carrier of A,u) is non empty Relation-like the carrier of A -defined the carrier of c2 -valued Function-like V17( the carrier of A) quasi_total Element of bool [: the carrier of A, the carrier of c2:]
[: the carrier of A, the carrier of c2:] is non empty Relation-like set
bool [: the carrier of A, the carrier of c2:] is non empty set
( the carrier of X, the carrier of c2,A) * ( the carrier of c2, the carrier of A,u) 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:]
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
c2 is non empty TopStruct
the carrier of c2 is non empty set
[: the carrier of X, the carrier of c2:] is Relation-like set
bool [: the carrier of X, the carrier of c2:] is non empty set
[#] c2 is non empty non proper Element of bool the carrier of c2
bool the carrier of c2 is non empty set
A is Relation-like the carrier of X -defined the carrier of c2 -valued Function-like V17( the carrier of X) quasi_total Element of bool [: the carrier of X, the carrier of c2:]
dom A is Element of bool the carrier of X
rng A is Element of bool the carrier of c2
( the carrier of X, the carrier of c2,A) is Relation-like the carrier of c2 -defined the carrier of X -valued Function-like quasi_total Element of bool [: the carrier of c2, the carrier of X:]
[: the carrier of c2, the carrier of X:] is Relation-like set
bool [: the carrier of c2, the carrier of X:] is non empty set
A is Element of bool the carrier of X
( the carrier of X, the carrier of c2,A) " A is Element of bool the carrier of c2

(A ") " A is set
A .: A is Element of bool the carrier of c2
A " (A .: A) is Element of bool the carrier of X
A is Element of bool the carrier of c2
A " A is Element of bool the carrier of X
A .: (A " A) is Element of bool the carrier of c2
A is Element of bool the carrier of X
( the carrier of X, the carrier of c2,A) " A is Element of bool the carrier of c2
(A ") " A is set
A .: A is Element of bool the carrier of c2
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

the carrier of c2 is set
[: the carrier of X, the carrier of c2:] is Relation-like set
bool [: the carrier of X, the carrier of c2:] is non empty set
[#] c2 is non proper closed Element of bool the carrier of c2
bool the carrier of c2 is non empty set
A is Relation-like the carrier of X -defined the carrier of c2 -valued Function-like quasi_total Element of bool [: the carrier of X, the carrier of c2:]
dom A is Element of bool the carrier of X
rng A is Element of bool the carrier of c2
A is Element of bool the carrier of c2
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 c2
A " (Cl A) is Element of bool the carrier of X
( the carrier of X, the carrier of c2,A) is Relation-like the carrier of c2 -defined the carrier of X -valued Function-like V17( the carrier of c2) quasi_total Element of bool [: the carrier of c2, the carrier of X:]
[: the carrier of c2, the carrier of X:] is Relation-like set
bool [: the carrier of c2, the carrier of X:] is non empty set
( the carrier of X, the carrier of c2,A) .: (Cl A) is Element of bool the carrier of X
( the carrier of X, the carrier of c2,A) .: A is Element of bool the carrier of X
Cl (( the carrier of X, the carrier of c2,A) .: A) is Element of bool the carrier of X
A is Element of bool the carrier of c2
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 c2
A " (Cl A) is Element of bool the carrier of X
A is Element of bool the carrier of c2
Cl A is Element of bool the carrier of c2
( the carrier of X, the carrier of c2,A) .: (Cl A) is Element of bool the carrier of X
A " (Cl A) is Element of bool the carrier of X
( the carrier of X, the carrier of c2,A) .: A is Element of bool the carrier of X
A " A is Element of bool the carrier of X
Cl (( the carrier of X, the carrier of c2,A) .: A) is Element of bool the carrier of X

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
c2 is non empty TopSpace-like TopStruct
the carrier of c2 is non empty set
[: the carrier of X, the carrier of c2:] is Relation-like set
bool [: the carrier of X, the carrier of c2:] is non empty set
[#] c2 is non empty non proper closed Element of bool the carrier of c2
bool the carrier of c2 is non empty set
A is Relation-like the carrier of X -defined the carrier of c2 -valued Function-like V17( the carrier of X) quasi_total Element of bool [: the carrier of X, the carrier of c2:]
dom A is Element of bool the carrier of X
rng A is Element of bool the carrier of c2
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 c2
A .: A is Element of bool the carrier of c2
Cl (A .: A) is Element of bool the carrier of c2
( the carrier of X, the carrier of c2,A) is Relation-like the carrier of c2 -defined the carrier of X -valued Function-like quasi_total Element of bool [: the carrier of c2, the carrier of X:]
[: the carrier of c2, the carrier of X:] is Relation-like set
bool [: the carrier of c2, the carrier of X:] is non empty set
( the carrier of X, the carrier of c2,A) " A is Element of bool the carrier of c2
Cl (( the carrier of X, the carrier of c2,A) " A) is Element of bool the carrier of c2
( the carrier of X, the carrier of c2,A) " (Cl A) is Element of bool the carrier of c2
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 c2
A .: A is Element of bool the carrier of c2
Cl (A .: A) is Element of bool the carrier of c2
A is Element of bool the carrier of X
( the carrier of X, the carrier of c2,A) " A is Element of bool the carrier of c2
A .: A is Element of bool the carrier of c2
Cl A is Element of bool the carrier of X
( the carrier of X, the carrier of c2,A) " (Cl A) is Element of bool the carrier of c2
A .: (Cl A) is Element of bool the carrier of c2
Cl (( the carrier of X, the carrier of c2,A) " A) is Element of bool the carrier of c2
X is non empty TopSpace-like TopStruct
the carrier of X is non empty set
c2 is non empty TopSpace-like TopStruct
the carrier of c2 is non empty set
[: the carrier of X, the carrier of c2:] is non empty Relation-like set
bool [: the carrier of X, the carrier of c2:] is non empty set
bool the carrier of X is non empty set
A is non empty Relation-like the carrier of X -defined the carrier of c2 -valued Function-like V17( the carrier of X) quasi_total Element of bool [: the carrier of X, the carrier of c2:]
A is Element of bool the carrier of X
A .: A is Element of bool the carrier of c2
bool the carrier of c2 is non empty set

u is Element of bool the carrier of c2
y is Element of bool the carrier of c2
u \/ y is Element of bool the carrier of c2
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 c2
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 c2
A " (u /\ (Cl y)) is Element of bool the carrier of X

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

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
c15 is Element of bool the carrier of X
c16 is Element of bool the carrier of X
c15 \/ c16 is Element of bool the carrier of X
X is non empty TopSpace-like TopStruct
the carrier of X is non empty set
c2 is non empty TopSpace-like TopStruct
the carrier of c2 is non empty set
[: the carrier of X, the carrier of c2:] is non empty Relation-like set
bool [: the carrier of X, the carrier of c2:] is non empty set
bool the carrier of c2 is non empty set
A is non empty Relation-like the carrier of X -defined the carrier of c2 -valued Function-like V17( the carrier of X) quasi_total Element of bool [: the carrier of X, the carrier of c2:]
A is Element of bool the carrier of c2
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 c2,A) is non empty Relation-like the carrier of c2 -defined the carrier of X -valued Function-like V17( the carrier of c2) quasi_total Element of bool [: the carrier of c2, the carrier of X:]
[: the carrier of c2, the carrier of X:] is non empty Relation-like set
bool [: the carrier of c2, the carrier of X:] is non empty set
( the carrier of X, the carrier of c2,A) .: A is Element of bool the carrier of X
rng A is non empty Element of bool the carrier of c2
[#] c2 is non empty non proper closed Element of bool the carrier of c2
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

c2 is Element of bool the carrier of X
A is Element of bool the carrier of X
c2 \/ A is Element of bool the carrier of X
the Element of A is Element of A
the Element of c2 is Element of c2
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 " c2 is Element of bool the carrier of GY
f " A is Element of bool the carrier of GY
(f " c2) \/ (f " A) is Element of bool the carrier of GY
(rng f) /\ A is Element of bool the carrier of X

(rng f) /\ c2 is Element of bool the carrier of X
(f " c2) /\ (f " A) is Element of bool the carrier of GY
c2 /\ A is Element of bool the carrier of X
f " (c2 /\ A) is Element of bool the carrier of GY
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)
c2 is Element of bool (bool 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
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)
c2 is Element of bool (bool 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
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