:: LFUZZY_1 semantic presentation

REAL is non empty V43() V44() V45() V49() V52() set
NAT is V43() V44() V45() V46() V47() V48() V49() Element of bool REAL
bool REAL is non empty set
COMPLEX is non empty V43() V49() V52() set
{} is empty Relation-like non-empty empty-yielding V43() V44() V45() V46() V47() V48() V49() set
the empty Relation-like non-empty empty-yielding V43() V44() V45() V46() V47() V48() V49() set is empty Relation-like non-empty empty-yielding V43() V44() V45() V46() V47() V48() V49() set
1 is non empty ordinal natural V24() ext-real positive non negative real V43() V44() V45() V46() V47() V48() V50() V51() Element of NAT
{{},1} is non empty set
omega is V43() V44() V45() V46() V47() V48() V49() set
bool omega is non empty set
bool NAT is non empty set
RAT is non empty V43() V44() V45() V46() V49() V52() set
INT is non empty V43() V44() V45() V46() V47() V49() V52() set
[:REAL,REAL:] is non empty Relation-like set
bool [:REAL,REAL:] is non empty set
K336() is non empty V92() L8()
the carrier of K336() is non empty set
K341() is non empty V92() V114() V115() V116() V118() V148() V149() V150() V151() V152() V153() L8()
K342() is non empty V92() V116() V118() V151() V152() V153() M13(K341())
K343() is non empty V92() V114() V116() V118() V151() V152() V153() V154() M16(K341(),K342())
K345() is non empty V92() V114() V116() V118() L8()
K346() is non empty V92() V114() V116() V118() V154() M13(K345())
0 is empty Relation-like non-empty empty-yielding ordinal natural V24() ext-real non positive non negative real V43() V44() V45() V46() V47() V48() V49() V50() V51() Element of NAT
[.0,1.] is non empty V43() V44() V45() Element of bool REAL
RealPoset [.0,1.] is non empty V183() reflexive transitive antisymmetric V191() with_suprema with_infima complete connected distributive Heyting real V278() L14()
the carrier of (RealPoset [.0,1.]) is non empty set
[:COMPLEX,COMPLEX:] is non empty Relation-like set
bool [:COMPLEX,COMPLEX:] is non empty set
[:COMPLEX,REAL:] is non empty Relation-like set
bool [:COMPLEX,REAL:] is non empty set
X is non empty set
[:X,REAL:] is non empty Relation-like set
bool [:X,REAL:] is non empty set
R is non empty Relation-like X -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:X,REAL:]
X is non empty set
R is non empty set
[:X,R:] is non empty Relation-like set
[:[:X,R:],REAL:] is non empty Relation-like set
bool [:[:X,R:],REAL:] is non empty set
S is non empty Relation-like [:X,R:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:[:X,R:],REAL:]
Q is non empty Relation-like [:X,R:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:[:X,R:],REAL:]
RP is Element of X
c is Element of R
S . (RP,c) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
[RP,c] is set
{RP,c} is non empty set
{RP} is non empty set
{{RP,c},{RP}} is non empty set
S . [RP,c] is set
Q . (RP,c) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
Q . [RP,c] is set
dom S is non empty Relation-like X -defined R -valued Element of bool [:X,R:]
bool [:X,R:] is non empty set
[RP,c] is Element of [:X,R:]
dom S is non empty Relation-like X -defined R -valued Element of bool [:X,R:]
bool [:X,R:] is non empty set
RP is set
S . RP is V24() ext-real real Element of REAL
Q . RP is V24() ext-real real Element of REAL
c is set
t is set
[c,t] is set
{c,t} is non empty set
{c} is non empty set
{{c,t},{c}} is non empty set
n is Element of X
i is Element of R
S . (n,i) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
[n,i] is set
{n,i} is non empty set
{n} is non empty set
{{n,i},{n}} is non empty set
S . [n,i] is set
Q . (n,i) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
Q . [n,i] is set
dom Q is non empty Relation-like X -defined R -valued Element of bool [:X,R:]
X is non empty set
[:X,REAL:] is non empty Relation-like set
bool [:X,REAL:] is non empty set
R is non empty Relation-like X -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:X,REAL:]
S is non empty Relation-like X -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:X,REAL:]
dom R is non empty Element of bool X
bool X is non empty set
Q is Element of X
R . Q is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
S . Q is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
dom S is non empty Element of bool X
X is non empty set
R is non empty set
[:X,R:] is non empty Relation-like set
[:[:X,R:],REAL:] is non empty Relation-like set
bool [:[:X,R:],REAL:] is non empty set
S is non empty Relation-like [:X,R:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:[:X,R:],REAL:]
Q is non empty Relation-like [:X,R:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:[:X,R:],REAL:]
dom S is non empty Relation-like X -defined R -valued Element of bool [:X,R:]
bool [:X,R:] is non empty set
RP is set
c is set
[RP,c] is set
{RP,c} is non empty set
{RP} is non empty set
{{RP,c},{RP}} is non empty set
S . (RP,c) is V24() ext-real real Element of REAL
S . [RP,c] is set
Q . (RP,c) is V24() ext-real real Element of REAL
Q . [RP,c] is set
t is Element of X
i is Element of R
S . (t,i) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
[t,i] is set
{t,i} is non empty set
{t} is non empty set
{{t,i},{t}} is non empty set
S . [t,i] is set
Q . (t,i) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
Q . [t,i] is set
dom Q is non empty Relation-like X -defined R -valued Element of bool [:X,R:]
X is non empty set
[:X,REAL:] is non empty Relation-like set
bool [:X,REAL:] is non empty set
R is non empty Relation-like X -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:X,REAL:]
S is non empty Relation-like X -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:X,REAL:]
Q is Element of X
R . Q is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
S . Q is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
X is non empty set
[:X,REAL:] is non empty Relation-like set
bool [:X,REAL:] is non empty set
R is non empty Relation-like X -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:X,REAL:]
X is non empty set
[:X,REAL:] is non empty Relation-like set
bool [:X,REAL:] is non empty set
R is non empty Relation-like X -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:X,REAL:]
S is non empty Relation-like X -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:X,REAL:]
Q is non empty Relation-like X -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:X,REAL:]
RP is Element of X
R . RP is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
Q . RP is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
S . RP is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
X is non empty set
R is non empty set
[:X,R:] is non empty Relation-like set
[:[:X,R:],REAL:] is non empty Relation-like set
bool [:[:X,R:],REAL:] is non empty set
S is non empty set
[:R,S:] is non empty Relation-like set
[:[:R,S:],REAL:] is non empty Relation-like set
bool [:[:R,S:],REAL:] is non empty set
Q is non empty Relation-like [:X,R:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:[:X,R:],REAL:]
RP is non empty Relation-like [:X,R:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:[:X,R:],REAL:]
c is non empty Relation-like [:R,S:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:[:R,S:],REAL:]
t is non empty Relation-like [:R,S:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:[:R,S:],REAL:]
Q (#) c is non empty Relation-like [:X,S:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:[:X,S:],REAL:]
[:X,S:] is non empty Relation-like set
[:[:X,S:],REAL:] is non empty Relation-like set
bool [:[:X,S:],REAL:] is non empty set
RP (#) t is non empty Relation-like [:X,S:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:[:X,S:],REAL:]
i is Element of [:X,S:]
(Q (#) c) . i is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
(RP (#) t) . i is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
n is set
j is set
[n,j] is set
{n,j} is non empty set
{n} is non empty set
{{n,j},{n}} is non empty set
f is set
[n,f] is set
{n,f} is non empty set
{{n,f},{n}} is non empty set
Q . [n,f] is V24() ext-real real Element of REAL
RP . [n,f] is V24() ext-real real Element of REAL
[f,j] is set
{f,j} is non empty set
{f} is non empty set
{{f,j},{f}} is non empty set
c . [f,j] is V24() ext-real real Element of REAL
t . [f,j] is V24() ext-real real Element of REAL
X is non empty set
[:X,REAL:] is non empty Relation-like set
bool [:X,REAL:] is non empty set
Q is non empty Relation-like X -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:X,REAL:]
RP is non empty Relation-like X -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:X,REAL:]
min (Q,RP) is non empty Relation-like X -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:X,REAL:]
min (RP,Q) is non empty Relation-like X -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:X,REAL:]
Q is non empty Relation-like X -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:X,REAL:]
RP is non empty Relation-like X -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:X,REAL:]
max (Q,RP) is non empty Relation-like X -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:X,REAL:]
max (RP,Q) is non empty Relation-like X -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:X,REAL:]
X is non empty set
[:X,REAL:] is non empty Relation-like set
bool [:X,REAL:] is non empty set
R is non empty Relation-like X -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:X,REAL:]
S is non empty Relation-like X -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:X,REAL:]
(X,R,S) is non empty Relation-like X -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:X,REAL:]
Q is Element of X
(X,R,S) . Q is V24() ext-real real Element of REAL
R . Q is V24() ext-real real Element of REAL
(X,R,S) . Q is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
R . Q is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
S . Q is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
min ((R . Q),(S . Q)) is V24() ext-real real set
X is non empty set
[:X,REAL:] is non empty Relation-like set
bool [:X,REAL:] is non empty set
R is non empty Relation-like X -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:X,REAL:]
S is non empty Relation-like X -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:X,REAL:]
(X,R,S) is non empty Relation-like X -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:X,REAL:]
Q is Element of X
R . Q is V24() ext-real real Element of REAL
(X,R,S) . Q is V24() ext-real real Element of REAL
(X,R,S) . Q is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
R . Q is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
S . Q is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
max ((R . Q),(S . Q)) is V24() ext-real real set
X is non empty set
[:X,X:] is non empty Relation-like set
[:[:X,X:],REAL:] is non empty Relation-like set
bool [:[:X,X:],REAL:] is non empty set
X is non empty set
[:X,X:] is non empty Relation-like set
[:[:X,X:],REAL:] is non empty Relation-like set
bool [:[:X,X:],REAL:] is non empty set
R is non empty Relation-like [:X,X:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:[:X,X:],REAL:]
Imf (X,X) is non empty Relation-like [:X,X:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:[:X,X:],REAL:]
S is Element of X
R . (S,S) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
[S,S] is set
{S,S} is non empty set
{S} is non empty set
{{S,S},{S}} is non empty set
R . [S,S] is set
(Imf (X,X)) . (S,S) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
(Imf (X,X)) . [S,S] is set
S is Element of X
Q is Element of X
(Imf (X,X)) . (S,Q) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
[S,Q] is set
{S,Q} is non empty set
{S} is non empty set
{{S,Q},{S}} is non empty set
(Imf (X,X)) . [S,Q] is set
R . (S,Q) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
R . [S,Q] is set
X is non empty set
[:X,X:] is non empty Relation-like set
[:[:X,X:],REAL:] is non empty Relation-like set
bool [:[:X,X:],REAL:] is non empty set
X is non empty set
[:X,X:] is non empty Relation-like set
[:[:X,X:],REAL:] is non empty Relation-like set
bool [:[:X,X:],REAL:] is non empty set
R is non empty Relation-like [:X,X:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:[:X,X:],REAL:]
converse R is non empty Relation-like [:X,X:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:[:X,X:],REAL:]
S is Element of X
Q is Element of X
R . (S,Q) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
[S,Q] is set
{S,Q} is non empty set
{S} is non empty set
{{S,Q},{S}} is non empty set
R . [S,Q] is set
R . (Q,S) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
[Q,S] is set
{Q,S} is non empty set
{Q} is non empty set
{{Q,S},{Q}} is non empty set
R . [Q,S] is set
dom R is non empty Relation-like X -defined X -valued Element of bool [:X,X:]
bool [:X,X:] is non empty set
S is set
Q is set
[S,Q] is set
{S,Q} is non empty set
{S} is non empty set
{{S,Q},{S}} is non empty set
(converse R) . (S,Q) is V24() ext-real real Element of REAL
(converse R) . [S,Q] is set
R . (S,Q) is V24() ext-real real Element of REAL
R . [S,Q] is set
RP is Element of X
c is Element of X
R . (RP,c) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
[RP,c] is set
{RP,c} is non empty set
{RP} is non empty set
{{RP,c},{RP}} is non empty set
R . [RP,c] is set
R . (c,RP) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
[c,RP] is set
{c,RP} is non empty set
{c} is non empty set
{{c,RP},{c}} is non empty set
R . [c,RP] is set
dom (converse R) is non empty Relation-like X -defined X -valued Element of bool [:X,X:]
X is non empty set
[:X,X:] is non empty Relation-like set
[:[:X,X:],REAL:] is non empty Relation-like set
bool [:[:X,X:],REAL:] is non empty set
X is non empty set
R is non empty set
[:X,R:] is non empty Relation-like set
[:[:X,R:],REAL:] is non empty Relation-like set
bool [:[:X,R:],REAL:] is non empty set
S is non empty set
[:R,S:] is non empty Relation-like set
[:[:R,S:],REAL:] is non empty Relation-like set
bool [:[:R,S:],REAL:] is non empty set
Q is non empty Relation-like [:X,R:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:[:X,R:],REAL:]
RP is non empty Relation-like [:R,S:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:[:R,S:],REAL:]
c is Element of X
t is Element of S
min (Q,RP,c,t) is non empty Relation-like R -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:R,REAL:]
[:R,REAL:] is non empty Relation-like set
bool [:R,REAL:] is non empty set
rng (min (Q,RP,c,t)) is non empty V43() V44() V45() Element of bool REAL
{ ((Q . [c,b₁]) "/\" (RP . [b₁,t])) where b₁ is Element of R : verum } is set
dom (min (Q,RP,c,t)) is non empty Element of bool R
bool R is non empty set
[:(dom (min (Q,RP,c,t))),(rng (min (Q,RP,c,t))):] is non empty Relation-like set
bool [:(dom (min (Q,RP,c,t))),(rng (min (Q,RP,c,t))):] is non empty set
n is set
j is Element of R
[c,j] is Element of [:X,R:]
{c,j} is non empty set
{c} is non empty set
{{c,j},{c}} is non empty set
Q . [c,j] is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
[j,t] is Element of [:R,S:]
{j,t} is non empty set
{j} is non empty set
{{j,t},{j}} is non empty set
RP . [j,t] is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
(Q . [c,j]) "/\" (RP . [j,t]) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
min ((Q . [c,j]),(RP . [j,t])) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
(min (Q,RP,c,t)) . j is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
j is Element of R
(min (Q,RP,c,t)) . j is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
[c,j] is Element of [:X,R:]
{c,j} is non empty set
{{c,j},{c}} is non empty set
Q . [c,j] is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
[j,t] is Element of [:R,S:]
{j,t} is non empty set
{j} is non empty set
{{j,t},{j}} is non empty set
RP . [j,t] is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
(Q . [c,j]) "/\" (RP . [j,t]) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
min ((Q . [c,j]),(RP . [j,t])) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
X is non empty set
[:X,X:] is non empty Relation-like set
[:[:X,X:],REAL:] is non empty Relation-like set
bool [:[:X,X:],REAL:] is non empty set
R is non empty Relation-like [:X,X:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:[:X,X:],REAL:]
R (#) R is non empty Relation-like [:X,X:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:[:X,X:],REAL:]
S is Element of X
Q is Element of X
[S,Q] is Element of [:X,X:]
{S,Q} is non empty set
{S} is non empty set
{{S,Q},{S}} is non empty set
R . [S,Q] is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
RP is Element of X
[Q,RP] is Element of [:X,X:]
{Q,RP} is non empty set
{Q} is non empty set
{{Q,RP},{Q}} is non empty set
R . [Q,RP] is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
(R . [S,Q]) "/\" (R . [Q,RP]) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
min ((R . [S,Q]),(R . [Q,RP])) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
[S,RP] is Element of [:X,X:]
{S,RP} is non empty set
{{S,RP},{S}} is non empty set
R . [S,RP] is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
R . (S,Q) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
[S,Q] is set
R . [S,Q] is set
R . (Q,RP) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
[Q,RP] is set
R . [Q,RP] is set
(R . (S,Q)) "/\" (R . (Q,RP)) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
min ((R . (S,Q)),(R . (Q,RP))) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
{ ((R . (S,b₁)) "/\" (R . (b₁,RP))) where b₁ is Element of X : verum } is set
"\/" ( { ((R . (S,b₁)) "/\" (R . (b₁,RP))) where b₁ is Element of X : verum } ,(RealPoset [.0,1.])) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
(R (#) R) . (S,RP) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
[S,RP] is set
(R (#) R) . [S,RP] is set
R . (S,RP) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
R . [S,RP] is set
S is Element of X
Q is Element of X
(R (#) R) . (S,Q) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
[S,Q] is set
{S,Q} is non empty set
{S} is non empty set
{{S,Q},{S}} is non empty set
(R (#) R) . [S,Q] is set
R . (S,Q) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
R . [S,Q] is set
min (R,R,S,Q) is non empty Relation-like X -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:X,REAL:]
[:X,REAL:] is non empty Relation-like set
bool [:X,REAL:] is non empty set
rng (min (R,R,S,Q)) is non empty V43() V44() V45() Element of bool REAL
[S,Q] is Element of [:X,X:]
R . [S,Q] is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
c is V24() ext-real real set
{ ((R . [S,b₁]) "/\" (R . [b₁,Q])) where b₁ is Element of X : verum } is set
t is Element of X
[S,t] is Element of [:X,X:]
{S,t} is non empty set
{{S,t},{S}} is non empty set
R . [S,t] is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
[t,Q] is Element of [:X,X:]
{t,Q} is non empty set
{t} is non empty set
{{t,Q},{t}} is non empty set
R . [t,Q] is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
(R . [S,t]) "/\" (R . [t,Q]) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
min ((R . [S,t]),(R . [t,Q])) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
upper_bound (rng (min (R,R,S,Q))) is V24() ext-real real Element of REAL
X is non empty set
[:X,X:] is non empty Relation-like set
[:[:X,X:],REAL:] is non empty Relation-like set
bool [:[:X,X:],REAL:] is non empty set
X is non empty set
Imf (X,X) is non empty Relation-like [:X,X:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:[:X,X:],REAL:]
[:X,X:] is non empty Relation-like set
[:[:X,X:],REAL:] is non empty Relation-like set
bool [:[:X,X:],REAL:] is non empty set
R is Element of X
S is Element of X
(Imf (X,X)) . (R,S) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
[R,S] is set
{R,S} is non empty set
{R} is non empty set
{{R,S},{R}} is non empty set
(Imf (X,X)) . [R,S] is set
(Imf (X,X)) . (S,R) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
[S,R] is set
{S,R} is non empty set
{S} is non empty set
{{S,R},{S}} is non empty set
(Imf (X,X)) . [S,R] is set
R is Element of X
S is Element of X
[R,S] is Element of [:X,X:]
{R,S} is non empty set
{R} is non empty set
{{R,S},{R}} is non empty set
(Imf (X,X)) . [R,S] is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
Q is Element of X
[S,Q] is Element of [:X,X:]
{S,Q} is non empty set
{S} is non empty set
{{S,Q},{S}} is non empty set
(Imf (X,X)) . [S,Q] is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
((Imf (X,X)) . [R,S]) "/\" ((Imf (X,X)) . [S,Q]) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
min (((Imf (X,X)) . [R,S]),((Imf (X,X)) . [S,Q])) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
[R,Q] is Element of [:X,X:]
{R,Q} is non empty set
{{R,Q},{R}} is non empty set
(Imf (X,X)) . [R,Q] is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
(Imf (X,X)) . (R,S) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
[R,S] is set
(Imf (X,X)) . [R,S] is set
(Imf (X,X)) . (S,Q) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
[S,Q] is set
(Imf (X,X)) . [S,Q] is set
min (((Imf (X,X)) . (R,S)),((Imf (X,X)) . (S,Q))) is V24() ext-real real set
((Imf (X,X)) . (R,S)) "/\" ((Imf (X,X)) . (S,Q)) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
min (((Imf (X,X)) . (R,S)),((Imf (X,X)) . (S,Q))) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
(Imf (X,X)) . (R,Q) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
[R,Q] is set
(Imf (X,X)) . [R,Q] is set
(Imf (X,X)) . (R,S) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
[R,S] is set
(Imf (X,X)) . [R,S] is set
(Imf (X,X)) . (S,Q) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
[S,Q] is set
(Imf (X,X)) . [S,Q] is set
min (((Imf (X,X)) . (R,S)),((Imf (X,X)) . (S,Q))) is V24() ext-real real set
min (((Imf (X,X)) . (R,S)),0) is V24() ext-real real set
min (0,0) is ordinal natural V24() ext-real non negative real set
((Imf (X,X)) . (R,S)) "/\" ((Imf (X,X)) . (S,Q)) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
min (((Imf (X,X)) . (R,S)),((Imf (X,X)) . (S,Q))) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
(Imf (X,X)) . (R,Q) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
[R,Q] is set
(Imf (X,X)) . [R,Q] is set
(Imf (X,X)) . (R,S) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
[R,S] is set
(Imf (X,X)) . [R,S] is set
(Imf (X,X)) . (S,Q) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
[S,Q] is set
(Imf (X,X)) . [S,Q] is set
min (((Imf (X,X)) . (R,S)),((Imf (X,X)) . (S,Q))) is V24() ext-real real set
min (((Imf (X,X)) . (R,S)),0) is V24() ext-real real set
min (1,0) is ordinal natural V24() ext-real non negative real set
((Imf (X,X)) . (R,S)) "/\" ((Imf (X,X)) . (S,Q)) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
min (((Imf (X,X)) . (R,S)),((Imf (X,X)) . (S,Q))) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
(Imf (X,X)) . (R,Q) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
[R,Q] is set
(Imf (X,X)) . [R,Q] is set
(Imf (X,X)) . (R,S) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
[R,S] is set
(Imf (X,X)) . [R,S] is set
(Imf (X,X)) . (S,Q) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
[S,Q] is set
(Imf (X,X)) . [S,Q] is set
min (((Imf (X,X)) . (R,S)),((Imf (X,X)) . (S,Q))) is V24() ext-real real set
min (((Imf (X,X)) . (R,S)),1) is V24() ext-real real set
min (0,1) is ordinal natural V24() ext-real non negative real set
((Imf (X,X)) . (R,S)) "/\" ((Imf (X,X)) . (S,Q)) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
min (((Imf (X,X)) . (R,S)),((Imf (X,X)) . (S,Q))) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
(Imf (X,X)) . (R,Q) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
[R,Q] is set
(Imf (X,X)) . [R,Q] is set
(Imf (X,X)) . (R,S) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
[R,S] is set
(Imf (X,X)) . [R,S] is set
(Imf (X,X)) . (S,Q) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
[S,Q] is set
(Imf (X,X)) . [S,Q] is set
min (((Imf (X,X)) . (R,S)),((Imf (X,X)) . (S,Q))) is V24() ext-real real set
min (((Imf (X,X)) . (R,S)),0) is V24() ext-real real set
min (0,0) is ordinal natural V24() ext-real non negative real set
((Imf (X,X)) . (R,S)) "/\" ((Imf (X,X)) . (S,Q)) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
min (((Imf (X,X)) . (R,S)),((Imf (X,X)) . (S,Q))) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
(Imf (X,X)) . (R,Q) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
[R,Q] is set
(Imf (X,X)) . [R,Q] is set
R is Element of X
S is Element of X
(Imf (X,X)) . (R,S) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
[R,S] is set
{R,S} is non empty set
{R} is non empty set
{{R,S},{R}} is non empty set
(Imf (X,X)) . [R,S] is set
(Imf (X,X)) . (S,R) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
[S,R] is set
{S,R} is non empty set
{S} is non empty set
{{S,R},{S}} is non empty set
(Imf (X,X)) . [S,R] is set
X is non empty set
[:X,X:] is non empty Relation-like set
[:[:X,X:],REAL:] is non empty Relation-like set
bool [:[:X,X:],REAL:] is non empty set
Imf (X,X) is non empty Relation-like [:X,X:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued (X) (X) (X) (X) Element of bool [:[:X,X:],REAL:]
X is non empty set
[:X,X:] is non empty Relation-like set
[:[:X,X:],REAL:] is non empty Relation-like set
bool [:[:X,X:],REAL:] is non empty set
R is non empty Relation-like [:X,X:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:[:X,X:],REAL:]
S is non empty Relation-like [:X,X:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:[:X,X:],REAL:]
([:X,X:],R,S) is non empty Relation-like [:X,X:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:[:X,X:],REAL:]
converse ([:X,X:],R,S) is non empty Relation-like [:X,X:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:[:X,X:],REAL:]
converse R is non empty Relation-like [:X,X:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:[:X,X:],REAL:]
converse S is non empty Relation-like [:X,X:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:[:X,X:],REAL:]
X is non empty set
[:X,X:] is non empty Relation-like set
[:[:X,X:],REAL:] is non empty Relation-like set
bool [:[:X,X:],REAL:] is non empty set
R is non empty Relation-like [:X,X:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:[:X,X:],REAL:]
S is non empty Relation-like [:X,X:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:[:X,X:],REAL:]
([:X,X:],R,S) is non empty Relation-like [:X,X:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:[:X,X:],REAL:]
converse ([:X,X:],R,S) is non empty Relation-like [:X,X:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:[:X,X:],REAL:]
converse R is non empty Relation-like [:X,X:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:[:X,X:],REAL:]
converse S is non empty Relation-like [:X,X:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:[:X,X:],REAL:]
X is non empty set
[:X,X:] is non empty Relation-like set
[:[:X,X:],REAL:] is non empty Relation-like set
bool [:[:X,X:],REAL:] is non empty set
R is non empty Relation-like [:X,X:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued (X) Element of bool [:[:X,X:],REAL:]
S is non empty Relation-like [:X,X:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued (X) Element of bool [:[:X,X:],REAL:]
([:X,X:],R,S) is non empty Relation-like [:X,X:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:[:X,X:],REAL:]
converse ([:X,X:],R,S) is non empty Relation-like [:X,X:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:[:X,X:],REAL:]
([:X,X:],R,S) is non empty Relation-like [:X,X:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:[:X,X:],REAL:]
converse ([:X,X:],R,S) is non empty Relation-like [:X,X:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:[:X,X:],REAL:]
X is non empty set
[:X,X:] is non empty Relation-like set
[:[:X,X:],REAL:] is non empty Relation-like set
bool [:[:X,X:],REAL:] is non empty set
R is non empty Relation-like [:X,X:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:[:X,X:],REAL:]
S is non empty Relation-like [:X,X:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:[:X,X:],REAL:]
([:X,X:],R,S) is non empty Relation-like [:X,X:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:[:X,X:],REAL:]
([:X,X:],R,S) (#) ([:X,X:],R,S) is non empty Relation-like [:X,X:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:[:X,X:],REAL:]
Q is Element of X
RP is Element of X
(([:X,X:],R,S) (#) ([:X,X:],R,S)) . (Q,RP) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
[Q,RP] is set
{Q,RP} is non empty set
{Q} is non empty set
{{Q,RP},{Q}} is non empty set
(([:X,X:],R,S) (#) ([:X,X:],R,S)) . [Q,RP] is set
([:X,X:],R,S) . (Q,RP) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
([:X,X:],R,S) . [Q,RP] is set
R (#) S is non empty Relation-like [:X,X:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:[:X,X:],REAL:]
S (#) S is non empty Relation-like [:X,X:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:[:X,X:],REAL:]
([:X,X:],(R (#) S),(S (#) S)) is non empty Relation-like [:X,X:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:[:X,X:],REAL:]
[Q,RP] is Element of [:X,X:]
([:X,X:],(R (#) S),(S (#) S)) . [Q,RP] is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
(S (#) S) . [Q,RP] is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
(R (#) S) . [Q,RP] is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
min (((S (#) S) . [Q,RP]),((R (#) S) . [Q,RP])) is V24() ext-real real set
(S (#) S) . (Q,RP) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
(S (#) S) . [Q,RP] is set
S . (Q,RP) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
S . [Q,RP] is set
S . [Q,RP] is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
R (#) R is non empty Relation-like [:X,X:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:[:X,X:],REAL:]
S (#) R is non empty Relation-like [:X,X:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:[:X,X:],REAL:]
([:X,X:],(R (#) R),(S (#) R)) is non empty Relation-like [:X,X:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:[:X,X:],REAL:]
([:X,X:],(R (#) R),(S (#) R)) . [Q,RP] is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
(R (#) R) . [Q,RP] is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
(S (#) R) . [Q,RP] is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
min (((R (#) R) . [Q,RP]),((S (#) R) . [Q,RP])) is V24() ext-real real set
(R (#) R) . (Q,RP) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
(R (#) R) . [Q,RP] is set
R . (Q,RP) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
R . [Q,RP] is set
R . [Q,RP] is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
min ((([:X,X:],(R (#) R),(S (#) R)) . [Q,RP]),(([:X,X:],(R (#) S),(S (#) S)) . [Q,RP])) is V24() ext-real real set
min ((R . [Q,RP]),(S . [Q,RP])) is V24() ext-real real set
([:X,X:],R,S) (#) R is non empty Relation-like [:X,X:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:[:X,X:],REAL:]
([:X,X:],R,S) (#) S is non empty Relation-like [:X,X:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:[:X,X:],REAL:]
([:X,X:],(([:X,X:],R,S) (#) R),(([:X,X:],R,S) (#) S)) is non empty Relation-like [:X,X:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:[:X,X:],REAL:]
(([:X,X:],R,S) (#) ([:X,X:],R,S)) . [Q,RP] is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
([:X,X:],(([:X,X:],R,S) (#) R),(([:X,X:],R,S) (#) S)) . [Q,RP] is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
(([:X,X:],R,S) (#) S) . [Q,RP] is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
(([:X,X:],R,S) (#) R) . [Q,RP] is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
min (((([:X,X:],R,S) (#) R) . [Q,RP]),((([:X,X:],R,S) (#) S) . [Q,RP])) is V24() ext-real real set
X is non empty set
[:X,X:] is non empty Relation-like set
[:[:X,X:],REAL:] is non empty Relation-like set
bool [:[:X,X:],REAL:] is non empty set
R is non empty Relation-like [:X,X:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued (X) Element of bool [:[:X,X:],REAL:]
S is non empty Relation-like [:X,X:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued (X) Element of bool [:[:X,X:],REAL:]
([:X,X:],R,S) is non empty Relation-like [:X,X:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:[:X,X:],REAL:]
([:X,X:],R,S) (#) ([:X,X:],R,S) is non empty Relation-like [:X,X:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:[:X,X:],REAL:]
X is set
R is non empty set
chi (X,R) is Relation-like [.0,1.] -valued Function-like set
[:R,REAL:] is non empty Relation-like set
bool [:R,REAL:] is non empty set
chi (X,R) is Relation-like R -defined REAL -valued [.0,1.] -valued Function-like Element of bool [:R,REAL:]
dom (chi (X,R)) is Element of bool R
bool R is non empty set
X is non empty set
[:X,X:] is non empty Relation-like set
bool [:X,X:] is non empty set
R is Relation-like X -defined X -valued Element of bool [:X,X:]
(R,[:X,X:]) is non empty Relation-like [:X,X:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:[:X,X:],REAL:]
[:[:X,X:],REAL:] is non empty Relation-like set
bool [:[:X,X:],REAL:] is non empty set
S is Element of X
(R,[:X,X:]) . (S,S) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
[S,S] is set
{S,S} is non empty set
{S} is non empty set
{{S,S},{S}} is non empty set
(R,[:X,X:]) . [S,S] is set
[S,S] is Element of [:X,X:]
X is non empty set
[:X,X:] is non empty Relation-like set
bool [:X,X:] is non empty set
R is Relation-like X -defined X -valued Element of bool [:X,X:]
(R,[:X,X:]) is non empty Relation-like [:X,X:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:[:X,X:],REAL:]
[:[:X,X:],REAL:] is non empty Relation-like set
bool [:[:X,X:],REAL:] is non empty set
field R is set
S is Element of X
Q is Element of X
(R,[:X,X:]) . (S,Q) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
[S,Q] is set
{S,Q} is non empty set
{S} is non empty set
{{S,Q},{S}} is non empty set
(R,[:X,X:]) . [S,Q] is set
(R,[:X,X:]) . (Q,S) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
[Q,S] is set
{Q,S} is non empty set
{Q} is non empty set
{{Q,S},{Q}} is non empty set
(R,[:X,X:]) . [Q,S] is set
[S,Q] is Element of [:X,X:]
[Q,S] is Element of [:X,X:]
X is non empty set
[:X,X:] is non empty Relation-like set
bool [:X,X:] is non empty set
R is Relation-like X -defined X -valued Element of bool [:X,X:]
(R,[:X,X:]) is non empty Relation-like [:X,X:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:[:X,X:],REAL:]
[:[:X,X:],REAL:] is non empty Relation-like set
bool [:[:X,X:],REAL:] is non empty set
field R is set
S is Element of X
Q is Element of X
(R,[:X,X:]) . (S,Q) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
[S,Q] is set
{S,Q} is non empty set
{S} is non empty set
{{S,Q},{S}} is non empty set
(R,[:X,X:]) . [S,Q] is set
(R,[:X,X:]) . (Q,S) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
[Q,S] is set
{Q,S} is non empty set
{Q} is non empty set
{{Q,S},{Q}} is non empty set
(R,[:X,X:]) . [Q,S] is set
[S,Q] is Element of [:X,X:]
[Q,S] is Element of [:X,X:]
(R,[:X,X:]) . [S,Q] is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
(R,[:X,X:]) . [S,Q] is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
X is non empty set
[:X,X:] is non empty Relation-like set
bool [:X,X:] is non empty set
R is Relation-like X -defined X -valued Element of bool [:X,X:]
(R,[:X,X:]) is non empty Relation-like [:X,X:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:[:X,X:],REAL:]
[:[:X,X:],REAL:] is non empty Relation-like set
bool [:[:X,X:],REAL:] is non empty set
S is Element of X
Q is Element of X
[S,Q] is Element of [:X,X:]
{S,Q} is non empty set
{S} is non empty set
{{S,Q},{S}} is non empty set
(R,[:X,X:]) . [S,Q] is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
RP is Element of X
[Q,RP] is Element of [:X,X:]
{Q,RP} is non empty set
{Q} is non empty set
{{Q,RP},{Q}} is non empty set
(R,[:X,X:]) . [Q,RP] is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
((R,[:X,X:]) . [S,Q]) "/\" ((R,[:X,X:]) . [Q,RP]) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
min (((R,[:X,X:]) . [S,Q]),((R,[:X,X:]) . [Q,RP])) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
[S,RP] is Element of [:X,X:]
{S,RP} is non empty set
{{S,RP},{S}} is non empty set
(R,[:X,X:]) . [S,RP] is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
field R is set
min (1,((R,[:X,X:]) . [Q,RP])) is V24() ext-real real set
min (1,1) is ordinal natural V24() ext-real non negative real set
min (1,((R,[:X,X:]) . [Q,RP])) is V24() ext-real real set
min (1,0) is ordinal natural V24() ext-real non negative real set
min (0,((R,[:X,X:]) . [Q,RP])) is V24() ext-real real set
min (0,1) is ordinal natural V24() ext-real non negative real set
min (0,((R,[:X,X:]) . [Q,RP])) is V24() ext-real real set
min (0,0) is ordinal natural V24() ext-real non negative real set
X is non empty set
Zmf (X,X) is non empty Relation-like [:X,X:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:[:X,X:],REAL:]
[:X,X:] is non empty Relation-like set
[:[:X,X:],REAL:] is non empty Relation-like set
bool [:[:X,X:],REAL:] is non empty set
R is Element of X
S is Element of X
(Zmf (X,X)) . (R,S) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
[R,S] is set
{R,S} is non empty set
{R} is non empty set
{{R,S},{R}} is non empty set
(Zmf (X,X)) . [R,S] is set
(Zmf (X,X)) . (S,R) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
[S,R] is set
{S,R} is non empty set
{S} is non empty set
{{S,R},{S}} is non empty set
(Zmf (X,X)) . [S,R] is set
[R,S] is Element of [:X,X:]
(Zmf (X,X)) . [R,S] is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
[S,R] is Element of [:X,X:]
(Zmf (X,X)) . [S,R] is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
R is Element of X
S is Element of X
(Zmf (X,X)) . (R,S) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
[R,S] is set
{R,S} is non empty set
{R} is non empty set
{{R,S},{R}} is non empty set
(Zmf (X,X)) . [R,S] is set
(Zmf (X,X)) . (S,R) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
[S,R] is set
{S,R} is non empty set
{S} is non empty set
{{S,R},{S}} is non empty set
(Zmf (X,X)) . [S,R] is set
[R,S] is Element of [:X,X:]
(Zmf (X,X)) . [R,S] is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
R is Element of X
S is Element of X
[R,S] is Element of [:X,X:]
{R,S} is non empty set
{R} is non empty set
{{R,S},{R}} is non empty set
(Zmf (X,X)) . [R,S] is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
Q is Element of X
[S,Q] is Element of [:X,X:]
{S,Q} is non empty set
{S} is non empty set
{{S,Q},{S}} is non empty set
(Zmf (X,X)) . [S,Q] is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
((Zmf (X,X)) . [R,S]) "/\" ((Zmf (X,X)) . [S,Q]) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
min (((Zmf (X,X)) . [R,S]),((Zmf (X,X)) . [S,Q])) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
[R,Q] is Element of [:X,X:]
{R,Q} is non empty set
{{R,Q},{R}} is non empty set
(Zmf (X,X)) . [R,Q] is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
min (0,((Zmf (X,X)) . [S,Q])) is V24() ext-real real set
min (0,0) is ordinal natural V24() ext-real non negative real set
X is non empty set
Umf (X,X) is non empty Relation-like [:X,X:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:[:X,X:],REAL:]
[:X,X:] is non empty Relation-like set
[:[:X,X:],REAL:] is non empty Relation-like set
bool [:[:X,X:],REAL:] is non empty set
R is Element of X
S is Element of X
(Umf (X,X)) . (R,S) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
[R,S] is set
{R,S} is non empty set
{R} is non empty set
{{R,S},{R}} is non empty set
(Umf (X,X)) . [R,S] is set
(Umf (X,X)) . (S,R) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
[S,R] is set
{S,R} is non empty set
{S} is non empty set
{{S,R},{S}} is non empty set
(Umf (X,X)) . [S,R] is set
[R,S] is Element of [:X,X:]
(Umf (X,X)) . [R,S] is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
[S,R] is Element of [:X,X:]
(Umf (X,X)) . [S,R] is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
R is Element of X
S is Element of X
[R,S] is Element of [:X,X:]
{R,S} is non empty set
{R} is non empty set
{{R,S},{R}} is non empty set
(Umf (X,X)) . [R,S] is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
Q is Element of X
[S,Q] is Element of [:X,X:]
{S,Q} is non empty set
{S} is non empty set
{{S,Q},{S}} is non empty set
(Umf (X,X)) .