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

bool is non empty set
X is ext-real V21() real set

F is ext-real V21() real set

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

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

rng Y is set
union (rng Y) is set
A is set
dom Y is set
F is set
Y . F is set

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

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

(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

A . Z is Element of bool X
dom A is set

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

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

x is set
A . x is set
F . x is set

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

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

(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

(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

(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

A . F is Element of bool X
(X,A) . F is Element of bool X
X \ ((X,A) . F) is Element of bool X

(X,A) . F is Element of bool X
A . F is Element of bool X
X \ ((X,A) . F) is Element of bool X

(X,A) . F is Element of bool X

A . F is Element of bool X

(X,A) . x is Element of bool X

(X,A) . Z is Element of bool X

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

[: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):]
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

(X,()) . F is set
((Y `) followed_by (A `)) . F is set
(X,()) . F is Element of bool X
() . F is Element of bool X
(() . F) ` is Element of bool X
X \ (() . F) is set
((Y `) followed_by (A `)) . F is Element of bool X
(X,()) . F is Element of bool X
() . F is Element of bool X
(() . F) ` is Element of bool X
X \ (() . 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

[:NAT,(bool X):] is non empty Relation-like set
bool [:NAT,(bool X):] is non empty cap-closed set
(X,()) is Element of bool X
(X,()) 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,())) is Element of bool X
rng (X,()) is set
union (rng (X,())) is set
(X,(X,())) ` is Element of bool X
X \ (X,(X,())) 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 `),(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

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

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

[:NAT,(bool Y):] is non empty Relation-like set
bool [:NAT,(bool Y):] is non empty cap-closed set
rng () is set
{x,Z} is non empty set
(Y,()) is Element of bool Y
(Y,()) 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,())) is Element of bool Y
rng (Y,()) is set
union (rng (Y,())) is set
(Y,(Y,())) ` is Element of bool Y
Y \ (Y,(Y,())) 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,Y:] is non empty Relation-like set
bool [:NAT,Y:] 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 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)

(X,A) is Element of bool X
rng A is set
union (rng A) is set

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

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

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

A is non empty cap-closed (X) (X) Element of bool (bool X)
rng Y is set

Y . F is Element of bool X

Y . F is Element of bool X

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

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)

dom F is 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)

bool [:A,REAL:] is non empty cap-closed 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

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)

bool [:Y,REAL:] is non empty cap-closed 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

bool [:Y,REAL:] 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 non empty cap-closed (X) (X) Element of bool (bool X)

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

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

(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

(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

(X,Y,x,F) . Z is ext-real V21() real Element of REAL

x . Z is Element of bool X

x . Z is Element of bool X

(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

(X,Y,x,F) . Z is ext-real V21() real Element of REAL

rng x is set
Z is ext-real V21() real Element of REAL

(X,Y,x,F) . Z is ext-real V21() real Element of REAL

x . Z is Element of bool X

x . c8 is Element of bool X

x . Z is Element of bool X

(X,Y,x,F) . c8 is ext-real V21() real Element of REAL

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)

(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

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 . (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 . (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 . (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 . (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 . 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 . 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 . (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 . (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 . (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 . (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)
{ b1 where b1 is Element of bool (bool X) : ( Y c= b1 & b1 is non empty cap-closed (X) (X) Element of bool (bool X) ) } is set
meet { b1 where b1 is Element of bool (bool X) : ( Y c= b1 & b1 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

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

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
is V65() V66() V67() set
Y is ext-real V21() real set
{ (b1) where b1 is ext-real V21() real Element of REAL : verum } is set
bool () is non empty cap-closed set
bool REAL is non empty cap-closed ( REAL ) ( REAL ) Element of bool ()
X is set
Y is ext-real V21() real Element of REAL
(Y) is V65() V66() V67() Element of bool REAL
is V65() V66() V67() set
() is Element of bool ()
(REAL,()) is non empty cap-closed ( REAL ) ( REAL ) Element of bool ()
() is non empty cap-closed ( REAL ) ( REAL ) Element of bool ()
X is set
bool X is non empty cap-closed set
Y is Element of bool X
A is Element of 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):]
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

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