:: PROB_1 semantic presentation

REAL is non empty V52() V65() V66() V67() V71() set
NAT is non empty epsilon-transitive epsilon-connected ordinal V65() V66() V67() V68() V69() V70() V71() Element of bool REAL
bool REAL is non empty set
COMPLEX is non empty V52() V65() V71() set
omega is non empty epsilon-transitive epsilon-connected ordinal V65() V66() V67() V68() V69() V70() V71() set
bool omega is non empty set
bool NAT is non empty set
RAT is non empty V52() V65() V66() V67() V68() V71() set
INT is non empty V52() V65() V66() V67() V68() V69() V71() set
{} is empty ext-real non positive non negative epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V21() real Relation-like non-empty empty-yielding RAT -valued Function-like one-to-one constant functional complex-valued ext-real-valued real-valued natural-valued V65() V66() V67() V68() V69() V70() V71() set
0 is empty ext-real non positive non negative epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V21() real Relation-like non-empty empty-yielding RAT -valued Function-like one-to-one constant functional complex-valued ext-real-valued real-valued natural-valued V65() V66() V67() V68() V69() V70() V71() Element of NAT
[:NAT,REAL:] is non empty Relation-like complex-valued ext-real-valued real-valued set
bool [:NAT,REAL:] is non empty set
X is ext-real V21() real set
Y is Relation-like NAT -defined REAL -valued Function-like V37( NAT , REAL ) complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]
lim Y is ext-real V21() real Element of REAL
A is ext-real epsilon-transitive epsilon-connected ordinal natural V21() real V65() V66() V67() V68() V69() V70() Element of NAT
A is ext-real epsilon-transitive epsilon-connected ordinal natural V21() real V65() V66() V67() V68() V69() V70() Element of NAT
F is ext-real V21() real set
x is ext-real epsilon-transitive epsilon-connected ordinal natural V21() real V65() V66() V67() V68() V69() V70() Element of NAT
Y . x is ext-real V21() real Element of REAL
(Y . x) - X is ext-real V21() real Element of REAL
abs ((Y . x) - X) is ext-real V21() real Element of REAL
X is set
bool X is non empty set
bool (bool X) is non empty set
X is set
bool X is non empty Element of bool (bool X)
bool X is non empty set
bool (bool X) is non empty set
Y is set
A is set
Y /\ A is set
X is set
bool X is non empty cap-closed set
bool (bool X) is non empty cap-closed set
bool X is non empty cap-closed Element of bool (bool X)
Y is Element of bool X
Y ` is Element of bool X
X \ Y is set
Y is Element of bool (bool X)
X is set
bool X is non empty cap-closed set
bool (bool X) is non empty cap-closed set
bool X is non empty cap-closed (X) Element of bool (bool X)
X is set
bool X is non empty cap-closed set
bool (bool X) is non empty cap-closed set
Y is Element of bool X
A is Element of bool X
{Y,A} is non empty set
bool X is non empty cap-closed (X) Element of bool (bool X)
x is set
X is set
bool X is non empty cap-closed set
bool (bool X) is non empty cap-closed set
Y is non empty cap-closed (X) Element of bool (bool X)
A is set
F is set
A \/ F is set
x is Element of bool X
x ` is Element of bool X
X \ x is set
Z is Element of bool X
Z ` is Element of bool X
X \ Z is set
(x `) /\ (Z `) is Element of bool X
x \/ Z is Element of bool X
(x \/ Z) ` is Element of bool X
X \ (x \/ Z) is set
((x \/ Z) `) ` is Element of bool X
X \ ((x \/ Z) `) is set
X is set
bool X is non empty cap-closed set
bool (bool X) is non empty cap-closed set
Y is non empty cap-closed (X) Element of bool (bool X)
A is Element of bool X
A ` is Element of bool X
X \ A is set
A /\ (A `) is Element of bool X
X is set
bool X is non empty cap-closed set
bool (bool X) is non empty cap-closed set
Y is non empty cap-closed (X) Element of bool (bool X)
A is Element of bool X
A ` is Element of bool X
X \ A is set
A \/ (A `) is Element of bool X
[#] X is non proper Element of bool X
X is set
bool X is non empty cap-closed set
bool (bool X) is non empty cap-closed set
Y is non empty cap-closed (X) Element of bool (bool X)
A is Element of bool X
F is Element of bool X
A \ F is Element of bool X
F ` is Element of bool X
X \ F is set
A /\ (F `) is Element of bool X
X is set
bool X is non empty cap-closed set
bool (bool X) is non empty cap-closed set
Y is non empty cap-closed (X) Element of bool (bool X)
A is set
F is set
A \ F is Element of bool A
bool A is non empty cap-closed set
(A \ F) \/ F is set
A \/ F is set
X is set
{{},X} is non empty set
Y is set
A is set
Y /\ A is set
X is set
{{},X} is non empty cap-closed set
bool X is non empty cap-closed set
bool (bool X) is non empty cap-closed set
bool X is non empty cap-closed (X) Element of bool (bool X)
A is Element of bool X
A ` is Element of bool X
X \ A is set
{} X is empty ext-real non positive non negative epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V21() real Relation-like non-empty empty-yielding RAT -valued Function-like one-to-one constant functional complex-valued ext-real-valued real-valued natural-valued V65() V66() V67() V68() V69() V70() V71() Element of bool X
Y is Element of bool (bool X)
X is set
bool X is non empty cap-closed (X) Element of bool (bool X)
bool X is non empty cap-closed set
bool (bool X) is non empty cap-closed set
X is set
bool X is non empty cap-closed set
bool (bool X) is non empty cap-closed set
{{},X} is non empty cap-closed set
bool X is non empty cap-closed (X) Element of bool (bool X)
Y is non empty cap-closed (X) Element of bool (bool X)
A is set
X is set
bool X is non empty cap-closed (X) Element of bool (bool X)
bool X is non empty cap-closed set
bool (bool X) is non empty cap-closed set
[:NAT,(bool X):] is non empty Relation-like set
bool [:NAT,(bool X):] is non empty cap-closed set
Y is Relation-like NAT -defined bool X -valued Function-like V37( NAT , bool X) Element of bool [:NAT,(bool X):]
rng Y is set
union (rng Y) is set
A is set
dom Y is set
F is set
Y . F is set
x is ext-real epsilon-transitive epsilon-connected ordinal natural V21() real V65() V66() V67() V68() V69() V70() Element of NAT
Y . x is Element of bool X
X is set
bool X is non empty cap-closed (X) Element of bool (bool X)
bool X is non empty cap-closed set
bool (bool X) is non empty cap-closed set
[:NAT,(bool X):] is non empty Relation-like set
bool [:NAT,(bool X):] is non empty cap-closed set
Y is Relation-like NAT -defined bool X -valued Function-like V37( NAT , bool X) Element of bool [:NAT,(bool X):]
Union Y is set
rng Y is set
union (rng Y) is set
X is set
bool X is non empty cap-closed (X) Element of bool (bool X)
bool X is non empty cap-closed set
bool (bool X) is non empty cap-closed set
[:NAT,(bool X):] is non empty Relation-like set
bool [:NAT,(bool X):] is non empty cap-closed set
Y is set
A is Relation-like NAT -defined bool X -valued Function-like V37( NAT , bool X) Element of bool [:NAT,(bool X):]
(X,A) is Element of bool X
rng A is set
union (rng A) is set
x is set
Z is set
dom A is set
Z is set
A . Z is set
Z is ext-real epsilon-transitive epsilon-connected ordinal natural V21() real V65() V66() V67() V68() V69() V70() Element of NAT
A . Z is Element of bool X
dom A is set
x is ext-real epsilon-transitive epsilon-connected ordinal natural V21() real V65() V66() V67() V68() V69() V70() Element of NAT
A . x is Element of bool X
X is set
bool X is non empty cap-closed (X) Element of bool (bool X)
bool X is non empty cap-closed set
bool (bool X) is non empty cap-closed set
[:NAT,(bool X):] is non empty Relation-like set
bool [:NAT,(bool X):] is non empty cap-closed set
Y is Relation-like NAT -defined bool X -valued Function-like V37( NAT , bool X) Element of bool [:NAT,(bool X):]
A is Relation-like NAT -defined bool X -valued Function-like V37( NAT , bool X) Element of bool [:NAT,(bool X):]
A is Relation-like NAT -defined bool X -valued Function-like V37( NAT , bool X) Element of bool [:NAT,(bool X):]
F is ext-real epsilon-transitive epsilon-connected ordinal natural V21() real V65() V66() V67() V68() V69() V70() Element of NAT
A . F is Element of bool X
Y . F is Element of bool X
(Y . F) ` is Element of bool X
X \ (Y . F) is set
A is Relation-like NAT -defined bool X -valued Function-like V37( NAT , bool X) Element of bool [:NAT,(bool X):]
F is Relation-like NAT -defined bool X -valued Function-like V37( NAT , bool X) Element of bool [:NAT,(bool X):]
x is set
A . x is set
F . x is set
Z is ext-real epsilon-transitive epsilon-connected ordinal natural V21() real V65() V66() V67() V68() V69() V70() Element of NAT
A . Z is Element of bool X
Y . Z is Element of bool X
(Y . Z) ` is Element of bool X
X \ (Y . Z) is set
F . Z is Element of bool X
dom A is set
dom F is set
A is Relation-like NAT -defined bool X -valued Function-like V37( NAT , bool X) Element of bool [:NAT,(bool X):]
F is Relation-like NAT -defined bool X -valued Function-like V37( NAT , bool X) Element of bool [:NAT,(bool X):]
x is ext-real epsilon-transitive epsilon-connected ordinal natural V21() real V65() V66() V67() V68() V69() V70() Element of NAT
F . x is Element of bool X
A . x is Element of bool X
(A . x) ` is Element of bool X
X \ (A . x) is set
(F . x) ` is Element of bool X
X \ (F . x) is set
((F . x) `) ` is Element of bool X
X \ ((F . x) `) is set
X is set
bool X is non empty cap-closed (X) Element of bool (bool X)
bool X is non empty cap-closed set
bool (bool X) is non empty cap-closed set
[:NAT,(bool X):] is non empty Relation-like set
bool [:NAT,(bool X):] is non empty cap-closed set
Y is Relation-like NAT -defined bool X -valued Function-like V37( NAT , bool X) Element of bool [:NAT,(bool X):]
(X,Y) is Relation-like NAT -defined bool X -valued Function-like V37( NAT , bool X) Element of bool [:NAT,(bool X):]
(X,(X,Y)) is Element of bool X
rng (X,Y) is set
union (rng (X,Y)) is set
(X,(X,Y)) ` is Element of bool X
X \ (X,(X,Y)) is set
X is set
bool X is non empty cap-closed (X) Element of bool (bool X)
bool X is non empty cap-closed set
bool (bool X) is non empty cap-closed set
[:NAT,(bool X):] is non empty Relation-like set
bool [:NAT,(bool X):] is non empty cap-closed set
Y is set
A is Relation-like NAT -defined bool X -valued Function-like V37( NAT , bool X) Element of bool [:NAT,(bool X):]
(X,A) is Element of bool X
(X,A) is Relation-like NAT -defined bool X -valued Function-like V37( NAT , bool X) Element of bool [:NAT,(bool X):]
(X,(X,A)) is Element of bool X
rng (X,A) is set
union (rng (X,A)) is set
(X,(X,A)) ` is Element of bool X
X \ (X,(X,A)) is set
F is ext-real epsilon-transitive epsilon-connected ordinal natural V21() real V65() V66() V67() V68() V69() V70() Element of NAT
(X,A) . F is Element of bool X
X \ ((X,A) . F) is Element of bool X
A . F is Element of bool X
(A . F) ` is Element of bool X
X \ (A . F) is set
((A . F) `) ` is Element of bool X
X \ ((A . F) `) is set
F is ext-real epsilon-transitive epsilon-connected ordinal natural V21() real V65() V66() V67() V68() V69() V70() Element of NAT
A . F is Element of bool X
(X,A) . F is Element of bool X
X \ ((X,A) . F) is Element of bool X
F is ext-real epsilon-transitive epsilon-connected ordinal natural V21() real V65() V66() V67() V68() V69() V70() Element of NAT
(X,A) . F is Element of bool X
A . F is Element of bool X
X \ ((X,A) . F) is Element of bool X
F is ext-real epsilon-transitive epsilon-connected ordinal natural V21() real V65() V66() V67() V68() V69() V70() Element of NAT
(X,A) . F is Element of bool X
F is ext-real epsilon-transitive epsilon-connected ordinal natural V21() real V65() V66() V67() V68() V69() V70() Element of NAT
A . F is Element of bool X
x is ext-real epsilon-transitive epsilon-connected ordinal natural V21() real V65() V66() V67() V68() V69() V70() Element of NAT
(X,A) . x is Element of bool X
Z is ext-real epsilon-transitive epsilon-connected ordinal natural V21() real V65() V66() V67() V68() V69() V70() Element of NAT
(X,A) . Z is Element of bool X
Z is ext-real epsilon-transitive epsilon-connected ordinal natural V21() real V65() V66() V67() V68() V69() V70() Element of NAT
A . Z is Element of bool X
X is set
bool X is non empty cap-closed set
Y is Element of bool X
A is Element of bool X
Y followed_by A is Relation-like NAT -defined bool X -valued Function-like V37( NAT , bool X) Element of bool [:NAT,(bool X):]
[:NAT,(bool X):] is non empty Relation-like set
bool [:NAT,(bool X):] is non empty cap-closed set
(X,(Y followed_by A)) is Relation-like NAT -defined bool X -valued Function-like V37( NAT , bool X) Element of bool [:NAT,(bool X):]
bool X is non empty cap-closed (X) Element of bool (bool X)
bool (bool X) is non empty cap-closed set
[:NAT,(bool X):] is non empty Relation-like set
bool [:NAT,(bool X):] is non empty cap-closed set
Y ` is Element of bool X
X \ Y is set
A ` is Element of bool X
X \ A is set
(Y `) followed_by (A `) is Relation-like NAT -defined bool X -valued Function-like V37( NAT , bool X) Element of bool [:NAT,(bool X):]
F is ext-real epsilon-transitive epsilon-connected ordinal natural V21() real V65() V66() V67() V68() V69() V70() Element of NAT
(X,(Y followed_by A)) . F is set
((Y `) followed_by (A `)) . F is set
(X,(Y followed_by A)) . F is Element of bool X
(Y followed_by A) . F is Element of bool X
((Y followed_by A) . F) ` is Element of bool X
X \ ((Y followed_by A) . F) is set
((Y `) followed_by (A `)) . F is Element of bool X
(X,(Y followed_by A)) . F is Element of bool X
(Y followed_by A) . F is Element of bool X
((Y followed_by A) . F) ` is Element of bool X
X \ ((Y followed_by A) . F) is set
((Y `) followed_by (A `)) . F is Element of bool X
X is set
bool X is non empty cap-closed set
Y is Element of bool X
A is Element of bool X
Y followed_by A is Relation-like NAT -defined bool X -valued Function-like V37( NAT , bool X) Element of bool [:NAT,(bool X):]
[:NAT,(bool X):] is non empty Relation-like set
bool [:NAT,(bool X):] is non empty cap-closed set
(X,(Y followed_by A)) is Element of bool X
(X,(Y followed_by A)) is Relation-like NAT -defined bool X -valued Function-like V37( NAT , bool X) Element of bool [:NAT,(bool X):]
bool X is non empty cap-closed (X) Element of bool (bool X)
bool (bool X) is non empty cap-closed set
[:NAT,(bool X):] is non empty Relation-like set
bool [:NAT,(bool X):] is non empty cap-closed set
(X,(X,(Y followed_by A))) is Element of bool X
rng (X,(Y followed_by A)) is set
union (rng (X,(Y followed_by A))) is set
(X,(X,(Y followed_by A))) ` is Element of bool X
X \ (X,(X,(Y followed_by A))) is set
Y /\ A is Element of bool X
Y ` is Element of bool X
X \ Y is set
A ` is Element of bool X
X \ A is set
(Y `) followed_by (A `) is Relation-like NAT -defined bool X -valued Function-like V37( NAT , bool X) Element of bool [:NAT,(bool X):]
{(Y `),(A `)} is non empty set
(Y `) \/ (A `) is Element of bool X
(Y `) ` is Element of bool X
X \ (Y `) is set
(A `) ` is Element of bool X
X \ (A `) is set
((Y `) `) /\ ((A `) `) is Element of bool X
X is set
bool X is non empty cap-closed set
bool (bool X) is non empty cap-closed set
X is set
bool X is non empty cap-closed set
bool (bool X) is non empty cap-closed set
bool X is non empty cap-closed (X) Element of bool (bool X)
[:NAT,(bool X):] is non empty Relation-like set
bool [:NAT,(bool X):] is non empty cap-closed set
Y is Relation-like NAT -defined bool X -valued Function-like V37( NAT , bool X) Element of bool [:NAT,(bool X):]
rng Y is set
(X,Y) is Element of bool X
(X,Y) is Relation-like NAT -defined bool X -valued Function-like V37( NAT , bool X) Element of bool [:NAT,(bool X):]
(X,(X,Y)) is Element of bool X
rng (X,Y) is set
union (rng (X,Y)) is set
(X,(X,Y)) ` is Element of bool X
X \ (X,(X,Y)) is set
Y is Element of bool (bool X)
X is set
bool X is non empty cap-closed set
bool (bool X) is non empty cap-closed set
bool X is non empty cap-closed (X) (X) Element of bool (bool X)
X is set
bool X is non empty cap-closed (X) (X) Element of bool (bool X)
bool X is non empty cap-closed set
bool (bool X) is non empty cap-closed set
[:NAT,(bool X):] is non empty Relation-like set
bool [:NAT,(bool X):] is non empty cap-closed set
Y is non empty set
A is Relation-like NAT -defined bool X -valued Function-like V37( NAT , bool X) Element of bool [:NAT,(bool X):]
rng A is set
(X,A) is Element of bool X
(X,A) is Relation-like NAT -defined bool X -valued Function-like V37( NAT , bool X) Element of bool [:NAT,(bool X):]
(X,(X,A)) is Element of bool X
rng (X,A) is set
union (rng (X,A)) is set
(X,(X,A)) ` is Element of bool X
X \ (X,(X,A)) is set
F is Element of bool X
F ` is Element of bool X
X \ F is set
Z is non empty set
x is set
bool x is non empty cap-closed (x) (x) Element of bool (bool x)
bool x is non empty cap-closed set
bool (bool x) is non empty cap-closed set
[:NAT,(bool x):] is non empty Relation-like set
bool [:NAT,(bool x):] is non empty cap-closed set
X is set
Y is set
bool Y is non empty cap-closed set
bool (bool Y) is non empty cap-closed set
A is set
F is set
A /\ F is set
x is Element of bool Y
Z is Element of bool Y
x followed_by Z is Relation-like NAT -defined bool Y -valued Function-like V37( NAT , bool Y) Element of bool [:NAT,(bool Y):]
[:NAT,(bool Y):] is non empty Relation-like set
bool [:NAT,(bool Y):] is non empty cap-closed set
rng (x followed_by Z) is set
{x,Z} is non empty set
(Y,(x followed_by Z)) is Element of bool Y
(Y,(x followed_by Z)) is Relation-like NAT -defined bool Y -valued Function-like V37( NAT , bool Y) Element of bool [:NAT,(bool Y):]
bool Y is non empty cap-closed (Y) (Y) Element of bool (bool Y)
[:NAT,(bool Y):] is non empty Relation-like set
bool [:NAT,(bool Y):] is non empty cap-closed set
(Y,(Y,(x followed_by Z))) is Element of bool Y
rng (Y,(x followed_by Z)) is set
union (rng (Y,(x followed_by Z))) is set
(Y,(Y,(x followed_by Z))) ` is Element of bool Y
Y \ (Y,(Y,(x followed_by Z))) is set
X is set
bool X is non empty cap-closed set
bool (bool X) is non empty cap-closed set
Y is non empty (X) (X) Element of bool (bool X)
A is non empty (X) (X) Element of bool (bool X)
X is set
bool X is non empty cap-closed set
bool (bool X) is non empty cap-closed set
bool X is non empty cap-closed (X) (X) Element of bool (bool X)
[:NAT,(bool X):] is non empty Relation-like set
bool [:NAT,(bool X):] is non empty cap-closed set
Y is non empty Element of bool (bool X)
the Element of Y is Element of Y
NAT --> the Element of Y is Relation-like NAT -defined Y -valued Function-like V37( NAT ,Y) Element of bool [:NAT,Y:]
[:NAT,Y:] is non empty Relation-like set
bool [:NAT,Y:] is non empty cap-closed set
F is Relation-like NAT -defined bool X -valued Function-like V37( NAT , bool X) Element of bool [:NAT,(bool X):]
X is set
bool X is non empty cap-closed set
bool (bool X) is non empty cap-closed set
X is set
bool X is non empty cap-closed set
bool (bool X) is non empty cap-closed set
bool X is non empty cap-closed (X) (X) Element of bool (bool X)
[:NAT,(bool X):] is non empty Relation-like set
bool [:NAT,(bool X):] is non empty cap-closed set
Y is non empty cap-closed (X) (X) Element of bool (bool X)
A is Relation-like NAT -defined bool X -valued Y -valued Function-like V37( NAT , bool X) Element of bool [:NAT,(bool X):]
(X,A) is Element of bool X
rng A is set
union (rng A) is set
F is Relation-like NAT -defined bool X -valued Function-like V37( NAT , bool X) Element of bool [:NAT,(bool X):]
rng F is set
(X,F) is Relation-like NAT -defined bool X -valued Function-like V37( NAT , bool X) Element of bool [:NAT,(bool X):]
x is ext-real epsilon-transitive epsilon-connected ordinal natural V21() real set
(X,F) . x is Element of bool X
F . x is Element of bool X
(F . x) ` is Element of bool X
X \ (F . x) is set
F is Relation-like NAT -defined bool X -valued Function-like V37( NAT , bool X) Element of bool [:NAT,(bool X):]
rng F is set
(X,F) is Relation-like NAT -defined bool X -valued Function-like V37( NAT , bool X) Element of bool [:NAT,(bool X):]
(X,(X,F)) is Relation-like NAT -defined bool X -valued Function-like V37( NAT , bool X) Element of bool [:NAT,(bool X):]
(X,(X,(X,F))) is Element of bool X
rng (X,(X,F)) is set
union (rng (X,(X,F))) is set
x is ext-real epsilon-transitive epsilon-connected ordinal natural V21() real set
(X,F) . x is Element of bool X
rng (X,F) is set
(X,(X,F)) is Element of bool X
(X,(X,(X,F))) ` is Element of bool X
X \ (X,(X,(X,F))) is set
((X,(X,(X,F))) `) ` is Element of bool X
X \ ((X,(X,(X,F))) `) is set
F is Relation-like NAT -defined bool X -valued Function-like V37( NAT , bool X) Element of bool [:NAT,(bool X):]
rng F is set
(X,F) is Element of bool X
union (rng F) is set
(X,F) is Relation-like NAT -defined bool X -valued Function-like V37( NAT , bool X) Element of bool [:NAT,(bool X):]
(X,(X,F)) is Relation-like NAT -defined bool X -valued Function-like V37( NAT , bool X) Element of bool [:NAT,(bool X):]
(X,(X,(X,F))) is Element of bool X
rng (X,(X,F)) is set
union (rng (X,(X,F))) is set
X is set
bool X is non empty cap-closed set
bool (bool X) is non empty cap-closed set
X is set
bool X is non empty cap-closed set
bool (bool X) is non empty cap-closed set
Y is non empty cap-closed (X) (X) Element of bool (bool X)
A is Element of Y
X is set
bool X is non empty cap-closed set
bool (bool X) is non empty cap-closed set
Y is set
A is non empty cap-closed (X) (X) Element of bool (bool X)
X is set
bool X is non empty cap-closed set
bool (bool X) is non empty cap-closed set
Y is non empty cap-closed (X) (X) Element of bool (bool X)
A is (X,Y)
F is (X,Y)
A /\ F is Element of bool X
X is set
bool X is non empty cap-closed set
bool (bool X) is non empty cap-closed set
Y is non empty cap-closed (X) (X) Element of bool (bool X)
A is (X,Y)
A ` is Element of bool X
X \ A is set
X is set
bool X is non empty cap-closed set
bool (bool X) is non empty cap-closed set
Y is non empty cap-closed (X) (X) Element of bool (bool X)
A is (X,Y)
F is (X,Y)
A \/ F is Element of bool X
X is set
bool X is non empty cap-closed set
bool (bool X) is non empty cap-closed set
Y is non empty cap-closed (X) (X) Element of bool (bool X)
X is set
bool X is non empty cap-closed set
bool (bool X) is non empty cap-closed set
Y is non empty cap-closed (X) (X) Element of bool (bool X)
X is set
bool X is non empty cap-closed set
bool (bool X) is non empty cap-closed set
Y is non empty cap-closed (X) (X) Element of bool (bool X)
A is (X,Y)
F is (X,Y)
A \ F is Element of bool X
X is set
bool X is non empty cap-closed set
bool (bool X) is non empty cap-closed set
Y is non empty cap-closed (X) (X) Element of bool (bool X)
X is set
bool X is non empty cap-closed set
bool (bool X) is non empty cap-closed set
Y is non empty cap-closed (X) (X) Element of bool (bool X)
X is set
bool X is non empty cap-closed set
bool (bool X) is non empty cap-closed set
Y is non empty cap-closed (X) (X) Element of bool (bool X)
A is (X,Y)
F is (X,Y)
A /\ F is set
A \/ F is set
A \ F is set
X is set
bool X is non empty cap-closed (X) (X) Element of bool (bool X)
bool X is non empty cap-closed set
bool (bool X) is non empty cap-closed set
[:NAT,(bool X):] is non empty Relation-like set
bool [:NAT,(bool X):] is non empty cap-closed set
Y is Relation-like NAT -defined bool X -valued Function-like V37( NAT , bool X) Element of bool [:NAT,(bool X):]
A is non empty cap-closed (X) (X) Element of bool (bool X)
rng Y is set
F is ext-real epsilon-transitive epsilon-connected ordinal natural V21() real V65() V66() V67() V68() V69() V70() Element of NAT
Y . F is Element of bool X
F is ext-real epsilon-transitive epsilon-connected ordinal natural V21() real V65() V66() V67() V68() V69() V70() Element of NAT
Y . F is Element of bool X
F is ext-real epsilon-transitive epsilon-connected ordinal natural V21() real set
Y . F is Element of bool X
rng Y is set
X is set
bool X is non empty cap-closed (X) (X) Element of bool (bool X)
bool X is non empty cap-closed set
bool (bool X) is non empty cap-closed set
[:NAT,(bool X):] is non empty Relation-like set
bool [:NAT,(bool X):] is non empty cap-closed set
Y is Relation-like NAT -defined bool X -valued Function-like V37( NAT , bool X) Element of bool [:NAT,(bool X):]
A is non empty cap-closed (X) (X) Element of bool (bool X)
(X,Y) is Element of bool X
rng Y is set
union (rng Y) is set
1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V21() real V65() V66() V67() V68() V69() V70() Element of NAT
X is set
bool X is non empty cap-closed set
bool (bool X) is non empty cap-closed set
Y is set
A is non empty cap-closed (X) (X) Element of bool (bool X)
F is Relation-like Function-like set
dom F is set
F is Relation-like Function-like set
dom F is set
x is Element of bool X
F . x is set
X is set
bool X is non empty cap-closed set
bool (bool X) is non empty cap-closed set
Y is set
A is non empty cap-closed (X) (X) Element of bool (bool X)
[:A,REAL:] is non empty Relation-like complex-valued ext-real-valued real-valued set
bool [:A,REAL:] is non empty cap-closed set
F is Relation-like Function-like set
dom F is set
rng F is set
x is set
Z is set
F . Z is set
Z is Element of bool X
x is Relation-like A -defined REAL -valued Function-like V37(A, REAL ) complex-valued ext-real-valued real-valued Element of bool [:A,REAL:]
Z is Element of bool X
x . Z is ext-real V21() real Element of REAL
X is set
bool X is non empty cap-closed set
bool (bool X) is non empty cap-closed set
bool X is non empty cap-closed (X) (X) Element of bool (bool X)
[:NAT,(bool X):] is non empty Relation-like set
bool [:NAT,(bool X):] is non empty cap-closed set
Y is non empty cap-closed (X) (X) Element of bool (bool X)
[:Y,REAL:] is non empty Relation-like complex-valued ext-real-valued real-valued set
bool [:Y,REAL:] is non empty cap-closed set
A is Relation-like NAT -defined bool X -valued Y -valued Function-like V37( NAT , bool X) Element of bool [:NAT,(bool X):]
F is Relation-like Y -defined REAL -valued Function-like V37(Y, REAL ) complex-valued ext-real-valued real-valued Element of bool [:Y,REAL:]
A * F is Relation-like NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued set
rng A is set
dom F is set
dom (A * F) is set
dom A is set
rng (A * F) is V65() V66() V67() set
X is set
bool X is non empty cap-closed set
bool (bool X) is non empty cap-closed set
Y is non empty cap-closed (X) (X) Element of bool (bool X)
bool X is non empty cap-closed (X) (X) Element of bool (bool X)
[:NAT,(bool X):] is non empty Relation-like set
bool [:NAT,(bool X):] is non empty cap-closed set
[:Y,REAL:] is non empty Relation-like complex-valued ext-real-valued real-valued set
bool [:Y,REAL:] is non empty cap-closed set
A is Relation-like NAT -defined Y -valued bool X -valued Function-like V37( NAT , bool X) Element of bool [:NAT,(bool X):]
F is Relation-like Y -defined REAL -valued Function-like V37(Y, REAL ) complex-valued ext-real-valued real-valued Element of bool [:Y,REAL:]
A * F is Relation-like NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued set
X is non empty set
bool X is non empty cap-closed set
bool (bool X) is non empty cap-closed set
Y is non empty cap-closed (X) (X) Element of bool (bool X)
[:Y,REAL:] is non empty Relation-like complex-valued ext-real-valued real-valued set
bool [:Y,REAL:] is non empty cap-closed set
bool X is non empty cap-closed (X) (X) Element of bool (bool X)
[:NAT,(bool X):] is non empty Relation-like set
bool [:NAT,(bool X):] is non empty cap-closed set
the Element of X is Element of X
F is Relation-like Y -defined REAL -valued Function-like V37(Y, REAL ) complex-valued ext-real-valued real-valued Element of bool [:Y,REAL:]
F . X is ext-real V21() real Element of REAL
x is (X,Y)
F . x is ext-real V21() real Element of REAL
(X,Y) is (X,Y)
x is (X,Y)
F . x is ext-real V21() real Element of REAL
Z is (X,Y)
(X,Y,x,Z) is (X,Y)
F . (X,Y,x,Z) is ext-real V21() real Element of REAL
F . Z is ext-real V21() real Element of REAL
(F . x) + (F . Z) is ext-real V21() real Element of REAL
x is Relation-like NAT -defined Y -valued bool X -valued Function-like V37( NAT , bool X) Element of bool [:NAT,(bool X):]
(X,Y,x,F) is Relation-like NAT -defined REAL -valued Function-like V37( NAT , REAL ) complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]
lim (X,Y,x,F) is ext-real V21() real Element of REAL
(X,x) is Element of bool X
(X,x) is Relation-like NAT -defined bool X -valued Function-like V37( NAT , bool X) Element of bool [:NAT,(bool X):]
(X,(X,x)) is Element of bool X
rng (X,x) is set
union (rng (X,x)) is set
(X,(X,x)) ` is Element of bool X
X \ (X,(X,x)) is set
F . (X,x) is ext-real V21() real Element of REAL
Z is ext-real epsilon-transitive epsilon-connected ordinal natural V21() real V65() V66() V67() V68() V69() V70() Element of NAT
(X,Y,x,F) . Z is ext-real V21() real Element of REAL
x . Z is Element of bool X
F . (x . Z) is ext-real V21() real Element of REAL
dom (X,Y,x,F) is set
Z is ext-real epsilon-transitive epsilon-connected ordinal natural V21() real V65() V66() V67() V68() V69() V70() Element of NAT
(X,Y,x,F) . Z is ext-real V21() real Element of REAL
rng x is set
x . Z is Element of bool X
F . (x . Z) is ext-real V21() real Element of REAL
Z is ext-real epsilon-transitive epsilon-connected ordinal natural V21() real V65() V66() V67() V68() V69() V70() Element of NAT
(X,Y,x,F) . Z is ext-real V21() real Element of REAL
Z is ext-real epsilon-transitive epsilon-connected ordinal natural V21() real V65() V66() V67() V68() V69() V70() Element of NAT
x . Z is Element of bool X
Z is ext-real epsilon-transitive epsilon-connected ordinal natural V21() real V65() V66() V67() V68() V69() V70() Element of NAT
x . Z is Element of bool X
Z is ext-real epsilon-transitive epsilon-connected ordinal natural V21() real V65() V66() V67() V68() V69() V70() Element of NAT
(X,Y,x,F) . Z is ext-real V21() real Element of REAL
x . Z is Element of bool X
rng x is set
F . (x . Z) is ext-real V21() real Element of REAL
Z is ext-real epsilon-transitive epsilon-connected ordinal natural V21() real V65() V66() V67() V68() V69() V70() Element of NAT
(X,Y,x,F) . Z is ext-real V21() real Element of REAL
Z is ext-real epsilon-transitive epsilon-connected ordinal natural V21() real V65() V66() V67() V68() V69() V70() Element of NAT
rng x is set
Z is ext-real V21() real Element of REAL
Z is ext-real epsilon-transitive epsilon-connected ordinal natural V21() real V65() V66() V67() V68() V69() V70() Element of NAT
(X,Y,x,F) . Z is ext-real V21() real Element of REAL
Z is ext-real epsilon-transitive epsilon-connected ordinal natural V21() real V65() V66() V67() V68() V69() V70() Element of NAT
Z is ext-real epsilon-transitive epsilon-connected ordinal natural V21() real V65() V66() V67() V68() V69() V70() Element of NAT
x . Z is Element of bool X
Z is ext-real epsilon-transitive epsilon-connected ordinal natural V21() real V65() V66() V67() V68() V69() V70() Element of NAT
c<sub>8</sub> is ext-real epsilon-transitive epsilon-connected ordinal natural V21() real V65() V66() V67() V68() V69() V70() Element of NAT
x . c<sub>8</sub> is Element of bool X
Z is ext-real epsilon-transitive epsilon-connected ordinal natural V21() real V65() V66() V67() V68() V69() V70() Element of NAT
x . Z is Element of bool X
c<sub>8</sub> is ext-real epsilon-transitive epsilon-connected ordinal natural V21() real V65() V66() V67() V68() V69() V70() Element of NAT
(X,Y,x,F) . c<sub>8</sub> is ext-real V21() real Element of REAL
Z is ext-real epsilon-transitive epsilon-connected ordinal natural V21() real V65() V66() V67() V68() V69() V70() Element of NAT
x . Z is Element of bool X
X is non empty set
bool X is non empty cap-closed set
bool (bool X) is non empty cap-closed set
Y is non empty cap-closed (X) (X) Element of bool (bool X)
F is Relation-like Y -defined REAL -valued Function-like V37(Y, REAL ) complex-valued ext-real-valued real-valued (X,Y)
(X,Y) is (X,Y)
{} \/ (X,Y) is set
F . (X,Y) is ext-real V21() real Element of REAL
A is (X,Y)
F . A is ext-real V21() real Element of REAL
(F . A) + 1 is ext-real V21() real Element of REAL
F . {} is ext-real V21() real Element of REAL
X is non empty set
bool X is non empty cap-closed set
bool (bool X) is non empty cap-closed set
Y is non empty cap-closed (X) (X) Element of bool (bool X)
A is Relation-like Y -defined REAL -valued Function-like V37(Y, REAL ) complex-valued ext-real-valued real-valued zeroed (X,Y)
(X,Y) is (X,Y)
A . (X,Y) is ext-real V21() real Element of REAL
X is non empty set
bool X is non empty cap-closed set
bool (bool X) is non empty cap-closed set
Y is non empty cap-closed (X) (X) Element of bool (bool X)
(X,Y) is (X,Y)
A is (X,Y)
(X,Y,(X,Y),A) is (X,Y)
F is Relation-like Y -defined REAL -valued Function-like V37(Y, REAL ) complex-valued ext-real-valued real-valued zeroed (X,Y)
F . (X,Y,(X,Y),A) is ext-real V21() real Element of REAL
F . A is ext-real V21() real Element of REAL
(F . (X,Y,(X,Y),A)) + (F . A) is ext-real V21() real Element of REAL
(X,Y,(X,Y,(X,Y),A),A) is (X,Y)
A ` is Element of bool X
X \ A is set
(A `) \/ A is Element of bool X
[#] X is non empty non proper Element of bool X
F . X is ext-real V21() real Element of REAL
X is non empty set
bool X is non empty cap-closed set
bool (bool X) is non empty cap-closed set
Y is non empty cap-closed (X) (X) Element of bool (bool X)
(X,Y) is (X,Y)
A is (X,Y)
(X,Y,(X,Y),A) is (X,Y)
F is Relation-like Y -defined REAL -valued Function-like V37(Y, REAL ) complex-valued ext-real-valued real-valued zeroed (X,Y)
F . (X,Y,(X,Y),A) is ext-real V21() real Element of REAL
F . A is ext-real V21() real Element of REAL
1 - (F . A) is ext-real V21() real Element of REAL
(F . (X,Y,(X,Y),A)) + (F . A) is ext-real V21() real Element of REAL
X is non empty set
bool X is non empty cap-closed set
bool (bool X) is non empty cap-closed set
Y is non empty cap-closed (X) (X) Element of bool (bool X)
A is (X,Y)
F is (X,Y)
(X,Y,F,A) is (X,Y)
x is Relation-like Y -defined REAL -valued Function-like V37(Y, REAL ) complex-valued ext-real-valued real-valued zeroed (X,Y)
x . (X,Y,F,A) is ext-real V21() real Element of REAL
x . F is ext-real V21() real Element of REAL
x . A is ext-real V21() real Element of REAL
(x . F) - (x . A) is ext-real V21() real Element of REAL
(x . A) + (x . (X,Y,F,A)) is ext-real V21() real Element of REAL
(X,Y,A,(X,Y,F,A)) is (X,Y)
x . (X,Y,A,(X,Y,F,A)) is ext-real V21() real Element of REAL
X is non empty set
bool X is non empty cap-closed set
bool (bool X) is non empty cap-closed set
Y is non empty cap-closed (X) (X) Element of bool (bool X)
A is (X,Y)
F is (X,Y)
x is Relation-like Y -defined REAL -valued Function-like V37(Y, REAL ) complex-valued ext-real-valued real-valued zeroed (X,Y)
x . A is ext-real V21() real Element of REAL
x . F is ext-real V21() real Element of REAL
(X,Y,F,A) is (X,Y)
x . (X,Y,F,A) is ext-real V21() real Element of REAL
(x . F) - (x . A) is ext-real V21() real Element of REAL
0 + (x . A) is ext-real V21() real Element of REAL
X is non empty set
bool X is non empty cap-closed set
bool (bool X) is non empty cap-closed set
Y is non empty cap-closed (X) (X) Element of bool (bool X)
A is (X,Y)
F is Relation-like Y -defined REAL -valued Function-like V37(Y, REAL ) complex-valued ext-real-valued real-valued zeroed (X,Y)
F . A is ext-real V21() real Element of REAL
(X,Y) is (X,Y)
F . (X,Y) is ext-real V21() real Element of REAL
X is non empty set
bool X is non empty cap-closed set
bool (bool X) is non empty cap-closed set
Y is non empty cap-closed (X) (X) Element of bool (bool X)
A is (X,Y)
F is (X,Y)
(X,Y,A,F) is (X,Y)
(X,Y,F,A) is (X,Y)
x is Relation-like Y -defined REAL -valued Function-like V37(Y, REAL ) complex-valued ext-real-valued real-valued zeroed (X,Y)
x . (X,Y,A,F) is ext-real V21() real Element of REAL
x . A is ext-real V21() real Element of REAL
x . (X,Y,F,A) is ext-real V21() real Element of REAL
(x . A) + (x . (X,Y,F,A)) is ext-real V21() real Element of REAL
(X,Y,A,(X,Y,F,A)) is (X,Y)
x . (X,Y,A,(X,Y,F,A)) is ext-real V21() real Element of REAL
X is non empty set
bool X is non empty cap-closed set
bool (bool X) is non empty cap-closed set
Y is non empty cap-closed (X) (X) Element of bool (bool X)
A is (X,Y)
F is (X,Y)
(X,Y,A,F) is (X,Y)
(X,Y,A,F) is (X,Y)
(X,Y,F,(X,Y,A,F)) is (X,Y)
x is Relation-like Y -defined REAL -valued Function-like V37(Y, REAL ) complex-valued ext-real-valued real-valued zeroed (X,Y)
x . (X,Y,A,F) is ext-real V21() real Element of REAL
x . A is ext-real V21() real Element of REAL
x . (X,Y,F,(X,Y,A,F)) is ext-real V21() real Element of REAL
(x . A) + (x . (X,Y,F,(X,Y,A,F))) is ext-real V21() real Element of REAL
(X,Y,F,A) is (X,Y)
x . (X,Y,F,A) is ext-real V21() real Element of REAL
(x . A) + (x . (X,Y,F,A)) is ext-real V21() real Element of REAL
X is non empty set
bool X is non empty cap-closed set
bool (bool X) is non empty cap-closed set
Y is non empty cap-closed (X) (X) Element of bool (bool X)
A is (X,Y)
F is (X,Y)
(X,Y,A,F) is (X,Y)
(X,Y,A,F) is (X,Y)
x is Relation-like Y -defined REAL -valued Function-like V37(Y, REAL ) complex-valued ext-real-valued real-valued zeroed (X,Y)
x . (X,Y,A,F) is ext-real V21() real Element of REAL
x . A is ext-real V21() real Element of REAL
x . F is ext-real V21() real Element of REAL
(x . A) + (x . F) is ext-real V21() real Element of REAL
x . (X,Y,A,F) is ext-real V21() real Element of REAL
((x . A) + (x . F)) - (x . (X,Y,A,F)) is ext-real V21() real Element of REAL
(X,Y,F,(X,Y,A,F)) is (X,Y)
x . (X,Y,F,(X,Y,A,F)) is ext-real V21() real Element of REAL
(x . A) + (x . (X,Y,F,(X,Y,A,F))) is ext-real V21() real Element of REAL
(x . F) - (x . (X,Y,A,F)) is ext-real V21() real Element of REAL
(x . A) + ((x . F) - (x . (X,Y,A,F))) is ext-real V21() real Element of REAL
X is non empty set
bool X is non empty cap-closed set
bool (bool X) is non empty cap-closed set
Y is non empty cap-closed (X) (X) Element of bool (bool X)
A is (X,Y)
F is (X,Y)
(X,Y,A,F) is (X,Y)
x is Relation-like Y -defined REAL -valued Function-like V37(Y, REAL ) complex-valued ext-real-valued real-valued zeroed (X,Y)
x . (X,Y,A,F) is ext-real V21() real Element of REAL
x . A is ext-real V21() real Element of REAL
x . F is ext-real V21() real Element of REAL
(x . A) + (x . F) is ext-real V21() real Element of REAL
(X,Y,A,F) is (X,Y)
x . (X,Y,A,F) is ext-real V21() real Element of REAL
((x . A) + (x . F)) - (x . (X,Y,A,F)) is ext-real V21() real Element of REAL
X is set
bool X is non empty cap-closed (X) (X) Element of bool (bool X)
bool X is non empty cap-closed set
bool (bool X) is non empty cap-closed set
X is non empty set
bool X is non empty cap-closed set
bool (bool X) is non empty cap-closed set
Y is Element of bool (bool X)
{ b<sub>1</sub> where b<sub>1</sub> is Element of bool (bool X) : ( Y c= b<sub>1</sub> & b<sub>1</sub> is non empty cap-closed (X) (X) Element of bool (bool X) ) } is set
meet { b<sub>1</sub> where b<sub>1</sub> is Element of bool (bool X) : ( Y c= b<sub>1</sub> & b<sub>1</sub> is non empty cap-closed (X) (X) Element of bool (bool X) ) } is set
x is set
Z is Element of bool (bool X)
bool X is non empty cap-closed (X) (X) Element of bool (bool X)
x is Element of bool X
x ` is Element of bool X
X \ x is set
Z is set
Z is Element of bool (bool X)
[:NAT,(bool X):] is non empty Relation-like set
bool [:NAT,(bool X):] is non empty cap-closed set
x is Relation-like NAT -defined bool X -valued Function-like V37( NAT , bool X) Element of bool [:NAT,(bool X):]
rng x is set
(X,x) is Element of bool X
(X,x) is Relation-like NAT -defined bool X -valued Function-like V37( NAT , bool X) Element of bool [:NAT,(bool X):]
(X,(X,x)) is Element of bool X
rng (X,x) is set
union (rng (X,x)) is set
(X,(X,x)) ` is Element of bool X
X \ (X,(X,x)) is set
Z is set
Z is ext-real epsilon-transitive epsilon-connected ordinal natural V21() real set
x . Z is Element of bool X
Z is Element of bool (bool X)
x is set
Z is Element of bool (bool X)
x is non empty cap-closed (X) (X) Element of bool (bool X)
Z is set
Z is Element of bool (bool X)
Z is set
A is non empty cap-closed (X) (X) Element of bool (bool X)
F is non empty cap-closed (X) (X) Element of bool (bool X)
-infty is non empty ext-real non positive negative non real set
X is ext-real set
].-infty,X.[ is V65() V66() V67() set
Y is ext-real V21() real set
{ (b<sub>1</sub>) where b<sub>1</sub> is ext-real V21() real Element of REAL : verum } is set
bool (bool REAL) is non empty cap-closed set
bool REAL is non empty cap-closed ( REAL ) ( REAL ) Element of bool (bool REAL)
X is set
Y is ext-real V21() real Element of REAL
(Y) is V65() V66() V67() Element of bool REAL
].-infty,Y.[ is V65() V66() V67() set
() is Element of bool (bool REAL)
(REAL,()) is non empty cap-closed ( REAL ) ( REAL ) Element of bool (bool REAL)
() is non empty cap-closed ( REAL ) ( REAL ) Element of bool (bool REAL)
X is set
bool X is non empty cap-closed set
Y is Element of bool X
A is Element of bool X
Y followed_by A is Relation-like NAT -defined bool X -valued Function-like V37( NAT , bool X) Element of bool [:NAT,(bool X):]
[:NAT,(bool X):] is non empty Relation-like set
bool [:NAT,(bool X):] is non empty cap-closed set
(X,(Y followed_by A)) is Relation-like NAT -defined bool X -valued Function-like V37( NAT , bool X) Element of bool [:NAT,(bool X):]
bool X is non empty cap-closed (X) (X) Element of bool (bool X)
bool (bool X) is non empty cap-closed set
[:NAT,(bool X):] is non empty Relation-like set
bool [:NAT,(bool X):] is non empty cap-closed set
Y ` is Element of bool X
X \ Y is set
A ` is Element of bool X
X \ A is set
(Y `) followed_by (A `) is Relation-like NAT -defined bool X -valued Function-like V37( NAT , bool X) Element of bool [:NAT,(bool X):]
X is set
bool X is non empty cap-closed set
bool (bool X) is non empty cap-closed set
Y is set
A is Element of bool (bool X)
bool A is non empty cap-closed (A) (A) Element of bool (bool A)
bool A is non empty cap-closed set
bool (bool A) is non empty cap-closed set
[:Y,(bool A):] is Relation-like set
bool [:Y,(bool A):] is non empty cap-closed set
F is Relation-like Y -defined bool A -valued Function-like V37(Y, bool A) Element of bool [:Y,(bool A):]
x is set
F . x is set
dom F is set
rng F is set
bool X is non empty cap-closed (X) (X) Element of bool (bool X)
bool (bool X) is non empty cap-closed ( bool X) ( bool X) Element of bool (bool (bool X))
bool (bool X) is non empty cap-closed set
bool (bool (bool X)) is non empty cap-closed set
dom F is set
dom F is set