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
{ (b1 "/\" Z) where b1 is Element of the carrier of X : b1 in Y } is set
"\/" ( { (b1 "/\" Z) where b1 is Element of the carrier of X : b1 in Y } ,X) is Element of the carrier of X
{ (Z "/\" b1) where b1 is Element of the carrier of X : b1 in Y } is set
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)
F1() is non empty total reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded bounded RelStr
the carrier of F1() is non empty set
F2() is non empty set
F3() is non empty set
{ ("\/" ( { F4(b1,b2) where b2 is Element of F3() : P2[b2] } ,F1())) where b1 is Element of F2() : P1[b1] } is set
"\/" ( { ("\/" ( { F4(b1,b2) where b2 is Element of F3() : P2[b2] } ,F1())) where b1 is Element of F2() : P1[b1] } ,F1()) is Element of the carrier of F1()
{ F4(b1,b2) where b1 is Element of F2(), b2 is Element of F3() : ( P1[b1] & P2[b2] ) } is set
"\/" ( { F4(b1,b2) where b1 is Element of F2(), b2 is Element of F3() : ( P1[b1] & P2[b2] ) } ,F1()) is Element of the carrier of F1()
bool the carrier of F1() is non empty set
{ ("\/" (b1,F1())) where b1 is Element of bool the carrier of F1() : S1[b1] } is set
"\/" ( { ("\/" (b1,F1())) where b1 is Element of bool the carrier of F1() : S1[b1] } ,F1()) is Element of the carrier of F1()
{ b1 where b1 is Element of bool the carrier of F1() : S1[b1] } is set
union { b1 where b1 is Element of bool the carrier of F1() : S1[b1] } is set
"\/" ((union { b1 where b1 is Element of bool the carrier of F1() : S1[b1] } ),F1()) is Element of the carrier of F1()
X is set
Y is Element of F2()
Z is Element of F3()
F4(Y,Z) is Element of the carrier of F1()
{ F4(Y,b1) where b1 is Element of F3() : P2[b1] } is set
R is set
S is Element of F3()
F4(Y,S) is Element of the carrier of F1()
R is Element of bool the carrier of F1()
S is set
T is Element of F3()
F4(Y,T) is Element of the carrier of F1()
S is Element of F2()
X is set
Y is Element of F2()
{ F4(Y,b1) where b1 is Element of F3() : P2[b1] } is set
"\/" ( { F4(Y,b1) where b1 is Element of F3() : P2[b1] } ,F1()) is Element of the carrier of F1()
W is set
R is Element of F3()
F4(Y,R) is Element of the carrier of F1()
W is Element of bool the carrier of F1()
R is set
S is set
T is Element of F3()
F4(Y,T) is Element of the carrier of F1()
R is Element of F2()
Z is Element of bool the carrier of F1()
"\/" (Z,F1()) is Element of the carrier of F1()
W is Element of F2()
X is set
Y is Element of bool the carrier of F1()
"\/" (Y,F1()) is Element of the carrier of F1()
Z is Element of F2()
Z is Element of F2()
W is set
{ F4(Z,b1) where b1 is Element of F3() : P2[b1] } is set
R is Element of F3()
F4(Z,R) is Element of the carrier of F1()
R is Element of F3()
F4(Z,R) is Element of the carrier of F1()
X is set
Y is set
Z is Element of bool the carrier of F1()
W is Element of F2()
W is Element of F2()
R is Element of F3()
F4(W,R) is Element of the carrier of F1()
F1() is non empty total reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded bounded RelStr
the carrier of F1() is non empty set
F3() is non empty set
F2() is non empty set
{ ("\/" ( { F4(b2,b1) where b2 is Element of F2() : P1[b2] } ,F1())) where b1 is Element of F3() : P2[b1] } is set
"\/" ( { ("\/" ( { F4(b2,b1) where b2 is Element of F2() : P1[b2] } ,F1())) where b1 is Element of F3() : P2[b1] } ,F1()) is Element of the carrier of F1()
{ F4(b1,b2) where b1 is Element of F2(), b2 is Element of F3() : ( P1[b1] & P2[b2] ) } is set
"\/" ( { F4(b1,b2) where b1 is Element of F2(), b2 is Element of F3() : ( P1[b1] & P2[b2] ) } ,F1()) is Element of the carrier of F1()
bool the carrier of F1() is non empty set
{ ("\/" (b1,F1())) where b1 is Element of bool the carrier of F1() : S1[b1] } is set
"\/" ( { ("\/" (b1,F1())) where b1 is Element of bool the carrier of F1() : S1[b1] } ,F1()) is Element of the carrier of F1()
{ b1 where b1 is Element of bool the carrier of F1() : S1[b1] } is set
union { b1 where b1 is Element of bool the carrier of F1() : S1[b1] } is set
"\/" ((union { b1 where b1 is Element of bool the carrier of F1() : S1[b1] } ),F1()) is Element of the carrier of F1()
X is set
Y is Element of F2()
Z is Element of F3()
F4(Y,Z) is Element of the carrier of F1()
{ F4(b1,Z) where b1 is Element of F2() : P1[b1] } is set
R is set
S is Element of F2()
F4(S,Z) is Element of the carrier of F1()
R is Element of bool the carrier of F1()
S is set
T is Element of F2()
F4(T,Z) is Element of the carrier of F1()
S is Element of F3()
X is set
Y is Element of F3()
{ F4(b1,Y) where b1 is Element of F2() : P1[b1] } is set
"\/" ( { F4(b1,Y) where b1 is Element of F2() : P1[b1] } ,F1()) is Element of the carrier of F1()
W is set
R is Element of F2()
F4(R,Y) is Element of the carrier of F1()
W is Element of bool the carrier of F1()
R is set
S is set
T is Element of F2()
F4(T,Y) is Element of the carrier of F1()
R is Element of F3()
Z is Element of bool the carrier of F1()
"\/" (Z,F1()) is Element of the carrier of F1()
W is Element of F3()
X is set
Y is Element of bool the carrier of F1()
"\/" (Y,F1()) is Element of the carrier of F1()
Z is Element of F3()
Z is Element of F3()
W is set
{ F4(b1,Z) where b1 is Element of F2() : P1[b1] } is set
R is Element of F2()
F4(R,Z) is Element of the carrier of F1()
R is Element of F2()
F4(R,Z) is Element of the carrier of F1()
X is set
Y is set
Z is Element of bool the carrier of F1()
W is Element of F3()
W is Element of F3()
R is Element of F2()
F4(R,W) is Element of the carrier of F1()
F1() is non empty set
F2() is non empty set
{ F3(b1,b2) where b1 is Element of F1(), b2 is Element of F2() : P1[b1,b2] } is set
{ F4(b1,b2) where b1 is Element of F1(), b2 is Element of F2() : P1[b1,b2] } is set
Z is set
W is Element of F1()
R is Element of F2()
F3(W,R) is set
F4(W,R) is set
W is Element of F1()
R is Element of F2()
F4(W,R) is set
F3(W,R) is set
F1() is non empty set
F2() is non empty set
{ F3(b1,b2) where b1 is Element of F1(), b2 is Element of F2() : P1[b1,b2] } is set
{ F4(b1,b2) where b1 is Element of F1(), b2 is Element of F2() : P2[b1,b2] } is set
{ F4(b1,b2) where b1 is Element of F1(), b2 is Element of F2() : P1[b1,b2] } is set
F1() is non empty total reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded bounded RelStr
the carrier of F1() is non empty set
F2() is non empty set
F3() is non empty set
{ ("\/" ( { F4(b1,b2) where b2 is Element of F3() : P2[b2] } ,F1())) where b1 is Element of F2() : P1[b1] } is set
"\/" ( { ("\/" ( { F4(b1,b2) where b2 is Element of F3() : P2[b2] } ,F1())) where b1 is Element of F2() : P1[b1] } ,F1()) is Element of the carrier of F1()
{ ("\/" ( { F5(b2,b1) where b2 is Element of F2() : P1[b2] } ,F1())) where b1 is Element of F3() : P2[b1] } is set
"\/" ( { ("\/" ( { F5(b2,b1) where b2 is Element of F2() : P1[b2] } ,F1())) where b1 is Element of F3() : P2[b1] } ,F1()) is Element of the carrier of F1()
X is Element of F2()
Y is Element of F3()
Z is Element of F2()
W is Element of F3()
X is Element of F2()
Y is Element of F3()
F4(X,Y) is Element of the carrier of F1()
F5(X,Y) is Element of the carrier of F1()
{ F4(b1,b2) where b1 is Element of F2(), b2 is Element of F3() : S1[b1,b2] } is set
{ F5(b1,b2) where b1 is Element of F2(), b2 is Element of F3() : S1[b1,b2] } is set
{ F4(b1,b2) where b1 is Element of F2(), b2 is Element of F3() : ( P1[b1] & P2[b2] ) } is set
"\/" ( { F4(b1,b2) where b1 is Element of F2(), b2 is Element of F3() : ( P1[b1] & P2[b2] ) } ,F1()) is Element of the carrier of F1()
{ F5(b1,b2) where b1 is Element of F2(), b2 is Element of F3() : ( P1[b1] & P2[b2] ) } is set
"\/" ( { F5(b1,b2) where b1 is Element of F2(), b2 is Element of F3() : ( P1[b1] & P2[b2] ) } ,F1()) is Element of the carrier of F1()
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,b1) "/\" (Y,Z,R,b1,T)) where b1 is Element of Y : verum } is set
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,b1) "/\" (Y,Z,R,b1,T)) where b1 is Element of Y : verum } is set
"\/" ( { ((X,Y,W,S,b1) "/\" (Y,Z,R,b1,T)) where b1 is Element of Y : verum } ,([.0,1.])) is V24() ext-real real Element of the carrier of ([.0,1.])
[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,b1) "/\" (Y,Z,R,b1,T)) "/\" x) where b1 is Element of Y : verum } is set
"\/" ( { (((X,Y,W,S,b1) "/\" (Y,Z,R,b1,T)) "/\" x) where b1 is Element of Y : verum } ,([.0,1.])) is V24() ext-real real Element of the carrier of ([.0,1.])
{ ((X,Y,W,S,b1) "/\" (Y,Z,R,b1,T)) where b1 is Element of Y : verum } is 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,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.])
{ (b1 "/\" x) where b1 is V24() ext-real real Element of the carrier of ([.0,1.]) : b1 in { ((X,Y,W,S,b1) "/\" (Y,Z,R,b1,T)) where b2 is Element of Y : verum } } is set
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,b1) "/\" (Y,Z,R,b1,T)) where b1 is Element of Y : verum } ,([.0,1.])) is V24() ext-real real Element of the carrier of ([.0,1.])
("\/" ( { ((X,Y,W,S,b1) "/\" (Y,Z,R,b1,T)) where b1 is Element of Y : verum } ,([.0,1.]))) "/\" x is V24() ext-real real Element of the carrier of ([.0,1.])
(([.0,1.]),("\/" ( { ((X,Y,W,S,b1) "/\" (Y,Z,R,b1,T)) where b1 is Element of Y : verum } ,([.0,1.]))),x) is V24() ext-real real Element of the carrier of ([.0,1.])
"\/" ( { (b1 "/\" x) where b1 is V24() ext-real real Element of the carrier of ([.0,1.]) : b1 in { ((X,Y,W,S,b1) "/\" (Y,Z,R,b1,T)) where b2 is Element of Y : verum } } ,([.0,1.])) 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 "/\" (X,Z,(W (#) R),S,T) is V24() ext-real real Element of the carrier of ([.0,1.])
(([.0,1.]),x,(X,Z,(W (#) R),S,T)) is V24() ext-real real Element of the carrier of ([.0,1.])
{ ((x "/\" (X,Y,W,S,b1)) "/\" (Y,Z,R,b1,T)) where b1 is Element of Y : verum } is set
"\/" ( { ((x "/\" (X,Y,W,S,b1)) "/\" (Y,Z,R,b1,T)) where b1 is Element of Y : verum } ,([.0,1.])) is V24() ext-real real Element of the carrier of ([.0,1.])
{ (((X,Y,W,S,b1) "/\" (Y,Z,R,b1,T)) "/\" x) where b1 is Element of Y : verum } is set
x is set
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
x "/\" (X,Y,W,S,A) is V24() ext-real real Element of the carrier of ([.0,1.])
(([.0,1.]),x,(X,Y,W,S,A)) is V24() ext-real real Element of the carrier of ([.0,1.])
(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 "/\" (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 "/\" (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) 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.])
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 "/\" (X,Y,W,S,A) is V24() ext-real real Element of the carrier of ([.0,1.])
(([.0,1.]),x,(X,Y,W,S,A)) is V24() ext-real real Element of the carrier of ([.0,1.])
(x "/\" (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 "/\" (X,Y,W,S,A)),(Y,Z,R,A,T)) 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 non empty set
[:Z,W:] is non empty set
[:[:Z,W:],REAL:] is non empty set
bool [:[:Z,W:],REAL:] is non empty set
[:X,W:] is non empty set
R is Relation-like [:X,Y:] -defined REAL -valued [.0,1.] -valued Function-like quasi_total Element of bool [:[:X,Y:],REAL:]
S is Relation-like [:Y,Z:] -defined REAL -valued [.0,1.] -valued Function-like quasi_total Element of bool [:[:Y,Z:],REAL:]
R (#) S 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
T is Relation-like [:Z,W:] -defined REAL -valued [.0,1.] -valued Function-like quasi_total Element of bool [:[:Z,W:],REAL:]
(R (#) S) (#) T is Relation-like [:X,W:] -defined REAL -valued [.0,1.] -valued Function-like quasi_total Element of bool [:[:X,W:],REAL:]
[:[:X,W:],REAL:] is non empty set
bool [:[:X,W:],REAL:] is non empty set
S (#) T is Relation-like [:Y,W:] -defined REAL -valued [.0,1.] -valued Function-like quasi_total Element of bool [:[:Y,W:],REAL:]
[:Y,W:] is non empty set
[:[:Y,W:],REAL:] is non empty set
bool [:[:Y,W:],REAL:] is non empty set
R (#) (S (#) T) is Relation-like [:X,W:] -defined REAL -valued [.0,1.] -valued Function-like quasi_total Element of bool [:[:X,W:],REAL:]
x is set
w is set
((R (#) S) (#) T) . (x,w) is V24() ext-real real Element of REAL
[x,w] is set
{x,w} is set
{x} is set
{{x,w},{x}} is set
((R (#) S) (#) T) . [x,w] is set
(R (#) (S (#) T)) . (x,w) is V24() ext-real real Element of REAL
(R (#) (S (#) T)) . [x,w] is set
x is Element of X
w is Element of W
{ ("\/" ( { (((X,Y,R,x,b2) "/\" (Y,Z,S,b2,b1)) "/\" (Z,W,T,b1,w)) where b2 is Element of Y : verum } ,([.0,1.]))) where b1 is Element of Z : verum } is set
{ ((X,Z,(R (#) S),x,b1) "/\" (Z,W,T,b1,w)) where b1 is Element of Z : verum } is set
{ ("\/" ( { (((X,Y,R,x,b1) "/\" (Y,Z,S,b1,b2)) "/\" (Z,W,T,b2,w)) where b2 is Element of Z : verum } ,([.0,1.]))) where b1 is Element of Y : verum } is set
{ ((X,Y,R,x,b1) "/\" (Y,W,(S (#) T),b1,w)) where b1 is Element of Y : verum } is set
c is set
y is Element of Z
(Z,W,T,y,w) is V24() ext-real real Element of the carrier of ([.0,1.])
[y,w] is set
{y,w} is set
{y} is set
{{y,w},{y}} is set
T . [y,w] is set
{ (((X,Y,R,x,b1) "/\" (Y,Z,S,b1,y)) "/\" (Z,W,T,y,w)) where b1 is Element of Y : verum } is set
"\/" ( { (((X,Y,R,x,b1) "/\" (Y,Z,S,b1,y)) "/\" (Z,W,T,y,w)) where b1 is Element of Y : verum } ,([.0,1.])) is V24() ext-real real Element of the carrier of ([.0,1.])
(X,Z,(R (#) S),x,y) is V24() ext-real real Element of the carrier of ([.0,1.])
[x,y] is set
{x,y} is set
{x} is set
{{x,y},{x}} is set
(R (#) S) . [x,y] is set
(X,Z,(R (#) S),x,y) "/\" (Z,W,T,y,w) is V24() ext-real real Element of the carrier of ([.0,1.])
(([.0,1.]),(X,Z,(R (#) S),x,y),(Z,W,T,y,w)) is V24() ext-real real Element of the carrier of ([.0,1.])
y is Element of Z
(X,Z,(R (#) S),x,y) is V24() ext-real real Element of the carrier of ([.0,1.])
[x,y] is set
{x,y} is set
{{x,y},{x}} is set
(R (#) S) . [x,y] is set
(Z,W,T,y,w) is V24() ext-real real Element of the carrier of ([.0,1.])
[y,w] is set
{y,w} is set
{y} is set
{{y,w},{y}} is set
T . [y,w] is set
(X,Z,(R (#) S),x,y) "/\" (Z,W,T,y,w) is V24() ext-real real Element of the carrier of ([.0,1.])
(([.0,1.]),(X,Z,(R (#) S),x,y),(Z,W,T,y,w)) is V24() ext-real real Element of the carrier of ([.0,1.])
{ (((X,Y,R,x,b1) "/\" (Y,Z,S,b1,y)) "/\" (Z,W,T,y,w)) where b1 is Element of Y : verum } is set
"\/" ( { (((X,Y,R,x,b1) "/\" (Y,Z,S,b1,y)) "/\" (Z,W,T,y,w)) where b1 is Element of Y : verum } ,([.0,1.])) is V24() ext-real real Element of the carrier of ([.0,1.])
c is Element of Y
(X,Y,R,x,c) is V24() ext-real real Element of the carrier of ([.0,1.])
[x,c] is set
{x,c} is set
{x} is set
{{x,c},{x}} is set
R . [x,c] is set
y is Element of Z
(Y,Z,S,c,y) is V24() ext-real real Element of the carrier of ([.0,1.])
[c,y] is set
{c,y} is set
{c} is set
{{c,y},{c}} is set
S . [c,y] is set
(X,Y,R,x,c) "/\" (Y,Z,S,c,y) is V24() ext-real real Element of the carrier of ([.0,1.])
(([.0,1.]),(X,Y,R,x,c),(Y,Z,S,c,y)) is V24() ext-real real Element of the carrier of ([.0,1.])
(Z,W,T,y,w) is V24() ext-real real Element of the carrier of ([.0,1.])
[y,w] is set
{y,w} is set
{y} is set
{{y,w},{y}} is set
T . [y,w] is set
((X,Y,R,x,c) "/\" (Y,Z,S,c,y)) "/\" (Z,W,T,y,w) is V24() ext-real real Element of the carrier of ([.0,1.])
(([.0,1.]),((X,Y,R,x,c) "/\" (Y,Z,S,c,y)),(Z,W,T,y,w)) is V24() ext-real real Element of the carrier of ([.0,1.])
{ ("\/" ( { H1(b1,b2) where b2 is Element of Z : S1[b2] } ,([.0,1.]))) where b1 is Element of Y : S1[b1] } is set
"\/" ( { ("\/" ( { H1(b1,b2) where b2 is Element of Z : S1[b2] } ,([.0,1.]))) where b1 is Element of Y : S1[b1] } ,([.0,1.])) is V24() ext-real real Element of the carrier of ([.0,1.])
{ ("\/" ( { H1(b2,b1) where b2 is Element of Y : S1[b2] } ,([.0,1.]))) where b1 is Element of Z : S1[b1] } is set
"\/" ( { ("\/" ( { H1(b2,b1) where b2 is Element of Y : S1[b2] } ,([.0,1.]))) where b1 is Element of Z : S1[b1] } ,([.0,1.])) is V24() ext-real real Element of the carrier of ([.0,1.])
c is set
y is Element of Y
(X,Y,R,x,y) is V24() ext-real real Element of the carrier of ([.0,1.])
[x,y] is set
{x,y} is set
{x} is set
{{x,y},{x}} is set
R . [x,y] is set
{ (((X,Y,R,x,y) "/\" (Y,Z,S,y,b1)) "/\" (Z,W,T,b1,w)) where b1 is Element of Z : verum } is set
"\/" ( { (((X,Y,R,x,y) "/\" (Y,Z,S,y,b1)) "/\" (Z,W,T,b1,w)) where b1 is Element of Z : verum } ,([.0,1.])) is V24() ext-real real Element of the carrier of ([.0,1.])
(Y,W,(S (#) T),y,w) is V24() ext-real real Element of the carrier of ([.0,1.])
[y,w] is set
{y,w} is set
{y} is set
{{y,w},{y}} is set
(S (#) T) . [y,w] is set
(X,Y,R,x,y) "/\" (Y,W,(S (#) T),y,w) is V24() ext-real real Element of the carrier of ([.0,1.])
(([.0,1.]),(X,Y,R,x,y),(Y,W,(S (#) T),y,w)) is V24() ext-real real Element of the carrier of ([.0,1.])
y is Element of Y
(X,Y,R,x,y) is V24() ext-real real Element of the carrier of ([.0,1.])
[x,y] is set
{x,y} is set
{{x,y},{x}} is set
R . [x,y] is set
(Y,W,(S (#) T),y,w) is V24() ext-real real Element of the carrier of ([.0,1.])
[y,w] is set
{y,w} is set
{y} is set
{{y,w},{y}} is set
(S (#) T) . [y,w] is set
(X,Y,R,x,y) "/\" (Y,W,(S (#) T),y,w) is V24() ext-real real Element of the carrier of ([.0,1.])
(([.0,1.]),(X,Y,R,x,y),(Y,W,(S (#) T),y,w)) is V24() ext-real real Element of the carrier of ([.0,1.])
{ (((X,Y,R,x,y) "/\" (Y,Z,S,y,b1)) "/\" (Z,W,T,b1,w)) where b1 is Element of Z : verum } is set
"\/" ( { (((X,Y,R,x,y) "/\" (Y,Z,S,y,b1)) "/\" (Z,W,T,b1,w)) where b1 is Element of Z : verum } ,([.0,1.])) is V24() ext-real real Element of the carrier of ([.0,1.])
(X,W,((R (#) S) (#) T),x,w) is V24() ext-real real Element of the carrier of ([.0,1.])
[x,w] is set
{x,w} is set
{x} is set
{{x,w},{x}} is set
((R (#) S) (#) T) . [x,w] is set
"\/" ( { ((X,Z,(R (#) S),x,b1) "/\" (Z,W,T,b1,w)) where b1 is Element of Z : verum } ,([.0,1.])) is V24() ext-real real Element of the carrier of ([.0,1.])
(X,W,(R (#) (S (#) T)),x,w) is V24() ext-real real Element of the carrier of ([.0,1.])
(R (#) (S (#) T)) . [x,w] is set
"\/" ( { ((X,Y,R,x,b1) "/\" (Y,W,(S (#) T),b1,w)) where b1 is Element of Y : verum } ,([.0,1.])) is V24() ext-real real Element of the carrier of ([.0,1.])
dom ((R (#) S) (#) T) is Relation-like X -defined W -valued Element of bool [:X,W:]
bool [:X,W:] is non empty set
dom (R (#) (S (#) T)) is Relation-like X -defined W -valued Element of bool [:X,W:]