:: 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₂ 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
c₂ 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
c₂ is Element of bool (bool the carrier of X)
union c₂ is Element of bool the carrier of X
the Element of union c₂ is 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₂ is Element of bool (bool the carrier of X)
union c₂ 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 c₂) \ (union A) is Element of bool the carrier of X
c₂ \ A is Element of bool (bool the carrier of X)
union (c₂ \ 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
c₂ is Element of bool (bool X)
COMPLEMENT c₂ is Element of bool (bool X)
COMPLEMENT (COMPLEMENT c₂) is Element of bool (bool X)
X is set
bool X is non empty set
bool (bool X) is non empty set
c₂ is Element of bool (bool X)
COMPLEMENT c₂ is Element of bool (bool X)
meet (COMPLEMENT c₂) is Element of bool X
union c₂ is Element of bool X
(union c₂) ` is Element of bool X
X \ (union c<sub>2</sub>) is set
[#] X is non proper Element of bool X
([#] X) \ (union c<sub>2</sub>) is Element of bool X
X is set
bool X is non empty set
bool (bool X) is non empty set
c<sub>2</sub> is Element of bool (bool X)
COMPLEMENT c<sub>2</sub> is Element of bool (bool X)
union (COMPLEMENT c<sub>2</sub>) is Element of bool X
meet c<sub>2</sub> is Element of bool X
(meet c<sub>2</sub>) ` is Element of bool X
X \ (meet c₂) is set
[#] X is non proper Element of bool X
([#] X) \ (meet c₂) is Element of bool X
X \ (meet c₂) 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
c₂ is Element of bool (bool the carrier of X)
COMPLEMENT c₂ 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
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₂) 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₂ is Element of bool (bool the carrier of X)
COMPLEMENT c₂ is Element of bool (bool the carrier of X)
COMPLEMENT (COMPLEMENT c₂) 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
c₂ is Element of bool (bool the carrier of X)
COMPLEMENT c₂ 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
c<sub>2</sub> is Element of bool (bool the carrier of X)
COMPLEMENT c<sub>2</sub> is Element of bool (bool the carrier of X)
COMPLEMENT (COMPLEMENT c<sub>2</sub>) 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
c<sub>2</sub> 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
c<sub>2</sub> 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
c<sub>2</sub> is Element of bool (bool the carrier of X)
A is Element of bool (bool the carrier of X)
c<sub>2</sub> \/ 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<sub>2</sub> is Element of bool (bool the carrier of X)
A is Element of bool (bool the carrier of X)
c<sub>2</sub> /\ 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<sub>2</sub> is Element of bool (bool the carrier of X)
A is Element of bool (bool the carrier of X)
c<sub>2</sub> \ 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<sub>2</sub> is Element of bool (bool the carrier of X)
A is Element of bool (bool the carrier of X)
c<sub>2</sub> \/ 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<sub>2</sub> is Element of bool (bool the carrier of X)
A is Element of bool (bool the carrier of X)
c<sub>2</sub> /\ 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<sub>2</sub> is Element of bool (bool the carrier of X)
A is Element of bool (bool the carrier of X)
c<sub>2</sub> \ A is Element of bool (bool the carrier of X)
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<sub>2</sub> is Element of bool (bool the carrier of X)
union c<sub>2</sub> 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
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<sub>2</sub> is Element of bool (bool the carrier of X)
meet c<sub>2</sub> is Element of bool the carrier of X
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<sub>2</sub> is Element of bool (bool the carrier of X)
union c<sub>2</sub> is Element of bool the carrier of X
COMPLEMENT c<sub>2</sub> 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 (COMPLEMENT c<sub>2</sub>) is Element of bool the carrier of X
(union c<sub>2</sub>) ` is Element of bool the carrier of X
the carrier of X \ (union c₂) is set
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₂ is Element of bool (bool the carrier of X)
meet c₂ is Element of bool the carrier of X
COMPLEMENT c₂ 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 (COMPLEMENT c₂) is Element of bool the carrier of X
(meet c₂) ` is Element of bool the carrier of X
the carrier of X \ (meet c<sub>2</sub>) is set
{} 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<sub>2</sub> is SubSpace of X
the carrier of c<sub>2</sub> is set
bool the carrier of c<sub>2</sub> is non empty set
bool (bool the carrier of c<sub>2</sub>) is non empty set
A is Element of bool (bool the carrier of c<sub>2</sub>)
[#] c<sub>2</sub> is non proper Element of bool the carrier of c<sub>2</sub>
[#] X is non proper Element of bool the carrier of X
bool the carrier of c<sub>2</sub> is non empty Element of bool (bool the carrier of c<sub>2</sub>)
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<sub>2</sub> is SubSpace of X
the carrier of c<sub>2</sub> is set
bool the carrier of c<sub>2</sub> is non empty set
[#] c<sub>2</sub> is non proper Element of bool the carrier of c<sub>2</sub>
A is Element of bool the carrier of c<sub>2</sub>
the topology of c<sub>2</sub> is Element of bool (bool the carrier of c<sub>2</sub>)
bool (bool the carrier of c<sub>2</sub>) 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 /\ ([#] c<sub>2</sub>) is Element of bool the carrier of c<sub>2</sub>
u is Element of bool the carrier of X
y is Element of bool the carrier of X
y /\ ([#] c<sub>2</sub>) is Element of bool the carrier of c<sub>2</sub>
A is Element of bool the carrier of X
A /\ ([#] c<sub>2</sub>) is Element of bool the carrier of c<sub>2</sub>
X is TopStruct
the carrier of X is set
bool the carrier of X is non empty set
c<sub>2</sub> 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
c<sub>2</sub> /\ ([#] 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
c<sub>2</sub> 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
c<sub>2</sub> /\ ([#] 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
c<sub>2</sub> 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
c<sub>2</sub> 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
c<sub>2</sub> is Element of bool the carrier of X
A is Element of bool the carrier of X
c<sub>2</sub> /\ 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
c<sub>2</sub> is Element of bool the carrier of X
X | c<sub>2</sub> is strict SubSpace of X
the carrier of (X | c<sub>2</sub>) is set
bool the carrier of (X | c<sub>2</sub>) is non empty set
bool (bool the carrier of (X | c<sub>2</sub>)) is non empty set
A is Element of bool (bool the carrier of X)
A is Element of bool (bool the carrier of (X | c<sub>2</sub>))
A is Element of bool (bool the carrier of (X | c<sub>2</sub>))
u is Element of bool (bool the carrier of (X | c<sub>2</sub>))
y is set
x is Element of bool the carrier of (X | c<sub>2</sub>)
GY is Element of bool the carrier of X
GY /\ c<sub>2</sub> is Element of bool the carrier of X
x is Element of bool the carrier of (X | c<sub>2</sub>)
GY is Element of bool the carrier of X
GY /\ c<sub>2</sub> 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<sub>2</sub> is Element of bool the carrier of X
A is Element of bool (bool the carrier of X)
(X,c<sub>2</sub>,A) is Element of bool (bool the carrier of (X | c<sub>2</sub>))
X | c<sub>2</sub> is strict SubSpace of X
the carrier of (X | c<sub>2</sub>) is set
bool the carrier of (X | c<sub>2</sub>) is non empty set
bool (bool the carrier of (X | c<sub>2</sub>)) is non empty set
A is Element of bool (bool the carrier of X)
(X,c<sub>2</sub>,A) is Element of bool (bool the carrier of (X | c<sub>2</sub>))
u is set
y is Element of bool the carrier of (X | c<sub>2</sub>)
x is Element of bool the carrier of X
x /\ c<sub>2</sub> 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<sub>2</sub> is Element of bool the carrier of X
A is Element of bool the carrier of X
c<sub>2</sub> /\ 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
c<sub>2</sub> is Element of bool the carrier of X
A is Element of bool the carrier of X
c<sub>2</sub> /\ 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
c<sub>2</sub> is Element of bool the carrier of X
X | c<sub>2</sub> is strict SubSpace of X
the carrier of (X | c<sub>2</sub>) is set
A is Element of bool (bool the carrier of X)
union A is Element of bool the carrier of X
(X,c<sub>2</sub>,A) is Element of bool (bool the carrier of (X | c<sub>2</sub>))
bool the carrier of (X | c<sub>2</sub>) is non empty set
bool (bool the carrier of (X | c<sub>2</sub>)) is non empty set
union (X,c<sub>2</sub>,A) is Element of bool the carrier of (X | c<sub>2</sub>)
A is set
u is set
u /\ c<sub>2</sub> is Element of bool the carrier of X
[#] (X | c<sub>2</sub>) is non proper Element of bool the carrier of (X | c<sub>2</sub>)
y is Element of bool the carrier of X
y /\ c<sub>2</sub> is Element of bool the carrier of X
x is Element of bool the carrier of (X | c<sub>2</sub>)
u is set
y is Element of bool the carrier of (X | c<sub>2</sub>)
x is Element of bool the carrier of X
x /\ c<sub>2</sub> 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<sub>2</sub> is Element of bool the carrier of X
X | c<sub>2</sub> is strict SubSpace of X
the carrier of (X | c<sub>2</sub>) is set
A is Element of bool (bool the carrier of X)
(X,c<sub>2</sub>,A) is Element of bool (bool the carrier of (X | c<sub>2</sub>))
bool the carrier of (X | c<sub>2</sub>) is non empty set
bool (bool the carrier of (X | c<sub>2</sub>)) is non empty set
union (X,c<sub>2</sub>,A) is Element of bool the carrier of (X | c<sub>2</sub>)
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<sub>2</sub>)
x is Element of bool the carrier of X
x /\ c<sub>2</sub> 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<sub>2</sub> is Element of bool the carrier of X
X | c<sub>2</sub> is strict SubSpace of X
the carrier of (X | c<sub>2</sub>) is set
A is Element of bool (bool the carrier of X)
(X,c<sub>2</sub>,A) is Element of bool (bool the carrier of (X | c<sub>2</sub>))
bool the carrier of (X | c<sub>2</sub>) is non empty set
bool (bool the carrier of (X | c<sub>2</sub>)) is non empty set
union (X,c<sub>2</sub>,A) is Element of bool the carrier of (X | c<sub>2</sub>)
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<sub>2</sub> is Element of bool the carrier of X
A is Element of bool (bool the carrier of X)
(X,c<sub>2</sub>,A) is Element of bool (bool the carrier of (X | c<sub>2</sub>))
X | c<sub>2</sub> is strict SubSpace of X
the carrier of (X | c<sub>2</sub>) is set
bool the carrier of (X | c<sub>2</sub>) is non empty set
bool (bool the carrier of (X | c<sub>2</sub>)) is non empty set
A is set
u is Element of bool the carrier of X
u /\ c<sub>2</sub> is Element of bool the carrier of X
y is set
x is Element of bool the carrier of X
x /\ c<sub>2</sub> is Element of bool the carrier of X
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<sub>2</sub> is Element of bool the carrier of X
[#] (X | c<sub>2</sub>) is non proper Element of bool the carrier of (X | c<sub>2</sub>)
GY is Element of bool the carrier of (X | c<sub>2</sub>)
y is Element of bool the carrier of (X | c<sub>2</sub>)
x is Element of bool the carrier of X
x /\ c<sub>2</sub> 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
c<sub>2</sub> is Element of bool the carrier of X
X | c<sub>2</sub> is strict SubSpace of X
A is Element of bool (bool the carrier of X)
(X,c<sub>2</sub>,A) is Element of bool (bool the carrier of (X | c<sub>2</sub>))
the carrier of (X | c<sub>2</sub>) is set
bool the carrier of (X | c<sub>2</sub>) is non empty set
bool (bool the carrier of (X | c<sub>2</sub>)) is non empty set
A is Element of bool the carrier of (X | c<sub>2</sub>)
u is Element of bool the carrier of X
u /\ c<sub>2</sub> is Element of bool the carrier of X
y is Element of bool the carrier of X
[#] (X | c<sub>2</sub>) is non proper Element of bool the carrier of (X | c<sub>2</sub>)
y /\ ([#] (X | c<sub>2</sub>)) is Element of bool the carrier of (X | c<sub>2</sub>)
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<sub>2</sub> is Element of bool the carrier of X
X | c<sub>2</sub> is strict SubSpace of X
A is Element of bool (bool the carrier of X)
(X,c<sub>2</sub>,A) is Element of bool (bool the carrier of (X | c<sub>2</sub>))
the carrier of (X | c<sub>2</sub>) is set
bool the carrier of (X | c<sub>2</sub>) is non empty set
bool (bool the carrier of (X | c<sub>2</sub>)) is non empty set
A is Element of bool the carrier of (X | c<sub>2</sub>)
u is Element of bool the carrier of X
u /\ c<sub>2</sub> is Element of bool the carrier of X
y is Element of bool the carrier of X
[#] (X | c<sub>2</sub>) is non proper Element of bool the carrier of (X | c<sub>2</sub>)
y /\ ([#] (X | c<sub>2</sub>)) is Element of bool the carrier of (X | c<sub>2</sub>)
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<sub>2</sub> is SubSpace of X
the carrier of c<sub>2</sub> is set
bool the carrier of c<sub>2</sub> is non empty set
bool (bool the carrier of c<sub>2</sub>) is non empty set
[#] c<sub>2</sub> is non proper Element of bool the carrier of c<sub>2</sub>
A is Element of bool (bool the carrier of c<sub>2</sub>)
[#] 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<sub>2</sub>
Q2 is Element of bool the carrier of X
Q2 /\ ([#] c<sub>2</sub>) is Element of bool the carrier of c<sub>2</sub>
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<sub>2</sub> is Element of bool the carrier of X
A is Element of bool (bool the carrier of X)
(X,c<sub>2</sub>,A) is Element of bool (bool the carrier of (X | c<sub>2</sub>))
X | c<sub>2</sub> is strict SubSpace of X
the carrier of (X | c<sub>2</sub>) is set
bool the carrier of (X | c<sub>2</sub>) is non empty set
bool (bool the carrier of (X | c<sub>2</sub>)) is non empty set
A is set
u is Element of bool the carrier of X
u /\ c<sub>2</sub> is Element of bool the carrier of X
y is set
x is Element of bool the carrier of X
x /\ c<sub>2</sub> is Element of bool the carrier of X
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<sub>2</sub> is Element of bool the carrier of X
[#] (X | c<sub>2</sub>) is non proper Element of bool the carrier of (X | c<sub>2</sub>)
GY is Element of bool the carrier of (X | c<sub>2</sub>)
y is Element of bool the carrier of (X | c<sub>2</sub>)
x is Element of bool the carrier of X
x /\ c<sub>2</sub> 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 /\ c<sub>2</sub> is Element of bool the carrier of X
X is 1-sorted
the carrier of X is set
c<sub>2</sub> is 1-sorted
the carrier of c<sub>2</sub> is set
[: the carrier of X, the carrier of c<sub>2</sub>:] is Relation-like set
bool [: the carrier of X, the carrier of c<sub>2</sub>:] is non empty set
[#] c<sub>2</sub> is non proper Element of bool the carrier of c<sub>2</sub>
bool the carrier of c<sub>2</sub> 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 c<sub>2</sub> -valued Function-like quasi_total Element of bool [: the carrier of X, the carrier of c<sub>2</sub>:]
A " ([#] c<sub>2</sub>) is Element of bool the carrier of X
rng A is Element of bool the carrier of c<sub>2</sub>
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<sub>2</sub> is non empty 1-sorted
the carrier of c<sub>2</sub> is non empty set
[: the carrier of X, the carrier of c<sub>2</sub>:] is Relation-like set
bool [: the carrier of X, the carrier of c<sub>2</sub>:] is non empty set
bool the carrier of c<sub>2</sub> is non empty set
bool (bool the carrier of c<sub>2</sub>) is non empty set
A is Relation-like the carrier of X -defined the carrier of c<sub>2</sub> -valued Function-like V17( the carrier of X) quasi_total Element of bool [: the carrier of X, the carrier of c<sub>2</sub>:]
" A is Relation-like Function-like set
A is Element of bool (bool the carrier of c<sub>2</sub>)
(" 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<sub>2</sub> is TopStruct
the carrier of c<sub>2</sub> is set
[: the carrier of X, the carrier of c<sub>2</sub>:] is Relation-like set
bool [: the carrier of X, the carrier of c<sub>2</sub>:] is non empty set
[#] c<sub>2</sub> is non proper Element of bool the carrier of c<sub>2</sub>
bool the carrier of c<sub>2</sub> 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 c<sub>2</sub> -valued Function-like quasi_total Element of bool [: the carrier of X, the carrier of c<sub>2</sub>:]
A is Element of bool the carrier of c<sub>2</sub>
A ` is Element of bool the carrier of c₂
the carrier of c₂ \ A is set
A " (A `) is Element of bool the carrier of X
A " ([#] c<sub>2</sub>) is Element of bool the carrier of X
A " A is Element of bool the carrier of X
(A " ([#] c<sub>2</sub>)) \ (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 c₂
A " A is Element of bool the carrier of X
A ` is Element of bool the carrier of c<sub>2</sub>
the carrier of c<sub>2</sub> \ A is set
A " (A `) is Element of bool the carrier of X
(A " ([#] c₂)) \ (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
X is TopSpace-like TopStruct
the carrier of X is set
c<sub>2</sub> is TopSpace-like TopStruct
the carrier of c<sub>2</sub> is set
[: the carrier of X, the carrier of c<sub>2</sub>:] is Relation-like set
bool [: the carrier of X, the carrier of c<sub>2</sub>:] is non empty set
bool the carrier of c<sub>2</sub> is non empty set
A is Relation-like the carrier of X -defined the carrier of c<sub>2</sub> -valued Function-like quasi_total Element of bool [: the carrier of X, the carrier of c<sub>2</sub>:]
A is Element of bool the carrier of c<sub>2</sub>
Cl A is Element of bool the carrier of c<sub>2</sub>
Cl (Cl A) is Element of bool the carrier of c<sub>2</sub>
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<sub>2</sub>
A " A is Element of bool the carrier of X
Cl A is Element of bool the carrier of c<sub>2</sub>
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<sub>2</sub> is non empty TopSpace-like TopStruct
the carrier of c<sub>2</sub> is non empty set
[: the carrier of X, the carrier of c<sub>2</sub>:] is Relation-like set
bool [: the carrier of X, the carrier of c<sub>2</sub>:] is non empty set
A is Relation-like the carrier of X -defined the carrier of c<sub>2</sub> -valued Function-like V17( the carrier of X) quasi_total Element of bool [: the carrier of X, the carrier of c<sub>2</sub>:]
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<sub>2</sub>
bool the carrier of c<sub>2</sub> 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 c<sub>2</sub>
A " (Cl (A .: A)) is Element of bool the carrier of X
A .: (Cl A) is Element of bool the carrier of c<sub>2</sub>
A .: (A " (Cl (A .: A))) is Element of bool the carrier of c<sub>2</sub>
A is Element of bool the carrier of c<sub>2</sub>
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<sub>2</sub>
A " (A .: (Cl (A " A))) is Element of bool the carrier of X
A .: (A " A) is Element of bool the carrier of c<sub>2</sub>
Cl (A .: (A " A)) is Element of bool the carrier of c<sub>2</sub>
Cl A is Element of bool the carrier of c<sub>2</sub>
A " (Cl A) is Element of bool the carrier of X
X is TopStruct
the carrier of X is set
c<sub>2</sub> is TopStruct
the carrier of c<sub>2</sub> 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 c<sub>2</sub>:] is Relation-like set
bool [: the carrier of A, the carrier of c<sub>2</sub>:] 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 c<sub>2</sub> -valued Function-like quasi_total Element of bool [: the carrier of A, the carrier of c<sub>2</sub>:]
u * A is Relation-like the carrier of X -defined the carrier of c<sub>2</sub> -valued Function-like quasi_total Element of bool [: the carrier of X, the carrier of c<sub>2</sub>:]
[: the carrier of X, the carrier of c<sub>2</sub>:] is Relation-like set
bool [: the carrier of X, the carrier of c<sub>2</sub>:] is non empty set
bool the carrier of c<sub>2</sub> is non empty set
y is Element of bool the carrier of c<sub>2</sub>
(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<sub>2</sub> is non empty TopStruct
the carrier of c<sub>2</sub> is non empty set
[: the carrier of X, the carrier of c<sub>2</sub>:] is Relation-like set
bool [: the carrier of X, the carrier of c<sub>2</sub>:] is non empty set
bool the carrier of c<sub>2</sub> is non empty set
bool (bool the carrier of c<sub>2</sub>) is non empty set
A is Relation-like the carrier of X -defined the carrier of c<sub>2</sub> -valued Function-like V17( the carrier of X) quasi_total Element of bool [: the carrier of X, the carrier of c<sub>2</sub>:]
" A is Relation-like Function-like set
A is Element of bool (bool the carrier of c<sub>2</sub>)
(" 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<sub>2</sub>
A " GY is Element of bool the carrier of X
[#] c<sub>2</sub> is non empty non proper Element of bool the carrier of c<sub>2</sub>
[#] X is non proper Element of bool the carrier of X
X is TopStruct
the carrier of X is set
c<sub>2</sub> is TopStruct
the carrier of c<sub>2</sub> is set
[: the carrier of X, the carrier of c<sub>2</sub>:] is Relation-like set
bool [: the carrier of X, the carrier of c<sub>2</sub>:] is non empty set
bool the carrier of c<sub>2</sub> is non empty set
bool (bool the carrier of c<sub>2</sub>) 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 c<sub>2</sub> -valued Function-like quasi_total Element of bool [: the carrier of X, the carrier of c<sub>2</sub>:]
" A is Relation-like Function-like set
A is Element of bool (bool the carrier of c<sub>2</sub>)
(" 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<sub>2</sub>
A " GY is Element of bool the carrier of X
X is set
c<sub>2</sub> is set
[:X,c<sub>2</sub>:] is Relation-like set
bool [:X,c<sub>2</sub>:] is non empty set
A is Relation-like X -defined c<sub>2</sub> -valued Function-like quasi_total Element of bool [:X,c<sub>2</sub>:]
A " is Relation-like Function-like set
[:c<sub>2</sub>,X:] is Relation-like set
bool [:c<sub>2</sub>,X:] is non empty set
rng A is Element of bool c<sub>2</sub>
bool c<sub>2</sub> is non empty set
[#] c<sub>2</sub> is non proper Element of bool c<sub>2</sub>
X is set
c<sub>2</sub> is set
[:X,c<sub>2</sub>:] is Relation-like set
bool [:X,c<sub>2</sub>:] 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
c<sub>2</sub> is non empty 1-sorted
the carrier of c<sub>2</sub> is non empty set
[: the carrier of X, the carrier of c<sub>2</sub>:] is Relation-like set
bool [: the carrier of X, the carrier of c<sub>2</sub>:] is non empty set
[#] c<sub>2</sub> is non empty non proper Element of bool the carrier of c<sub>2</sub>
bool the carrier of c<sub>2</sub> is non empty set
A is Relation-like the carrier of X -defined the carrier of c<sub>2</sub> -valued Function-like V17( the carrier of X) quasi_total Element of bool [: the carrier of X, the carrier of c<sub>2</sub>:]
rng A is Element of bool the carrier of c<sub>2</sub>
( the carrier of X, the carrier of c<sub>2</sub>,A) is Relation-like the carrier of c<sub>2</sub> -defined the carrier of X -valued Function-like quasi_total Element of bool [: the carrier of c<sub>2</sub>, the carrier of X:]
[: the carrier of c<sub>2</sub>, the carrier of X:] is Relation-like set
bool [: the carrier of c<sub>2</sub>, the carrier of X:] is non empty set
dom ( the carrier of X, the carrier of c<sub>2</sub>,A) is Element of bool the carrier of c<sub>2</sub>
rng ( the carrier of X, the carrier of c<sub>2</sub>,A) is Element of bool the carrier of X
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<sub>2</sub> is 1-sorted
the carrier of c<sub>2</sub> is set
[: the carrier of X, the carrier of c<sub>2</sub>:] is Relation-like set
bool [: the carrier of X, the carrier of c<sub>2</sub>:] is non empty set
[#] c<sub>2</sub> is non proper Element of bool the carrier of c<sub>2</sub>
bool the carrier of c<sub>2</sub> is non empty set
A is Relation-like the carrier of X -defined the carrier of c<sub>2</sub> -valued Function-like quasi_total Element of bool [: the carrier of X, the carrier of c<sub>2</sub>:]
rng A is Element of bool the carrier of c<sub>2</sub>
( the carrier of X, the carrier of c<sub>2</sub>,A) is Relation-like the carrier of c<sub>2</sub> -defined the carrier of X -valued Function-like quasi_total Element of bool [: the carrier of c<sub>2</sub>, the carrier of X:]
[: the carrier of c<sub>2</sub>, the carrier of X:] is Relation-like set
bool [: the carrier of c<sub>2</sub>, the carrier of X:] is non empty set
A " is Relation-like Function-like set
X is 1-sorted
the carrier of X is set
c<sub>2</sub> is non empty 1-sorted
the carrier of c<sub>2</sub> is non empty set
[: the carrier of X, the carrier of c<sub>2</sub>:] is Relation-like set
bool [: the carrier of X, the carrier of c<sub>2</sub>:] is non empty set
[#] c<sub>2</sub> is non empty non proper Element of bool the carrier of c<sub>2</sub>
bool the carrier of c<sub>2</sub> is non empty set
A is Relation-like the carrier of X -defined the carrier of c<sub>2</sub> -valued Function-like V17( the carrier of X) quasi_total Element of bool [: the carrier of X, the carrier of c<sub>2</sub>:]
rng A is Element of bool the carrier of c<sub>2</sub>
( the carrier of X, the carrier of c<sub>2</sub>,A) is Relation-like the carrier of c<sub>2</sub> -defined the carrier of X -valued Function-like quasi_total Element of bool [: the carrier of c<sub>2</sub>, the carrier of X:]
[: the carrier of c<sub>2</sub>, the carrier of X:] is Relation-like set
bool [: the carrier of c<sub>2</sub>, the carrier of X:] is non empty set
( the carrier of c<sub>2</sub>, the carrier of X,( the carrier of X, the carrier of c<sub>2</sub>,A)) is Relation-like the carrier of X -defined the carrier of c<sub>2</sub> -valued Function-like V17( the carrier of X) quasi_total Element of bool [: the carrier of X, the carrier of c<sub>2</sub>:]
A " is Relation-like Function-like set
(A ") " is Relation-like Function-like set
( the carrier of X, the carrier of c<sub>2</sub>,A) " is Relation-like Function-like set
rng ( the carrier of X, the carrier of c<sub>2</sub>,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
c<sub>2</sub> is 1-sorted
the carrier of c<sub>2</sub> is set
[: the carrier of X, the carrier of c<sub>2</sub>:] is Relation-like set
bool [: the carrier of X, the carrier of c<sub>2</sub>:] is non empty set
[#] c<sub>2</sub> is non proper Element of bool the carrier of c<sub>2</sub>
bool the carrier of c<sub>2</sub> is non empty set
A is Relation-like the carrier of X -defined the carrier of c<sub>2</sub> -valued Function-like quasi_total Element of bool [: the carrier of X, the carrier of c<sub>2</sub>:]
rng A is Element of bool the carrier of c<sub>2</sub>
( the carrier of X, the carrier of c<sub>2</sub>,A) is Relation-like the carrier of c<sub>2</sub> -defined the carrier of X -valued Function-like quasi_total Element of bool [: the carrier of c<sub>2</sub>, the carrier of X:]
[: the carrier of c<sub>2</sub>, the carrier of X:] is Relation-like set
bool [: the carrier of c<sub>2</sub>, the carrier of X:] is non empty set
( the carrier of X, the carrier of c<sub>2</sub>,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
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<sub>2</sub>,A) is Relation-like the carrier of c<sub>2</sub> -defined the carrier of c<sub>2</sub> -valued Function-like Element of bool [: the carrier of c<sub>2</sub>, the carrier of c<sub>2</sub>:]
[: the carrier of c<sub>2</sub>, the carrier of c<sub>2</sub>:] is Relation-like set
bool [: the carrier of c<sub>2</sub>, the carrier of c<sub>2</sub>:] is non empty set
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<sub>2</sub> -valued Function-like set
X is 1-sorted
the carrier of X is set
c<sub>2</sub> is non empty 1-sorted
the carrier of c<sub>2</sub> is non empty set
[: the carrier of X, the carrier of c<sub>2</sub>:] is Relation-like set
bool [: the carrier of X, the carrier of c<sub>2</sub>:] is non empty set
A is non empty 1-sorted
the carrier of A is non empty set
[: the carrier of c<sub>2</sub>, the carrier of A:] is non empty Relation-like set
bool [: the carrier of c<sub>2</sub>, the carrier of A:] is non empty set
[#] c<sub>2</sub> is non empty non proper Element of bool the carrier of c<sub>2</sub>
bool the carrier of c<sub>2</sub> 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 c<sub>2</sub> -valued Function-like V17( the carrier of X) quasi_total Element of bool [: the carrier of X, the carrier of c<sub>2</sub>:]
rng A is Element of bool the carrier of c<sub>2</sub>
( the carrier of X, the carrier of c<sub>2</sub>,A) is Relation-like the carrier of c<sub>2</sub> -defined the carrier of X -valued Function-like quasi_total Element of bool [: the carrier of c<sub>2</sub>, the carrier of X:]
[: the carrier of c<sub>2</sub>, the carrier of X:] is Relation-like set
bool [: the carrier of c<sub>2</sub>, the carrier of X:] is non empty set
u is non empty Relation-like the carrier of c<sub>2</sub> -defined the carrier of A -valued Function-like V17( the carrier of c<sub>2</sub>) quasi_total Element of bool [: the carrier of c<sub>2</sub>, the carrier of A:]
dom u is non empty Element of bool the carrier of c<sub>2</sub>
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<sub>2</sub>, the carrier of A,u) is non empty Relation-like the carrier of A -defined the carrier of c<sub>2</sub> -valued Function-like V17( the carrier of A) quasi_total Element of bool [: the carrier of A, the carrier of c<sub>2</sub>:]
[: the carrier of A, the carrier of c<sub>2</sub>:] is non empty Relation-like set
bool [: the carrier of A, the carrier of c<sub>2</sub>:] is non empty set
( the carrier of X, the carrier of c<sub>2</sub>,A) * ( the carrier of c<sub>2</sub>, 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
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<sub>2</sub> is 1-sorted
the carrier of c<sub>2</sub> is set
[: the carrier of X, the carrier of c<sub>2</sub>:] is Relation-like set
bool [: the carrier of X, the carrier of c<sub>2</sub>:] is non empty set
bool the carrier of X is non empty set
[#] c<sub>2</sub> is non proper Element of bool the carrier of c<sub>2</sub>
bool the carrier of c<sub>2</sub> is non empty set
A is Relation-like the carrier of X -defined the carrier of c<sub>2</sub> -valued Function-like quasi_total Element of bool [: the carrier of X, the carrier of c<sub>2</sub>:]
rng A is Element of bool the carrier of c<sub>2</sub>
( the carrier of X, the carrier of c<sub>2</sub>,A) is Relation-like the carrier of c<sub>2</sub> -defined the carrier of X -valued Function-like quasi_total Element of bool [: the carrier of c<sub>2</sub>, the carrier of X:]
[: the carrier of c<sub>2</sub>, the carrier of X:] is Relation-like set
bool [: the carrier of c<sub>2</sub>, 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 c<sub>2</sub>
( the carrier of X, the carrier of c<sub>2</sub>,A) " A is Element of bool the carrier of c<sub>2</sub>
A " is Relation-like Function-like set
(A ") " A is set
X is 1-sorted
the carrier of X is set
c<sub>2</sub> is 1-sorted
the carrier of c<sub>2</sub> is set
[: the carrier of X, the carrier of c<sub>2</sub>:] is Relation-like set
bool [: the carrier of X, the carrier of c<sub>2</sub>:] is non empty set
bool the carrier of c<sub>2</sub> is non empty set
[#] c<sub>2</sub> is non proper Element of bool the carrier of c<sub>2</sub>
A is Relation-like the carrier of X -defined the carrier of c<sub>2</sub> -valued Function-like quasi_total Element of bool [: the carrier of X, the carrier of c<sub>2</sub>:]
rng A is Element of bool the carrier of c<sub>2</sub>
( the carrier of X, the carrier of c<sub>2</sub>,A) is Relation-like the carrier of c<sub>2</sub> -defined the carrier of X -valued Function-like quasi_total Element of bool [: the carrier of c<sub>2</sub>, the carrier of X:]
[: the carrier of c<sub>2</sub>, the carrier of X:] is Relation-like set
bool [: the carrier of c<sub>2</sub>, the carrier of X:] is non empty set
A is Element of bool the carrier of c<sub>2</sub>
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<sub>2</sub>,A) .: A is Element of bool the carrier of X
A " is Relation-like Function-like set
(A ") .: A is set
X is TopStruct
the carrier of X is set
c<sub>2</sub> is TopStruct
the carrier of c<sub>2</sub> is set
[: the carrier of X, the carrier of c<sub>2</sub>:] is Relation-like set
bool [: the carrier of X, the carrier of c<sub>2</sub>:] is non empty set
X is TopStruct
the carrier of X is set
c<sub>2</sub> is non empty TopStruct
the carrier of c<sub>2</sub> is non empty set
[: the carrier of X, the carrier of c<sub>2</sub>:] is Relation-like set
bool [: the carrier of X, the carrier of c<sub>2</sub>:] is non empty set
A is Relation-like the carrier of X -defined the carrier of c<sub>2</sub> -valued Function-like V17( the carrier of X) quasi_total Element of bool [: the carrier of X, the carrier of c<sub>2</sub>:]
( the carrier of X, the carrier of c<sub>2</sub>,A) is Relation-like the carrier of c<sub>2</sub> -defined the carrier of X -valued Function-like quasi_total Element of bool [: the carrier of c<sub>2</sub>, the carrier of X:]
[: the carrier of c<sub>2</sub>, the carrier of X:] is Relation-like set
bool [: the carrier of c<sub>2</sub>, the carrier of X:] is non empty set
rng A is Element of bool the carrier of c<sub>2</sub>
bool the carrier of c<sub>2</sub> is non empty set
[#] c<sub>2</sub> is non empty non proper Element of bool the carrier of c<sub>2</sub>
dom ( the carrier of X, the carrier of c<sub>2</sub>,A) is Element of bool the carrier of c<sub>2</sub>
rng ( the carrier of X, the carrier of c<sub>2</sub>,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 c<sub>2</sub>, the carrier of X,( the carrier of X, the carrier of c<sub>2</sub>,A)) is Relation-like the carrier of X -defined the carrier of c<sub>2</sub> -valued Function-like V17( the carrier of X) quasi_total Element of bool [: the carrier of X, the carrier of c<sub>2</sub>:]
X is non empty TopStruct
the carrier of X is non empty set
c<sub>2</sub> is non empty TopStruct
the carrier of c<sub>2</sub> is non empty set
[: the carrier of X, the carrier of c<sub>2</sub>:] is non empty Relation-like set
bool [: the carrier of X, the carrier of c<sub>2</sub>:] is non empty set
A is non empty TopStruct
the carrier of A is non empty set
[: the carrier of c<sub>2</sub>, the carrier of A:] is non empty Relation-like set
bool [: the carrier of c<sub>2</sub>, the carrier of A:] is non empty set
A is non empty Relation-like the carrier of X -defined the carrier of c<sub>2</sub> -valued Function-like V17( the carrier of X) quasi_total Element of bool [: the carrier of X, the carrier of c<sub>2</sub>:]
u is non empty Relation-like the carrier of c<sub>2</sub> -defined the carrier of A -valued Function-like V17( the carrier of c<sub>2</sub>) quasi_total Element of bool [: the carrier of c<sub>2</sub>, 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 c<sub>2</sub>
bool the carrier of c<sub>2</sub> is non empty set
[#] c<sub>2</sub> is non empty non proper Element of bool the carrier of c<sub>2</sub>
dom u is non empty Element of bool the carrier of c<sub>2</sub>
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<sub>2</sub>,A) is non empty Relation-like the carrier of c<sub>2</sub> -defined the carrier of X -valued Function-like V17( the carrier of c<sub>2</sub>) quasi_total Element of bool [: the carrier of c<sub>2</sub>, the carrier of X:]
[: the carrier of c<sub>2</sub>, the carrier of X:] is non empty Relation-like set
bool [: the carrier of c<sub>2</sub>, the carrier of X:] is non empty set
( the carrier of c<sub>2</sub>, the carrier of A,u) is non empty Relation-like the carrier of A -defined the carrier of c<sub>2</sub> -valued Function-like V17( the carrier of A) quasi_total Element of bool [: the carrier of A, the carrier of c<sub>2</sub>:]
[: the carrier of A, the carrier of c<sub>2</sub>:] is non empty Relation-like set
bool [: the carrier of A, the carrier of c<sub>2</sub>:] is non empty set
( the carrier of X, the carrier of c<sub>2</sub>,A) * ( the carrier of c<sub>2</sub>, 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
c<sub>2</sub> is non empty TopStruct
the carrier of c<sub>2</sub> is non empty set
[: the carrier of X, the carrier of c<sub>2</sub>:] is Relation-like set
bool [: the carrier of X, the carrier of c<sub>2</sub>:] is non empty set
[#] c<sub>2</sub> is non empty non proper Element of bool the carrier of c<sub>2</sub>
bool the carrier of c<sub>2</sub> is non empty set
A is Relation-like the carrier of X -defined the carrier of c<sub>2</sub> -valued Function-like V17( the carrier of X) quasi_total Element of bool [: the carrier of X, the carrier of c<sub>2</sub>:]
dom A is Element of bool the carrier of X
rng A is Element of bool the carrier of c<sub>2</sub>
( the carrier of X, the carrier of c<sub>2</sub>,A) is Relation-like the carrier of c<sub>2</sub> -defined the carrier of X -valued Function-like quasi_total Element of bool [: the carrier of c<sub>2</sub>, the carrier of X:]
[: the carrier of c<sub>2</sub>, the carrier of X:] is Relation-like set
bool [: the carrier of c<sub>2</sub>, the carrier of X:] is non empty set
A is Element of bool the carrier of X
( the carrier of X, the carrier of c<sub>2</sub>,A) " A is Element of bool the carrier of c<sub>2</sub>
A " is Relation-like Function-like set
(A ") " A is set
A .: A is Element of bool the carrier of c<sub>2</sub>
A " (A .: A) is Element of bool the carrier of X
A is Element of bool the carrier of c<sub>2</sub>
A " A is Element of bool the carrier of X
A .: (A " A) is Element of bool the carrier of c<sub>2</sub>
A is Element of bool the carrier of X
( the carrier of X, the carrier of c<sub>2</sub>,A) " A is Element of bool the carrier of c<sub>2</sub>
(A ") " A is set
A .: A is Element of bool the carrier of c<sub>2</sub>
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<sub>2</sub> is TopSpace-like TopStruct
the carrier of c<sub>2</sub> is set
[: the carrier of X, the carrier of c<sub>2</sub>:] is Relation-like set
bool [: the carrier of X, the carrier of c<sub>2</sub>:] is non empty set
[#] c<sub>2</sub> is non proper closed Element of bool the carrier of c<sub>2</sub>
bool the carrier of c<sub>2</sub> is non empty set
A is Relation-like the carrier of X -defined the carrier of c<sub>2</sub> -valued Function-like quasi_total Element of bool [: the carrier of X, the carrier of c<sub>2</sub>:]
dom A is Element of bool the carrier of X
rng A is Element of bool the carrier of c<sub>2</sub>
A is Element of bool the carrier of c<sub>2</sub>
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<sub>2</sub>
A " (Cl A) is Element of bool the carrier of X
( the carrier of X, the carrier of c<sub>2</sub>,A) is Relation-like the carrier of c<sub>2</sub> -defined the carrier of X -valued Function-like V17( the carrier of c<sub>2</sub>) quasi_total Element of bool [: the carrier of c<sub>2</sub>, the carrier of X:]
[: the carrier of c<sub>2</sub>, the carrier of X:] is Relation-like set
bool [: the carrier of c<sub>2</sub>, the carrier of X:] is non empty set
( the carrier of X, the carrier of c<sub>2</sub>,A) .: (Cl A) is Element of bool the carrier of X
( the carrier of X, the carrier of c<sub>2</sub>,A) .: A is Element of bool the carrier of X
Cl (( the carrier of X, the carrier of c<sub>2</sub>,A) .: A) is Element of bool the carrier of X
A is Element of bool the carrier of c<sub>2</sub>
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<sub>2</sub>
A " (Cl A) is Element of bool the carrier of X
A is Element of bool the carrier of c<sub>2</sub>
Cl A is Element of bool the carrier of c<sub>2</sub>
( the carrier of X, the carrier of c<sub>2</sub>,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 c<sub>2</sub>,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 c<sub>2</sub>,A) .: A) is Element of bool the carrier of X
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<sub>2</sub> is non empty TopSpace-like TopStruct
the carrier of c<sub>2</sub> is non empty set
[: the carrier of X, the carrier of c<sub>2</sub>:] is Relation-like set
bool [: the carrier of X, the carrier of c<sub>2</sub>:] is non empty set
[#] c<sub>2</sub> is non empty non proper closed Element of bool the carrier of c<sub>2</sub>
bool the carrier of c<sub>2</sub> is non empty set
A is Relation-like the carrier of X -defined the carrier of c<sub>2</sub> -valued Function-like V17( the carrier of X) quasi_total Element of bool [: the carrier of X, the carrier of c<sub>2</sub>:]
dom A is Element of bool the carrier of X
rng A is Element of bool the carrier of c<sub>2</sub>
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<sub>2</sub>
A .: A is Element of bool the carrier of c<sub>2</sub>
Cl (A .: A) is Element of bool the carrier of c<sub>2</sub>
( the carrier of X, the carrier of c<sub>2</sub>,A) is Relation-like the carrier of c<sub>2</sub> -defined the carrier of X -valued Function-like quasi_total Element of bool [: the carrier of c<sub>2</sub>, the carrier of X:]
[: the carrier of c<sub>2</sub>, the carrier of X:] is Relation-like set
bool [: the carrier of c<sub>2</sub>, the carrier of X:] is non empty set
( the carrier of X, the carrier of c<sub>2</sub>,A) " A is Element of bool the carrier of c<sub>2</sub>
Cl (( the carrier of X, the carrier of c<sub>2</sub>,A) " A) is Element of bool the carrier of c<sub>2</sub>
( the carrier of X, the carrier of c<sub>2</sub>,A) " (Cl A) is Element of bool the carrier of c<sub>2</sub>
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<sub>2</sub>
A .: A is Element of bool the carrier of c<sub>2</sub>
Cl (A .: A) is Element of bool the carrier of c<sub>2</sub>
A is Element of bool the carrier of X
( the carrier of X, the carrier of c<sub>2</sub>,A) " A is Element of bool the carrier of c<sub>2</sub>
A .: A is Element of bool the carrier of c<sub>2</sub>
Cl A is Element of bool the carrier of X
( the carrier of X, the carrier of c<sub>2</sub>,A) " (Cl A) is Element of bool the carrier of c<sub>2</sub>
A .: (Cl A) is Element of bool the carrier of c<sub>2</sub>
Cl (( the carrier of X, the carrier of c<sub>2</sub>,A) " A) is Element of bool the carrier of c<sub>2</sub>
X is non empty TopSpace-like TopStruct
the carrier of X is non empty set
c<sub>2</sub> is non empty TopSpace-like TopStruct
the carrier of c<sub>2</sub> is non empty set
[: the carrier of X, the carrier of c<sub>2</sub>:] is non empty Relation-like set
bool [: the carrier of X, the carrier of c<sub>2</sub>:] 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 c<sub>2</sub> -valued Function-like V17( the carrier of X) quasi_total Element of bool [: the carrier of X, the carrier of c<sub>2</sub>:]
A is Element of bool the carrier of X
A .: A is Element of bool the carrier of c<sub>2</sub>
bool the carrier of c<sub>2</sub> is non empty set
{} c<sub>2</sub> 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 c<sub>2</sub>
u is Element of bool the carrier of c<sub>2</sub>
y is Element of bool the carrier of c<sub>2</sub>
u \/ y is Element of bool the carrier of c<sub>2</sub>
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<sub>2</sub>
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<sub>2</sub>
A " (u /\ (Cl y)) is Element of bool the carrier of X
A " ({} c<sub>2</sub>) 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
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<sub>2</sub>
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<sub>2</sub>
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<sub>15</sub> is Element of bool the carrier of X
c<sub>16</sub> is Element of bool the carrier of X
c<sub>15</sub> \/ c<sub>16</sub> is Element of bool the carrier of X
X is non empty TopSpace-like TopStruct
the carrier of X is non empty set
c<sub>2</sub> is non empty TopSpace-like TopStruct
the carrier of c<sub>2</sub> is non empty set
[: the carrier of X, the carrier of c<sub>2</sub>:] is non empty Relation-like set
bool [: the carrier of X, the carrier of c<sub>2</sub>:] is non empty set
bool the carrier of c<sub>2</sub> is non empty set
A is non empty Relation-like the carrier of X -defined the carrier of c<sub>2</sub> -valued Function-like V17( the carrier of X) quasi_total Element of bool [: the carrier of X, the carrier of c<sub>2</sub>:]
A is Element of bool the carrier of c<sub>2</sub>
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<sub>2</sub>,A) is non empty Relation-like the carrier of c<sub>2</sub> -defined the carrier of X -valued Function-like V17( the carrier of c<sub>2</sub>) quasi_total Element of bool [: the carrier of c<sub>2</sub>, the carrier of X:]
[: the carrier of c<sub>2</sub>, the carrier of X:] is non empty Relation-like set
bool [: the carrier of c<sub>2</sub>, the carrier of X:] is non empty set
( the carrier of X, the carrier of c<sub>2</sub>,A) .: A is Element of bool the carrier of X
rng A is non empty Element of bool the carrier of c<sub>2</sub>
[#] c<sub>2</sub> is non empty non proper closed Element of bool the carrier of c<sub>2</sub>
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<sub>2</sub> is Element of bool the carrier of X
A is Element of bool the carrier of X
c<sub>2</sub> \/ A is Element of bool the carrier of X
the Element of A is Element of A
the Element of c<sub>2</sub> is Element of c<sub>2</sub>
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<sub>2</sub> is Element of bool the carrier of GY
f " A is Element of bool the carrier of GY
(f " c<sub>2</sub>) \/ (f " A) is Element of bool the carrier of GY
(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<sub>2</sub> is Element of bool the carrier of X
(f " c<sub>2</sub>) /\ (f " A) is Element of bool the carrier of GY
c<sub>2</sub> /\ A is Element of bool the carrier of X
f " (c<sub>2</sub> /\ 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)
c<sub>2</sub> 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)
c<sub>2</sub> 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