:: LFUZZY_0 semantic presentation

REAL is non empty V36() V174() V175() V176() V180() set

NAT is V174() V175() V176() V177() V178() V179() V180() Element of bool REAL

bool REAL is non empty set

COMPLEX is non empty V36() V174() V180() set

omega is V174() V175() V176() V177() V178() V179() V180() set

bool omega is non empty set

bool NAT is non empty set

RAT is non empty V36() V174() V175() V176() V177() V180() set

INT is non empty V36() V174() V175() V176() V177() V178() V180() set

[:REAL,REAL:] is non empty set

bool [:REAL,REAL:] is non empty set

K379() is non empty V123() L12()

the carrier of K379() is non empty set

<REAL,+> is non empty V123() V145() V146() V147() V149() left-invertible right-invertible V198() left-cancelable right-cancelable V201() L12()

K385() is non empty V123() V147() V149() left-cancelable right-cancelable V201() SubStr of <REAL,+>

<NAT,+> is non empty V123() V145() V147() V149() left-cancelable right-cancelable V201() uniquely-decomposable SubStr of K385()

<REAL,*> is non empty V123() V145() V147() V149() L12()

<NAT,*> is non empty V123() V145() V147() V149() uniquely-decomposable SubStr of <REAL,*>

{} is set

the empty V174() V175() V176() V177() V178() V179() V180() set is empty V174() V175() V176() V177() V178() V179() V180() set

1 is non empty natural V24() ext-real positive real V104() V105() V174() V175() V176() V177() V178() V179() Element of NAT

{{},1} is set

ExtREAL is non empty V175() set

0 is natural V24() ext-real real V104() V105() V174() V175() V176() V177() V178() V179() Element of NAT

[.0,1.] is V174() V175() V176() Element of bool REAL

[:COMPLEX,COMPLEX:] is non empty set

bool [:COMPLEX,COMPLEX:] is non empty set

[:COMPLEX,REAL:] is non empty set

bool [:COMPLEX,REAL:] is non empty set

[:[:COMPLEX,COMPLEX:],COMPLEX:] is non empty set

bool [:[:COMPLEX,COMPLEX:],COMPLEX:] is non empty set

[:[:REAL,REAL:],REAL:] is non empty set

bool [:[:REAL,REAL:],REAL:] is non empty set

[:RAT,RAT:] is non empty set

bool [:RAT,RAT:] is non empty set

[:[:RAT,RAT:],RAT:] is non empty set

bool [:[:RAT,RAT:],RAT:] is non empty set

[:INT,INT:] is non empty set

bool [:INT,INT:] is non empty set

[:[:INT,INT:],INT:] is non empty set

bool [:[:INT,INT:],INT:] is non empty set

[:NAT,NAT:] is set

[:[:NAT,NAT:],NAT:] is set

bool [:[:NAT,NAT:],NAT:] is non empty set

X is RelStr

the carrier of X is set

Y is V24() ext-real real set

Z is V24() ext-real real set

[.Y,Z.] is V174() V175() V176() Element of bool REAL

X is RelStr

the carrier of X is set

the InternalRel of X is Relation-like the carrier of X -defined the carrier of X -valued Element of bool [: the carrier of X, the carrier of X:]

[: the carrier of X, the carrier of X:] is set

bool [: the carrier of X, the carrier of X:] is non empty set

Y is V24() ext-real real set

Z is V24() ext-real real set

[Y,Z] is set

{Y,Z} is V174() V175() V176() set

{Y} is V174() V175() V176() set

{{Y,Z},{Y}} is set

X is V174() V175() V176() Element of bool REAL

the empty trivial V51() {} -element strict total reflexive transitive antisymmetric () RelStr is empty trivial V51() {} -element strict total reflexive transitive antisymmetric () RelStr

the carrier of the empty trivial V51() {} -element strict total reflexive transitive antisymmetric () RelStr is empty trivial V36() V174() V175() V176() V177() V178() V179() V180() set

Y is non empty set

Z is non empty strict RelStr

the carrier of Z is non empty set

the InternalRel of Z is Relation-like the carrier of Z -defined the carrier of Z -valued Element of bool [: the carrier of Z, the carrier of Z:]

[: the carrier of Z, the carrier of Z:] is non empty set

bool [: the carrier of Z, the carrier of Z:] is non empty set

W is V24() ext-real real set

R is V24() ext-real real set

[W,R] is set

{W,R} is V174() V175() V176() set

{W} is V174() V175() V176() set

{{W,R},{W}} is set

S is Element of the carrier of Z

T is Element of the carrier of Z

x is V24() ext-real real set

w is V24() ext-real real set

x is V24() ext-real real set

w is V24() ext-real real set

Y is strict RelStr

the carrier of Y is set

X is () RelStr

the carrier of X is set

Y is () RelStr

the carrier of Y is set

the InternalRel of X is Relation-like the carrier of X -defined the carrier of X -valued Element of bool [: the carrier of X, the carrier of X:]

[: the carrier of X, the carrier of X:] is set

bool [: the carrier of X, the carrier of X:] is non empty set

