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

x . c

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

(X,Y,x,F) . c

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

meet { b

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

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