:: FUZZY_4 semantic presentation

REAL is non empty V43() V44() V45() V49() V50() set
NAT is V43() V44() V45() V46() V47() V48() V49() Element of bool REAL
bool REAL is non empty set
COMPLEX is non empty V43() V49() V50() set
{} is Relation-like non-empty empty-yielding RAT -valued empty V33() V34() V35() V36() V43() V44() V45() V46() V47() V48() V49() set
RAT is non empty V43() V44() V45() V46() V49() V50() set
1 is non empty natural V28() real ext-real positive non negative V43() V44() V45() V46() V47() V48() V60() V61() Element of NAT
{{},1} is non empty set
ExtREAL is non empty V44() set
INT is non empty V43() V44() V45() V46() V47() V49() V50() set
omega is V43() V44() V45() V46() V47() V48() V49() set
bool omega is non empty set
bool NAT is non empty set
0 is Relation-like non-empty empty-yielding RAT -valued empty natural V28() real ext-real non positive non negative V33() V34() V35() V36() V43() V44() V45() V46() V47() V48() V49() V60() V61() Element of NAT
[.0,1.] is V43() V44() V45() Element of bool REAL
[:COMPLEX,COMPLEX:] is Relation-like non empty V33() set
bool [:COMPLEX,COMPLEX:] is non empty set
[:COMPLEX,REAL:] is Relation-like non empty V33() V34() V35() set
bool [:COMPLEX,REAL:] is non empty set
[:[:COMPLEX,COMPLEX:],COMPLEX:] is Relation-like non empty V33() set
bool [:[:COMPLEX,COMPLEX:],COMPLEX:] is non empty set
[:REAL,REAL:] is Relation-like non empty V33() V34() V35() set
bool [:REAL,REAL:] is non empty set
[:[:REAL,REAL:],REAL:] is Relation-like non empty V33() V34() V35() set
bool [:[:REAL,REAL:],REAL:] is non empty set
[:RAT,RAT:] is Relation-like RAT -valued non empty V33() V34() V35() set
bool [:RAT,RAT:] is non empty set
[:[:RAT,RAT:],RAT:] is Relation-like RAT -valued non empty V33() V34() V35() set
bool [:[:RAT,RAT:],RAT:] is non empty set
[:INT,INT:] is Relation-like RAT -valued INT -valued non empty V33() V34() V35() set
bool [:INT,INT:] is non empty set
[:[:INT,INT:],INT:] is Relation-like RAT -valued INT -valued non empty V33() V34() V35() set
bool [:[:INT,INT:],INT:] is non empty set
[:NAT,NAT:] is Relation-like RAT -valued INT -valued V33() V34() V35() V36() set
[:[:NAT,NAT:],NAT:] is Relation-like RAT -valued INT -valued V33() V34() V35() V36() set
bool [:[:NAT,NAT:],NAT:] is non empty set
X is non empty set
[:X,REAL:] is Relation-like non empty V33() V34() V35() set
bool [:X,REAL:] is non empty set
Y is Relation-like X -defined REAL -valued [.0,1.] -valued V6() V18(X, REAL ) V33() V34() V35() Element of bool [:X,REAL:]
rng Y is V43() V44() V45() Element of bool REAL
dom Y is Element of bool X
bool X is non empty set
x is Element of X
Y . x is V28() real ext-real Element of REAL
X is non empty set
[:X,REAL:] is Relation-like non empty V33() V34() V35() set
bool [:X,REAL:] is non empty set
Y is Relation-like X -defined REAL -valued [.0,1.] -valued V6() V18(X, REAL ) V33() V34() V35() Element of bool [:X,REAL:]
rng Y is non empty V43() V44() V45() Element of bool REAL
dom Y is Element of bool X
bool X is non empty set
upper_bound (rng Y) is V28() real ext-real Element of REAL
lower_bound (rng Y) is V28() real ext-real Element of REAL
x is set
Y . x is V28() real ext-real Element of REAL
x is set
Y . x is V28() real ext-real Element of REAL
x is set
Y . x is V28() real ext-real Element of REAL
y is set
Y . y is V28() real ext-real Element of REAL
X is non empty set
[:X,REAL:] is Relation-like non empty V33() V34() V35() set
bool [:X,REAL:] is non empty set
Y is Relation-like X -defined REAL -valued [.0,1.] -valued V6() V18(X, REAL ) V33() V34() V35() Element of bool [:X,REAL:]
x is Relation-like X -defined REAL -valued [.0,1.] -valued V6() V18(X, REAL ) V33() V34() V35() Element of bool [:X,REAL:]
rng Y is non empty V43() V44() V45() Element of bool REAL
upper_bound (rng Y) is V28() real ext-real Element of REAL
rng x is non empty V43() V44() V45() Element of bool REAL
upper_bound (rng x) is V28() real ext-real Element of REAL
dom Y is Element of bool X
bool X is non empty set
y is V28() real ext-real set
(upper_bound (rng Y)) - y is V28() real ext-real set
f is V28() real ext-real set
x is set
Y . x is V28() real ext-real Element of REAL
x . x is V28() real ext-real Element of REAL
y is V28() real ext-real set
(upper_bound (rng Y)) - y is V28() real ext-real set
f is set
x . f is V28() real ext-real Element of REAL
dom x is Element of bool X
X is non empty set
Y is non empty set
[:X,Y:] is Relation-like non empty set
[:[:X,Y:],REAL:] is Relation-like non empty V33() V34() V35() set
bool [:[:X,Y:],REAL:] is non empty set
x is Relation-like [:X,Y:] -defined REAL -valued [.0,1.] -valued V6() V18([:X,Y:], REAL ) V33() V34() V35() Element of bool [:[:X,Y:],REAL:]
y is set
x . y is V28() real ext-real Element of REAL
f is Element of [:X,Y:]
x . f is V28() real ext-real Element of REAL
Umf (X,Y) is Relation-like [:X,Y:] -defined REAL -valued [.0,1.] -valued V6() V18([:X,Y:], REAL ) V33() V34() V35() Element of bool [:[:X,Y:],REAL:]
K136([:X,Y:],[:X,Y:]) is Relation-like [:X,Y:] -defined {{},1} -valued V6() V18([:X,Y:],{{},1}) Element of bool [:[:X,Y:],{{},1}:]
[:[:X,Y:],{{},1}:] is Relation-like non empty set
bool [:[:X,Y:],{{},1}:] is non empty set
(Umf (X,Y)) . f is V28() real ext-real Element of REAL
Zmf (X,Y) is Relation-like [:X,Y:] -defined REAL -valued [.0,1.] -valued V6() V18([:X,Y:], REAL ) V33() V34() V35() Element of bool [:[:X,Y:],REAL:]
K136({},[:X,Y:]) is Relation-like [:X,Y:] -defined {{},1} -valued V6() V18([:X,Y:],{{},1}) Element of bool [:[:X,Y:],{{},1}:]
(Zmf (X,Y)) . f is V28() real ext-real Element of REAL
dom x is Relation-like X -defined Y -valued Element of bool [:X,Y:]
bool [:X,Y:] is non empty set
X is non empty set
Y is non empty set
[:X,Y:] is Relation-like non empty set
[:[:X,Y:],REAL:] is Relation-like non empty V33() V34() V35() set
bool [:[:X,Y:],REAL:] is non empty set
x is Relation-like [:X,Y:] -defined REAL -valued [.0,1.] -valued V6() V18([:X,Y:], REAL ) V33() V34() V35() Element of bool [:[:X,Y:],REAL:]
y is set
f is set
x . (y,f) is set
[y,f] is set
{y,f} is non empty set
{y} is non empty set
{{y,f},{y}} is non empty set
K11(x,[y,f]) is V28() real ext-real set
x . [y,f] is V28() real ext-real Element of REAL
X is non empty set
Y is non empty set
[:X,Y:] is Relation-like non empty set
[:[:X,Y:],REAL:] is Relation-like non empty V33() V34() V35() set
bool [:[:X,Y:],REAL:] is non empty set
x is non empty set
z is non empty set
[:x,z:] is Relation-like non empty set
[:[:x,z:],REAL:] is Relation-like non empty V33() V34() V35() set
bool [:[:x,z:],REAL:] is non empty set
x is Relation-like [:X,Y:] -defined REAL -valued [.0,1.] -valued V6() V18([:X,Y:], REAL ) V33() V34() V35() Element of bool [:[:X,Y:],REAL:]
y is set
f is set
(X,Y,x,y,f) is V28() real ext-real Element of REAL
[y,f] is set
{y,f} is non empty set
{y} is non empty set
{{y,f},{y}} is non empty set
K11(x,[y,f]) is V28() real ext-real set
r is Relation-like [:x,z:] -defined REAL -valued [.0,1.] -valued V6() V18([:x,z:], REAL ) V33() V34() V35() Element of bool [:[:x,z:],REAL:]
y is set
z is set
(x,z,r,y,z) is V28() real ext-real Element of REAL
[y,z] is set
{y,z} is non empty set
{y} is non empty set
{{y,z},{y}} is non empty set
K11(r,[y,z]) is V28() real ext-real set
Y is non empty set
X is non empty set
[:Y,X:] is Relation-like non empty set
[:[:Y,X:],REAL:] is Relation-like non empty V33() V34() V35() set
bool [:[:Y,X:],REAL:] is non empty set
Y is non empty set
X is non empty set
[:Y,X:] is Relation-like non empty set
[:[:Y,X:],REAL:] is Relation-like non empty V33() V34() V35() set
bool [:[:Y,X:],REAL:] is non empty set
x is Relation-like [:Y,X:] -defined REAL -valued [.0,1.] -valued V6() V18([:Y,X:], REAL ) V33() V34() V35() Element of bool [:[:Y,X:],REAL:]
~ x is Relation-like V6() set
[:X,Y:] is Relation-like non empty set
[:[:X,Y:],REAL:] is Relation-like non empty V33() V34() V35() set
bool [:[:X,Y:],REAL:] is non empty set
dom x is Relation-like Y -defined X -valued Element of bool [:Y,X:]
bool [:Y,X:] is non empty set
dom (~ x) is set
rng x is non empty V43() V44() V45() Element of bool REAL
rng (~ x) is set
f is Relation-like [:X,Y:] -defined REAL -valued V6() V33() V34() V35() Element of bool [:[:X,Y:],REAL:]
y is Relation-like [:X,Y:] -defined REAL -valued [.0,1.] -valued V6() V18([:X,Y:], REAL ) V33() V34() V35() Element of bool [:[:X,Y:],REAL:]
dom x is Relation-like Y -defined X -valued Element of bool [:Y,X:]
bool [:Y,X:] is non empty set
f is set
x is set
[f,x] is set
{f,x} is non empty set
{f} is non empty set
{{f,x},{f}} is non empty set
(X,Y,y,f,x) is V28() real ext-real Element of REAL
K11(y,[f,x]) is V28() real ext-real set
(Y,X,x,x,f) is V28() real ext-real Element of REAL
[x,f] is set
{x,f} is non empty set
{x} is non empty set
{{x,f},{x}} is non empty set
K11(x,[x,f]) is V28() real ext-real set
dom y is Relation-like X -defined Y -valued Element of bool [:X,Y:]
bool [:X,Y:] is non empty set
f is set
x is set
z is set
[x,z] is set
{x,z} is non empty set
{x} is non empty set
{{x,z},{x}} is non empty set
[z,x] is set
{z,x} is non empty set
{z} is non empty set
{{z,x},{z}} is non empty set
z is set
x is set
[z,x] is set
{z,x} is non empty set
{z} is non empty set
{{z,x},{z}} is non empty set
[x,z] is set
{x,z} is non empty set
{x} is non empty set
{{x,z},{x}} is non empty set
f is set
x is set
[f,x] is set
{f,x} is non empty set
{f} is non empty set
{{f,x},{f}} is non empty set
(X,Y,y,x,f) is V28() real ext-real Element of REAL
[x,f] is set
{x,f} is non empty set
{x} is non empty set
{{x,f},{x}} is non empty set
K11(y,[x,f]) is V28() real ext-real set
(Y,X,x,f,x) is V28() real ext-real Element of REAL
K11(x,[f,x]) is V28() real ext-real set
X is non empty set
Y is non empty set
[:X,Y:] is Relation-like non empty set
[:[:X,Y:],REAL:] is Relation-like non empty V33() V34() V35() set
bool [:[:X,Y:],REAL:] is non empty set
x is Relation-like [:X,Y:] -defined REAL -valued [.0,1.] -valued V6() V18([:X,Y:], REAL ) V33() V34() V35() Element of bool [:[:X,Y:],REAL:]
(Y,X,x) is Relation-like [:Y,X:] -defined REAL -valued [.0,1.] -valued V6() V18([:Y,X:], REAL ) V33() V34() V35() Element of bool [:[:Y,X:],REAL:]
[:Y,X:] is Relation-like non empty set
[:[:Y,X:],REAL:] is Relation-like non empty V33() V34() V35() set
bool [:[:Y,X:],REAL:] is non empty set
(X,Y,(Y,X,x)) is Relation-like [:X,Y:] -defined REAL -valued [.0,1.] -valued V6() V18([:X,Y:], REAL ) V33() V34() V35() Element of bool [:[:X,Y:],REAL:]
dom x is Relation-like X -defined Y -valued Element of bool [:X,Y:]
bool [:X,Y:] is non empty set
y is Element of [:X,Y:]
(X,Y,(Y,X,x)) . y is V28() real ext-real Element of REAL
x . y is V28() real ext-real Element of REAL
f is set
x is set
[f,x] is set
{f,x} is non empty set
{f} is non empty set
{{f,x},{f}} is non empty set
[x,f] is set
{x,f} is non empty set
{x} is non empty set
{{x,f},{x}} is non empty set
(X,Y,(X,Y,(Y,X,x)),f,x) is V28() real ext-real Element of REAL
K11((X,Y,(Y,X,x)),[f,x]) is V28() real ext-real set
(Y,X,(Y,X,x),x,f) is V28() real ext-real Element of REAL
K11((Y,X,x),[x,f]) is V28() real ext-real set
(X,Y,x,f,x) is V28() real ext-real Element of REAL
K11(x,[f,x]) is V28() real ext-real set
dom (X,Y,(Y,X,x)) is Relation-like X -defined Y -valued Element of bool [:X,Y:]
X is non empty set
Y is non empty set
[:X,Y:] is Relation-like non empty set
[:[:X,Y:],REAL:] is Relation-like non empty V33() V34() V35() set
bool [:[:X,Y:],REAL:] is non empty set
[:Y,X:] is Relation-like non empty set
x is Relation-like [:X,Y:] -defined REAL -valued [.0,1.] -valued V6() V18([:X,Y:], REAL ) V33() V34() V35() Element of bool [:[:X,Y:],REAL:]
(Y,X,x) is Relation-like [:Y,X:] -defined REAL -valued [.0,1.] -valued V6() V18([:Y,X:], REAL ) V33() V34() V35() Element of bool [:[:Y,X:],REAL:]
[:[:Y,X:],REAL:] is Relation-like non empty V33() V34() V35() set
bool [:[:Y,X:],REAL:] is non empty set
1_minus (Y,X,x) is Relation-like [:Y,X:] -defined REAL -valued [.0,1.] -valued V6() V18([:Y,X:], REAL ) V33() V34() V35() Element of bool [:[:Y,X:],REAL:]
1_minus x is Relation-like [:X,Y:] -defined REAL -valued [.0,1.] -valued V6() V18([:X,Y:], REAL ) V33() V34() V35() Element of bool [:[:X,Y:],REAL:]
(Y,X,(1_minus x)) is Relation-like [:Y,X:] -defined REAL -valued [.0,1.] -valued V6() V18([:Y,X:], REAL ) V33() V34() V35() Element of bool [:[:Y,X:],REAL:]
dom (Y,X,(1_minus x)) is Relation-like Y -defined X -valued Element of bool [:Y,X:]
bool [:Y,X:] is non empty set
y is Element of [:Y,X:]
(1_minus (Y,X,x)) . y is V28() real ext-real Element of REAL
(Y,X,(1_minus x)) . y is V28() real ext-real Element of REAL
f is set
x is set
[f,x] is set
{f,x} is non empty set
{f} is non empty set
{{f,x},{f}} is non empty set
[x,f] is set
{x,f} is non empty set
{x} is non empty set
{{x,f},{x}} is non empty set
(Y,X,(1_minus (Y,X,x)),f,x) is V28() real ext-real Element of REAL
K11((1_minus (Y,X,x)),[f,x]) is V28() real ext-real set
(Y,X,(Y,X,x),f,x) is V28() real ext-real Element of REAL
K11((Y,X,x),[f,x]) is V28() real ext-real set
1 - (Y,X,(Y,X,x),f,x) is V28() real ext-real set
(X,Y,x,x,f) is V28() real ext-real Element of REAL
K11(x,[x,f]) is V28() real ext-real set
1 - (X,Y,x,x,f) is V28() real ext-real set
(X,Y,(1_minus x),x,f) is V28() real ext-real Element of REAL
K11((1_minus x),[x,f]) is V28() real ext-real set
(Y,X,(Y,X,(1_minus x)),f,x) is V28() real ext-real Element of REAL
K11((Y,X,(1_minus x)),[f,x]) is V28() real ext-real set
dom (1_minus (Y,X,x)) is Relation-like Y -defined X -valued Element of bool [:Y,X:]
X is non empty set
Y is non empty set
[:X,Y:] is Relation-like non empty set
[:[:X,Y:],REAL:] is Relation-like non empty V33() V34() V35() set
bool [:[:X,Y:],REAL:] is non empty set
[:Y,X:] is Relation-like non empty set
x is Relation-like [:X,Y:] -defined REAL -valued [.0,1.] -valued V6() V18([:X,Y:], REAL ) V33() V34() V35() Element of bool [:[:X,Y:],REAL:]
y is Relation-like [:X,Y:] -defined REAL -valued [.0,1.] -valued V6() V18([:X,Y:], REAL ) V33() V34() V35() Element of bool [:[:X,Y:],REAL:]
max (x,y) is Relation-like [:X,Y:] -defined REAL -valued [.0,1.] -valued V6() V18([:X,Y:], REAL ) V33() V34() V35() Element of bool [:[:X,Y:],REAL:]
(Y,X,(max (x,y))) is Relation-like [:Y,X:] -defined REAL -valued [.0,1.] -valued V6() V18([:Y,X:], REAL ) V33() V34() V35() Element of bool [:[:Y,X:],REAL:]
[:[:Y,X:],REAL:] is Relation-like non empty V33() V34() V35() set
bool [:[:Y,X:],REAL:] is non empty set
(Y,X,x) is Relation-like [:Y,X:] -defined REAL -valued [.0,1.] -valued V6() V18([:Y,X:], REAL ) V33() V34() V35() Element of bool [:[:Y,X:],REAL:]
(Y,X,y) is Relation-like [:Y,X:] -defined REAL -valued [.0,1.] -valued V6() V18([:Y,X:], REAL ) V33() V34() V35() Element of bool [:[:Y,X:],REAL:]
max ((Y,X,x),(Y,X,y)) is Relation-like [:Y,X:] -defined REAL -valued [.0,1.] -valued V6() V18([:Y,X:], REAL ) V33() V34() V35() Element of bool [:[:Y,X:],REAL:]
dom (max ((Y,X,x),(Y,X,y))) is Relation-like Y -defined X -valued Element of bool [:Y,X:]
bool [:Y,X:] is non empty set
f is Element of [:Y,X:]
(Y,X,(max (x,y))) . f is V28() real ext-real Element of REAL
(max ((Y,X,x),(Y,X,y))) . f is V28() real ext-real Element of REAL
x is set
z is set
[x,z] is set
{x,z} is non empty set
{x} is non empty set
{{x,z},{x}} is non empty set
[z,x] is set
{z,x} is non empty set
{z} is non empty set
{{z,x},{z}} is non empty set
(Y,X,(Y,X,(max (x,y))),x,z) is V28() real ext-real Element of REAL
K11((Y,X,(max (x,y))),[x,z]) is V28() real ext-real set
(X,Y,(max (x,y)),z,x) is V28() real ext-real Element of REAL
K11((max (x,y)),[z,x]) is V28() real ext-real set
(X,Y,x,z,x) is V28() real ext-real Element of REAL
K11(x,[z,x]) is V28() real ext-real set
(X,Y,y,z,x) is V28() real ext-real Element of REAL
K11(y,[z,x]) is V28() real ext-real set
max ((X,Y,x,z,x),(X,Y,y,z,x)) is V28() real ext-real Element of REAL
(Y,X,(Y,X,x),x,z) is V28() real ext-real Element of REAL
K11((Y,X,x),[x,z]) is V28() real ext-real set
max ((Y,X,(Y,X,x),x,z),(X,Y,y,z,x)) is V28() real ext-real Element of REAL
(Y,X,(Y,X,y),x,z) is V28() real ext-real Element of REAL
K11((Y,X,y),[x,z]) is V28() real ext-real set
max ((Y,X,(Y,X,x),x,z),(Y,X,(Y,X,y),x,z)) is V28() real ext-real Element of REAL
(Y,X,(max ((Y,X,x),(Y,X,y))),x,z) is V28() real ext-real Element of REAL
K11((max ((Y,X,x),(Y,X,y))),[x,z]) is V28() real ext-real set
dom (Y,X,(max (x,y))) is Relation-like Y -defined X -valued Element of bool [:Y,X:]
X is non empty set
Y is non empty set
[:X,Y:] is Relation-like non empty set
[:[:X,Y:],REAL:] is Relation-like non empty V33() V34() V35() set
bool [:[:X,Y:],REAL:] is non empty set
[:Y,X:] is Relation-like non empty set
x is Relation-like [:X,Y:] -defined REAL -valued [.0,1.] -valued V6() V18([:X,Y:], REAL ) V33() V34() V35() Element of bool [:[:X,Y:],REAL:]
y is Relation-like [:X,Y:] -defined REAL -valued [.0,1.] -valued V6() V18([:X,Y:], REAL ) V33() V34() V35() Element of bool [:[:X,Y:],REAL:]
min (x,y) is Relation-like [:X,Y:] -defined REAL -valued [.0,1.] -valued V6() V18([:X,Y:], REAL ) V33() V34() V35() Element of bool [:[:X,Y:],REAL:]
(Y,X,(min (x,y))) is Relation-like [:Y,X:] -defined REAL -valued [.0,1.] -valued V6() V18([:Y,X:], REAL ) V33() V34() V35() Element of bool [:[:Y,X:],REAL:]
[:[:Y,X:],REAL:] is Relation-like non empty V33() V34() V35() set
bool [:[:Y,X:],REAL:] is non empty set
(Y,X,x) is Relation-like [:Y,X:] -defined REAL -valued [.0,1.] -valued V6() V18([:Y,X:], REAL ) V33() V34() V35() Element of bool [:[:Y,X:],REAL:]
(Y,X,y) is Relation-like [:Y,X:] -defined REAL -valued [.0,1.] -valued V6() V18([:Y,X:], REAL ) V33() V34() V35() Element of bool [:[:Y,X:],REAL:]
min ((Y,X,x),(Y,X,y)) is Relation-like [:Y,X:] -defined REAL -valued [.0,1.] -valued V6() V18([:Y,X:], REAL ) V33() V34() V35() Element of bool [:[:Y,X:],REAL:]
dom (min ((Y,X,x),(Y,X,y))) is Relation-like Y -defined X -valued Element of bool [:Y,X:]
bool [:Y,X:] is non empty set
f is Element of [:Y,X:]
(Y,X,(min (x,y))) . f is V28() real ext-real Element of REAL
(min ((Y,X,x),(Y,X,y))) . f is V28() real ext-real Element of REAL
x is set
z is set
[x,z] is set
{x,z} is non empty set
{x} is non empty set
{{x,z},{x}} is non empty set
[z,x] is set
{z,x} is non empty set
{z} is non empty set
{{z,x},{z}} is non empty set
(Y,X,(Y,X,(min (x,y))),x,z) is V28() real ext-real Element of REAL
K11((Y,X,(min (x,y))),[x,z]) is V28() real ext-real set
(X,Y,(min (x,y)),z,x) is V28() real ext-real Element of REAL
K11((min (x,y)),[z,x]) is V28() real ext-real set
(X,Y,x,z,x) is V28() real ext-real Element of REAL
K11(x,[z,x]) is V28() real ext-real set
(X,Y,y,z,x) is V28() real ext-real Element of REAL
K11(y,[z,x]) is V28() real ext-real set
min ((X,Y,x,z,x),(X,Y,y,z,x)) is V28() real ext-real Element of REAL
(Y,X,(Y,X,x),x,z) is V28() real ext-real Element of REAL
K11((Y,X,x),[x,z]) is V28() real ext-real set
min ((Y,X,(Y,X,x),x,z),(X,Y,y,z,x)) is V28() real ext-real Element of REAL
(Y,X,(Y,X,y),x,z) is V28() real ext-real Element of REAL
K11((Y,X,y),[x,z]) is V28() real ext-real set
min ((Y,X,(Y,X,x),x,z),(Y,X,(Y,X,y),x,z)) is V28() real ext-real Element of REAL
dom (Y,X,(min (x,y))) is Relation-like Y -defined X -valued Element of bool [:Y,X:]
X is non empty set
Y is non empty set
[:X,Y:] is Relation-like non empty set
[:[:X,Y:],REAL:] is Relation-like non empty V33() V34() V35() set
bool [:[:X,Y:],REAL:] is non empty set
x is Relation-like [:X,Y:] -defined REAL -valued [.0,1.] -valued V6() V18([:X,Y:], REAL ) V33() V34() V35() Element of bool [:[:X,Y:],REAL:]
y is Relation-like [:X,Y:] -defined REAL -valued [.0,1.] -valued V6() V18([:X,Y:], REAL ) V33() V34() V35() Element of bool [:[:X,Y:],REAL:]
(Y,X,x) is Relation-like [:Y,X:] -defined REAL -valued [.0,1.] -valued V6() V18([:Y,X:], REAL ) V33() V34() V35() Element of bool [:[:Y,X:],REAL:]
[:Y,X:] is Relation-like non empty set
[:[:Y,X:],REAL:] is Relation-like non empty V33() V34() V35() set
bool [:[:Y,X:],REAL:] is non empty set
(Y,X,y) is Relation-like [:Y,X:] -defined REAL -valued [.0,1.] -valued V6() V18([:Y,X:], REAL ) V33() V34() V35() Element of bool [:[:Y,X:],REAL:]
f is set
x is set
[f,x] is set
{f,x} is non empty set
{f} is non empty set
{{f,x},{f}} is non empty set
x . [f,x] is V28() real ext-real Element of REAL
y . [f,x] is V28() real ext-real Element of REAL
[x,f] is set
{x,f} is non empty set
{x} is non empty set
{{x,f},{x}} is non empty set
(Y,X,x) . [x,f] is V28() real ext-real Element of REAL
(Y,X,y) . [x,f] is V28() real ext-real Element of REAL
(X,Y,y,f,x) is V28() real ext-real Element of REAL
K11(y,[f,x]) is V28() real ext-real set
(Y,X,(Y,X,y),x,f) is V28() real ext-real Element of REAL
K11((Y,X,y),[x,f]) is V28() real ext-real set
(X,Y,x,f,x) is V28() real ext-real Element of REAL
K11(x,[f,x]) is V28() real ext-real set
(Y,X,(Y,X,x),x,f) is V28() real ext-real Element of REAL
K11((Y,X,x),[x,f]) is V28() real ext-real set
X is non empty set
Y is non empty set
[:X,Y:] is Relation-like non empty set
[:[:X,Y:],REAL:] is Relation-like non empty V33() V34() V35() set
bool [:[:X,Y:],REAL:] is non empty set
x is Relation-like [:X,Y:] -defined REAL -valued [.0,1.] -valued V6() V18([:X,Y:], REAL ) V33() V34() V35() Element of bool [:[:X,Y:],REAL:]
y is Relation-like [:X,Y:] -defined REAL -valued [.0,1.] -valued V6() V18([:X,Y:], REAL ) V33() V34() V35() Element of bool [:[:X,Y:],REAL:]
(Y,X,x) is Relation-like [:Y,X:] -defined REAL -valued [.0,1.] -valued V6() V18([:Y,X:], REAL ) V33() V34() V35() Element of bool [:[:Y,X:],REAL:]
[:Y,X:] is Relation-like non empty set
[:[:Y,X:],REAL:] is Relation-like non empty V33() V34() V35() set
bool [:[:Y,X:],REAL:] is non empty set
(Y,X,y) is Relation-like [:Y,X:] -defined REAL -valued [.0,1.] -valued V6() V18([:Y,X:], REAL ) V33() V34() V35() Element of bool [:[:Y,X:],REAL:]
f is Element of [:Y,X:]
(Y,X,x) . f is V28() real ext-real Element of REAL
(Y,X,y) . f is V28() real ext-real Element of REAL
x is set
z is set
[x,z] is set
{x,z} is non empty set
{x} is non empty set
{{x,z},{x}} is non empty set
x is set
z is set
[z,x] is set
{z,x} is non empty set
{z} is non empty set
{{z,x},{z}} is non empty set
[x,z] is set
{x,z} is non empty set
{x} is non empty set
{{x,z},{x}} is non empty set
x . [x,z] is V28() real ext-real Element of REAL
y . [x,z] is V28() real ext-real Element of REAL
X is non empty set
Y is non empty set
[:X,Y:] is Relation-like non empty set
[:[:X,Y:],REAL:] is Relation-like non empty V33() V34() V35() set
bool [:[:X,Y:],REAL:] is non empty set
[:Y,X:] is Relation-like non empty set
x is Relation-like [:X,Y:] -defined REAL -valued [.0,1.] -valued V6() V18([:X,Y:], REAL ) V33() V34() V35() Element of bool [:[:X,Y:],REAL:]
y is Relation-like [:X,Y:] -defined REAL -valued [.0,1.] -valued V6() V18([:X,Y:], REAL ) V33() V34() V35() Element of bool [:[:X,Y:],REAL:]
x \ y is Relation-like [:X,Y:] -defined REAL -valued [.0,1.] -valued V6() V18([:X,Y:], REAL ) V33() V34() V35() Element of bool [:[:X,Y:],REAL:]
1_minus y is Relation-like [:X,Y:] -defined REAL -valued [.0,1.] -valued V6() V18([:X,Y:], REAL ) V33() V34() V35() Element of bool [:[:X,Y:],REAL:]
min (x,(1_minus y)) is Relation-like [:X,Y:] -defined REAL -valued [.0,1.] -valued V6() V18([:X,Y:], REAL ) V33() V34() V35() Element of bool [:[:X,Y:],REAL:]
(Y,X,(x \ y)) is Relation-like [:Y,X:] -defined REAL -valued [.0,1.] -valued V6() V18([:Y,X:], REAL ) V33() V34() V35() Element of bool [:[:Y,X:],REAL:]
[:[:Y,X:],REAL:] is Relation-like non empty V33() V34() V35() set
bool [:[:Y,X:],REAL:] is non empty set
(Y,X,x) is Relation-like [:Y,X:] -defined REAL -valued [.0,1.] -valued V6() V18([:Y,X:], REAL ) V33() V34() V35() Element of bool [:[:Y,X:],REAL:]
(Y,X,y) is Relation-like [:Y,X:] -defined REAL -valued [.0,1.] -valued V6() V18([:Y,X:], REAL ) V33() V34() V35() Element of bool [:[:Y,X:],REAL:]
(Y,X,x) \ (Y,X,y) is Relation-like [:Y,X:] -defined REAL -valued [.0,1.] -valued V6() V18([:Y,X:], REAL ) V33() V34() V35() Element of bool [:[:Y,X:],REAL:]
1_minus (Y,X,y) is Relation-like [:Y,X:] -defined REAL -valued [.0,1.] -valued V6() V18([:Y,X:], REAL ) V33() V34() V35() Element of bool [:[:Y,X:],REAL:]
min ((Y,X,x),(1_minus (Y,X,y))) is Relation-like [:Y,X:] -defined REAL -valued [.0,1.] -valued V6() V18([:Y,X:], REAL ) V33() V34() V35() Element of bool [:[:Y,X:],REAL:]
(Y,X,(1_minus y)) is Relation-like [:Y,X:] -defined REAL -valued [.0,1.] -valued V6() V18([:Y,X:], REAL ) V33() V34() V35() Element of bool [:[:Y,X:],REAL:]
min ((Y,X,x),(Y,X,(1_minus y))) is Relation-like [:Y,X:] -defined REAL -valued [.0,1.] -valued V6() V18([:Y,X:], REAL ) V33() V34() V35() Element of bool [:[:Y,X:],REAL:]
X is non empty set
Y is non empty set
[:X,Y:] is Relation-like non empty set
[:[:X,Y:],REAL:] is Relation-like non empty V33() V34() V35() set
bool [:[:X,Y:],REAL:] is non empty set
[:Y,X:] is Relation-like non empty set
x is Relation-like [:X,Y:] -defined REAL -valued [.0,1.] -valued V6() V18([:X,Y:], REAL ) V33() V34() V35() Element of bool [:[:X,Y:],REAL:]
y is Relation-like [:X,Y:] -defined REAL -valued [.0,1.] -valued V6() V18([:X,Y:], REAL ) V33() V34() V35() Element of bool [:[:X,Y:],REAL:]
x \+\ y is Relation-like [:X,Y:] -defined REAL -valued [.0,1.] -valued V6() V18([:X,Y:], REAL ) V33() V34() V35() Element of bool [:[:X,Y:],REAL:]
1_minus y is Relation-like [:X,Y:] -defined REAL -valued [.0,1.] -valued V6() V18([:X,Y:], REAL ) V33() V34() V35() Element of bool [:[:X,Y:],REAL:]
min (x,(1_minus y)) is Relation-like [:X,Y:] -defined REAL -valued [.0,1.] -valued V6() V18([:X,Y:], REAL ) V33() V34() V35() Element of bool [:[:X,Y:],REAL:]
1_minus x is Relation-like [:X,Y:] -defined REAL -valued [.0,1.] -valued V6() V18([:X,Y:], REAL ) V33() V34() V35() Element of bool [:[:X,Y:],REAL:]
min ((1_minus x),y) is Relation-like [:X,Y:] -defined REAL -valued [.0,1.] -valued V6() V18([:X,Y:], REAL ) V33() V34() V35() Element of bool [:[:X,Y:],REAL:]
max ((min (x,(1_minus y))),(min ((1_minus x),y))) is Relation-like [:X,Y:] -defined REAL -valued [.0,1.] -valued V6() V18([:X,Y:], REAL ) V33() V34() V35() Element of bool [:[:X,Y:],REAL:]
(Y,X,(x \+\ y)) is Relation-like [:Y,X:] -defined REAL -valued [.0,1.] -valued V6() V18([:Y,X:], REAL ) V33() V34() V35() Element of bool [:[:Y,X:],REAL:]
[:[:Y,X:],REAL:] is Relation-like non empty V33() V34() V35() set
bool [:[:Y,X:],REAL:] is non empty set
(Y,X,x) is Relation-like [:Y,X:] -defined REAL -valued [.0,1.] -valued V6() V18([:Y,X:], REAL ) V33() V34() V35() Element of bool [:[:Y,X:],REAL:]
(Y,X,y) is Relation-like [:Y,X:] -defined REAL -valued [.0,1.] -valued V6() V18([:Y,X:], REAL ) V33() V34() V35() Element of bool [:[:Y,X:],REAL:]
(Y,X,x) \+\ (Y,X,y) is Relation-like [:Y,X:] -defined REAL -valued [.0,1.] -valued V6() V18([:Y,X:], REAL ) V33() V34() V35() Element of bool [:[:Y,X:],REAL:]
1_minus (Y,X,y) is Relation-like [:Y,X:] -defined REAL -valued [.0,1.] -valued V6() V18([:Y,X:], REAL ) V33() V34() V35() Element of bool [:[:Y,X:],REAL:]
min ((Y,X,x),(1_minus (Y,X,y))) is Relation-like [:Y,X:] -defined REAL -valued [.0,1.] -valued V6() V18([:Y,X:], REAL ) V33() V34() V35() Element of bool [:[:Y,X:],REAL:]
1_minus (Y,X,x) is Relation-like [:Y,X:] -defined REAL -valued [.0,1.] -valued V6() V18([:Y,X:], REAL ) V33() V34() V35() Element of bool [:[:Y,X:],REAL:]
min ((1_minus (Y,X,x)),(Y,X,y)) is Relation-like [:Y,X:] -defined REAL -valued [.0,1.] -valued V6() V18([:Y,X:], REAL ) V33() V34() V35() Element of bool [:[:Y,X:],REAL:]
max ((min ((Y,X,x),(1_minus (Y,X,y)))),(min ((1_minus (Y,X,x)),(Y,X,y)))) is Relation-like [:Y,X:] -defined REAL -valued [.0,1.] -valued V6() V18([:Y,X:], REAL ) V33() V34() V35() Element of bool [:[:Y,X:],REAL:]
(Y,X,(min (x,(1_minus y)))) is Relation-like [:Y,X:] -defined REAL -valued [.0,1.] -valued V6() V18([:Y,X:], REAL ) V33() V34() V35() Element of bool [:[:Y,X:],REAL:]
(Y,X,(min ((1_minus x),y))) is Relation-like [:Y,X:] -defined REAL -valued [.0,1.] -valued V6() V18([:Y,X:], REAL ) V33() V34() V35() Element of bool [:[:Y,X:],REAL:]
max ((Y,X,(min (x,(1_minus y)))),(Y,X,(min ((1_minus x),y)))) is Relation-like [:Y,X:] -defined REAL -valued [.0,1.] -valued V6() V18([:Y,X:], REAL ) V33() V34() V35() Element of bool [:[:Y,X:],REAL:]
(Y,X,(1_minus y)) is Relation-like [:Y,X:] -defined REAL -valued [.0,1.] -valued V6() V18([:Y,X:], REAL ) V33() V34() V35() Element of bool [:[:Y,X:],REAL:]
min ((Y,X,x),(Y,X,(1_minus y))) is Relation-like [:Y,X:] -defined REAL -valued [.0,1.] -valued V6() V18([:Y,X:], REAL ) V33() V34() V35() Element of bool [:[:Y,X:],REAL:]
max ((min ((Y,X,x),(Y,X,(1_minus y)))),(Y,X,(min ((1_minus x),y)))) is Relation-like [:Y,X:] -defined REAL -valued [.0,1.] -valued V6() V18([:Y,X:], REAL ) V33() V34() V35() Element of bool [:[:Y,X:],REAL:]
(Y,X,(1_minus x)) is Relation-like [:Y,X:] -defined REAL -valued [.0,1.] -valued V6() V18([:Y,X:], REAL ) V33() V34() V35() Element of bool [:[:Y,X:],REAL:]
min ((Y,X,(1_minus x)),(Y,X,y)) is Relation-like [:Y,X:] -defined REAL -valued [.0,1.] -valued V6() V18([:Y,X:], REAL ) V33() V34() V35() Element of bool [:[:Y,X:],REAL:]
max ((min ((Y,X,x),(Y,X,(1_minus y)))),(min ((Y,X,(1_minus x)),(Y,X,y)))) is Relation-like [:Y,X:] -defined REAL -valued [.0,1.] -valued V6() V18([:Y,X:], REAL ) V33() V34() V35() Element of bool [:[:Y,X:],REAL:]
max ((min ((Y,X,x),(1_minus (Y,X,y)))),(min ((Y,X,(1_minus x)),(Y,X,y)))) is Relation-like [:Y,X:] -defined REAL -valued [.0,1.] -valued V6() V18([:Y,X:], REAL ) V33() V34() V35() Element of bool [:[:Y,X:],REAL:]
X is non empty set
Y is non empty set
[:X,Y:] is Relation-like non empty set
[:[:X,Y:],REAL:] is Relation-like non empty V33() V34() V35() set
bool [:[:X,Y:],REAL:] is non empty set
x is non empty set
[:Y,x:] is Relation-like non empty set
[:[:Y,x:],REAL:] is Relation-like non empty V33() V34() V35() set
bool [:[:Y,x:],REAL:] is non empty set
x is set
z is set
[:Y,REAL:] is Relation-like non empty V33() V34() V35() set
bool [:Y,REAL:] is non empty set
y is Relation-like [:X,Y:] -defined REAL -valued [.0,1.] -valued V6() V18([:X,Y:], REAL ) V33() V34() V35() Element of bool [:[:X,Y:],REAL:]
f is Relation-like [:Y,x:] -defined REAL -valued [.0,1.] -valued V6() V18([:Y,x:], REAL ) V33() V34() V35() Element of bool [:[:Y,x:],REAL:]
r is set
y is set
[x,r] is set
{x,r} is non empty set
{x} is non empty set
{{x,r},{x}} is non empty set
y . [x,r] is V28() real ext-real Element of REAL
[r,z] is set
{r,z} is non empty set
{r} is non empty set
{{r,z},{r}} is non empty set
f . [r,z] is V28() real ext-real Element of REAL
min ((y . [x,r]),(f . [r,z])) is V28() real ext-real Element of REAL
z is set
r is set
y is set
[x,r] is set
{x,r} is non empty set
{x} is non empty set
{{x,r},{x}} is non empty set
y . [x,r] is V28() real ext-real Element of REAL
[r,z] is set
{r,z} is non empty set
{r} is non empty set
{{r,z},{r}} is non empty set
f . [r,z] is V28() real ext-real Element of REAL
min ((y . [x,r]),(f . [r,z])) is V28() real ext-real Element of REAL
r is Relation-like Y -defined REAL -valued V6() V33() V34() V35() Element of bool [:Y,REAL:]
dom r is Element of bool Y
bool Y is non empty set
rng r is V43() V44() V45() Element of bool REAL
y is set
[x,y] is set
{x,y} is non empty set
{x} is non empty set
{{x,y},{x}} is non empty set
y . [x,y] is V28() real ext-real Element of REAL
[y,z] is set
{y,z} is non empty set
{y} is non empty set
{{y,z},{y}} is non empty set
f . [y,z] is V28() real ext-real Element of REAL
min ((y . [x,y]),(f . [y,z])) is V28() real ext-real Element of REAL
z is set
z is set
rng y is non empty V43() V44() V45() Element of bool REAL
y is Element of Y
r . y is V28() real ext-real Element of REAL
[x,y] is set
{x,y} is non empty set
{x} is non empty set
{{x,y},{x}} is non empty set
y . [x,y] is V28() real ext-real Element of REAL
[y,z] is set
{y,z} is non empty set
{y} is non empty set
{{y,z},{y}} is non empty set
f . [y,z] is V28() real ext-real Element of REAL
min ((y . [x,y]),(f . [y,z])) is V28() real ext-real Element of REAL
dom y is Relation-like X -defined Y -valued Element of bool [:X,Y:]
bool [:X,Y:] is non empty set
dom f is Relation-like Y -defined x -valued Element of bool [:Y,x:]
bool [:Y,x:] is non empty set
rng f is non empty V43() V44() V45() Element of bool REAL
y is non empty V43() V44() V45() V72() closed_interval real-bounded interval Element of bool REAL
lower_bound y is V28() real ext-real Element of REAL
upper_bound y is V28() real ext-real Element of REAL
[.(lower_bound y),(upper_bound y).] is V43() V44() V45() Element of bool REAL
y is Element of Y
r . y is V28() real ext-real Element of REAL
[x,y] is set
{x,y} is non empty set
{x} is non empty set
{{x,y},{x}} is non empty set
y . [x,y] is V28() real ext-real Element of REAL
[y,z] is set
{y,z} is non empty set
{y} is non empty set
{{y,z},{y}} is non empty set
f . [y,z] is V28() real ext-real Element of REAL
min ((y . [x,y]),(f . [y,z])) is V28() real ext-real Element of REAL
r is Relation-like Y -defined REAL -valued [.0,1.] -valued V6() V18(Y, REAL ) V33() V34() V35() Element of bool [:Y,REAL:]
y is Relation-like Y -defined REAL -valued [.0,1.] -valued V6() V18(Y, REAL ) V33() V34() V35() Element of bool [:Y,REAL:]
z is Element of Y
r . z is V28() real ext-real Element of REAL
y . z is V28() real ext-real Element of REAL
[x,z] is set
{x,z} is non empty set
{x} is non empty set
{{x,z},{x}} is non empty set
y . [x,z] is V28() real ext-real Element of REAL
[z,z] is set
{z,z} is non empty set
{z} is non empty set
{{z,z},{z}} is non empty set
f . [z,z] is V28() real ext-real Element of REAL
min ((y . [x,z]),(f . [z,z])) is V28() real ext-real Element of REAL
dom y is Element of bool Y
bool Y is non empty set
dom r is Element of bool Y
X is non empty set
Y is non empty set
[:X,Y:] is Relation-like non empty set
[:[:X,Y:],REAL:] is Relation-like non empty V33() V34() V35() set
bool [:[:X,Y:],REAL:] is non empty set
x is non empty set
[:Y,x:] is Relation-like non empty set
[:[:Y,x:],REAL:] is Relation-like non empty V33() V34() V35() set
bool [:[:Y,x:],REAL:] is non empty set
[:X,x:] is Relation-like non empty set
[:[:X,x:],REAL:] is Relation-like non empty V33() V34() V35() set
bool [:[:X,x:],REAL:] is non empty set
y is Relation-like [:X,Y:] -defined REAL -valued [.0,1.] -valued V6() V18([:X,Y:], REAL ) V33() V34() V35() Element of bool [:[:X,Y:],REAL:]
f is Relation-like [:Y,x:] -defined REAL -valued [.0,1.] -valued V6() V18([:Y,x:], REAL ) V33() V34() V35() Element of bool [:[:Y,x:],REAL:]
x is set
z is set
r is set
(X,Y,x,y,f,x,z) is Relation-like Y -defined REAL -valued [.0,1.] -valued V6() V18(Y, REAL ) V33() V34() V35() Element of bool [:Y,REAL:]
[:Y,REAL:] is Relation-like non empty V33() V34() V35() set
bool [:Y,REAL:] is non empty set
rng (X,Y,x,y,f,x,z) is non empty V43() V44() V45() Element of bool REAL
upper_bound (rng (X,Y,x,y,f,x,z)) is V28() real ext-real Element of REAL
y is set
x is set
z is set
r is set
(X,Y,x,y,f,x,z) is Relation-like Y -defined REAL -valued [.0,1.] -valued V6() V18(Y, REAL ) V33() V34() V35() Element of bool [:Y,REAL:]
[:Y,REAL:] is Relation-like non empty V33() V34() V35() set
bool [:Y,REAL:] is non empty set
rng (X,Y,x,y,f,x,z) is non empty V43() V44() V45() Element of bool REAL
upper_bound (rng (X,Y,x,y,f,x,z)) is V28() real ext-real Element of REAL
x is Relation-like [:X,x:] -defined REAL -valued V6() V33() V34() V35() Element of bool [:[:X,x:],REAL:]
dom x is Relation-like X -defined x -valued Element of bool [:X,x:]
bool [:X,x:] is non empty set
z is set
r is set
[z,r] is set
{z,r} is non empty set
{z} is non empty set
{{z,r},{z}} is non empty set
(X,Y,x,y,f,z,r) is Relation-like Y -defined REAL -valued [.0,1.] -valued V6() V18(Y, REAL ) V33() V34() V35() Element of bool [:Y,REAL:]
[:Y,REAL:] is Relation-like non empty V33() V34() V35() set
bool [:Y,REAL:] is non empty set
rng (X,Y,x,y,f,z,r) is non empty V43() V44() V45() Element of bool REAL
upper_bound (rng (X,Y,x,y,f,z,r)) is V28() real ext-real Element of REAL
y is set
rng x is V43() V44() V45() Element of bool REAL
r is set
y is Element of [:X,x:]
x . y is V28() real ext-real Element of REAL
z is non empty V43() V44() V45() V72() closed_interval real-bounded interval Element of bool REAL
lower_bound z is V28() real ext-real Element of REAL
upper_bound z is V28() real ext-real Element of REAL
[.(lower_bound z),(upper_bound z).] is V43() V44() V45() Element of bool REAL
z is set
y is set
(X,Y,x,y,f,z,y) is Relation-like Y -defined REAL -valued [.0,1.] -valued V6() V18(Y, REAL ) V33() V34() V35() Element of bool [:Y,REAL:]
[:Y,REAL:] is Relation-like non empty V33() V34() V35() set
bool [:Y,REAL:] is non empty set
rng (X,Y,x,y,f,z,y) is non empty V43() V44() V45() Element of bool REAL
upper_bound (rng (X,Y,x,y,f,z,y)) is V28() real ext-real Element of REAL
lower_bound (rng (X,Y,x,y,f,z,y)) is V28() real ext-real Element of REAL
z is set
y is set
[z,y] is set
{z,y} is non empty set
{z} is non empty set
{{z,y},{z}} is non empty set
x . (z,y) is set
K11(x,[z,y]) is V28() real ext-real set
(X,Y,x,y,f,z,y) is Relation-like Y -defined REAL -valued [.0,1.] -valued V6() V18(Y, REAL ) V33() V34() V35() Element of bool [:Y,REAL:]
[:Y,REAL:] is Relation-like non empty V33() V34() V35() set
bool [:Y,REAL:] is non empty set
rng (X,Y,x,y,f,z,y) is non empty V43() V44() V45() Element of bool REAL
upper_bound (rng (X,Y,x,y,f,z,y)) is V28() real ext-real Element of REAL
x is Relation-like [:X,x:] -defined REAL -valued [.0,1.] -valued V6() V18([:X,x:], REAL ) V33() V34() V35() Element of bool [:[:X,x:],REAL:]
z is Relation-like [:X,x:] -defined REAL -valued [.0,1.] -valued V6() V18([:X,x:], REAL ) V33() V34() V35() Element of bool [:[:X,x:],REAL:]
r is Element of [:X,x:]
x . r is V28() real ext-real Element of REAL
z . r is V28() real ext-real Element of REAL
y is set
z is set
[y,z] is set
{y,z} is non empty set
{y} is non empty set
{{y,z},{y}} is non empty set
(X,x,z,y,z) is V28() real ext-real Element of REAL
K11(z,[y,z]) is V28() real ext-real set
(X,Y,x,y,f,y,z) is Relation-like Y -defined REAL -valued [.0,1.] -valued V6() V18(Y, REAL ) V33() V34() V35() Element of bool [:Y,REAL:]
[:Y,REAL:] is Relation-like non empty V33() V34() V35() set
bool [:Y,REAL:] is non empty set
rng (X,Y,x,y,f,y,z) is non empty V43() V44() V45() Element of bool REAL
upper_bound (rng (X,Y,x,y,f,y,z)) is V28() real ext-real Element of REAL
(X,x,x,y,z) is V28() real ext-real Element of REAL
K11(x,[y,z]) is V28() real ext-real set
dom z is Relation-like X -defined x -valued Element of bool [:X,x:]
bool [:X,x:] is non empty set
dom x is Relation-like X -defined x -valued Element of bool [:X,x:]
X is non empty set
Y is non empty set
[:X,Y:] is Relation-like non empty set
[:[:X,Y:],REAL:] is Relation-like non empty V33() V34() V35() set
bool [:[:X,Y:],REAL:] is non empty set
x is non empty set
[:Y,x:] is Relation-like non empty set
[:[:Y,x:],REAL:] is Relation-like non empty V33() V34() V35() set
bool [:[:Y,x:],REAL:] is non empty set
y is Relation-like [:X,Y:] -defined REAL -valued [.0,1.] -valued V6() V18([:X,Y:], REAL ) V33() V34() V35() Element of bool [:[:X,Y:],REAL:]
f is Relation-like [:Y,x:] -defined REAL -valued [.0,1.] -valued V6() V18([:Y,x:], REAL ) V33() V34() V35() Element of bool [:[:Y,x:],REAL:]
x is Relation-like [:Y,x:] -defined REAL -valued [.0,1.] -valued V6() V18([:Y,x:], REAL ) V33() V34() V35() Element of bool [:[:Y,x:],REAL:]
max (f,x) is Relation-like [:Y,x:] -defined REAL -valued [.0,1.] -valued V6() V18([:Y,x:], REAL ) V33() V34() V35() Element of bool [:[:Y,x:],REAL:]
z is set
r is set
(X,Y,x,y,(max (f,x)),z,r) is Relation-like Y -defined REAL -valued [.0,1.] -valued V6() V18(Y, REAL ) V33() V34() V35() Element of bool [:Y,REAL:]
[:Y,REAL:] is Relation-like non empty V33() V34() V35() set
bool [:Y,REAL:] is non empty set
rng (X,Y,x,y,(max (f,x)),z,r) is non empty V43() V44() V45() Element of bool REAL
upper_bound (rng (X,Y,x,y,(max (f,x)),z,r)) is V28() real ext-real Element of REAL
(X,Y,x,y,f,z,r) is Relation-like Y -defined REAL -valued [.0,1.] -valued V6() V18(Y, REAL ) V33() V34() V35() Element of bool [:Y,REAL:]
rng (X,Y,x,y,f,z,r) is non empty V43() V44() V45() Element of bool REAL
upper_bound (rng (X,Y,x,y,f,z,r)) is V28() real ext-real Element of REAL
(X,Y,x,y,x,z,r) is Relation-like Y -defined REAL -valued [.0,1.] -valued V6() V18(Y, REAL ) V33() V34() V35() Element of bool [:Y,REAL:]
rng (X,Y,x,y,x,z,r) is non empty V43() V44() V45() Element of bool REAL
upper_bound (rng (X,Y,x,y,x,z,r)) is V28() real ext-real Element of REAL
max ((upper_bound (rng (X,Y,x,y,f,z,r))),(upper_bound (rng (X,Y,x,y,x,z,r)))) is V28() real ext-real Element of REAL
max ((X,Y,x,y,f,z,r),(X,Y,x,y,x,z,r)) is Relation-like Y -defined REAL -valued [.0,1.] -valued V6() V18(Y, REAL ) V33() V34() V35() Element of bool [:Y,REAL:]
y is Element of Y
(max ((X,Y,x,y,f,z,r),(X,Y,x,y,x,z,r))) . y is V28() real ext-real Element of REAL
(X,Y,x,y,(max (f,x)),z,r) . y is V28() real ext-real Element of REAL
[y,r] is set
{y,r} is non empty set
{y} is non empty set
{{y,r},{y}} is non empty set
(X,Y,x,y,f,z,r) . y is V28() real ext-real Element of REAL
(X,Y,x,y,x,z,r) . y is V28() real ext-real Element of REAL
max (((X,Y,x,y,f,z,r) . y),((X,Y,x,y,x,z,r) . y)) is V28() real ext-real Element of REAL
[z,y] is set
{z,y} is non empty set
{z} is non empty set
{{z,y},{z}} is non empty set
y . [z,y] is V28() real ext-real Element of REAL
x . [y,r] is V28() real ext-real Element of REAL
min ((y . [z,y]),(x . [y,r])) is V28() real ext-real Element of REAL
max (((X,Y,x,y,f,z,r) . y),(min ((y . [z,y]),(x . [y,r])))) is V28() real ext-real Element of REAL
f . [y,r] is V28() real ext-real Element of REAL
min ((y . [z,y]),(f . [y,r])) is V28() real ext-real Element of REAL
max ((min ((y . [z,y]),(f . [y,r]))),(min ((y . [z,y]),(x . [y,r])))) is V28() real ext-real Element of REAL
max ((f . [y,r]),(x . [y,r])) is V28() real ext-real Element of REAL
min ((y . [z,y]),(max ((f . [y,r]),(x . [y,r])))) is V28() real ext-real Element of REAL
(max (f,x)) . [y,r] is V28() real ext-real Element of REAL
min ((y . [z,y]),((max (f,x)) . [y,r])) is V28() real ext-real Element of REAL
dom (X,Y,x,y,(max (f,x)),z,r) is Element of bool Y
bool Y is non empty set
rng (max ((X,Y,x,y,f,z,r),(X,Y,x,y,x,z,r))) is non empty V43() V44() V45() Element of bool REAL
dom (max ((X,Y,x,y,f,z,r),(X,Y,x,y,x,z,r))) is Element of bool Y
upper_bound (rng (max ((X,Y,x,y,f,z,r),(X,Y,x,y,x,z,r)))) is V28() real ext-real Element of REAL
y is V28() real ext-real set
(upper_bound (rng (max ((X,Y,x,y,f,z,r),(X,Y,x,y,x,z,r))))) - y is V28() real ext-real set
y is V28() real ext-real set
y is set
(max ((X,Y,x,y,f,z,r),(X,Y,x,y,x,z,r))) . y is V28() real ext-real Element of REAL
y is V28() real ext-real set
(upper_bound (rng (max ((X,Y,x,y,f,z,r),(X,Y,x,y,x,z,r))))) - y is V28() real ext-real set
y is set
(max ((X,Y,x,y,f,z,r),(X,Y,x,y,x,z,r))) . y is V28() real ext-real Element of REAL
(X,Y,x,y,f,z,r) . y is V28() real ext-real Element of REAL
(X,Y,x,y,x,z,r) . y is V28() real ext-real Element of REAL
max (((X,Y,x,y,f,z,r) . y),((X,Y,x,y,x,z,r) . y)) is V28() real ext-real Element of REAL
y is set
(X,Y,x,y,f,z,r) . y is V28() real ext-real Element of REAL
(X,Y,x,y,x,z,r) . y is V28() real ext-real Element of REAL
dom (X,Y,x,y,x,z,r) is Element of bool Y
dom (X,Y,x,y,f,z,r) is Element of bool Y
y is V28() real ext-real set
(upper_bound (rng (max ((X,Y,x,y,f,z,r),(X,Y,x,y,x,z,r))))) - y is V28() real ext-real set
y is set
(max ((X,Y,x,y,f,z,r),(X,Y,x,y,x,z,r))) . y is V28() real ext-real Element of REAL
dom (X,Y,x,y,x,z,r) is Element of bool Y
y is V28() real ext-real set
(upper_bound (rng (X,Y,x,y,x,z,r))) - y is V28() real ext-real set
y is V28() real ext-real set
y is set
(X,Y,x,y,x,z,r) . y is V28() real ext-real Element of REAL
y is V28() real ext-real set
(upper_bound (rng (X,Y,x,y,x,z,r))) - y is V28() real ext-real set
y is set
(X,Y,x,y,x,z,r) . y is V28() real ext-real Element of REAL
(X,Y,x,y,f,z,r) . y is V28() real ext-real Element of REAL
max (((X,Y,x,y,f,z,r) . y),((X,Y,x,y,x,z,r) . y)) is V28() real ext-real Element of REAL
(max ((X,Y,x,y,f,z,r),(X,Y,x,y,x,z,r))) . y is V28() real ext-real Element of REAL
dom (X,Y,x,y,f,z,r) is Element of bool Y
y is V28() real ext-real set
(upper_bound (rng (X,Y,x,y,f,z,r))) - y is V28() real ext-real set
y is V28() real ext-real set
y is set
(X,Y,x,y,f,z,r) . y is V28() real ext-real Element of REAL
y is V28() real ext-real set
(upper_bound (rng (X,Y,x,y,f,z,r))) - y is V28() real ext-real set
y is set
(X,Y,x,y,f,z,r) . y is V28() real ext-real Element of REAL
(X,Y,x,y,x,z,r) . y is V28() real ext-real Element of REAL
max (((X,Y,x,y,f,z,r) . y),((X,Y,x,y,x,z,r) . y)) is V28() real ext-real Element of REAL
(max ((X,Y,x,y,f,z,r),(X,Y,x,y,x,z,r))) . y is V28() real ext-real Element of REAL
X is non empty set
Y is non empty set
[:X,Y:] is Relation-like non empty set
[:[:X,Y:],REAL:] is Relation-like non empty V33() V34() V35() set
bool [:[:X,Y:],REAL:] is non empty set
x is non empty set
[:Y,x:] is Relation-like non empty set
[:[:Y,x:],REAL:] is Relation-like non empty V33() V34() V35() set
bool [:[:Y,x:],REAL:] is non empty set
[:X,x:] is Relation-like non empty set
y is Relation-like [:X,Y:] -defined REAL -valued [.0,1.] -valued V6() V18([:X,Y:], REAL ) V33() V34() V35() Element of bool [:[:X,Y:],REAL:]
f is Relation-like [:Y,x:] -defined REAL -valued [.0,1.] -valued V6() V18([:Y,x:], REAL ) V33() V34() V35() Element of bool [:[:Y,x:],REAL:]
x is Relation-like [:Y,x:] -defined REAL -valued [.0,1.] -valued V6() V18([:Y,x:], REAL ) V33() V34() V35() Element of bool [:[:Y,x:],REAL:]
max (f,x) is Relation-like [:Y,x:] -defined REAL -valued [.0,1.] -valued V6() V18([:Y,x:], REAL ) V33() V34() V35() Element of bool [:[:Y,x:],REAL:]
(X,Y,x,y,(max (f,x))) is Relation-like [:X,x:] -defined REAL -valued [.0,1.] -valued V6() V18([:X,x:], REAL ) V33() V34() V35() Element of bool [:[:X,x:],REAL:]
[:[:X,x:],REAL:] is Relation-like non empty V33() V34() V35() set
bool [:[:X,x:],REAL:] is non empty set
(X,Y,x,y,f) is Relation-like [:X,x:] -defined REAL -valued [.0,1.] -valued V6() V18([:X,x:], REAL ) V33() V34() V35() Element of bool [:[:X,x:],REAL:]
(X,Y,x,y,x) is Relation-like [:X,x:] -defined REAL -valued [.0,1.] -valued V6() V18([:X,x:], REAL ) V33() V34() V35() Element of bool [:[:X,x:],REAL:]
max ((X,Y,x,y,f),(X,Y,x,y,x)) is Relation-like [:X,x:] -defined REAL -valued [.0,1.] -valued V6() V18([:X,x:], REAL ) V33() V34() V35() Element of bool [:[:X,x:],REAL:]
dom (max ((X,Y,x,y,f),(X,Y,x,y,x))) is Relation-like X -defined x -valued Element of bool [:X,x:]
bool [:X,x:] is non empty set
z is Element of [:X,x:]
(X,Y,x,y,(max (f,x))) . z is V28() real ext-real Element of REAL
(max ((X,Y,x,y,f),(X,Y,x,y,x))) . z is V28() real ext-real Element of REAL
r is set
y is set
[r,y] is set
{r,y} is non empty set
{r} is non empty set
{{r,y},{r}} is non empty set
(X,x,(X,Y,x,y,(max (f,x))),r,y) is V28() real ext-real Element of REAL
K11((X,Y,x,y,(max (f,x))),[r,y]) is V28() real ext-real set
(X,Y,x,y,(max (f,x)),r,y) is Relation-like Y -defined REAL -valued [.0,1.] -valued V6() V18(Y, REAL ) V33() V34() V35() Element of bool [:Y,REAL:]
[:Y,REAL:] is Relation-like non empty V33() V34() V35() set
bool [:Y,REAL:] is non empty set
rng (X,Y,x,y,(max (f,x)),r,y) is non empty V43() V44() V45() Element of bool REAL
upper_bound (rng (X,Y,x,y,(max (f,x)),r,y)) is V28() real ext-real Element of REAL
(X,Y,x,y,f,r,y) is Relation-like Y -defined REAL -valued [.0,1.] -valued V6() V18(Y, REAL ) V33() V34() V35() Element of bool [:Y,REAL:]
rng (X,Y,x,y,f,r,y) is non empty V43() V44() V45() Element of bool REAL
upper_bound (rng (X,Y,x,y,f,r,y)) is V28() real ext-real Element of REAL
(X,Y,x,y,x,r,y) is Relation-like Y -defined REAL -valued [.0,1.] -valued V6() V18(Y, REAL ) V33() V34() V35() Element of bool [:Y,REAL:]
rng (X,Y,x,y,x,r,y) is non empty V43() V44() V45() Element of bool REAL
upper_bound (rng (X,Y,x,y,x,r,y)) is V28() real ext-real Element of REAL
max ((upper_bound (rng (X,Y,x,y,f,r,y))),(upper_bound (rng (X,Y,x,y,x,r,y)))) is V28() real ext-real Element of REAL
(X,x,(X,Y,x,y,f),r,y) is V28() real ext-real Element of REAL
K11((X,Y,x,y,f),[r,y]) is V28() real ext-real set
max ((X,x,(X,Y,x,y,f),r,y),(upper_bound (rng (X,Y,x,y,x,r,y)))) is V28() real ext-real Element of REAL
(X,x,(X,Y,x,y,x),r,y) is V28() real ext-real Element of REAL
K11((X,Y,x,y,x),[r,y]) is V28() real ext-real set
max ((X,x,(X,Y,x,y,f),r,y),(X,x,(X,Y,x,y,x),r,y)) is V28() real ext-real Element of REAL
dom (X,Y,x,y,(max (f,x))) is Relation-like X -defined x -valued Element of bool [:X,x:]
X is non empty set
Y is non empty set
[:X,Y:] is Relation-like non empty set
[:[:X,Y:],REAL:] is Relation-like non empty V33() V34() V35() set
bool [:[:X,Y:],REAL:] is non empty set
x is non empty set
[:Y,x:] is Relation-like non empty set
[:[:Y,x:],REAL:] is Relation-like non empty V33() V34() V35() set
bool [:[:Y,x:],REAL:] is non empty set
y is Relation-like [:X,Y:] -defined REAL -valued [.0,1.] -valued V6() V18([:X,Y:], REAL ) V33() V34() V35() Element of bool [:[:X,Y:],REAL:]
f is Relation-like [:X,Y:] -defined REAL -valued [.0,1.] -valued V6() V18([:X,Y:], REAL ) V33() V34() V35() Element of bool [:[:X,Y:],REAL:]
max (y,f) is Relation-like [:X,Y:] -defined REAL -valued [.0,1.] -valued V6() V18([:X,Y:], REAL ) V33() V34() V35() Element of bool [:[:X,Y:],REAL:]
x is Relation-like [:Y,x:] -defined REAL -valued [.0,1.] -valued V6() V18([:Y,x:], REAL ) V33() V34() V35() Element of bool [:[:Y,x:],REAL:]
z is set
r is set
(X,Y,x,(max (y,f)),x,z,r) is Relation-like Y -defined REAL -valued [.0,1.] -valued V6() V18(Y, REAL ) V33() V34() V35() Element of bool [:Y,REAL:]
[:Y,REAL:] is Relation-like non empty V33() V34() V35() set
bool [:Y,REAL:] is non empty set
rng (X,Y,x,(max (y,f)),x,z,r) is non empty V43() V44() V45() Element of bool REAL
upper_bound (rng (X,Y,x,(max (y,f)),x,z,r)) is V28() real ext-real Element of REAL
(X,Y,x,y,x,z,r) is Relation-like Y -defined REAL -valued [.0,1.] -valued V6() V18(Y, REAL ) V33() V34() V35() Element of bool [:Y,REAL:]
rng (X,Y,x,y,x,z,r) is non empty V43() V44() V45() Element of bool REAL
upper_bound (rng (X,Y,x,y,x,z,r)) is V28() real ext-real Element of REAL
(X,Y,x,f,x,z,r) is Relation-like Y -defined REAL -valued [.0,1.] -valued V6() V18(Y, REAL ) V33() V34() V35() Element of bool [:Y,REAL:]
rng (X,Y,x,f,x,z,r) is non empty V43() V44() V45() Element of bool REAL
upper_bound (rng (X,Y,x,f,x,z,r)) is V28() real ext-real Element of REAL
max ((upper_bound (rng (X,Y,x,y,x,z,r))),(upper_bound (rng (X,Y,x,f,x,z,r)))) is V28() real ext-real Element of REAL
max ((X,Y,x,y,x,z,r),(X,Y,x,f,x,z,r)) is Relation-like Y -defined REAL -valued [.0,1.] -valued V6() V18(Y, REAL ) V33() V34() V35() Element of bool [:Y,REAL:]
y is Element of Y
(X,Y,x,(max (y,f)),x,z,r) . y is V28() real ext-real Element of REAL
(max ((X,Y,x,y,x,z,r),(X,Y,x,f,x,z,r))) . y is V28() real ext-real Element of REAL
[z,y] is set
{z,y} is non empty set
{z} is non empty set
{{z,y},{z}} is non empty set
(max (y,f)) . [z,y] is V28() real ext-real Element of REAL
[y,r] is set
{y,r} is non empty set
{y} is non empty set
{{y,r},{y}} is non empty set
x . [y,r] is V28() real ext-real Element of REAL
min (((max (y,f)) . [z,y]),(x . [y,r])) is V28() real ext-real Element of REAL
y . [z,y] is V28() real ext-real Element of REAL
f . [z,y] is V28() real ext-real Element of REAL
max ((y . [z,y]),(f . [z,y])) is V28() real ext-real Element of REAL
min ((max ((y . [z,y]),(f . [z,y]))),(x . [y,r])) is V28() real ext-real Element of REAL
min ((y . [z,y]),(x . [y,r])) is V28() real ext-real Element of REAL
min ((f . [z,y]),(x . [y,r])) is V28() real ext-real Element of REAL
max ((min ((y . [z,y]),(x . [y,r]))),(min ((f . [z,y]),(x . [y,r])))) is V28() real ext-real Element of REAL
(X,Y,x,f,x,z,r) . y is V28() real ext-real Element of REAL
max ((min ((y . [z,y]),(x . [y,r]))),((X,Y,x,f,x,z,r) . y)) is V28() real ext-real Element of REAL
(X,Y,x,y,x,z,r) . y is V28() real ext-real Element of REAL
max (((X,Y,x,y,x,z,r) . y),((X,Y,x,f,x,z,r) . y)) is V28() real ext-real Element of REAL
dom (max ((X,Y,x,y,x,z,r),(X,Y,x,f,x,z,r))) is Element of bool Y
bool Y is non empty set
rng (max ((X,Y,x,y,x,z,r),(X,Y,x,f,x,z,r))) is non empty V43() V44() V45() Element of bool REAL
upper_bound (rng (max ((X,Y,x,y,x,z,r),(X,Y,x,f,x,z,r)))) is V28() real ext-real Element of REAL
y is set
(max ((X,Y,x,y,x,z,r),(X,Y,x,f,x,z,r))) . y is V28() real ext-real Element of REAL
dom (X,Y,x,f,x,z,r) is Element of bool Y
y is set
(X,Y,x,f,x,z,r) . y is V28() real ext-real Element of REAL
y is V28() real ext-real set
(upper_bound (rng (X,Y,x,f,x,z,r))) - y is V28() real ext-real set
y is V28() real ext-real set
y is set
(X,Y,x,f,x,z,r) . y is V28() real ext-real Element of REAL
(X,Y,x,y,x,z,r) . y is V28() real ext-real Element of REAL
max (((X,Y,x,y,x,z,r) . y),((X,Y,x,f,x,z,r) . y)) is V28() real ext-real Element of REAL
(max ((X,Y,x,y,x,z,r),(X,Y,x,f,x,z,r))) . y is V28() real ext-real Element of REAL
y is V28() real ext-real set
(upper_bound (rng (X,Y,x,f,x,z,r))) - y is V28() real ext-real set
y is set
(max ((X,Y,x,y,x,z,r),(X,Y,x,f,x,z,r))) . y is V28() real ext-real Element of REAL
dom (X,Y,x,y,x,z,r) is Element of bool Y
y is V28() real ext-real set
(upper_bound (rng (X,Y,x,y,x,z,r))) - y is V28() real ext-real set
y is V28() real ext-real set
y is set
(X,Y,x,y,x,z,r) . y is V28() real ext-real Element of REAL
(X,Y,x,f,x,z,r) . y is V28() real ext-real Element of REAL
max (((X,Y,x,y,x,z,r) . y),((X,Y,x,f,x,z,r) . y)) is V28() real ext-real Element of REAL
(max ((X,Y,x,y,x,z,r),(X,Y,x,f,x,z,r))) . y is V28() real ext-real Element of REAL
y is V28() real ext-real set
(upper_bound (rng (X,Y,x,y,x,z,r))) - y is V28() real ext-real set
y is set
(max ((X,Y,x,y,x,z,r),(X,Y,x,f,x,z,r))) . y is V28() real ext-real Element of REAL
y is set
(X,Y,x,y,x,z,r) . y is V28() real ext-real Element of REAL
y is V28() real ext-real set
(upper_bound (rng (max ((X,Y,x,y,x,z,r),(X,Y,x,f,x,z,r))))) - y is V28() real ext-real set
y is V28() real ext-real set
y is set
(max ((X,Y,x,y,x,z,r),(X,Y,x,f,x,z,r))) . y is V28() real ext-real Element of REAL
(X,Y,x,f,x,z,r) . y is V28() real ext-real Element of REAL
(X,Y,x,y,x,z,r) . y is V28() real ext-real Element of REAL
max (((X,Y,x,y,x,z,r) . y),((X,Y,x,f,x,z,r) . y)) is V28() real ext-real Element of REAL
dom (X,Y,x,(max (y,f)),x,z,r) is Element of bool Y
X is non empty set
Y is non empty set
[:X,Y:] is Relation-like non empty set
[:[:X,Y:],REAL:] is Relation-like non empty V33() V34() V35() set
bool [:[:X,Y:],REAL:] is non empty set
x is non empty set
[:Y,x:] is Relation-like non empty set
[:[:Y,x:],REAL:] is Relation-like non empty V33() V34() V35() set
bool [:[:Y,x:],REAL:] is non empty set
[:X,x:] is Relation-like non empty set
y is Relation-like [:X,Y:] -defined REAL -valued [.0,1.] -valued V6() V18([:X,Y:], REAL ) V33() V34() V35() Element of bool [:[:X,Y:],REAL:]
f is Relation-like [:X,Y:] -defined REAL -valued [.0,1.] -valued V6() V18([:X,Y:], REAL ) V33() V34() V35() Element of bool [:[:X,Y:],REAL:]
max (y,f) is Relation-like [:X,Y:] -defined REAL -valued [.0,1.] -valued V6() V18([:X,Y:], REAL ) V33() V34() V35() Element of bool [:[:X,Y:],REAL:]
x is Relation-like [:Y,x:] -defined REAL -valued [.0,1.] -valued V6() V18([:Y,x:], REAL ) V33() V34() V35() Element of bool [:[:Y,x:],REAL:]
(X,Y,x,(max (y,f)),x) is Relation-like [:X,x:] -defined REAL -valued [.0,1.] -valued V6() V18([:X,x:], REAL ) V33() V34() V35() Element of bool [:[:X,x:],REAL:]
[:[:X,x:],REAL:] is Relation-like non empty V33() V34() V35() set
bool [:[:X,x:],REAL:] is non empty set
(X,Y,x,y,x) is Relation-like [:X,x:] -defined REAL -valued [.0,1.] -valued V6() V18([:X,x:], REAL ) V33() V34() V35() Element of bool [:[:X,x:],REAL:]
(X,Y,x,f,x) is Relation-like [:X,x:] -defined REAL -valued [.0,1.] -valued V6() V18([:X,x:], REAL ) V33() V34() V35() Element of bool [:[:X,x:],REAL:]
max ((X,Y,x,y,x),(X,Y,x,f,x)) is Relation-like [:X,x:] -defined REAL -valued [.0,1.] -valued V6() V18([:X,x:], REAL ) V33() V34() V35() Element of bool [:[:X,x:],REAL:]
dom (max ((X,Y,x,y,x),(X,Y,x,f,x))) is Relation-like X -defined x -valued Element of bool [:X,x:]
bool [:X,x:] is non empty set
z is Element of [:X,x:]
(X,Y,x,(max (y,f)),x) . z is V28() real ext-real Element of REAL
(max ((X,Y,x,y,x),(X,Y,x,f,x))) . z is V28() real ext-real Element of REAL
r is set
y is set
[r,y] is set
{r,y} is non empty set
{r} is non empty set
{{r,y},{r}} is non empty set
(X,x,(X,Y,x,(max (y,f)),x),r,y) is V28() real ext-real Element of REAL
K11((X,Y,x,(max (y,f)),x),[r,y]) is V28() real ext-real set
(X,Y,x,(max (y,f)),x,r,y) is Relation-like Y -defined REAL -valued [.0,1.] -valued V6() V18(Y, REAL ) V33() V34() V35() Element of bool [:Y,REAL:]
[:Y,REAL:] is Relation-like non empty V33() V34() V35() set
bool [:Y,REAL:] is non empty set
rng (X,Y,x,(max (y,f)),x,r,y) is non empty V43() V44() V45() Element of bool REAL
upper_bound (rng (X,Y,x,(max (y,f)),x,r,y)) is V28() real ext-real Element of REAL
(X,Y,x,y,x,r,y) is Relation-like Y -defined REAL -valued [.0,1.] -valued V6() V18(Y, REAL ) V33() V34() V35() Element of bool [:Y,REAL:]
rng (X,Y,x,y,x,r,y) is non empty V43() V44() V45() Element of bool REAL
upper_bound (rng (X,Y,x,y,x,r,y)) is V28() real ext-real Element of REAL
(X,Y,x,f,x,r,y) is Relation-like Y -defined REAL -valued [.0,1.] -valued V6() V18(Y, REAL ) V33() V34() V35() Element of bool [:Y,REAL:]
rng (X,Y,x,f,x,r,y) is non empty V43() V44() V45() Element of bool REAL
upper_bound (rng (X,Y,x,f,x,r,y)) is V28() real ext-real Element of REAL
max ((upper_bound (rng (X,Y,x,y,x,r,y))),(upper_bound (rng (X,Y,x,f,x,r,y)))) is V28() real ext-real Element of REAL
(X,x,(X,Y,x,y,x),r,y) is V28() real ext-real Element of REAL
K11((X,Y,x,y,x),[r,y]) is V28() real ext-real set
max ((X,x,(X,Y,x,y,x),r,y),(upper_bound (rng (X,Y,x,f,x,r,y)))) is V28() real ext-real Element of REAL
(X,x,(X,Y,x,f,x),r,y) is V28() real ext-real Element of REAL
K11((X,Y,x,f,x),[r,y]) is V28() real ext-real set
max ((X,x,(X,Y,x,y,x),r,y),(X,x,(X,Y,x,f,x),r,y)) is V28() real ext-real Element of REAL
dom (X,Y,x,(max (y,f)),x) is Relation-like X -defined x -valued Element of bool [:X,x:]
X is non empty set
Y is non empty set
[:X,Y:] is Relation-like non empty set
[:[:X,Y:],REAL:] is Relation-like non empty V33() V34() V35() set
bool [:[:X,Y:],REAL:] is non empty set
x is non empty set
[:Y,x:] is Relation-like non empty set
[:[:Y,x:],REAL:] is Relation-like non empty V33() V34() V35() set
bool [:[:Y,x:],REAL:] is non empty set
y is Relation-like [:X,Y:] -defined REAL -valued [.0,1.] -valued V6() V18([:X,Y:], REAL ) V33() V34() V35() Element of bool [:[:X,Y:],REAL:]
f is Relation-like [:Y,x:] -defined REAL -valued [.0,1.] -valued V6() V18([:Y,x:], REAL ) V33() V34() V35() Element of bool [:[:Y,x:],REAL:]
x is Relation-like [:Y,x:] -defined REAL -valued [.0,1.] -valued V6() V18([:Y,x:], REAL ) V33() V34() V35() Element of bool [:[:Y,x:],REAL:]
min (f,x) is Relation-like [:Y,x:] -defined REAL -valued [.0,1.] -valued V6() V18([:Y,x:], REAL ) V33() V34() V35() Element of bool [:[:Y,x:],REAL:]
z is set
r is set
(X,Y,x,y,(min (f,x)),z,r) is Relation-like Y -defined REAL -valued [.0,1.] -valued V6() V18(Y, REAL ) V33() V34() V35() Element of bool [:Y,REAL:]
[:Y,REAL:] is Relation-like non empty V33() V34() V35() set
bool [:Y,REAL:] is non empty set
rng (X,Y,x,y,(min (f,x)),z,r) is non empty V43() V44() V45() Element of bool REAL
upper_bound (rng (X,Y,x,y,(min (f,x)),z,r)) is V28() real ext-real Element of REAL
(X,Y,x,y,f,z,r) is Relation-like Y -defined REAL -valued [.0,1.] -valued V6() V18(Y, REAL ) V33() V34() V35() Element of bool [:Y,REAL:]
rng (X,Y,x,y,f,z,r) is non empty V43() V44() V45() Element of bool REAL
upper_bound (rng (X,Y,x,y,f,z,r)) is V28() real ext-real Element of REAL
(X,Y,x,y,x,z,r) is Relation-like Y -defined REAL -valued [.0,1.] -valued V6() V18(Y, REAL ) V33() V34() V35() Element of bool [:Y,REAL:]
rng (X,Y,x,y,x,z,r) is non empty V43() V44() V45() Element of bool REAL
upper_bound (rng (X,Y,x,y,x,z,r)) is V28() real ext-real Element of REAL
min ((upper_bound (rng (X,Y,x,y,f,z,r))),(upper_bound (rng (X,Y,x,y,x,z,r)))) is V28() real ext-real Element of REAL
dom (X,Y,x,y,(min (f,x)),z,r) is Element of bool Y
bool Y is non empty set
y is V28() real ext-real set
(upper_bound (rng (X,Y,x,y,(min (f,x)),z,r))) - y is V28() real ext-real set
y is V28() real ext-real set
y is set
(X,Y,x,y,(min (f,x)),z,r) . y is V28() real ext-real Element of REAL
[y,r] is set
{y,r} is non empty set
{y} is non empty set
{{y,r},{y}} is non empty set
[z,y] is set
{z,y} is non empty set
{z} is non empty set
{{z,y},{z}} is non empty set
y . [z,y] is V28() real ext-real Element of REAL
(min (f,x)) . [y,r] is V28() real ext-real Element of REAL
min ((y . [z,y]),((min (f,x)) . [y,r])) is V28() real ext-real Element of REAL
f . [y,r] is V28() real ext-real Element of REAL
x . [y,r] is V28() real ext-real Element of REAL
min ((f . [y,r]),(x . [y,r])) is V28() real ext-real Element of REAL
min ((y . [z,y]),(min ((f . [y,r]),(x . [y,r])))) is V28() real ext-real Element of REAL
min ((y . [z,y]),(f . [y,r])) is V28() real ext-real Element of REAL
min ((min ((y . [z,y]),(f . [y,r]))),(x . [y,r])) is V28() real ext-real Element of REAL
(X,Y,x,y,f,z,r) . y is V28() real ext-real Element of REAL
min (((X,Y,x,y,f,z,r) . y),(x . [y,r])) is V28() real ext-real Element of REAL
y is V28() real ext-real set
(upper_bound (rng (X,Y,x,y,(min (f,x)),z,r))) - y is V28() real ext-real set
y is V28() real ext-real set
y is set
(X,Y,x,y,(min (f,x)),z,r) . y is V28() real ext-real Element of REAL
[y,r] is set
{y,r} is non empty set
{y} is non empty set
{{y,r},{y}} is non empty set
[z,y] is set
{z,y} is non empty set
{z} is non empty set
{{z,y},{z}} is non empty set
y . [z,y] is V28() real ext-real Element of REAL
(min (f,x)) . [y,r] is V28() real ext-real Element of REAL
min ((y . [z,y]),((min (f,x)) . [y,r])) is V28() real ext-real Element of REAL
f . [y,r] is V28() real ext-real Element of REAL
x . [y,r] is V28() real ext-real Element of REAL
min ((f . [y,r]),(x . [y,r])) is V28() real ext-real Element of REAL
min ((y . [z,y]),(min ((f . [y,r]),(x . [y,r])))) is V28() real ext-real Element of REAL
min ((y . [z,y]),(x . [y,r])) is V28() real ext-real Element of REAL
min ((min ((y . [z,y]),(x . [y,r]))),(f . [y,r])) is V28() real ext-real Element of REAL
(X,Y,x,y,x,z,r) . y is V28() real ext-real Element of REAL
min (((X,Y,x,y,x,z,r) . y),(f . [y,r])) is V28() real ext-real Element of REAL
dom (X,Y,x,y,x,z,r) is Element of bool Y
y is set
(X,Y,x,y,x,z,r) . y is V28() real ext-real Element of REAL
y is V28() real ext-real set
(upper_bound (rng (X,Y,x,y,(min (f,x)),z,r))) - y is V28() real ext-real set
y is set
(X,Y,x,y,x,z,r) . y is V28() real ext-real Element of REAL
dom (X,Y,x,y,f,z,r) is Element of bool Y
y is set
(X,Y,x,y,f,z,r) . y is V28() real ext-real Element of REAL
y is V28() real ext-real set
(upper_bound (rng (X,Y,x,y,(min (f,x)),z,r))) - y is V28() real ext-real set
y is set
(X,Y,x,y,f,z,r) . y is V28() real ext-real Element of REAL
X is non empty set
Y is non empty set
[:X,Y:] is Relation-like non empty set
[:[:X,Y:],REAL:] is Relation-like non empty V33() V34() V35() set
bool [:[:X,Y:],REAL:] is non empty set
x is non empty set
[:Y,x:] is Relation-like non empty set
[:[:Y,x:],REAL:] is Relation-like non empty V33() V34() V35() set
bool [:[:Y,x:],REAL:] is non empty set
[:X,x:] is Relation-like non empty set
y is Relation-like [:X,Y:] -defined REAL -valued [.0,1.] -valued V6() V18([:X,Y:], REAL ) V33() V34() V35() Element of bool [:[:X,Y:],REAL:]
f is Relation-like [:Y,x:] -defined REAL -valued [.0,1.] -valued V6() V18([:Y,x:], REAL ) V33() V34() V35() Element of bool [:[:Y,x:],REAL:]
x is Relation-like [:Y,x:] -defined REAL -valued [.0,1.] -valued V6() V18([:Y,x:], REAL ) V33() V34() V35() Element of bool [:[:Y,x:],REAL:]
min (f,x) is Relation-like [:Y,x:] -defined REAL -valued [.0,1.] -valued V6() V18([:Y,x:], REAL ) V33() V34() V35() Element of bool [:[:Y,x:],REAL:]
(X,Y,x,y,(min (f,x))) is Relation-like [:X,x:] -defined REAL -valued [.0,1.] -valued V6() V18([:X,x:], REAL ) V33() V34() V35() Element of bool [:[:X,x:],REAL:]
[:[:X,x:],REAL:] is Relation-like non empty V33() V34() V35() set
bool [:[:X,x:],REAL:] is non empty set
(X,Y,x,y,f) is Relation-like [:X,x:] -defined REAL -valued [.0,1.] -valued V6() V18([:X,x:], REAL ) V33() V34() V35() Element of bool [:[:X,x:],REAL:]
(X,Y,x,y,x) is Relation-like [:X,x:] -defined REAL -valued [.0,1.] -valued V6() V18([:X,x:], REAL ) V33() V34() V35() Element of bool [:[:X,x:],REAL:]
min ((X,Y,x,y,f),(X,Y,x,y,x)) is Relation-like [:X,x:] -defined REAL -valued [.0,1.] -valued V6() V18([:X,x:], REAL ) V33() V34() V35() Element of bool [:[:X,x:],REAL:]
z is Element of [:X,x:]
(X,Y,x,y,(min (f,x))) . z is V28() real ext-real Element of REAL
(min ((X,Y,x,y,f),(X,Y,x,y,x))) . z is V28() real ext-real Element of REAL
r is set
y is set
[r,y] is set
{r,y} is non empty set
{r} is non empty set
{{r,y},{r}} is non empty set
(X,x,(X,Y,x,y,(min (f,x))),r,y) is V28() real ext-real Element of REAL
K11((X,Y,x,y,(min (f,x))),[r,y]) is V28() real ext-real set
(X,Y,x,y,(min (f,x)),r,y) is Relation-like Y -defined REAL -valued [.0,1.] -valued V6() V18(Y, REAL ) V33() V34() V35() Element of bool [:Y,REAL:]
[:Y,REAL:] is Relation-like non empty V33() V34() V35() set
bool [:Y,REAL:] is non empty set
rng (X,Y,x,y,(min (f,x)),r,y) is non empty V43() V44() V45() Element of bool REAL
upper_bound (rng (X,Y,x,y,(min (f,x)),r,y)) is V28() real ext-real Element of REAL
(X,x,(min ((X,Y,x,y,f),(X,Y,x,y,x))),r,y) is V28() real ext-real Element of REAL
K11((min ((X,Y,x,y,f),(X,Y,x,y,x))),[r,y]) is V28() real ext-real set
(X,x,(X,Y,x,y,f),r,y) is V28() real ext-real Element of REAL
K11((X,Y,x,y,f),[r,y]) is V28() real ext-real set
(X,x,(X,Y,x,y,x),r,y) is V28() real ext-real Element of REAL
K11((X,Y,x,y,x),[r,y]) is V28() real ext-real set
min ((X,x,(X,Y,x,y,f),r,y),(X,x,(X,Y,x,y,x),r,y)) is V28() real ext-real Element of REAL
(X,Y,x,y,x,r,y) is Relation-like Y -defined REAL -valued [.0,1.] -valued V6() V18(Y, REAL ) V33() V34() V35() Element of bool [:Y,REAL:]
rng (X,Y,x,y,x,r,y) is non empty V43() V44() V45() Element of bool REAL
upper_bound (rng (X,Y,x,y,x,r,y)) is V28() real ext-real Element of REAL
min ((X,x,(X,Y,x,y,f),r,y),(upper_bound (rng (X,Y,x,y,x,r,y)))) is V28() real ext-real Element of REAL
(X,Y,x,y,f,r,y) is Relation-like Y -defined REAL -valued [.0,1.] -valued V6() V18(Y, REAL ) V33() V34() V35() Element of bool [:Y,REAL:]
rng (X,Y,x,y,f,r,y) is non empty V43() V44() V45() Element of bool REAL
upper_bound (rng (X,Y,x,y,f,r,y)) is V28() real ext-real Element of REAL
min ((upper_bound (rng (X,Y,x,y,f,r,y))),(upper_bound (rng (X,Y,x,y,x,r,y)))) is V28() real ext-real Element of REAL
X is non empty set
Y is non empty set
[:X,Y:] is Relation-like non empty set
[:[:X,Y:],REAL:] is Relation-like non empty V33() V34() V35() set
bool [:[:X,Y:],REAL:] is non empty set
x is non empty set
[:Y,x:] is Relation-like non empty set
[:[:Y,x:],REAL:] is Relation-like non empty V33() V34() V35() set
bool [:[:Y,x:],REAL:] is non empty set
y is Relation-like [:X,Y:] -defined REAL -valued [.0,1.] -valued V6() V18([:X,Y:], REAL ) V33() V34() V35() Element of bool [:[:X,Y:],REAL:]
f is Relation-like [:X,Y:] -defined REAL -valued [.0,1.] -valued V6() V18([:X,Y:], REAL ) V33() V34() V35() Element of bool [:[:X,Y:],REAL:]
min (y,f) is Relation-like [:X,Y:] -defined REAL -valued [.0,1.] -valued V6() V18([:X,Y:], REAL ) V33() V34() V35() Element of bool [:[:X,Y:],REAL:]
x is Relation-like [:Y,x:] -defined REAL -valued [.0,1.] -valued V6() V18([:Y,x:], REAL ) V33() V34() V35() Element of bool [:[:Y,x:],REAL:]
z is set
r is set
(X,Y,x,(min (y,f)),x,z,r) is Relation-like Y -defined REAL -valued [.0,1.] -valued V6() V18(Y, REAL ) V33() V34() V35() Element of bool [:Y,REAL:]
[:Y,REAL:] is Relation-like non empty V33() V34() V35() set
bool [:Y,REAL:] is non empty set
rng (X,Y,x,(min (y,f)),x,z,r) is non empty V43() V44() V45() Element of bool REAL
upper_bound (rng (X,Y,x,(min (y,f)),x,z,r)) is V28() real ext-real Element of REAL
(X,Y,x,y,x,z,r) is Relation-like Y -defined REAL -valued [.0,1.] -valued V6() V18(Y, REAL ) V33() V34() V35() Element of bool [:Y,REAL:]
rng (X,Y,x,y,x,z,r) is non empty V43() V44() V45() Element of bool REAL
upper_bound (rng (X,Y,x,y,x,z,r)) is V28() real ext-real Element of REAL
(X,Y,x,f,x,z,r) is Relation-like Y -defined REAL -valued [.0,1.] -valued V6() V18(Y, REAL ) V33() V34() V35() Element of bool [:Y,REAL:]
rng (X,Y,x,f,x,z,r) is non empty V43() V44() V45() Element of bool REAL
upper_bound (rng (X,Y,x,f,x,z,r)) is V28() real ext-real Element of REAL
min ((upper_bound (rng (X,Y,x,y,x,z,r))),(upper_bound (rng (X,Y,x,f,x,z,r)))) is V28() real ext-real Element of REAL
dom (X,Y,x,(min (y,f)),x,z,r) is Element of bool Y
bool Y is non empty set
y is V28() real ext-real set
(upper_bound (rng (X,Y,x,(min (y,f)),x,z,r))) - y is V28() real ext-real set
y is V28() real ext-real set
y is set
(X,Y,x,(min (y,f)),x,z,r) . y is V28() real ext-real Element of REAL
[z,y] is set
{z,y} is non empty set
{z} is non empty set
{{z,y},{z}} is non empty set
(min (y,f)) . [z,y] is V28() real ext-real Element of REAL
[y,r] is set
{y,r} is non empty set
{y} is non empty set
{{y,r},{y}} is non empty set
x . [y,r] is V28() real ext-real Element of REAL
min (((min (y,f)) . [z,y]),(x . [y,r])) is V28() real ext-real Element of REAL
y . [z,y] is V28() real ext-real Element of REAL
f . [z,y] is V28() real ext-real Element of REAL
min ((y . [z,y]),(f . [z,y])) is V28() real ext-real Element of REAL
min ((min ((y . [z,y]),(f . [z,y]))),(x . [y,r])) is V28() real ext-real Element of REAL
min ((x . [y,r]),(y . [z,y])) is V28() real ext-real Element of REAL
min ((min ((x . [y,r]),(y . [z,y]))),(f . [z,y])) is V28() real ext-real Element of REAL
(X,Y,x,y,x,z,r) . y is V28() real ext-real Element of REAL
min (((X,Y,x,y,x,z,r) . y),(f . [z,y])) is V28() real ext-real Element of REAL
y is V28() real ext-real set
(upper_bound (rng (X,Y,x,(min (y,f)),x,z,r))) - y is V28() real ext-real set
y is V28() real ext-real set
y is set
(X,Y,x,(min (y,f)),x,z,r) . y is V28() real ext-real Element of REAL
[z,y] is set
{z,y} is non empty set
{z} is non empty set
{{z,y},{z}} is non empty set
(min (y,f)) . [z,y] is V28() real ext-real Element of REAL
[y,r] is set
{y,r} is non empty set
{y} is non empty set
{{y,r},{y}} is non empty set
x . [y,r] is V28() real ext-real Element of REAL
min (((min (y,f)) . [z,y]),(x . [y,r])) is V28() real ext-real Element of REAL
y . [z,y] is V28() real ext-real Element of REAL
f . [z,y] is V28() real ext-real Element of REAL
min ((y . [z,y]),(f . [z,y])) is V28() real ext-real Element of REAL
min ((min ((y . [z,y]),(f . [z,y]))),(x . [y,r])) is V28() real ext-real Element of REAL
min ((x . [y,r]),(f . [z,y])) is V28() real ext-real Element of REAL
min ((y . [z,y]),(min ((x . [y,r]),(f . [z,y])))) is V28() real ext-real Element of REAL
(X,Y,x,f,x,z,r) . y is V28() real ext-real Element of REAL
min (((X,Y,x,f,x,z,r) . y),(y . [z,y])) is V28() real ext-real Element of REAL
dom (X,Y,x,f,x,z,r) is Element of bool Y
y is set
(X,Y,x,f,x,z,r) . y is V28() real ext-real Element of REAL
y is V28() real ext-real set
(upper_bound (rng (X,Y,x,(min (y,f)),x,z,r))) - y is V28() real ext-real set
y is set
(X,Y,x,f,x,z,r) . y is V28() real ext-real Element of REAL
dom (X,Y,x,y,x,z,r) is Element of bool Y
y is set
(X,Y,x,y,x,z,r) . y is V28() real ext-real Element of REAL
y is V28() real ext-real set
(upper_bound (rng (X,Y,x,(min (y,f)),x,z,r))) - y is V28() real ext-real set
y is set
(X,Y,x,y,x,z,r) . y is V28() real ext-real Element of REAL
X is non empty set
Y is non empty set
[:X,Y:] is Relation-like non empty set
[:[:X,Y:],REAL:] is Relation-like non empty V33() V34() V35() set
bool [:[:X,Y:],REAL:] is non empty set
x is non empty set
[:Y,x:] is Relation-like non empty set
[:[:Y,x:],REAL:] is Relation-like non empty V33() V34() V35() set
bool [:[:Y,x:],REAL:] is non empty set
[:X,x:] is Relation-like non empty set
y is Relation-like [:X,Y:] -defined REAL -valued [.0,1.] -valued V6() V18([:X,Y:], REAL ) V33() V34() V35() Element of bool [:[:X,Y:],REAL:]
f is Relation-like [:X,Y:] -defined REAL -valued [.0,1.] -valued V6() V18([:X,Y:], REAL ) V33() V34() V35() Element of bool [:[:X,Y:],REAL:]
min (y,f) is Relation-like [:X,Y:] -defined REAL -valued [.0,1.] -valued V6() V18([:X,Y:], REAL ) V33() V34() V35() Element of bool [:[:X,Y:],REAL:]
x is Relation-like [:Y,x:] -defined REAL -valued [.0,1.] -valued V6() V18([:Y,x:], REAL ) V33() V34() V35() Element of bool [:[:Y,x:],REAL:]
(X,Y,x,(min (y,f)),x) is Relation-like [:X,x:] -defined REAL -valued [.0,1.] -valued V6() V18([:X,x:], REAL ) V33() V34() V35() Element of bool [:[:X,x:],REAL:]
[:[:X,x:],REAL:] is Relation-like non empty V33() V34() V35() set
bool [:[:X,x:],REAL:] is non empty set
(X,Y,x,y,x) is Relation-like [:X,x:] -defined REAL -valued [.0,1.] -valued V6() V18([:X,x:], REAL ) V33() V34() V35() Element of bool [:[:X,x:],REAL:]
(X,Y,x,f,x) is Relation-like [:X,x:] -defined REAL -valued [.0,1.] -valued V6() V18([:X,x:], REAL ) V33() V34() V35() Element of bool [:[:X,x:],REAL:]
min ((X,Y,x,y,x),(X,Y,x,f,x)) is Relation-like [:X,x:] -defined REAL -valued [.0,1.] -valued V6() V18([:X,x:], REAL ) V33() V34() V35() Element of bool [:[:X,x:],REAL:]
z is Element of [:X,x:]
(X,Y,x,(min (y,f)),x) . z is V28() real ext-real Element of REAL
(min ((X,Y,x,y,x),(X,Y,x,f,x))) . z is V28() real ext-real Element of REAL
r is set
y is set
[r,y] is set
{r,y} is non empty set
{r} is non empty set
{{r,y},{r}} is non empty set
(X,x,(X,Y,x,(min (y,f)),x),r,y) is V28() real ext-real Element of REAL
K11((X,Y,x,(min (y,f)),x),[r,y]) is V28() real ext-real set
(X,Y,x,(min (y,f)),x,r,y) is Relation-like Y -defined REAL -valued [.0,1.] -valued V6() V18(Y, REAL ) V33() V34() V35() Element of bool [:Y,REAL:]
[:Y,REAL:] is Relation-like non empty V33() V34() V35() set
bool [:Y,REAL:] is non empty set
rng (X,Y,x,(min (y,f)),x,r,y) is non empty V43() V44() V45() Element of bool REAL
upper_bound (rng (X,Y,x,(min (y,f)),x,r,y)) is V28() real ext-real Element of REAL
(X,x,(min ((X,Y,x,y,x),(X,Y,x,f,x))),r,y) is V28() real ext-real Element of REAL
K11((min ((X,Y,x,y,x),(X,Y,x,f,x))),[r,y]) is V28() real ext-real set
(X,x,(X,Y,x,y,x),r,y) is V28() real ext-real Element of REAL
K11((X,Y,x,y,x),[r,y]) is V28() real ext-real set
(X,x,(X,Y,x,f,x),r,y) is V28() real ext-real Element of REAL
K11((X,Y,x,f,x),[r,y]) is V28() real ext-real set
min ((X,x,(X,Y,x,y,x),r,y),(X,x,(X,Y,x,f,x),r,y)) is V28() real ext-real Element of REAL
(X,Y,x,y,x,r,y) is Relation-like Y -defined REAL -valued [.0,1.] -valued V6() V18(Y, REAL ) V33() V34() V35() Element of bool [:Y,REAL:]
rng (X,Y,x,y,x,r,y) is non empty V43() V44() V45() Element of bool REAL
upper_bound (rng (X,Y,x,y,x,r,y)) is V28() real ext-real Element of REAL
min ((upper_bound (rng (X,Y,x,y,x,r,y))),(X,x,(X,Y,x,f,x),r,y)) is V28() real ext-real Element of REAL
(X,Y,x,f,x,r,y) is Relation-like Y -defined REAL -valued [.0,1.] -valued V6() V18(Y, REAL ) V33() V34() V35() Element of bool [:Y,REAL:]
rng (X,Y,x,f,x,r,y) is non empty V43() V44() V45() Element of bool REAL
upper_bound (rng (X,Y,x,f,x,r,y)) is V28() real ext-real Element of REAL
min ((upper_bound (rng (X,Y,x,y,x,r,y))),(upper_bound (rng (X,Y,x,f,x,r,y)))) is V28() real ext-real Element of REAL
X is non empty set
Y is non empty set
[:X,Y:] is Relation-like non empty set
[:[:X,Y:],REAL:] is Relation-like non empty V33() V34() V35() set
bool [:[:X,Y:],REAL:] is non empty set
x is non empty set
[:Y,x:] is Relation-like non empty set
[:[:Y,x:],REAL:] is Relation-like non empty V33() V34() V35() set
bool [:[:Y,x:],REAL:] is non empty set
y is Relation-like [:X,Y:] -defined REAL -valued [.0,1.] -valued V6() V18([:X,Y:], REAL ) V33() V34() V35() Element of bool [:[:X,Y:],REAL:]
(Y,X,y) is Relation-like [:Y,X:] -defined REAL -valued [.0,1.] -valued V6() V18([:Y,X:], REAL ) V33() V34() V35() Element of bool [:[:Y,X:],REAL:]
[:Y,X:] is Relation-like non empty set
[:[:Y,X:],REAL:] is Relation-like non empty V33() V34() V35() set
bool [:[:Y,X:],REAL:] is non empty set
f is Relation-like [:Y,x:] -defined REAL -valued [.0,1.] -valued V6() V18([:Y,x:], REAL ) V33() V34() V35() Element of bool [:[:Y,x:],REAL:]
(x,Y,f) is Relation-like [:x,Y:] -defined REAL -valued [.0,1.] -valued V6() V18([:x,Y:], REAL ) V33() V34() V35() Element of bool [:[:x,Y:],REAL:]
[:x,Y:] is Relation-like non empty set
[:[:x,Y:],REAL:] is Relation-like non empty V33() V34() V35() set
bool [:[:x,Y:],REAL:] is non empty set
x is set
z is set
(x,Y,X,(x,Y,f),(Y,X,y),z,x) is Relation-like Y -defined REAL -valued [.0,1.] -valued V6() V18(Y, REAL ) V33() V34() V35() Element of bool [:Y,REAL:]
[:Y,REAL:] is Relation-like non empty V33() V34() V35() set
bool [:Y,REAL:] is non empty set
rng (x,Y,X,(x,Y,f),(Y,X,y),z,x) is non empty V43() V44() V45() Element of bool REAL
upper_bound (rng (x,Y,X,(x,Y,f),(Y,X,y),z,x)) is V28() real ext-real Element of REAL
(X,Y,x,y,f,x,z) is Relation-like Y -defined REAL -valued [.0,1.] -valued V6() V18(Y, REAL ) V33() V34() V35() Element of bool [:Y,REAL:]
rng (X,Y,x,y,f,x,z) is non empty V43() V44() V45() Element of bool REAL
upper_bound (rng (X,Y,x,y,f,x,z)) is V28() real ext-real Element of REAL
r is V28() real ext-real set
(upper_bound (rng (X,Y,x,y,f,x,z))) - r is V28() real ext-real set
y is V28() real ext-real set
dom (X,Y,x,y,f,x,z) is Element of bool Y
bool Y is non empty set
z is set
(X,Y,x,y,f,x,z) . z is V28() real ext-real Element of REAL
[z,z] is set
{z,z} is non empty set
{z} is non empty set
{{z,z},{z}} is non empty set
dom (x,Y,X,(x,Y,f),(Y,X,y),z,x) is Element of bool Y
(x,Y,X,(x,Y,f),(Y,X,y),z,x) . z is V28() real ext-real Element of REAL
[z,x] is set
{z,x} is non empty set
{z} is non empty set
{{z,x},{z}} is non empty set
(X,Y,y,x,z) is V28() real ext-real Element of REAL
[x,z] is set
{x,z} is non empty set
{x} is non empty set
{{x,z},{x}} is non empty set
K11(y,[x,z]) is V28() real ext-real set
(Y,x,f,z,z) is V28() real ext-real Element of REAL
[z,z] is set
{z,z} is non empty set
{{z,z},{z}} is non empty set
K11(f,[z,z]) is V28() real ext-real set
min ((X,Y,y,x,z),(Y,x,f,z,z)) is V28() real ext-real Element of REAL
(Y,X,(Y,X,y),z,x) is V28() real ext-real Element of REAL
K11((Y,X,y),[z,x]) is V28() real ext-real set
min ((Y,X,(Y,X,y),z,x),(Y,x,f,z,z)) is V28() real ext-real Element of REAL
(x,Y,(x,Y,f),z,z) is V28() real ext-real Element of REAL
K11((x,Y,f),[z,z]) is V28() real ext-real set
min ((Y,X,(Y,X,y),z,x),(x,Y,(x,Y,f),z,z)) is V28() real ext-real Element of REAL
r is V28() real ext-real set
(upper_bound (rng (x,Y,X,(x,Y,f),(Y,X,y),z,x))) - r is V28() real ext-real set
y is V28() real ext-real set
dom (x,Y,X,(x,Y,f),(Y,X,y),z,x) is Element of bool Y
bool Y is non empty set
z is set
(x,Y,X,(x,Y,f),(Y,X,y),z,x) . z is V28() real ext-real Element of REAL
[z,z] is set
{z,z} is non empty set
{z} is non empty set
{{z,z},{z}} is non empty set
dom (X,Y,x,y,f,x,z) is Element of bool Y
(X,Y,x,y,f,x,z) . z is V28() real ext-real Element of REAL
[z,x] is set
{z,x} is non empty set
{z} is non empty set
{{z,x},{z}} is non empty set
(x,Y,(x,Y,f),z,z) is V28() real ext-real Element of REAL
K11((x,Y,f),[z,z]) is V28() real ext-real set
(Y,X,(Y,X,y),z,x) is V28() real ext-real Element of REAL
K11((Y,X,y),[z,x]) is V28() real ext-real set
min ((x,Y,(x,Y,f),z,z),(Y,X,(Y,X,y),z,x)) is V28() real ext-real Element of REAL
(Y,x,f,z,z) is V28() real ext-real Element of REAL
[z,z] is set
{z,z} is non empty set
{{z,z},{z}} is non empty set
K11(f,[z,z]) is V28() real ext-real set
min ((Y,x,f,z,z),(Y,X,(Y,X,y),z,x)) is V28() real ext-real Element of REAL
(X,Y,y,x,z) is V28() real ext-real Element of REAL
[x,z] is set
{x,z} is non empty set
{x} is non empty set
{{x,z},{x}} is non empty set
K11(y,[x,z]) is V28() real ext-real set
min ((Y,x,f,z,z),(X,Y,y,x,z)) is V28() real ext-real Element of REAL
X is non empty set
Y is non empty set
[:X,Y:] is Relation-like non empty set
[:[:X,Y:],REAL:] is Relation-like non empty V33() V34() V35() set
bool [:[:X,Y:],REAL:] is non empty set
x is non empty set
[:Y,x:] is Relation-like non empty set
[:[:Y,x:],REAL:] is Relation-like non empty V33() V34() V35() set
bool [:[:Y,x:],REAL:] is non empty set
[:x,X:] is Relation-like non empty set
y is Relation-like [:X,Y:] -defined REAL -valued [.0,1.] -valued V6() V18([:X,Y:], REAL ) V33() V34() V35() Element of bool [:[:X,Y:],REAL:]
(Y,X,y) is Relation-like [:Y,X:] -defined REAL -valued [.0,1.] -valued V6() V18([:Y,X:], REAL ) V33() V34() V35() Element of bool [:[:Y,X:],REAL:]
[:Y,X:] is Relation-like non empty set
[:[:Y,X:],REAL:] is Relation-like non empty V33() V34() V35() set
bool [:[:Y,X:],REAL:] is non empty set
f is Relation-like [:Y,x:] -defined REAL -valued [.0,1.] -valued V6() V18([:Y,x:], REAL ) V33() V34() V35() Element of bool [:[:Y,x:],REAL:]
(X,Y,x,y,f) is Relation-like [:X,x:] -defined REAL -valued [.0,1.] -valued V6() V18([:X,x:], REAL ) V33() V34() V35() Element of bool [:[:X,x:],REAL:]
[:X,x:] is Relation-like non empty set
[:[:X,x:],REAL:] is Relation-like non empty V33() V34() V35() set
bool [:[:X,x:],REAL:] is non empty set
(x,X,(X,Y,x,y,f)) is Relation-like [:x,X:] -defined REAL -valued [.0,1.] -valued V6() V18([:x,X:], REAL ) V33() V34() V35() Element of bool [:[:x,X:],REAL:]
[:[:x,X:],REAL:] is Relation-like non empty V33() V34() V35() set
bool [:[:x,X:],REAL:] is non empty set
(x,Y,f) is Relation-like [:x,Y:] -defined REAL -valued [.0,1.] -valued V6() V18([:x,Y:], REAL ) V33() V34() V35() Element of bool [:[:x,Y:],REAL:]
[:x,Y:] is Relation-like non empty set
[:[:x,Y:],REAL:] is Relation-like non empty V33() V34() V35() set
bool [:[:x,Y:],REAL:] is non empty set
(x,Y,X,(x,Y,f),(Y,X,y)) is Relation-like [:x,X:] -defined REAL -valued [.0,1.] -valued V6() V18([:x,X:], REAL ) V33() V34() V35() Element of bool [:[:x,X:],REAL:]
dom (x,Y,X,(x,Y,f),(Y,X,y)) is Relation-like x -defined X -valued Element of bool [:x,X:]
bool [:x,X:] is non empty set
x is Element of [:x,X:]
(x,X,(X,Y,x,y,f)) . x is V28() real ext-real Element of REAL
(x,Y,X,(x,Y,f),(Y,X,y)) . x is V28() real ext-real Element of REAL
z is set
r is set
[z,r] is set
{z,r} is non empty set
{z} is non empty set
{{z,r},{z}} is non empty set
[r,z] is set
{r,z} is non empty set
{r} is non empty set
{{r,z},{r}} is non empty set
(x,X,(x,Y,X,(x,Y,f),(Y,X,y)),z,r) is V28() real ext-real Element of REAL
K11((x,Y,X,(x,Y,f),(Y,X,y)),[z,r]) is V28() real ext-real set
(x,Y,X,(x,Y,f),(Y,X,y),z,r) is Relation-like Y -defined REAL -valued [.0,1.] -valued V6() V18(Y, REAL ) V33() V34() V35() Element of bool [:Y,REAL:]
[:Y,REAL:] is Relation-like non empty V33() V34() V35() set
bool [:Y,REAL:] is non empty set
rng (x,Y,X,(x,Y,f),(Y,X,y),z,r) is non empty V43() V44() V45() Element of bool REAL
upper_bound (rng (x,Y,X,(x,Y,f),(Y,X,y),z,r)) is V28() real ext-real Element of REAL
(x,X,(x,X,(X,Y,x,y,f)),z,r) is V28() real ext-real Element of REAL
K11((x,X,(X,Y,x,y,f)),[z,r]) is V28() real ext-real set
(X,x,(X,Y,x,y,f),r,z) is V28() real ext-real Element of REAL
K11((X,Y,x,y,f),[r,z]) is V28() real ext-real set
(X,Y,x,y,f,r,z) is Relation-like Y -defined REAL -valued [.0,1.] -valued V6() V18(Y, REAL ) V33() V34() V35() Element of bool [:Y,REAL:]
rng (X,Y,x,y,f,r,z) is non empty V43() V44() V45() Element of bool REAL
upper_bound (rng (X,Y,x,y,f,r,z)) is V28() real ext-real Element of REAL
dom (x,X,(X,Y,x,y,f)) is Relation-like x -defined X -valued Element of bool [:x,X:]
X is non empty set
Y is non empty set
[:X,Y:] is Relation-like non empty set
[:[:X,Y:],REAL:] is Relation-like non empty V33() V34() V35() set
bool [:[:X,Y:],REAL:] is non empty set
x is non empty set
[:Y,x:] is Relation-like non empty set
[:[:Y,x:],REAL:] is Relation-like non empty V33() V34() V35() set
bool [:[:Y,x:],REAL:] is non empty set
y is Relation-like [:X,Y:] -defined REAL -valued [.0,1.] -valued V6() V18([:X,Y:], REAL ) V33() V34() V35() Element of bool [:[:X,Y:],REAL:]
f is Relation-like [:X,Y:] -defined REAL -valued [.0,1.] -valued V6() V18([:X,Y:], REAL ) V33() V34() V35() Element of bool [:[:X,Y:],REAL:]
x is Relation-like [:Y,x:] -defined REAL -valued [.0,1.] -valued V6() V18([:Y,x:], REAL ) V33() V34() V35() Element of bool [:[:Y,x:],REAL:]
z is Relation-like [:Y,x:] -defined REAL -valued [.0,1.] -valued V6() V18([:Y,x:], REAL ) V33() V34() V35() Element of bool [:[:Y,x:],REAL:]
(X,Y,x,y,x) is Relation-like [:X,x:] -defined REAL -valued [.0,1.] -valued V6() V18([:X,x:], REAL ) V33() V34() V35() Element of bool [:[:X,x:],REAL:]
[:X,x:] is Relation-like non empty set
[:[:X,x:],REAL:] is Relation-like non empty V33() V34() V35() set
bool [:[:X,x:],REAL:] is non empty set
(X,Y,x,f,z) is Relation-like [:X,x:] -defined REAL -valued [.0,1.] -valued V6() V18([:X,x:], REAL ) V33() V34() V35() Element of bool [:[:X,x:],REAL:]
r is set
y is set
[r,y] is set
{r,y} is non empty set
{r} is non empty set
{{r,y},{r}} is non empty set
(X,Y,x,y,x) . [r,y] is V28() real ext-real Element of REAL
(X,Y,x,f,z) . [r,y] is V28() real ext-real Element of REAL
(X,x,(X,Y,x,f,z),r,y) is V28() real ext-real Element of REAL
K11((X,Y,x,f,z),[r,y]) is V28() real ext-real set
(X,Y,x,f,z,r,y) is Relation-like Y -defined REAL -valued [.0,1.] -valued V6() V18(Y, REAL ) V33() V34() V35() Element of bool [:Y,REAL:]
[:Y,REAL:] is Relation-like non empty V33() V34() V35() set
bool [:Y,REAL:] is non empty set
rng (X,Y,x,f,z,r,y) is non empty V43() V44() V45() Element of bool REAL
upper_bound (rng (X,Y,x,f,z,r,y)) is V28() real ext-real Element of REAL
(X,Y,x,y,x,r,y) is Relation-like Y -defined REAL -valued [.0,1.] -valued V6() V18(Y, REAL ) V33() V34() V35() Element of bool [:Y,REAL:]
rng (X,Y,x,y,x,r,y) is non empty V43() V44() V45() Element of bool REAL
upper_bound (rng (X,Y,x,y,x,r,y)) is V28() real ext-real Element of REAL
z is V28() real ext-real set
(upper_bound (rng (X,Y,x,y,x,r,y))) - z is V28() real ext-real set
y is V28() real ext-real set
dom (X,Y,x,y,x,r,y) is Element of bool Y
bool Y is non empty set
y is set
(X,Y,x,y,x,r,y) . y is V28() real ext-real Element of REAL
[y,y] is set
{y,y} is non empty set
{y} is non empty set
{{y,y},{y}} is non empty set
x . [y,y] is V28() real ext-real Element of REAL
z . [y,y] is V28() real ext-real Element of REAL
[r,y] is set
{r,y} is non empty set
{{r,y},{r}} is non empty set
y . [r,y] is V28() real ext-real Element of REAL
f . [r,y] is V28() real ext-real Element of REAL
min ((y . [r,y]),(x . [y,y])) is V28() real ext-real Element of REAL
min ((f . [r,y]),(z . [y,y])) is V28() real ext-real Element of REAL
dom (X,Y,x,f,z,r,y) is Element of bool Y
(X,Y,x,f,z,r,y) . y is V28() real ext-real Element of REAL
(X,x,(X,Y,x,y,x),r,y) is V28() real ext-real Element of REAL
K11((X,Y,x,y,x),[r,y]) is V28() real ext-real set
X is non empty set
Y is non empty set
[:X,Y:] is Relation-like non empty set
[:[:X,Y:],REAL:] is Relation-like non empty V33() V34() V35() set
bool [:[:X,Y:],REAL:] is non empty set
x is non empty set
[:Y,x:] is Relation-like non empty set
[:[:Y,x:],REAL:] is Relation-like non empty V33() V34() V35() set
bool [:[:Y,x:],REAL:] is non empty set
y is Relation-like [:X,Y:] -defined REAL -valued [.0,1.] -valued V6() V18([:X,Y:], REAL ) V33() V34() V35() Element of bool [:[:X,Y:],REAL:]
f is Relation-like [:X,Y:] -defined REAL -valued [.0,1.] -valued V6() V18([:X,Y:], REAL ) V33() V34() V35() Element of bool [:[:X,Y:],REAL:]
x is Relation-like [:Y,x:] -defined REAL -valued [.0,1.] -valued V6() V18([:Y,x:], REAL ) V33() V34() V35() Element of bool [:[:Y,x:],REAL:]
z is Relation-like [:Y,x:] -defined REAL -valued [.0,1.] -valued V6() V18([:Y,x:], REAL ) V33() V34() V35() Element of bool [:[:Y,x:],REAL:]
(X,Y,x,y,x) is Relation-like [:X,x:] -defined REAL -valued [.0,1.] -valued V6() V18([:X,x:], REAL ) V33() V34() V35() Element of bool [:[:X,x:],REAL:]
[:X,x:] is Relation-like non empty set
[:[:X,x:],REAL:] is Relation-like non empty V33() V34() V35() set
bool [:[:X,x:],REAL:] is non empty set
(X,Y,x,f,z) is Relation-like [:X,x:] -defined REAL -valued [.0,1.] -valued V6() V18([:X,x:], REAL ) V33() V34() V35() Element of bool [:[:X,x:],REAL:]
r is Element of [:X,x:]
(X,Y,x,y,x) . r is V28() real ext-real Element of REAL
(X,Y,x,f,z) . r is V28() real ext-real Element of REAL
y is set
z is set
[y,z] is set
{y,z} is non empty set
{y} is non empty set
{{y,z},{y}} is non empty set
y is set
[y,y] is set
{y,y} is non empty set
{{y,y},{y}} is non empty set
y . [y,y] is V28() real ext-real Element of REAL
f . [y,y] is V28() real ext-real Element of REAL
[y,z] is set
{y,z} is non empty set
{y} is non empty set
{{y,z},{y}} is non empty set
x . [y,z] is V28() real ext-real Element of REAL
z . [y,z] is V28() real ext-real Element of REAL
X is non empty set
Y is non empty set
[:X,Y:] is Relation-like non empty set
[:[:X,Y:],REAL:] is Relation-like non empty V33() V34() V35() set
bool [:[:X,Y:],REAL:] is non empty set
x is set
y is set
f is set
x is set
x is set
y is set
f is set
x is Relation-like [:X,Y:] -defined REAL -valued V6() V33() V34() V35() Element of bool [:[:X,Y:],REAL:]
dom x is Relation-like X -defined Y -valued Element of bool [:X,Y:]
bool [:X,Y:] is non empty set
y is set
f is set
[y,f] is set
{y,f} is non empty set
{y} is non empty set
{{y,f},{y}} is non empty set
x is set
rng x is V43() V44() V45() Element of bool REAL
y is set
f is Element of [:X,Y:]
x . f is V28() real ext-real Element of REAL
x is set
z is set
[x,z] is set
{x,z} is non empty set
{x} is non empty set
{{x,z},{x}} is non empty set
r is non empty V43() V44() V45() V72() closed_interval real-bounded interval Element of bool REAL
lower_bound r is V28() real ext-real Element of REAL
upper_bound r is V28() real ext-real Element of REAL
[.(lower_bound r),(upper_bound r).] is V43() V44() V45() Element of bool REAL
x . (x,z) is set
K11(x,[x,z]) is V28() real ext-real set
x is Relation-like [:X,Y:] -defined REAL -valued [.0,1.] -valued V6() V18([:X,Y:], REAL ) V33() V34() V35() Element of bool [:[:X,Y:],REAL:]
y is Relation-like [:X,Y:] -defined REAL -valued [.0,1.] -valued V6() V18([:X,Y:], REAL ) V33() V34() V35() Element of bool [:[:X,Y:],REAL:]
f is set
x is set
(X,Y,x,f,x) is V28() real ext-real Element of REAL
[f,x] is set
{f,x} is non empty set
{f} is non empty set
{{f,x},{f}} is non empty set
K11(x,[f,x]) is V28() real ext-real set
(X,Y,y,f,x) is V28() real ext-real Element of REAL
K11(y,[f,x]) is V28() real ext-real set
dom y is Relation-like X -defined Y -valued Element of bool [:X,Y:]
bool [:X,Y:] is non empty set
dom x is Relation-like X -defined Y -valued Element of bool [:X,Y:]
X is non empty set
Y is non empty set
[:X,Y:] is Relation-like non empty set
y is non empty set
f is non empty set
[:y,f:] is Relation-like non empty set
Zmf (X,Y) is Relation-like [:X,Y:] -defined REAL -valued [.0,1.] -valued V6() V18([:X,Y:], REAL ) V33() V34() V35() Element of bool [:[:X,Y:],REAL:]
[:[:X,Y:],REAL:] is Relation-like non empty V33() V34() V35() set
bool [:[:X,Y:],REAL:] is non empty set
K136({},[:X,Y:]) is Relation-like [:X,Y:] -defined {{},1} -valued V6() V18([:X,Y:],{{},1}) Element of bool [:[:X,Y:],{{},1}:]
[:[:X,Y:],{{},1}:] is Relation-like non empty set
bool [:[:X,Y:],{{},1}:] is non empty set
x is Element of [:X,Y:]
(Zmf (X,Y)) . x is V28() real ext-real Element of REAL
Umf (y,f) is Relation-like [:y,f:] -defined REAL -valued [.0,1.] -valued V6() V18([:y,f:], REAL ) V33() V34() V35() Element of bool [:[:y,f:],REAL:]
[:[:y,f:],REAL:] is Relation-like non empty V33() V34() V35() set
bool [:[:y,f:],REAL:] is non empty set
K136([:y,f:],[:y,f:]) is Relation-like [:y,f:] -defined {{},1} -valued V6() V18([:y,f:],{{},1}) Element of bool [:[:y,f:],{{},1}:]
[:[:y,f:],{{},1}:] is Relation-like non empty set
bool [:[:y,f:],{{},1}:] is non empty set
x is Element of [:y,f:]
(Umf (y,f)) . x is V28() real ext-real Element of REAL
x is set
y is set
[x,y] is set
{x,y} is non empty set
{x} is non empty set
{{x,y},{x}} is non empty set
X is non empty set
Y is non empty set
[:X,Y:] is Relation-like non empty set
Zmf (X,Y) is Relation-like [:X,Y:] -defined REAL -valued [.0,1.] -valued V6() V18([:X,Y:], REAL ) V33() V34() V35() Element of bool [:[:X,Y:],REAL:]
[:[:X,Y:],REAL:] is Relation-like non empty V33() V34() V35() set
bool [:[:X,Y:],REAL:] is non empty set
K136({},[:X,Y:]) is Relation-like [:X,Y:] -defined {{},1} -valued V6() V18([:X,Y:],{{},1}) Element of bool [:[:X,Y:],{{},1}:]
[:[:X,Y:],{{},1}:] is Relation-like non empty set
bool [:[:X,Y:],{{},1}:] is non empty set
(Zmf (X,Y)) . [x,y] is V28() real ext-real Element of REAL
Umf (X,Y) is Relation-like [:X,Y:] -defined REAL -valued [.0,1.] -valued V6() V18([:X,Y:], REAL ) V33() V34() V35() Element of bool [:[:X,Y:],REAL:]
K136([:X,Y:],[:X,Y:]) is Relation-like [:X,Y:] -defined {{},1} -valued V6() V18([:X,Y:],{{},1}) Element of bool [:[:X,Y:],{{},1}:]
(Umf (X,Y)) . [x,y] is V28() real ext-real Element of REAL
X is non empty set
Y is non empty set
[:X,Y:] is Relation-like non empty set
[:[:X,Y:],REAL:] is Relation-like non empty V33() V34() V35() set
bool [:[:X,Y:],REAL:] is non empty set
x is non empty set
Zmf (x,X) is Relation-like [:x,X:] -defined REAL -valued [.0,1.] -valued V6() V18([:x,X:], REAL ) V33() V34() V35() Element of bool [:[:x,X:],REAL:]
[:x,X:] is Relation-like non empty set
[:[:x,X:],REAL:] is Relation-like non empty V33() V34() V35() set
bool [:[:x,X:],REAL:] is non empty set
K136({},[:x,X:]) is Relation-like [:x,X:] -defined {{},1} -valued V6() V18([:x,X:],{{},1}) Element of bool [:[:x,X:],{{},1}:]
[:[:x,X:],{{},1}:] is Relation-like non empty set
bool [:[:x,X:],{{},1}:] is non empty set
Zmf (x,Y) is Relation-like [:x,Y:] -defined REAL -valued [.0,1.] -valued V6() V18([:x,Y:], REAL ) V33() V34() V35() Element of bool [:[:x,Y:],REAL:]
[:x,Y:] is Relation-like non empty set
[:[:x,Y:],REAL:] is Relation-like non empty V33() V34() V35() set
bool [:[:x,Y:],REAL:] is non empty set
K136({},[:x,Y:]) is Relation-like [:x,Y:] -defined {{},1} -valued V6() V18([:x,Y:],{{},1}) Element of bool [:[:x,Y:],{{},1}:]
[:[:x,Y:],{{},1}:] is Relation-like non empty set
bool [:[:x,Y:],{{},1}:] is non empty set
y is Relation-like [:X,Y:] -defined REAL -valued [.0,1.] -valued V6() V18([:X,Y:], REAL ) V33() V34() V35() Element of bool [:[:X,Y:],REAL:]
f is set
x is set
(x,X,Y,(Zmf (x,X)),y,f,x) is Relation-like X -defined REAL -valued [.0,1.] -valued V6() V18(X, REAL ) V33() V34() V35() Element of bool [:X,REAL:]
[:X,REAL:] is Relation-like non empty V33() V34() V35() set
bool [:X,REAL:] is non empty set
rng (x,X,Y,(Zmf (x,X)),y,f,x) is non empty V43() V44() V45() Element of bool REAL
upper_bound (rng (x,X,Y,(Zmf (x,X)),y,f,x)) is V28() real ext-real Element of REAL
[f,x] is set
{f,x} is non empty set
{f} is non empty set
{{f,x},{f}} is non empty set
(Zmf (x,Y)) . [f,x] is V28() real ext-real Element of REAL
z is V28() real ext-real set
(upper_bound (rng (x,X,Y,(Zmf (x,X)),y,f,x))) - z is V28() real ext-real set
r is V28() real ext-real set
dom (x,X,Y,(Zmf (x,X)),y,f,x) is Element of bool X
bool X is non empty set
y is set
(x,X,Y,(Zmf (x,X)),y,f,x) . y is V28() real ext-real Element of REAL
[f,y] is set
{f,y} is non empty set
{{f,y},{f}} is non empty set
[y,x] is set
{y,x} is non empty set
{y} is non empty set
{{y,x},{y}} is non empty set
y . [y,x] is V28() real ext-real Element of REAL
(Zmf (x,X)) . [f,y] is V28() real ext-real Element of REAL
min (((Zmf (x,X)) . [f,y]),(y . [y,x])) is V28() real ext-real Element of REAL
min (0,(y . [y,x])) is V28() real ext-real Element of REAL
z is non empty V43() V44() V45() V72() closed_interval real-bounded interval Element of bool REAL
lower_bound z is V28() real ext-real Element of REAL
lower_bound (rng (x,X,Y,(Zmf (x,X)),y,f,x)) is V28() real ext-real Element of REAL
upper_bound z is V28() real ext-real Element of REAL
[.(lower_bound z),(upper_bound z).] is V43() V44() V45() Element of bool REAL
X is non empty set
Y is non empty set
[:X,Y:] is Relation-like non empty set
[:[:X,Y:],REAL:] is Relation-like non empty V33() V34() V35() set
bool [:[:X,Y:],REAL:] is non empty set
x is non empty set
[:x,Y:] is Relation-like non empty set
Zmf (x,X) is Relation-like [:x,X:] -defined REAL -valued [.0,1.] -valued V6() V18([:x,X:], REAL ) V33() V34() V35() Element of bool [:[:x,X:],REAL:]
[:x,X:] is Relation-like non empty set
[:[:x,X:],REAL:] is Relation-like non empty V33() V34() V35() set
bool [:[:x,X:],REAL:] is non empty set
K136({},[:x,X:]) is Relation-like [:x,X:] -defined {{},1} -valued V6() V18([:x,X:],{{},1}) Element of bool [:[:x,X:],{{},1}:]
[:[:x,X:],{{},1}:] is Relation-like non empty set
bool [:[:x,X:],{{},1}:] is non empty set
Zmf (x,Y) is Relation-like [:x,Y:] -defined REAL -valued [.0,1.] -valued V6() V18([:x,Y:], REAL ) V33() V34() V35() Element of bool [:[:x,Y:],REAL:]
[:[:x,Y:],REAL:] is Relation-like non empty V33() V34() V35() set
bool [:[:x,Y:],REAL:] is non empty set
K136({},[:x,Y:]) is Relation-like [:x,Y:] -defined {{},1} -valued V6() V18([:x,Y:],{{},1}) Element of bool [:[:x,Y:],{{},1}:]
[:[:x,Y:],{{},1}:] is Relation-like non empty set
bool [:[:x,Y:],{{},1}:] is non empty set
y is Relation-like [:X,Y:] -defined REAL -valued [.0,1.] -valued V6() V18([:X,Y:], REAL ) V33() V34() V35() Element of bool [:[:X,Y:],REAL:]
(x,X,Y,(Zmf (x,X)),y) is Relation-like [:x,Y:] -defined REAL -valued [.0,1.] -valued V6() V18([:x,Y:], REAL ) V33() V34() V35() Element of bool [:[:x,Y:],REAL:]
dom (Zmf (x,Y)) is Relation-like x -defined Y -valued Element of bool [:x,Y:]
bool [:x,Y:] is non empty set
f is Element of [:x,Y:]
(x,X,Y,(Zmf (x,X)),y) . f is V28() real ext-real Element of REAL
(Zmf (x,Y)) . f is V28() real ext-real Element of REAL
x is set
z is set
[x,z] is set
{x,z} is non empty set
{x} is non empty set
{{x,z},{x}} is non empty set
(x,Y,(x,X,Y,(Zmf (x,X)),y),x,z) is V28() real ext-real Element of REAL
K11((x,X,Y,(Zmf (x,X)),y),[x,z]) is V28() real ext-real set
(x,X,Y,(Zmf (x,X)),y,x,z) is Relation-like X -defined REAL -valued [.0,1.] -valued V6() V18(X, REAL ) V33() V34() V35() Element of bool [:X,REAL:]
[:X,REAL:] is Relation-like non empty V33() V34() V35() set
bool [:X,REAL:] is non empty set
rng (x,X,Y,(Zmf (x,X)),y,x,z) is non empty V43() V44() V45() Element of bool REAL
upper_bound (rng (x,X,Y,(Zmf (x,X)),y,x,z)) is V28() real ext-real Element of REAL
dom (x,X,Y,(Zmf (x,X)),y) is Relation-like x -defined Y -valued Element of bool [:x,Y:]
X is non empty set
Y is non empty set
[:X,Y:] is Relation-like non empty set
[:[:X,Y:],REAL:] is Relation-like non empty V33() V34() V35() set
bool [:[:X,Y:],REAL:] is non empty set
x is non empty set
Zmf (Y,x) is Relation-like [:Y,x:] -defined REAL -valued [.0,1.] -valued V6() V18([:Y,x:], REAL ) V33() V34() V35() Element of bool [:[:Y,x:],REAL:]
[:Y,x:] is Relation-like non empty set
[:[:Y,x:],REAL:] is Relation-like non empty V33() V34() V35() set
bool [:[:Y,x:],REAL:] is non empty set
K136({},[:Y,x:]) is Relation-like [:Y,x:] -defined {{},1} -valued V6() V18([:Y,x:],{{},1}) Element of bool [:[:Y,x:],{{},1}:]
[:[:Y,x:],{{},1}:] is Relation-like non empty set
bool [:[:Y,x:],{{},1}:] is non empty set
Zmf (X,x) is Relation-like [:X,x:] -defined REAL -valued [.0,1.] -valued V6() V18([:X,x:], REAL ) V33() V34() V35() Element of bool [:[:X,x:],REAL:]
[:X,x:] is Relation-like non empty set
[:[:X,x:],REAL:] is Relation-like non empty V33() V34() V35() set
bool [:[:X,x:],REAL:] is non empty set
K136({},[:X,x:]) is Relation-like [:X,x:] -defined {{},1} -valued V6() V18([:X,x:],{{},1}) Element of bool [:[:X,x:],{{},1}:]
[:[:X,x:],{{},1}:] is Relation-like non empty set
bool [:[:X,x:],{{},1}:] is non empty set
y is Relation-like [:X,Y:] -defined REAL -valued [.0,1.] -valued V6() V18([:X,Y:], REAL ) V33() V34() V35() Element of bool [:[:X,Y:],REAL:]
f is set
x is set
(X,Y,x,y,(Zmf (Y,x)),f,x) is Relation-like Y -defined REAL -valued [.0,1.] -valued V6() V18(Y, REAL ) V33() V34() V35() Element of bool [:Y,REAL:]
[:Y,REAL:] is Relation-like non empty V33() V34() V35() set
bool [:Y,REAL:] is non empty set
rng (X,Y,x,y,(Zmf (Y,x)),f,x) is non empty V43() V44() V45() Element of bool REAL
upper_bound (rng (X,Y,x,y,(Zmf (Y,x)),f,x)) is V28() real ext-real Element of REAL
[f,x] is set
{f,x} is non empty set
{f} is non empty set
{{f,x},{f}} is non empty set
(Zmf (X,x)) . [f,x] is V28() real ext-real Element of REAL
z is V28() real ext-real set
(upper_bound (rng (X,Y,x,y,(Zmf (Y,x)),f,x))) - z is V28() real ext-real set
r is V28() real ext-real set
dom (X,Y,x,y,(Zmf (Y,x)),f,x) is Element of bool Y
bool Y is non empty set
y is set
(X,Y,x,y,(Zmf (Y,x)),f,x) . y is V28() real ext-real Element of REAL
[y,x] is set
{y,x} is non empty set
{y} is non empty set
{{y,x},{y}} is non empty set
[f,y] is set
{f,y} is non empty set
{{f,y},{f}} is non empty set
y . [f,y] is V28() real ext-real Element of REAL
(Zmf (Y,x)) . [y,x] is V28() real ext-real Element of REAL
min ((y . [f,y]),((Zmf (Y,x)) . [y,x])) is V28() real ext-real Element of REAL
min ((y . [f,y]),0) is V28() real ext-real Element of REAL
z is non empty V43() V44() V45() V72() closed_interval real-bounded interval Element of bool REAL
lower_bound z is V28() real ext-real Element of REAL
lower_bound (rng (X,Y,x,y,(Zmf (Y,x)),f,x)) is V28() real ext-real Element of REAL
upper_bound z is V28() real ext-real Element of REAL
[.(lower_bound z),(upper_bound z).] is V43() V44() V45() Element of bool REAL
X is non empty set
Y is non empty set
[:X,Y:] is Relation-like non empty set
[:[:X,Y:],REAL:] is Relation-like non empty V33() V34() V35() set
bool [:[:X,Y:],REAL:] is non empty set
x is non empty set
[:X,x:] is Relation-like non empty set
Zmf (Y,x) is Relation-like [:Y,x:] -defined REAL -valued [.0,1.] -valued V6() V18([:Y,x:], REAL ) V33() V34() V35() Element of bool [:[:Y,x:],REAL:]
[:Y,x:] is Relation-like non empty set
[:[:Y,x:],REAL:] is Relation-like non empty V33() V34() V35() set
bool [:[:Y,x:],REAL:] is non empty set
K136({},[:Y,x:]) is Relation-like [:Y,x:] -defined {{},1} -valued V6() V18([:Y,x:],{{},1}) Element of bool [:[:Y,x:],{{},1}:]
[:[:Y,x:],{{},1}:] is Relation-like non empty set
bool [:[:Y,x:],{{},1}:] is non empty set
Zmf (X,x) is Relation-like [:X,x:] -defined REAL -valued [.0,1.] -valued V6() V18([:X,x:], REAL ) V33() V34() V35() Element of bool [:[:X,x:],REAL:]
[:[:X,x:],REAL:] is Relation-like non empty V33() V34() V35() set
bool [:[:X,x:],REAL:] is non empty set
K136({},[:X,x:]) is Relation-like [:X,x:] -defined {{},1} -valued V6() V18([:X,x:],{{},1}) Element of bool [:[:X,x:],{{},1}:]
[:[:X,x:],{{},1}:] is Relation-like non empty set
bool [:[:X,x:],{{},1}:] is non empty set
y is Relation-like [:X,Y:] -defined REAL -valued [.0,1.] -valued V6() V18([:X,Y:], REAL ) V33() V34() V35() Element of bool [:[:X,Y:],REAL:]
(X,Y,x,y,(Zmf (Y,x))) is Relation-like [:X,x:] -defined REAL -valued [.0,1.] -valued V6() V18([:X,x:], REAL ) V33() V34() V35() Element of bool [:[:X,x:],REAL:]
dom (Zmf (X,x)) is Relation-like X -defined x -valued Element of bool [:X,x:]
bool [:X,x:] is non empty set
f is Element of [:X,x:]
(X,Y,x,y,(Zmf (Y,x))) . f is V28() real ext-real Element of REAL
(Zmf (X,x)) . f is V28() real ext-real Element of REAL
x is set
z is set
[x,z] is set
{x,z} is non empty set
{x} is non empty set
{{x,z},{x}} is non empty set
(X,x,(X,Y,x,y,(Zmf (Y,x))),x,z) is V28() real ext-real Element of REAL
K11((X,Y,x,y,(Zmf (Y,x))),[x,z]) is V28() real ext-real set
(X,Y,x,y,(Zmf (Y,x)),x,z) is Relation-like Y -defined REAL -valued [.0,1.] -valued V6() V18(Y, REAL ) V33() V34() V35() Element of bool [:Y,REAL:]
[:Y,REAL:] is Relation-like non empty V33() V34() V35() set
bool [:Y,REAL:] is non empty set
rng (X,Y,x,y,(Zmf (Y,x)),x,z) is non empty V43() V44() V45() Element of bool REAL
upper_bound (rng (X,Y,x,y,(Zmf (Y,x)),x,z)) is V28() real ext-real Element of REAL
dom (X,Y,x,y,(Zmf (Y,x))) is Relation-like X -defined x -valued Element of bool [:X,x:]
X is non empty set
[:X,X:] is Relation-like non empty set
[:[:X,X:],REAL:] is Relation-like non empty V33() V34() V35() set
bool [:[:X,X:],REAL:] is non empty set
Zmf (X,X) is Relation-like [:X,X:] -defined REAL -valued [.0,1.] -valued V6() V18([:X,X:], REAL ) V33() V34() V35() Element of bool [:[:X,X:],REAL:]
K136({},[:X,X:]) is Relation-like [:X,X:] -defined {{},1} -valued V6() V18([:X,X:],{{},1}) Element of bool [:[:X,X:],{{},1}:]
[:[:X,X:],{{},1}:] is Relation-like non empty set
bool [:[:X,X:],{{},1}:] is non empty set
Y is Relation-like [:X,X:] -defined REAL -valued [.0,1.] -valued V6() V18([:X,X:], REAL ) V33() V34() V35() Element of bool [:[:X,X:],REAL:]
(X,X,X,Y,(Zmf (X,X))) is Relation-like [:X,X:] -defined REAL -valued [.0,1.] -valued V6() V18([:X,X:], REAL ) V33() V34() V35() Element of bool [:[:X,X:],REAL:]
(X,X,X,(Zmf (X,X)),Y) is Relation-like [:X,X:] -defined REAL -valued [.0,1.] -valued V6() V18([:X,X:], REAL ) V33() V34() V35() Element of bool [:[:X,X:],REAL:]
X is non empty set
Y is non empty set
(X,Y) is Relation-like [:X,Y:] -defined REAL -valued [.0,1.] -valued V6() V18([:X,Y:], REAL ) V33() V34() V35() Element of bool [:[:X,Y:],REAL:]
[:X,Y:] is Relation-like non empty set
[:[:X,Y:],REAL:] is Relation-like non empty V33() V34() V35() set
bool [:[:X,Y:],REAL:] is non empty set
x is Element of X
y is Element of Y
(X,Y,(X,Y),x,y) is V28() real ext-real Element of REAL
[x,y] is set
{x,y} is non empty set
{x} is non empty set
{{x,y},{x}} is non empty set
K11((X,Y),[x,y]) is V28() real ext-real set
X is non empty set
Y is non empty set
[:X,Y:] is Relation-like non empty set
[:[:X,Y:],REAL:] is Relation-like non empty V33() V34() V35() set
bool [:[:X,Y:],REAL:] is non empty set
x is Element of X
y is Element of Y
f is Relation-like [:X,Y:] -defined REAL -valued [.0,1.] -valued V6() V18([:X,Y:], REAL ) V33() V34() V35() Element of bool [:[:X,Y:],REAL:]
(Y,X,f) is Relation-like [:Y,X:] -defined REAL -valued [.0,1.] -valued V6() V18([:Y,X:], REAL ) V33() V34() V35() Element of bool [:[:Y,X:],REAL:]
[:Y,X:] is Relation-like non empty set
[:[:Y,X:],REAL:] is Relation-like non empty V33() V34() V35() set
bool [:[:Y,X:],REAL:] is non empty set
(Y,X,(Y,X,f),y,x) is V28() real ext-real Element of REAL
[y,x] is set
{y,x} is non empty set
{y} is non empty set
{{y,x},{y}} is non empty set
K11((Y,X,f),[y,x]) is V28() real ext-real set
(X,Y,f,x,y) is V28() real ext-real Element of REAL
[x,y] is set
{x,y} is non empty set
{x} is non empty set
{{x,y},{x}} is non empty set
K11(f,[x,y]) is V28() real ext-real set