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

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 . (S,b

(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

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