RelStr(# the carrier of X, the InternalRel of X #) is strict RelStr

the InternalRel of Y is Relation-like the carrier of Y -defined the carrier of Y -valued Element of bool [: the carrier of Y, the carrier of Y:]

[: the carrier of Y, the carrier of Y:] is set

bool [: the carrier of Y, the carrier of Y:] is non empty set

RelStr(# the carrier of Y, the InternalRel of Y #) is strict RelStr

W is set

R is set

[W,R] is set

{W,R} is set

{W} is set

{{W,R},{W}} is set

S is V24() ext-real real Element of REAL

T is V24() ext-real real Element of REAL

S is V24() ext-real real Element of REAL

T is V24() ext-real real Element of REAL

X is non empty () RelStr

the carrier of X is non empty set

Y is Element of the carrier of X

X is V174() V175() V176() Element of bool REAL

Y is strict RelStr

the carrier of Y is set

Y is strict () RelStr

the carrier of Y is set

Z is strict () RelStr

the carrier of Z is set

X is non empty V174() V175() V176() Element of bool REAL

(X) is strict () RelStr

X is RelStr

the carrier of X is set

X is non empty () RelStr

the carrier of X is non empty set

Y is V24() ext-real real Element of the carrier of X

Z is V24() ext-real real Element of the carrier of X

[Y,Z] is Element of [: the carrier of X, the carrier of X:]

[: the carrier of X, the carrier of X:] is non empty set

{Y,Z} is V174() V175() V176() set

{Y} is V174() V175() V176() set

{{Y,Z},{Y}} is set

the InternalRel of X is Relation-like the carrier of X -defined the carrier of X -valued Element of bool [: the carrier of X, the carrier of X:]

bool [: the carrier of X, the carrier of X:] is non empty set

X is RelStr

Y is non empty () RelStr

the carrier of Y is non empty set

Z is V24() ext-real real Element of the carrier of Y

W is V24() ext-real real Element of the carrier of Y

the carrier of Y is non empty set

Z is V24() ext-real real Element of the carrier of Y

W is V24() ext-real real Element of the carrier of Y

R is V24() ext-real real Element of the carrier of Y

the carrier of Y is non empty set

Z is V24() ext-real real Element of the carrier of Y

X is non empty total reflexive transitive antisymmetric () RelStr

the carrier of X is non empty set

Y is V24() ext-real real Element of the carrier of X

Z is V24() ext-real real Element of the carrier of X

X is non empty total reflexive transitive antisymmetric with_suprema with_infima connected () RelStr

the carrier of X is non empty set

Y is V24() ext-real real Element of the carrier of X

Z is V24() ext-real real Element of the carrier of X

max (Y,Z) is V24() ext-real real set

X is non empty total reflexive transitive antisymmetric with_suprema with_infima connected () RelStr

the carrier of X is non empty set

Y is V24() ext-real real Element of the carrier of X

Z is V24() ext-real real Element of the carrier of X

min (Y,Z) is V24() ext-real real set

X is non empty total reflexive transitive antisymmetric with_suprema with_infima connected () RelStr

Y is non empty total reflexive transitive antisymmetric with_suprema with_infima connected () RelStr

X is non empty total reflexive transitive antisymmetric with_suprema with_infima connected () RelStr

the carrier of X is non empty set

Y is V24() ext-real real Element of the carrier of X

Z is V24() ext-real real Element of the carrier of X

Y "\/" Z is V24() ext-real real Element of the carrier of X

(X,Y,Z) is V24() ext-real real Element of the carrier of X

W is V24() ext-real real Element of the carrier of X

Y "/\" Z is V24() ext-real real Element of the carrier of X

(X,Y,Z) is V24() ext-real real Element of the carrier of X

W is V24() ext-real real Element of the carrier of X

X is non empty total reflexive transitive antisymmetric with_suprema with_infima connected () RelStr

the carrier of X is non empty set

Y is V24() ext-real real Element of the carrier of X

Z is V24() ext-real real Element of the carrier of X

Y "\/" Z is V24() ext-real real Element of the carrier of X

(X,Y,Z) is V24() ext-real real Element of the carrier of X

X is non empty total reflexive transitive antisymmetric with_suprema with_infima connected () RelStr

the carrier of X is non empty set

Y is V24() ext-real real Element of the carrier of X

Z is V24() ext-real real Element of the carrier of X

Y "/\" Z is V24() ext-real real Element of the carrier of X

(X,Y,Z) is V24() ext-real real Element of the carrier of X

X is non empty total reflexive transitive antisymmetric with_suprema with_infima connected () RelStr

the carrier of X is non empty set

Y is V24() ext-real real set

W is V24() ext-real real Element of the carrier of X

Z is V24() ext-real real Element of the carrier of X

Y is V24() ext-real real Element of the carrier of X

Z is V24() ext-real real set

W is V24() ext-real real Element of the carrier of X

X is non empty total reflexive transitive antisymmetric with_suprema with_infima connected () RelStr

the carrier of X is non empty set

Y is V24() ext-real real set

W is V24() ext-real real Element of the carrier of X

Z is V24() ext-real real Element of the carrier of X

Y is V24() ext-real real Element of the carrier of X

Z is V24() ext-real real set

W is V24() ext-real real Element of the carrier of X

X is non empty RelStr

the carrier of X is non empty set

Y is V24() ext-real real set

Z is V24() ext-real real set

[.Y,Z.] is V174() V175() V176() Element of bool REAL

W is V24() ext-real real set

W is V24() ext-real real set

W is V24() ext-real real set

W is V24() ext-real real set

X is non empty total reflexive transitive antisymmetric with_suprema with_infima lower-bounded upper-bounded bounded connected () () RelStr

Y is set

the carrier of X is non empty set

Z is V24() ext-real real set

W is V24() ext-real real set

[.Z,W.] is V174() V175() V176() Element of bool REAL

R is V24() ext-real real Element of REAL

S is V24() ext-real real Element of REAL

[.R,S.] is V174() V175() V176() Element of bool REAL

Y /\ [.R,S.] is V174() V175() V176() Element of bool REAL

T is V174() V175() V176() Element of bool REAL

x is V24() ext-real real Element of the carrier of X

w is V24() ext-real real Element of the carrier of X

the V24() ext-real real Element of T is V24() ext-real real Element of T

w is V24() ext-real real Element of REAL

upper_bound T is V24() ext-real real Element of REAL

upper_bound [.R,S.] is V24() ext-real real Element of REAL

w is V24() ext-real real Element of the carrier of X

x is V24() ext-real real Element of the carrier of X

A is V24() ext-real real set

B is V24() ext-real real Element of the carrier of X

x is V24() ext-real real Element of the carrier of X

x is V24() ext-real real Element of the carrier of X

x is V24() ext-real real Element of the carrier of X

X is non empty total reflexive transitive antisymmetric with_suprema with_infima lower-bounded upper-bounded bounded connected () () RelStr

the carrier of X is non empty set

bool the carrier of X is non empty set

Y is directed filtered Element of bool the carrier of X

X is non empty total reflexive transitive antisymmetric with_suprema with_infima connected RelStr

the carrier of X is non empty set

Y is Element of the carrier of X

Z is Element of the carrier of X

W is Element of the carrier of X

Z "\/" W is Element of the carrier of X

Y "/\" (Z "\/" W) is Element of the carrier of X

Y "/\" Z is Element of the carrier of X

Y "/\" W is Element of the carrier of X

(Y "/\" Z) "\/" (Y "/\" W) is Element of the carrier of X

Y "\/" (Y "/\" W) is Element of the carrier of X

Y "\/" Y is Element of the carrier of X

Y "\/" (Y "/\" W) is Element of the carrier of X

Y "\/" Y is Element of the carrier of X

Y "\/" (Y "/\" W) is Element of the carrier of X

Y "\/" W is Element of the carrier of X

Y "\/" (Y "/\" W) is Element of the carrier of X

Y "\/" W is Element of the carrier of X

Z "\/" (Y "/\" W) is Element of the carrier of X

Z "\/" Y is Element of the carrier of X

Z "\/" (Y "/\" W) is Element of the carrier of X

Z "\/" Y is Element of the carrier of X

Z "\/" (Y "/\" W) is Element of the carrier of X

Z "\/" (Y "/\" W) is Element of the carrier of X

X is non empty total reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded bounded connected distributive satisfying_axiom_of_approximation () () RelStr

the carrier of X is non empty set

Y is V24() ext-real real Element of the carrier of X

Y "/\" is Relation-like the carrier of X -defined the carrier of X -valued Function-like quasi_total V256(X,X) Element of bool [: the carrier of X, the carrier of X:]

[: the carrier of X, the carrier of X:] is non empty set

bool [: the carrier of X, the carrier of X:] is non empty set

bool the carrier of X is non empty set

W is directed filtered Element of bool the carrier of X

(Y "/\") .: W is directed filtered Element of bool the carrier of X

"\/" (((Y "/\") .: W),X) is V24() ext-real real Element of the carrier of X

"\/" (W,X) is V24() ext-real real Element of the carrier of X

(Y "/\") . ("\/" (W,X)) is V24() ext-real real Element of the carrier of X

R is V24() ext-real real Element of the carrier of X

S is V24() ext-real real Element of the carrier of X

Y "/\" S is V24() ext-real real Element of the carrier of X

(X,Y,S) is V24() ext-real real Element of the carrier of X

(Y "/\") . S is V24() ext-real real Element of the carrier of X

Y "/\" ("\/" (W,X)) is V24() ext-real real Element of the carrier of X

(X,Y,("\/" (W,X))) is V24() ext-real real Element of the carrier of X

S is V24() ext-real real Element of the carrier of X

Y "/\" ("\/" (W,X)) is V24() ext-real real Element of the carrier of X

(X,Y,("\/" (W,X))) is V24() ext-real real Element of the carrier of X

(Y "/\") . S is V24() ext-real real Element of the carrier of X

Y "/\" S is V24() ext-real real Element of the carrier of X

(X,Y,S) is V24() ext-real real Element of the carrier of X

R is V24() ext-real real Element of the carrier of X

Y "/\" ("\/" (W,X)) is V24() ext-real real Element of the carrier of X

(X,Y,("\/" (W,X))) is V24() ext-real real Element of the carrier of X

S is set

(Y "/\") . S is set

T is V24() ext-real real Element of the carrier of X

Y "/\" T is V24() ext-real real Element of the carrier of X

(X,Y,T) is V24() ext-real real Element of the carrier of X

([.0,1.]) is non empty strict total reflexive transitive antisymmetric with_suprema with_infima connected distributive () RelStr

the carrier of ([.0,1.]) is non empty set

X is non empty set

Y is Relation-like X -defined Function-like total RelStr-yielding non-Empty reflexive-yielding set

product Y is non empty strict total reflexive constituted-Functions RelStr

the carrier of (product Y) is non empty set

W is Relation-like Function-like Element of the carrier of (product Y)

R is Relation-like Function-like Element of the carrier of (product Y)

S is Relation-like X -defined Function-like total set

T is Element of X

S . T is set

Y . T is non empty total reflexive RelStr

the carrier of (Y . T) is non empty set

W . T is Element of the carrier of (Y . T)

R . T is Element of the carrier of (Y . T)

(W . T) "\/" (R . T) is Element of the carrier of (Y . T)

dom S is Element of bool X

bool X is non empty set

T is Relation-like Function-like Element of the carrier of (product Y)

x is Element of X

Y . x is non empty total reflexive RelStr

W . x is Element of the carrier of (Y . x)

the carrier of (Y . x) is non empty set

T . x is Element of the carrier of (Y . x)

R . x is Element of the carrier of (Y . x)

(W . x) "\/" (R . x) is Element of the carrier of (Y . x)

x is Relation-like Function-like Element of the carrier of (product Y)

w is Element of X

Y . w is non empty total reflexive RelStr

T . w is Element of the carrier of (Y . w)

the carrier of (Y . w) is non empty set

x . w is Element of the carrier of (Y . w)

R . w is Element of the carrier of (Y . w)

W . w is Element of the carrier of (Y . w)

(W . w) "\/" (R . w) is Element of the carrier of (Y . w)

X is non empty set

Y is Relation-like X -defined Function-like total RelStr-yielding non-Empty reflexive-yielding set

product Y is non empty strict total reflexive constituted-Functions RelStr

the carrier of (product Y) is non empty set

W is Relation-like Function-like Element of the carrier of (product Y)

R is Relation-like Function-like Element of the carrier of (product Y)

S is Relation-like X -defined Function-like total set

T is Element of X

S . T is set

Y . T is non empty total reflexive RelStr

the carrier of (Y . T) is non empty set

W . T is Element of the carrier of (Y . T)

R . T is Element of the carrier of (Y . T)

(W . T) "/\" (R . T) is Element of the carrier of (Y . T)

dom S is Element of bool X

bool X is non empty set

T is Relation-like Function-like Element of the carrier of (product Y)

x is Element of X

Y . x is non empty total reflexive RelStr

T . x is Element of the carrier of (Y . x)

the carrier of (Y . x) is non empty set

W . x is Element of the carrier of (Y . x)

R . x is Element of the carrier of (Y . x)

(W . x) "/\" (R . x) is Element of the carrier of (Y . x)

x is Relation-like Function-like Element of the carrier of (product Y)

w is Element of X

Y . w is non empty total reflexive RelStr

x . w is Element of the carrier of (Y . w)

the carrier of (Y . w) is non empty set

T . w is Element of the carrier of (Y . w)

R . w is Element of the carrier of (Y . w)

W . w is Element of the carrier of (Y . w)

(W . w) "/\" (R . w) is Element of the carrier of (Y . w)

X is non empty set

Y is Relation-like X -defined Function-like total RelStr-yielding non-Empty reflexive-yielding set

product Y is non empty strict total reflexive constituted-Functions RelStr

the carrier of (product Y) is non empty set

Z is Relation-like Function-like Element of the carrier of (product Y)

W is Relation-like Function-like Element of the carrier of (product Y)

Z "/\" W is Relation-like Function-like Element of the carrier of (product Y)

R is Element of X

(Z "/\" W) . R is Element of the carrier of (Y . R)

Y . R is non empty total reflexive RelStr

the carrier of (Y . R) is non empty set

Z . R is Element of the carrier of (Y . R)

W . R is Element of the carrier of (Y . R)

(Z . R) "/\" (W . R) is Element of the carrier of (Y . R)

S is Element of X

Y . S is non empty total reflexive RelStr

S is Relation-like X -defined Function-like total set

T is Element of X

S . T is set

Y . T is non empty total reflexive RelStr

the carrier of (Y . T) is non empty set

Z . T is Element of the carrier of (Y . T)

W . T is Element of the carrier of (Y . T)

(Z . T) "/\" (W . T) is Element of the carrier of (Y . T)

dom S is Element of bool X

bool X is non empty set

T is Relation-like Function-like Element of the carrier of (product Y)

x is Element of X

Y . x is non empty total reflexive RelStr

T . x is Element of the carrier of (Y . x)

the carrier of (Y . x) is non empty set

Z . x is Element of the carrier of (Y . x)

W . x is Element of the carrier of (Y . x)

(Z . x) "/\" (W . x) is Element of the carrier of (Y . x)

x is Element of X

Y . x is non empty total reflexive RelStr

Z . x is Element of the carrier of (Y . x)

the carrier of (Y . x) is non empty set

W . x is Element of the carrier of (Y . x)

(Z . x) "/\" (W . x) is Element of the carrier of (Y . x)

(Z "/\" W) . x is Element of the carrier of (Y . x)

T . x is Element of the carrier of (Y . x)

X is non empty set

Y is Relation-like X -defined Function-like total RelStr-yielding non-Empty reflexive-yielding set

product Y is non empty strict total reflexive constituted-Functions RelStr

the carrier of (product Y) is non empty set

Z is Relation-like Function-like Element of the carrier of (product Y)

W is Relation-like Function-like Element of the carrier of (product Y)

Z "\/" W is Relation-like Function-like Element of the carrier of (product Y)

R is Element of X

(Z "\/" W) . R is Element of the carrier of (Y . R)

Y . R is non empty total reflexive RelStr

the carrier of (Y . R) is non empty set

Z . R is Element of the carrier of (Y . R)

W . R is Element of the carrier of (Y . R)

(Z . R) "\/" (W . R) is Element of the carrier of (Y . R)

S is Element of X

Y . S is non empty total reflexive RelStr

S is Relation-like X -defined Function-like total set

T is Element of X

S . T is set

Y . T is non empty total reflexive RelStr

the carrier of (Y . T) is non empty set

Z . T is Element of the carrier of (Y . T)

W . T is Element of the carrier of (Y . T)

(Z . T) "\/" (W . T) is Element of the carrier of (Y . T)

dom S is Element of bool X

bool X is non empty set

T is Relation-like Function-like Element of the carrier of (product Y)

x is Element of X

Y . x is non empty total reflexive RelStr

Z . x is Element of the carrier of (Y . x)

the carrier of (Y . x) is non empty set

T . x is Element of the carrier of (Y . x)

W . x is Element of the carrier of (Y . x)

(Z . x) "\/" (W . x) is Element of the carrier of (Y . x)

x is Element of X

Y . x is non empty total reflexive RelStr

(Z "\/" W) . x is Element of the carrier of (Y . x)

the carrier of (Y . x) is non empty set

Z . x is Element of the carrier of (Y . x)

W . x is Element of the carrier of (Y . x)

(Z . x) "\/" (W . x) is Element of the carrier of (Y . x)

T . x is Element of the carrier of (Y . x)

X is non empty set

Y is Relation-like X -defined Function-like total RelStr-yielding non-Empty reflexive-yielding set

product Y is non empty strict total reflexive constituted-Functions RelStr

Z is Element of X

Y . Z is non empty total reflexive RelStr

W is non empty total reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded bounded RelStr

the carrier of (product Y) is non empty set

R is Relation-like Function-like Element of the carrier of (product Y)

R "/\" is Relation-like the carrier of (product Y) -defined the carrier of (product Y) -valued Function-like quasi_total Element of bool [: the carrier of (product Y), the carrier of (product Y):]

[: the carrier of (product Y), the carrier of (product Y):] is non empty set

bool [: the carrier of (product Y), the carrier of (product Y):] is non empty set

the carrier of W is non empty set

[: the carrier of W, the carrier of W:] is non empty set

bool [: the carrier of W, the carrier of W:] is non empty set

x is Element of X

Y . x is non empty total reflexive RelStr

T is Relation-like the carrier of W -defined the carrier of W -valued Function-like quasi_total Element of bool [: the carrier of W, the carrier of W:]

bool the carrier of W is non empty set

x is Element of bool the carrier of W

bool the carrier of (product Y) is non empty set

T .: x is Element of bool the carrier of W

"\/" (x,W) is Element of the carrier of W

"\/" ((T .: x),W) is Element of the carrier of W

T . ("\/" (x,W)) is Element of the carrier of W

C is set

A is Relation-like Function-like Element of the carrier of (product Y)

dom A is set

D is Element of X

Y . D is non empty total reflexive RelStr

w is Element of bool the carrier of (product Y)

pi (w,D) is Element of bool the carrier of (Y . D)

the carrier of (Y . D) is non empty set

bool the carrier of (Y . D) is non empty set

R . D is Element of the carrier of (Y . D)

(R . D) "/\" is Relation-like the carrier of (Y . D) -defined the carrier of (Y . D) -valued Function-like quasi_total Element of bool [: the carrier of (Y . D), the carrier of (Y . D):]

[: the carrier of (Y . D), the carrier of (Y . D):] is non empty set

bool [: the carrier of (Y . D), the carrier of (Y . D):] is non empty set

((R . D) "/\") .: (pi (w,D)) is Element of bool the carrier of (Y . D)

w is Element of bool the carrier of (product Y)

pi (w,D) is Element of bool the carrier of (Y . D)

c is set

dom ((R . D) "/\") is Element of bool the carrier of (Y . D)

y is set

((R . D) "/\") . y is set

f3 is Relation-like Function-like set

f3 . D is set

h is Relation-like Function-like Element of the carrier of (product Y)

R "/\" h is Relation-like Function-like Element of the carrier of (product Y)

(R "/\") . h is Relation-like Function-like Element of the carrier of (product Y)

(R "/\") .: x is Element of bool the carrier of (product Y)

h . D is Element of the carrier of (Y . D)

(R . D) "/\" (h . D) is Element of the carrier of (Y . D)

(R "/\" h) . D is Element of the carrier of (Y . D)

c is set

y is Relation-like Function-like set

y . D is set

dom T is Element of bool the carrier of W

f3 is Relation-like Function-like Element of the carrier of (product Y)

h is set

T . h is set

h is Relation-like Function-like Element of the carrier of (product Y)

h . D is Element of the carrier of (Y . D)

f3 . D is Element of the carrier of (Y . D)

R "/\" h is Relation-like Function-like Element of the carrier of (product Y)

(R "/\" h) . D is Element of the carrier of (Y . D)

(R . D) "/\" (h . D) is Element of the carrier of (Y . D)

((R . D) "/\") . (h . D) is Element of the carrier of (Y . D)

B is Relation-like Function-like Element of the carrier of (product Y)

S is Element of the carrier of W

S "/\" ("\/" (x,W)) is Element of the carrier of W

B . D is Element of the carrier of (Y . D)

x is Relation-like Function-like Element of the carrier of (product Y)

x . D is Element of the carrier of (Y . D)

(R . D) "/\" (x . D) is Element of the carrier of (Y . D)

"\/" ((pi (w,D)),(Y . D)) is Element of the carrier of (Y . D)

(R . D) "/\" ("\/" ((pi (w,D)),(Y . D))) is Element of the carrier of (Y . D)

((R . D) "/\") . ("\/" ((pi (w,D)),(Y . D))) is Element of the carrier of (Y . D)

"\/" ((((R . D) "/\") .: (pi (w,D))),(Y . D)) is Element of the carrier of (Y . D)

A . C is set

B . C is set

dom B is set

X is non empty set

Y is non empty total reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded bounded distributive Heyting RelStr

Y |^ X is non empty strict total reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded bounded RelStr

X --> Y is non empty Relation-like X -defined {Y} -valued Function-like constant total quasi_total RelStr-yielding non-Empty reflexive-yielding Element of bool [:X,{Y}:]

{Y} is set

[:X,{Y}:] is set

bool [:X,{Y}:] is non empty set

Z is Element of X

(X --> Y) . Z is non empty total reflexive RelStr

product (X --> Y) is non empty strict total reflexive constituted-Functions RelStr

X is non empty set

([.0,1.]) |^ X is non empty strict total reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded bounded distributive Heyting RelStr

X is non empty set

(X) is non empty total reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded bounded distributive Heyting RelStr

([.0,1.]) |^ X is non empty strict total reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded bounded distributive Heyting RelStr

the carrier of (X) is non empty set

Funcs (X,[.0,1.]) is non empty FUNCTION_DOMAIN of X,[.0,1.]

the carrier of ([.0,1.]) is non empty set

Funcs (X, the carrier of ([.0,1.])) is non empty FUNCTION_DOMAIN of X, the carrier of ([.0,1.])

X is non empty set

(X) is non empty total reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded bounded distributive Heyting RelStr

([.0,1.]) |^ X is non empty strict total reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded bounded distributive Heyting RelStr

the carrier of (X) is non empty set

Y is Element of the carrier of (X)

Funcs (X,[.0,1.]) is non empty FUNCTION_DOMAIN of X,[.0,1.]

Z is Relation-like Function-like set

dom Z is set

rng Z is set

X is non empty set

(X) is non empty total reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded bounded distributive Heyting RelStr

([.0,1.]) |^ X is non empty strict total reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded bounded distributive Heyting RelStr

X is non empty total reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded bounded distributive Heyting RelStr

the carrier of X is non empty set

bool the carrier of X is non empty set

Y is Element of bool the carrier of X

"\/" (Y,X) is Element of the carrier of X

Z is Element of the carrier of X

("\/" (Y,X)) "/\" Z is Element of the carrier of X

{ (b

"\/" ( { (b

{ (Z "/\" b

S is set

T is Element of the carrier of X

T "/\" Z is Element of the carrier of X

S is set

T is Element of the carrier of X

Z "/\" T is Element of the carrier of X

S is Element of the carrier of X

S "/\" is Relation-like the carrier of X -defined the carrier of X -valued Function-like quasi_total V256(X,X) Element of bool [: the carrier of X, the carrier of X:]

[: the carrier of X, the carrier of X:] is non empty set

bool [: the carrier of X, the carrier of X:] is non empty set

X is non empty set

(X) is non empty total reflexive transitive antisymmetric with_suprema with_infima complete constituted-Functions lower-bounded upper-bounded bounded distributive Heyting RelStr

([.0,1.]) |^ X is non empty strict total reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded bounded distributive Heyting RelStr

the carrier of (X) is non empty set

[:X,REAL:] is non empty set

bool [:X,REAL:] is non empty set

Y is Relation-like Function-like Element of the carrier of (X)

Funcs (X,[.0,1.]) is non empty FUNCTION_DOMAIN of X,[.0,1.]

[:X,[.0,1.]:] is non empty set

bool [:X,[.0,1.]:] is non empty set

W is Relation-like Function-like set

dom W is set

rng W is set

Z is Relation-like X -defined [.0,1.] -valued Function-like Element of bool [:X,[.0,1.]:]

W is Relation-like X -defined REAL -valued Function-like Element of bool [:X,REAL:]

R is Relation-like Function-like set

dom R is set

rng R is set

X is non empty set

(X) is non empty total reflexive transitive antisymmetric with_suprema with_infima complete constituted-Functions lower-bounded upper-bounded bounded distributive Heyting RelStr

([.0,1.]) |^ X is non empty strict total reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded bounded distributive Heyting RelStr

the carrier of (X) is non empty set

Y is Relation-like Function-like Element of the carrier of (X)

[:X,REAL:] is non empty set

bool [:X,REAL:] is non empty set

X is non empty set

[:X,REAL:] is non empty set

bool [:X,REAL:] is non empty set

(X) is non empty total reflexive transitive antisymmetric with_suprema with_infima complete constituted-Functions lower-bounded upper-bounded bounded distributive Heyting RelStr

([.0,1.]) |^ X is non empty strict total reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded bounded distributive Heyting RelStr

the carrier of (X) is non empty set

Y is Relation-like X -defined REAL -valued [.0,1.] -valued Function-like quasi_total Element of bool [:X,REAL:]

dom Y is Element of bool X

bool X is non empty set

rng Y is V174() V175() V176() Element of bool REAL

Funcs (X,[.0,1.]) is non empty FUNCTION_DOMAIN of X,[.0,1.]

X is non empty set

[:X,REAL:] is non empty set

bool [:X,REAL:] is non empty set

Y is Relation-like X -defined REAL -valued [.0,1.] -valued Function-like quasi_total Element of bool [:X,REAL:]

(X) is non empty total reflexive transitive antisymmetric with_suprema with_infima complete constituted-Functions lower-bounded upper-bounded bounded distributive Heyting RelStr

([.0,1.]) |^ X is non empty strict total reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded bounded distributive Heyting RelStr

the carrier of (X) is non empty set

X is non empty set

[:X,REAL:] is non empty set

bool [:X,REAL:] is non empty set

Y is Relation-like X -defined REAL -valued [.0,1.] -valued Function-like quasi_total Element of bool [:X,REAL:]

Z is Element of X

Y . Z is set

the carrier of ([.0,1.]) is non empty set

Y . Z is V24() ext-real real Element of REAL

X is non empty set

Y is non empty set

[:X,Y:] is non empty set

[:[:X,Y:],REAL:] is non empty set

bool [:[:X,Y:],REAL:] is non empty set

Z is Relation-like [:X,Y:] -defined REAL -valued [.0,1.] -valued Function-like quasi_total Element of bool [:[:X,Y:],REAL:]

W is Element of X

R is Element of Y

Z . (W,R) is set

[W,R] is set

{W,R} is set

{W} is set

{{W,R},{W}} is set

Z . [W,R] is set

[W,R] is Element of [:X,Y:]

([:X,Y:],Z,[W,R]) is V24() ext-real real Element of the carrier of ([.0,1.])

X is non empty set

(X) is non empty total reflexive transitive antisymmetric with_suprema with_infima complete constituted-Functions lower-bounded upper-bounded bounded distributive Heyting RelStr

([.0,1.]) |^ X is non empty strict total reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded bounded distributive Heyting RelStr

the carrier of (X) is non empty set

Y is Relation-like Function-like Element of the carrier of (X)

Z is Element of X

Y . Z is set

(X,Y) is Relation-like X -defined REAL -valued [.0,1.] -valued Function-like quasi_total Element of bool [:X,REAL:]

[:X,REAL:] is non empty set

bool [:X,REAL:] is non empty set

(X,(X,Y),Z) is V24() ext-real real Element of the carrier of ([.0,1.])

X is non empty set

[:X,REAL:] is non empty set

bool [:X,REAL:] is non empty set

(X) is non empty total reflexive transitive antisymmetric with_suprema with_infima complete constituted-Functions lower-bounded upper-bounded bounded distributive Heyting RelStr

([.0,1.]) |^ X is non empty strict total reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded bounded distributive Heyting RelStr

Y is Relation-like X -defined REAL -valued [.0,1.] -valued Function-like quasi_total Element of bool [:X,REAL:]

(X,Y) is Relation-like Function-like Element of the carrier of (X)

the carrier of (X) is non empty set

Z is Relation-like X -defined REAL -valued [.0,1.] -valued Function-like quasi_total Element of bool [:X,REAL:]

(X,Z) is Relation-like Function-like Element of the carrier of (X)

X --> ([.0,1.]) is non empty Relation-like X -defined {([.0,1.])} -valued Function-like constant total quasi_total RelStr-yielding non-Empty reflexive-yielding Element of bool [:X,{([.0,1.])}:]

{([.0,1.])} is set

[:X,{([.0,1.])}:] is set

bool [:X,{([.0,1.])}:] is non empty set

product (X --> ([.0,1.])) is non empty strict total reflexive constituted-Functions RelStr

the carrier of (product (X --> ([.0,1.]))) is non empty set

S is Relation-like Function-like Element of the carrier of (product (X --> ([.0,1.])))

T is Relation-like Function-like Element of the carrier of (product (X --> ([.0,1.])))

x is Element of X

(X --> ([.0,1.])) . x is non empty total reflexive RelStr

S . x is Element of the carrier of ((X --> ([.0,1.])) . x)

the carrier of ((X --> ([.0,1.])) . x) is non empty set

T . x is Element of the carrier of ((X --> ([.0,1.])) . x)

(X,Y,x) is V24() ext-real real Element of the carrier of ([.0,1.])

(X,Z,x) is V24() ext-real real Element of the carrier of ([.0,1.])

the carrier of (product (X --> ([.0,1.]))) is non empty set

S is Element of X

(X,Y,S) is V24() ext-real real Element of the carrier of ([.0,1.])

(X,Z,S) is V24() ext-real real Element of the carrier of ([.0,1.])

(X --> ([.0,1.])) . S is non empty total reflexive RelStr

W is Relation-like Function-like Element of the carrier of (product (X --> ([.0,1.])))

W . S is Element of the carrier of ((X --> ([.0,1.])) . S)

the carrier of ((X --> ([.0,1.])) . S) is non empty set

R is Relation-like Function-like Element of the carrier of (product (X --> ([.0,1.])))

R . S is Element of the carrier of ((X --> ([.0,1.])) . S)

W is Element of X

(X,Y,W) is V24() ext-real real Element of the carrier of ([.0,1.])

(X,Z,W) is V24() ext-real real Element of the carrier of ([.0,1.])

R is Element of X

(X,Y,R) is V24() ext-real real Element of the carrier of ([.0,1.])

(X,Z,R) is V24() ext-real real Element of the carrier of ([.0,1.])

X is non empty set

(X) is non empty total reflexive transitive antisymmetric with_suprema with_infima complete constituted-Functions lower-bounded upper-bounded bounded distributive Heyting RelStr

([.0,1.]) |^ X is non empty strict total reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded bounded distributive Heyting RelStr

the carrier of (X) is non empty set

Y is Relation-like Function-like Element of the carrier of (X)

(X,Y) is Relation-like X -defined REAL -valued [.0,1.] -valued Function-like quasi_total Element of bool [:X,REAL:]

[:X,REAL:] is non empty set

bool [:X,REAL:] is non empty set

Z is Relation-like Function-like Element of the carrier of (X)

(X,Z) is Relation-like X -defined REAL -valued [.0,1.] -valued Function-like quasi_total Element of bool [:X,REAL:]

(X,(X,Y)) is Relation-like Function-like Element of the carrier of (X)

(X,(X,Z)) is Relation-like Function-like Element of the carrier of (X)

W is Element of X

(X,(X,Y),W) is V24() ext-real real Element of the carrier of ([.0,1.])

(X,(X,Z),W) is V24() ext-real real Element of the carrier of ([.0,1.])

X is non empty set

[:X,REAL:] is non empty set

bool [:X,REAL:] is non empty set

(X) is non empty total reflexive transitive antisymmetric with_suprema with_infima complete constituted-Functions lower-bounded upper-bounded bounded distributive Heyting RelStr

([.0,1.]) |^ X is non empty strict total reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded bounded distributive Heyting RelStr

Y is Relation-like X -defined REAL -valued [.0,1.] -valued Function-like quasi_total Element of bool [:X,REAL:]

(X,Y) is Relation-like Function-like Element of the carrier of (X)

the carrier of (X) is non empty set

Z is Relation-like X -defined REAL -valued [.0,1.] -valued Function-like quasi_total Element of bool [:X,REAL:]

max (Y,Z) is Relation-like X -defined REAL -valued [.0,1.] -valued Function-like quasi_total Element of bool [:X,REAL:]

(X,Z) is Relation-like Function-like Element of the carrier of (X)

(X,Y) "\/" (X,Z) is Relation-like Function-like Element of the carrier of (X)

X --> ([.0,1.]) is non empty Relation-like X -defined {([.0,1.])} -valued Function-like constant total quasi_total RelStr-yielding non-Empty reflexive-yielding Element of bool [:X,{([.0,1.])}:]

{([.0,1.])} is set

[:X,{([.0,1.])}:] is set

bool [:X,{([.0,1.])}:] is non empty set

product (X --> ([.0,1.])) is non empty strict total reflexive constituted-Functions RelStr

T is Element of X

(X --> ([.0,1.])) . T is non empty total reflexive RelStr

x is Element of X

(X --> ([.0,1.])) . x is non empty total reflexive RelStr

(X,((X,Y) "\/" (X,Z))) is Relation-like X -defined REAL -valued [.0,1.] -valued Function-like quasi_total Element of bool [:X,REAL:]

(X,(X,((X,Y) "\/" (X,Z))),T) is V24() ext-real real Element of the carrier of ([.0,1.])

(X,(X,Y),T) is V24() ext-real real Element of the carrier of ([.0,1.])

(X,(X,Z),T) is V24() ext-real real Element of the carrier of ([.0,1.])

(X,(X,Y),T) "\/" (X,(X,Z),T) is V24() ext-real real Element of the carrier of ([.0,1.])

(([.0,1.]),(X,(X,Y),T),(X,(X,Z),T)) is V24() ext-real real Element of the carrier of ([.0,1.])

(X,Y,T) is V24() ext-real real Element of the carrier of ([.0,1.])

(X,Z,T) is V24() ext-real real Element of the carrier of ([.0,1.])

(([.0,1.]),(X,Y,T),(X,Z,T)) is V24() ext-real real Element of the carrier of ([.0,1.])

X is non empty set

(X) is non empty total reflexive transitive antisymmetric with_suprema with_infima complete constituted-Functions lower-bounded upper-bounded bounded distributive Heyting RelStr

([.0,1.]) |^ X is non empty strict total reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded bounded distributive Heyting RelStr

the carrier of (X) is non empty set

Y is Relation-like Function-like Element of the carrier of (X)

(X,Y) is Relation-like X -defined REAL -valued [.0,1.] -valued Function-like quasi_total Element of bool [:X,REAL:]

[:X,REAL:] is non empty set

bool [:X,REAL:] is non empty set

Z is Relation-like Function-like Element of the carrier of (X)

Y "\/" Z is Relation-like Function-like Element of the carrier of (X)

(X,Z) is Relation-like X -defined REAL -valued [.0,1.] -valued Function-like quasi_total Element of bool [:X,REAL:]

max ((X,Y),(X,Z)) is Relation-like X -defined REAL -valued [.0,1.] -valued Function-like quasi_total Element of bool [:X,REAL:]

(X,(X,Y)) is Relation-like Function-like Element of the carrier of (X)

(X,(X,Z)) is Relation-like Function-like Element of the carrier of (X)

X is non empty set

[:X,REAL:] is non empty set

bool [:X,REAL:] is non empty set

(X) is non empty total reflexive transitive antisymmetric with_suprema with_infima complete constituted-Functions lower-bounded upper-bounded bounded distributive Heyting RelStr

([.0,1.]) |^ X is non empty strict total reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded bounded distributive Heyting RelStr

Y is Relation-like X -defined REAL -valued [.0,1.] -valued Function-like quasi_total Element of bool [:X,REAL:]

(X,Y) is Relation-like Function-like Element of the carrier of (X)

the carrier of (X) is non empty set

Z is Relation-like X -defined REAL -valued [.0,1.] -valued Function-like quasi_total Element of bool [:X,REAL:]

min (Y,Z) is Relation-like X -defined REAL -valued [.0,1.] -valued Function-like quasi_total Element of bool [:X,REAL:]

(X,Z) is Relation-like Function-like Element of the carrier of (X)

(X,Y) "/\" (X,Z) is Relation-like Function-like Element of the carrier of (X)

X --> ([.0,1.]) is non empty Relation-like X -defined {([.0,1.])} -valued Function-like constant total quasi_total RelStr-yielding non-Empty reflexive-yielding Element of bool [:X,{([.0,1.])}:]

{([.0,1.])} is set

[:X,{([.0,1.])}:] is set

bool [:X,{([.0,1.])}:] is non empty set

product (X --> ([.0,1.])) is non empty strict total reflexive constituted-Functions RelStr

T is Element of X

(X --> ([.0,1.])) . T is non empty total reflexive RelStr

x is Element of X

(X --> ([.0,1.])) . x is non empty total reflexive RelStr

(X,((X,Y) "/\" (X,Z))) is Relation-like X -defined REAL -valued [.0,1.] -valued Function-like quasi_total Element of bool [:X,REAL:]

(X,(X,((X,Y) "/\" (X,Z))),T) is V24() ext-real real Element of the carrier of ([.0,1.])

(X,(X,Y),T) is V24() ext-real real Element of the carrier of ([.0,1.])

(X,(X,Z),T) is V24() ext-real real Element of the carrier of ([.0,1.])

(X,(X,Y),T) "/\" (X,(X,Z),T) is V24() ext-real real Element of the carrier of ([.0,1.])

(([.0,1.]),(X,(X,Y),T),(X,(X,Z),T)) is V24() ext-real real Element of the carrier of ([.0,1.])

(X,Y,T) is V24() ext-real real Element of the carrier of ([.0,1.])

(X,Z,T) is V24() ext-real real Element of the carrier of ([.0,1.])

(([.0,1.]),(X,Y,T),(X,Z,T)) is V24() ext-real real Element of the carrier of ([.0,1.])

X is non empty set

(X) is non empty total reflexive transitive antisymmetric with_suprema with_infima complete constituted-Functions lower-bounded upper-bounded bounded distributive Heyting RelStr

([.0,1.]) |^ X is non empty strict total reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded bounded distributive Heyting RelStr

the carrier of (X) is non empty set

Y is Relation-like Function-like Element of the carrier of (X)

(X,Y) is Relation-like X -defined REAL -valued [.0,1.] -valued Function-like quasi_total Element of bool [:X,REAL:]

[:X,REAL:] is non empty set

bool [:X,REAL:] is non empty set

Z is Relation-like Function-like Element of the carrier of (X)

Y "/\" Z is Relation-like Function-like Element of the carrier of (X)

(X,Z) is Relation-like X -defined REAL -valued [.0,1.] -valued Function-like quasi_total Element of bool [:X,REAL:]

min ((X,Y),(X,Z)) is Relation-like X -defined REAL -valued [.0,1.] -valued Function-like quasi_total Element of bool [:X,REAL:]

(X,(X,Y)) is Relation-like Function-like Element of the carrier of (X)

(X,(X,Z)) is Relation-like Function-like Element of the carrier of (X)

F

the carrier of F

F

F

{ ("\/" ( { F

"\/" ( { ("\/" ( { F

{ F

"\/" ( { F

bool the carrier of F

{ ("\/" (b

"\/" ( { ("\/" (b

{ b

union { b

"\/" ((union { b

X is set

Y is Element of F

Z is Element of F

F

{ F

R is set

S is Element of F

F

R is Element of bool the carrier of F

S is set

T is Element of F

F

S is Element of F

X is set

Y is Element of F

{ F

"\/" ( { F

W is set

R is Element of F

F

W is Element of bool the carrier of F

R is set

S is set

T is Element of F

F

R is Element of F

Z is Element of bool the carrier of F

"\/" (Z,F

W is Element of F

X is set

Y is Element of bool the carrier of F

"\/" (Y,F

Z is Element of F

Z is Element of F

W is set

{ F

R is Element of F

F

R is Element of F

F

X is set

Y is set

Z is Element of bool the carrier of F

W is Element of F

W is Element of F

R is Element of F

F

F

the carrier of F

F

F

{ ("\/" ( { F

"\/" ( { ("\/" ( { F

{ F

"\/" ( { F

bool the carrier of F

{ ("\/" (b

"\/" ( { ("\/" (b

{ b

union { b

"\/" ((union { b

X is set

Y is Element of F

Z is Element of F

F

{ F

R is set

S is Element of F

F

R is Element of bool the carrier of F

S is set

T is Element of F

F

S is Element of F

X is set

Y is Element of F

{ F

"\/" ( { F

W is set

R is Element of F

F

W is Element of bool the carrier of F

R is set

S is set

T is Element of F

F

R is Element of F

Z is Element of bool the carrier of F

"\/" (Z,F

W is Element of F

X is set

Y is Element of bool the carrier of F

"\/" (Y,F

Z is Element of F

Z is Element of F

W is set

{ F

R is Element of F

F

R is Element of F

F

X is set

Y is set

Z is Element of bool the carrier of F

W is Element of F

W is Element of F

R is Element of F

F

F

F

{ F

{ F

Z is set

W is Element of F

R is Element of F

F

F

W is Element of F

R is Element of F

F

F

F

F

{ F

{ F

{ F

F

the carrier of F

F

F

{ ("\/" ( { F

"\/" ( { ("\/" ( { F

{ ("\/" ( { F

"\/" ( { ("\/" ( { F

X is Element of F

Y is Element of F

Z is Element of F

W is Element of F

X is Element of F

Y is Element of F

F

F

{ F

{ F

{ F

"\/" ( { F

{ F

"\/" ( { F

X is V24() ext-real real Element of the carrier of ([.0,1.])

X is non empty set

Y is non empty set

[:X,Y:] is non empty set

[:[:X,Y:],REAL:] is non empty set

bool [:[:X,Y:],REAL:] is non empty set

Z is non empty set

[:Y,Z:] is non empty set

[:[:Y,Z:],REAL:] is non empty set

bool [:[:Y,Z:],REAL:] is non empty set

W is Relation-like [:X,Y:] -defined REAL -valued [.0,1.] -valued Function-like quasi_total Element of bool [:[:X,Y:],REAL:]

R is Relation-like [:Y,Z:] -defined REAL -valued [.0,1.] -valued Function-like quasi_total Element of bool [:[:Y,Z:],REAL:]

S is Element of X

T is Element of Z

min (W,R,S,T) is Relation-like Y -defined REAL -valued [.0,1.] -valued Function-like quasi_total Element of bool [:Y,REAL:]

[:Y,REAL:] is non empty set

bool [:Y,REAL:] is non empty set

rng (min (W,R,S,T)) is V174() V175() V176() Element of bool REAL

{ ((X,Y,W,S,b

dom (min (W,R,S,T)) is Element of bool Y

bool Y is non empty set

[:(dom (min (W,R,S,T))),(rng (min (W,R,S,T))):] is set

bool [:(dom (min (W,R,S,T))),(rng (min (W,R,S,T))):] is non empty set

w is set

w is Element of Y

(X,Y,W,S,w) is V24() ext-real real Element of the carrier of ([.0,1.])

[S,w] is set

{S,w} is set

{S} is set

{{S,w},{S}} is set

W . [S,w] is set

(Y,Z,R,w,T) is V24() ext-real real Element of the carrier of ([.0,1.])

[w,T] is set

{w,T} is set

{w} is set

{{w,T},{w}} is set

R . [w,T] is set

(X,Y,W,S,w) "/\" (Y,Z,R,w,T) is V24() ext-real real Element of the carrier of ([.0,1.])

(([.0,1.]),(X,Y,W,S,w),(Y,Z,R,w,T)) is V24() ext-real real Element of the carrier of ([.0,1.])

(Y,(min (W,R,S,T)),w) is V24() ext-real real Element of the carrier of ([.0,1.])

w is Element of Y

(Y,(min (W,R,S,T)),w) is V24() ext-real real Element of the carrier of ([.0,1.])

(X,Y,W,S,w) is V24() ext-real real Element of the carrier of ([.0,1.])

[S,w] is set

{S,w} is set

{{S,w},{S}} is set

W . [S,w] is set

(Y,Z,R,w,T) is V24() ext-real real Element of the carrier of ([.0,1.])

[w,T] is set

{w,T} is set

{w} is set

{{w,T},{w}} is set

R . [w,T] is set

(X,Y,W,S,w) "/\" (Y,Z,R,w,T) is V24() ext-real real Element of the carrier of ([.0,1.])

(([.0,1.]),(X,Y,W,S,w),(Y,Z,R,w,T)) is V24() ext-real real Element of the carrier of ([.0,1.])

the Element of Y is Element of Y

(Y,(min (W,R,S,T)), the Element of Y) is V24() ext-real real Element of the carrier of ([.0,1.])

w is set

X is non empty set

Y is non empty set

[:X,Y:] is non empty set

[:[:X,Y:],REAL:] is non empty set

bool [:[:X,Y:],REAL:] is non empty set

Z is non empty set

[:Y,Z:] is non empty set

[:[:Y,Z:],REAL:] is non empty set

bool [:[:Y,Z:],REAL:] is non empty set

W is Relation-like [:X,Y:] -defined REAL -valued [.0,1.] -valued Function-like quasi_total Element of bool [:[:X,Y:],REAL:]

R is Relation-like [:Y,Z:] -defined REAL -valued [.0,1.] -valued Function-like quasi_total Element of bool [:[:Y,Z:],REAL:]

W (#) R is Relation-like [:X,Z:] -defined REAL -valued [.0,1.] -valued Function-like quasi_total Element of bool [:[:X,Z:],REAL:]

[:X,Z:] is non empty set

[:[:X,Z:],REAL:] is non empty set

bool [:[:X,Z:],REAL:] is non empty set

S is Element of X

T is Element of Z

(X,Z,(W (#) R),S,T) is V24() ext-real real Element of the carrier of ([.0,1.])

[S,T] is set

{S,T} is set

{S} is set

{{S,T},{S}} is set

(W (#) R) . [S,T] is set

{ ((X,Y,W,S,b

"\/" ( { ((X,Y,W,S,b

[S,T] is Element of [:X,Z:]

min (W,R,S,T) is Relation-like Y -defined REAL -valued [.0,1.] -valued Function-like quasi_total Element of bool [:Y,REAL:]

[:Y,REAL:] is non empty set

bool [:Y,REAL:] is non empty set

rng (min (W,R,S,T)) is V174() V175() V176() Element of bool REAL

upper_bound (rng (min (W,R,S,T))) is V24() ext-real real Element of REAL

w is V24() ext-real real Element of the carrier of ([.0,1.])

w is V24() ext-real real set

x is V24() ext-real real Element of the carrier of ([.0,1.])

([:X,Z:],(W (#) R),[S,T]) is V24() ext-real real Element of the carrier of ([.0,1.])

w is V24() ext-real real Element of the carrier of ([.0,1.])

w is Element of Y

(X,Y,W,S,w) is V24() ext-real real Element of the carrier of ([.0,1.])

[S,w] is set

{S,w} is set

{{S,w},{S}} is set

W . [S,w] is set

(Y,Z,R,w,T) is V24() ext-real real Element of the carrier of ([.0,1.])

[w,T] is set

{w,T} is set

{w} is set

{{w,T},{w}} is set

R . [w,T] is set

(X,Y,W,S,w) "/\" (Y,Z,R,w,T) is V24() ext-real real Element of the carrier of ([.0,1.])

(([.0,1.]),(X,Y,W,S,w),(Y,Z,R,w,T)) is V24() ext-real real Element of the carrier of ([.0,1.])

dom (min (W,R,S,T)) is Element of bool Y

bool Y is non empty set

x is V24() ext-real real Element of REAL

(Y,(min (W,R,S,T)),w) is V24() ext-real real Element of the carrier of ([.0,1.])

X is non empty set

Y is non empty set

[:X,Y:] is non empty set

[:[:X,Y:],REAL:] is non empty set

bool [:[:X,Y:],REAL:] is non empty set

Z is non empty set

[:Y,Z:] is non empty set

[:[:Y,Z:],REAL:] is non empty set

bool [:[:Y,Z:],REAL:] is non empty set

W is Relation-like [:X,Y:] -defined REAL -valued [.0,1.] -valued Function-like quasi_total Element of bool [:[:X,Y:],REAL:]

R is Relation-like [:Y,Z:] -defined REAL -valued [.0,1.] -valued Function-like quasi_total Element of bool [:[:Y,Z:],REAL:]

W (#) R is Relation-like [:X,Z:] -defined REAL -valued [.0,1.] -valued Function-like quasi_total Element of bool [:[:X,Z:],REAL:]

[:X,Z:] is non empty set

[:[:X,Z:],REAL:] is non empty set

bool [:[:X,Z:],REAL:] is non empty set

S is Element of X

T is Element of Z

(X,Z,(W (#) R),S,T) is V24() ext-real real Element of the carrier of ([.0,1.])

[S,T] is set

{S,T} is set

{S} is set

{{S,T},{S}} is set

(W (#) R) . [S,T] is set

x is V24() ext-real real Element of the carrier of ([.0,1.])

(X,Z,(W (#) R),S,T) "/\" x is V24() ext-real real Element of the carrier of ([.0,1.])

(([.0,1.]),(X,Z,(W (#) R),S,T),x) is V24() ext-real real Element of the carrier of ([.0,1.])

{ (((X,Y,W,S,b

"\/" ( { (((X,Y,W,S,b

{ ((X,Y,W,S,b

w is set

w is Element of Y

(X,Y,W,S,w) is V24() ext-real real Element of the carrier of ([.0,1.])

[S,w] is set

{S,w} is set

{{S,w},{S}} is set

W . [S,w] is set

(Y,Z,R,w,T) is V24() ext-real real Element of the carrier of ([.0,1.])

[w,T] is set

{w,T} is set

{w} is set

{{w,T},{w}} is set

R . [w,T] is set

(X,Y,W,S,w) "/\" (Y,Z,R,w,T) is V24() ext-real real Element of the carrier of ([.0,1.])

(([.0,1.]),(X,Y,W,S,w),(Y,Z,R,w,T)) is V24() ext-real real Element of the carrier of ([.0,1.])

{ (b

x is set

A is V24() ext-real real Element of the carrier of ([.0,1.])

A "/\" x is V24() ext-real real Element of the carrier of ([.0,1.])

(([.0,1.]),A,x) is V24() ext-real real Element of the carrier of ([.0,1.])

B is Element of Y

(X,Y,W,S,B) is V24() ext-real real Element of the carrier of ([.0,1.])

[S,B] is set

{S,B} is set

{{S,B},{S}} is set

W . [S,B] is set

(Y,Z,R,B,T) is V24() ext-real real Element of the carrier of ([.0,1.])

[B,T] is set

{B,T} is set

{B} is set

{{B,T},{B}} is set

R . [B,T] is set

(X,Y,W,S,B) "/\" (Y,Z,R,B,T) is V24() ext-real real Element of the carrier of ([.0,1.])

(([.0,1.]),(X,Y,W,S,B),(Y,Z,R,B,T)) is V24() ext-real real Element of the carrier of ([.0,1.])

A is Element of Y

(X,Y,W,S,A) is V24() ext-real real Element of the carrier of ([.0,1.])

[S,A] is set

{S,A} is set

{{S,A},{S}} is set

W . [S,A] is set

(Y,Z,R,A,T) is V24() ext-real real Element of the carrier of ([.0,1.])

[A,T] is set

{A,T} is set

{A} is set

{{A,T},{A}} is set

R . [A,T] is set

(X,Y,W,S,A) "/\" (Y,Z,R,A,T) is V24() ext-real real Element of the carrier of ([.0,1.])

(([.0,1.]),(X,Y,W,S,A),(Y,Z,R,A,T)) is V24() ext-real real Element of the carrier of ([.0,1.])

((X,Y,W,S,A) "/\" (Y,Z,R,A,T)) "/\" x is V24() ext-real real Element of the carrier of ([.0,1.])

(([.0,1.]),((X,Y,W,S,A) "/\" (Y,Z,R,A,T)),x) is V24() ext-real real Element of the carrier of ([.0,1.])

"\/" ( { ((X,Y,W,S,b

("\/" ( { ((X,Y,W,S,b

(([.0,1.]),("\/" ( { ((X,Y,W,S,b

"\/" ( { (b

X is non empty set

Y is non empty set

[:X,Y:] is non empty set

[:[:X,Y:],REAL:] is non empty set

bool [:[:X,Y:],REAL:] is non empty set

Z is non empty set

[:Y,Z:] is non empty set

[:[:Y,Z:],REAL:] is non empty set

bool [:[:Y,Z:],REAL:] is non empty set

W is Relation-like [:X,Y:] -defined REAL -valued [.0,1.] -valued Function-like quasi_total Element of bool [:[:X,Y:],REAL:]

R is Relation-like [:Y,Z:] -defined REAL -valued [.0,1.] -valued Function-like quasi_total Element of bool [:[:Y,Z:],REAL:]

W (#) R is Relation-like [:X,Z:] -defined REAL -valued [.0,1.] -valued Function-like quasi_total Element of bool [:[:X,Z:],REAL:]

[:X,Z:] is non empty set

[:[:X,Z:],REAL:] is non empty set

bool [:[:X,Z:],REAL:] is non empty set

S is Element of X

T is Element of Z

(X,Z,(W (#) R),S,T) is V24()