REAL is V267() V268() V269() V273() V283() V284() V286() set
NAT is non empty non trivial V25() non finite cardinal limit_cardinal countable denumerable V267() V268() V269() V270() V271() V272() V273() V281() V283() Element of bool REAL
bool REAL is non empty set
NAT is non empty non trivial V25() non finite cardinal limit_cardinal countable denumerable V267() V268() V269() V270() V271() V272() V273() V281() V283() set
bool NAT is non empty non trivial non finite set
bool NAT is non empty non trivial non finite set
K211() is set
{} is Relation-like non-empty empty-yielding RAT -valued Function-like one-to-one constant functional empty trivial V25() V29() finite finite-yielding V34() cardinal {} -element Cardinal-yielding countable Function-yielding V44() ext-real non positive non negative complex-valued ext-real-valued real-valued natural-valued increasing decreasing non-decreasing non-increasing V267() V268() V269() V270() V271() V272() V273() V283() V284() V285() V286() set
RAT is V267() V268() V269() V270() V273() set
{{}} is functional non empty trivial finite V34() 1 -element with_common_domain countable V267() V268() V269() V270() V271() V272() V281() V282() V283() V284() V285() set
1 is non empty V25() V29() finite cardinal countable V250() V251() ext-real positive non negative V255() V256() V267() V268() V269() V270() V271() V272() V281() V282() V283() V284() V285() Element of NAT
K189({{}}) is M8({{}})
[:K189({{}}),{{}}:] is Relation-like RAT -valued INT -valued complex-valued ext-real-valued real-valued natural-valued set
INT is V267() V268() V269() V270() V271() V273() set
bool [:K189({{}}),{{}}:] is non empty set
K98(K189({{}}),{{}}) is functional non empty set
{{},1} is non empty finite V34() countable V267() V268() V269() V270() V271() V272() V281() V282() V283() V284() V285() set
COMPLEX is V267() V273() set
[:COMPLEX,COMPLEX:] is Relation-like complex-valued set
bool [:COMPLEX,COMPLEX:] is non empty set
[:COMPLEX,REAL:] is Relation-like complex-valued ext-real-valued real-valued set
bool [:COMPLEX,REAL:] is non empty set
0 is Relation-like non-empty empty-yielding RAT -valued Function-like one-to-one constant functional empty trivial V25() V29() finite finite-yielding V34() cardinal {} -element Cardinal-yielding countable Function-yielding V44() V250() V251() ext-real non positive non negative V255() V256() complex-valued ext-real-valued real-valued natural-valued increasing decreasing non-decreasing non-increasing V267() V268() V269() V270() V271() V272() V273() V283() V284() V285() V286() Element of NAT
2 is non empty V25() V29() finite cardinal countable V250() V251() ext-real positive non negative V255() V256() V267() V268() V269() V270() V271() V272() V281() V282() V283() V284() V285() Element of NAT
card NAT is non empty non trivial V25() non finite cardinal set
[:NAT,REAL:] is Relation-like complex-valued ext-real-valued real-valued set
bool [:NAT,REAL:] is non empty set
id {{}} is Relation-like {{}} -defined {{}} -valued RAT -valued INT -valued Function-like one-to-one non empty V19({{}}) V20({{}},{{}}) V21({{}}) V22({{}},{{}}) finite countable Function-yielding V44() reflexive symmetric antisymmetric transitive complex-valued ext-real-valued real-valued natural-valued increasing non-decreasing Element of bool [:{{}},{{}}:]
[:{{}},{{}}:] is Relation-like RAT -valued INT -valued non empty finite countable complex-valued ext-real-valued real-valued natural-valued set
bool [:{{}},{{}}:] is non empty finite V34() countable set
RelStr(# {{}},(id {{}}) #) is non empty strict V81() reflexive transitive antisymmetric non void RelStr
[:NAT,NAT:] is Relation-like RAT -valued INT -valued non empty non trivial non finite complex-valued ext-real-valued real-valued natural-valued set
bool [:NAT,NAT:] is non empty non trivial non finite set
R is Relation-like Function-like set
dom R is set
IR is set
{IR} is non empty trivial finite 1 -element countable set
R . IR is set
IR .--> (R . IR) is Relation-like {IR} -defined Function-like one-to-one finite countable set
{IR} --> (R . IR) is Relation-like {IR} -defined {(R . IR)} -valued Function-like constant non empty V19({IR}) V20({IR},{(R . IR)}) finite countable Element of bool [:{IR},{(R . IR)}:]
{(R . IR)} is non empty trivial finite 1 -element countable set
[:{IR},{(R . IR)}:] is Relation-like non empty finite countable set
bool [:{IR},{(R . IR)}:] is non empty finite V34() countable set
dom (IR .--> (R . IR)) is trivial finite countable Element of bool {IR}
bool {IR} is non empty finite V34() countable set
CR is set
f is set
[CR,f] is V13() non empty set
{CR,f} is non empty finite countable set
{CR} is non empty trivial finite 1 -element countable set
{{CR,f},{CR}} is non empty finite V34() countable set
(IR .--> (R . IR)) . CR is set
R . CR is set
R is V25() V29() finite cardinal countable ext-real non negative set
R + 1 is non empty V25() V29() finite cardinal countable V250() V251() ext-real positive non negative V255() V256() V267() V268() V269() V270() V271() V272() V281() V282() V283() V284() V285() Element of NAT
{R} is non empty trivial finite V34() 1 -element countable V267() V268() V269() V270() V271() V272() V281() V282() V283() V284() V285() set
R \/ {R} is non empty finite countable set
F1() is V25() V29() finite cardinal countable V250() V251() ext-real non negative V255() V256() V267() V268() V269() V270() V271() V272() V283() V284() V285() Element of NAT
F2() is V25() V29() finite cardinal countable V250() V251() ext-real non negative V255() V256() V267() V268() V269() V270() V271() V272() V283() V284() V285() Element of NAT
{ F3(b1) where b1 is V25() V29() finite cardinal countable V250() V251() ext-real non negative V255() V256() V267() V268() V269() V270() V271() V272() V283() V284() V285() Element of NAT : ( not b1 <= F1() & b1 <= F2() & P1[b1] ) } is set
{ F3(b1) where b1 is V25() V29() finite cardinal countable V250() V251() ext-real non negative V255() V256() V267() V268() V269() V270() V271() V272() V283() V284() V285() Element of NAT : ( F1() <= b1 & b1 <= F2() & P1[b1] ) } is set
CR is set
f is V25() V29() finite cardinal countable V250() V251() ext-real non negative V255() V256() V267() V268() V269() V270() V271() V272() V283() V284() V285() Element of NAT
F3(f) is set
R is non empty non trivial non finite set
[:NAT,R:] is Relation-like non empty non trivial non finite set
bool [:NAT,R:] is non empty non trivial non finite set
card NAT is non empty non trivial V25() non finite cardinal set
card R is non empty non trivial V25() non finite cardinal set
IR is Relation-like Function-like set
dom IR is set
rng IR is set
CR is set
IR . CR is set
CR is Relation-like NAT -defined R -valued Function-like non empty V19( NAT ) V20( NAT ,R) Element of bool [:NAT,R:]
R is RelStr
the carrier of R is set
[:NAT, the carrier of R:] is Relation-like set
bool [:NAT, the carrier of R:] is non empty set
R is RelStr
the carrier of R is set
[:NAT, the carrier of R:] is Relation-like set
bool [:NAT, the carrier of R:] is non empty set
R is non empty transitive RelStr
the carrier of R is non empty set
[:NAT, the carrier of R:] is Relation-like non empty non trivial non finite set
bool [:NAT, the carrier of R:] is non empty non trivial non finite set
IR is Relation-like NAT -defined the carrier of R -valued Function-like non empty V19( NAT ) V20( NAT , the carrier of R) Element of bool [:NAT, the carrier of R:]
CR is V25() V29() finite cardinal countable V250() V251() ext-real non negative V255() V256() V267() V268() V269() V270() V271() V272() V283() V284() V285() Element of NAT
IR . CR is Element of the carrier of R
IR . 0 is Element of the carrier of R
f is V25() V29() finite cardinal countable V250() V251() ext-real non negative V255() V256() V267() V268() V269() V270() V271() V272() V283() V284() V285() Element of NAT
IR . f is Element of the carrier of R
f + 1 is non empty V25() V29() finite cardinal countable V250() V251() ext-real positive non negative V255() V256() V267() V268() V269() V270() V271() V272() V281() V282() V283() V284() V285() Element of NAT
IR . (f + 1) is Element of the carrier of R
[(IR . f),(IR . (f + 1))] is V13() non empty Element of the carrier of [:R,R:]
[:R,R:] is non empty strict transitive RelStr
the carrier of [:R,R:] is non empty set
{(IR . f),(IR . (f + 1))} is non empty finite countable set
{(IR . f)} is non empty trivial finite 1 -element countable set
{{(IR . f),(IR . (f + 1))},{(IR . f)}} is non empty finite V34() countable set
the InternalRel of R is Relation-like the carrier of R -defined the carrier of R -valued Element of bool [: the carrier of R, the carrier of R:]
[: the carrier of R, the carrier of R:] is Relation-like non empty set
bool [: the carrier of R, the carrier of R:] is non empty set
QOE is Element of the carrier of R
R is non empty RelStr
the InternalRel of R is Relation-like the carrier of R -defined the carrier of R -valued Element of bool [: the carrier of R, the carrier of R:]
the carrier of R is non empty set
[: the carrier of R, the carrier of R:] is Relation-like non empty set
bool [: the carrier of R, the carrier of R:] is non empty set
f is set
QOE is set
S is Element of the carrier of R
f9 is Element of the carrier of R
[f,QOE] is V13() non empty set
{f,QOE} is non empty finite countable set
{f} is non empty trivial finite 1 -element countable set
{{f,QOE},{f}} is non empty finite V34() countable set
[QOE,f] is V13() non empty set
{QOE,f} is non empty finite countable set
{QOE} is non empty trivial finite 1 -element countable set
{{QOE,f},{QOE}} is non empty finite V34() countable set
f is Element of the carrier of R
QOE is Element of the carrier of R
[f,QOE] is V13() non empty Element of the carrier of [:R,R:]
[:R,R:] is non empty strict RelStr
the carrier of [:R,R:] is non empty set
{f,QOE} is non empty finite countable set
{f} is non empty trivial finite 1 -element countable set
{{f,QOE},{f}} is non empty finite V34() countable set
[QOE,f] is V13() non empty Element of the carrier of [:R,R:]
{QOE,f} is non empty finite countable set
{QOE} is non empty trivial finite 1 -element countable set
{{QOE,f},{QOE}} is non empty finite V34() countable set
R is RelStr
the InternalRel of R is Relation-like the carrier of R -defined the carrier of R -valued Element of bool [: the carrier of R, the carrier of R:]
the carrier of R is set
[: the carrier of R, the carrier of R:] is Relation-like set
bool [: the carrier of R, the carrier of R:] is non empty set
IR is set
CR is set
the InternalRel of R -Seg CR is set
( the InternalRel of R -Seg CR) /\ IR is set
QOE is set
[QOE,CR] is V13() non empty set
{QOE,CR} is non empty finite countable set
{QOE} is non empty trivial finite 1 -element countable set
{{QOE,CR},{QOE}} is non empty finite V34() countable set
QOE is set
[QOE,CR] is V13() non empty set
{QOE,CR} is non empty finite countable set
{QOE} is non empty trivial finite 1 -element countable set
{{QOE,CR},{QOE}} is non empty finite V34() countable set
QOE is set
[QOE,CR] is V13() non empty set
{QOE,CR} is non empty finite countable set
{QOE} is non empty trivial finite 1 -element countable set
{{QOE,CR},{QOE}} is non empty finite V34() countable set
R is non empty transitive antisymmetric RelStr
the carrier of R is non empty set
the InternalRel of R is Relation-like the carrier of R -defined the carrier of R -valued Element of bool [: the carrier of R, the carrier of R:]
[: the carrier of R, the carrier of R:] is Relation-like non empty set
bool [: the carrier of R, the carrier of R:] is non empty set
IR is Element of the carrier of R
the InternalRel of R -Seg IR is set
f is set
( the InternalRel of R -Seg IR) /\ f is set
CR is set
[CR,IR] is V13() non empty set
{CR,IR} is non empty finite countable set
{CR} is non empty trivial finite 1 -element countable set
{{CR,IR},{CR}} is non empty finite V34() countable set
n is set
[n,CR] is V13() non empty set
{n,CR} is non empty finite countable set
{n} is non empty trivial finite 1 -element countable set
{{n,CR},{n}} is non empty finite V34() countable set
n is set
[n,CR] is V13() non empty set
{n,CR} is non empty finite countable set
{n} is non empty trivial finite 1 -element countable set
{{n,CR},{n}} is non empty finite V34() countable set
[n,IR] is V13() non empty set
{n,IR} is non empty finite countable set
{{n,IR},{n}} is non empty finite V34() countable set
f9 is Element of the carrier of R
n is set
[n,CR] is V13() non empty set
{n,CR} is non empty finite countable set
{n} is non empty trivial finite 1 -element countable set
{{n,CR},{n}} is non empty finite V34() countable set
R is RelStr
the carrier of R is set
the InternalRel of R is Relation-like the carrier of R -defined the carrier of R -valued Element of bool [: the carrier of R, the carrier of R:]
[: the carrier of R, the carrier of R:] is Relation-like set
bool [: the carrier of R, the carrier of R:] is non empty set
the InternalRel of R ~ is Relation-like the carrier of R -defined the carrier of R -valued Element of bool [: the carrier of R, the carrier of R:]
the InternalRel of R /\ ( the InternalRel of R ~) is Relation-like the carrier of R -defined the carrier of R -valued Element of bool [: the carrier of R, the carrier of R:]
f is set
[f,f] is V13() non empty set
{f,f} is non empty finite countable set
{f} is non empty trivial finite 1 -element countable set
{{f,f},{f}} is non empty finite V34() countable set
dom ( the InternalRel of R /\ ( the InternalRel of R ~)) is Element of bool the carrier of R
bool the carrier of R is non empty set
field ( the InternalRel of R /\ ( the InternalRel of R ~)) is set
f is set
QOE is set
[f,QOE] is V13() non empty set
{f,QOE} is non empty finite countable set
{f} is non empty trivial finite 1 -element countable set
{{f,QOE},{f}} is non empty finite V34() countable set
[QOE,f] is V13() non empty set
{QOE,f} is non empty finite countable set
{QOE} is non empty trivial finite 1 -element countable set
{{QOE,f},{QOE}} is non empty finite V34() countable set
f is set
QOE is set
S is set
[f,QOE] is V13() non empty set
{f,QOE} is non empty finite countable set
{f} is non empty trivial finite 1 -element countable set
{{f,QOE},{f}} is non empty finite V34() countable set
[QOE,S] is V13() non empty set
{QOE,S} is non empty finite countable set
{QOE} is non empty trivial finite 1 -element countable set
{{QOE,S},{QOE}} is non empty finite V34() countable set
[f,S] is V13() non empty set
{f,S} is non empty finite countable set
{{f,S},{f}} is non empty finite V34() countable set
R is RelStr
the carrier of R is set
(R) is Relation-like the carrier of R -defined the carrier of R -valued V19( the carrier of R) V20( the carrier of R, the carrier of R) reflexive symmetric transitive Element of bool [: the carrier of R, the carrier of R:]
[: the carrier of R, the carrier of R:] is Relation-like set
bool [: the carrier of R, the carrier of R:] is non empty set
IR is Element of the carrier of R
CR is Element of the carrier of R
Class ((R),CR) is Element of bool the carrier of R
bool the carrier of R is non empty set
the InternalRel of R is Relation-like the carrier of R -defined the carrier of R -valued Element of bool [: the carrier of R, the carrier of R:]
[IR,CR] is V13() non empty set
{IR,CR} is non empty finite countable set
{IR} is non empty trivial finite 1 -element countable set
{{IR,CR},{IR}} is non empty finite V34() countable set
the InternalRel of R ~ is Relation-like the carrier of R -defined the carrier of R -valued Element of bool [: the carrier of R, the carrier of R:]
the InternalRel of R /\ ( the InternalRel of R ~) is Relation-like the carrier of R -defined the carrier of R -valued Element of bool [: the carrier of R, the carrier of R:]
[CR,IR] is V13() non empty set
{CR,IR} is non empty finite countable set
{CR} is non empty trivial finite 1 -element countable set
{{CR,IR},{CR}} is non empty finite V34() countable set
R is RelStr
the carrier of R is set
(R) is Relation-like the carrier of R -defined the carrier of R -valued V19( the carrier of R) V20( the carrier of R, the carrier of R) reflexive symmetric transitive Element of bool [: the carrier of R, the carrier of R:]
[: the carrier of R, the carrier of R:] is Relation-like set
bool [: the carrier of R, the carrier of R:] is non empty set
Class (R) is with_non-empty_elements a_partition of the carrier of R
[:(Class (R)),(Class (R)):] is Relation-like set
bool [:(Class (R)),(Class (R)):] is non empty set
the InternalRel of R is Relation-like the carrier of R -defined the carrier of R -valued Element of bool [: the carrier of R, the carrier of R:]
f is Relation-like Class (R) -defined Class (R) -valued Element of bool [:(Class (R)),(Class (R)):]
QOE is set
S is set
[QOE,S] is V13() non empty set
{QOE,S} is non empty finite countable set
{QOE} is non empty trivial finite 1 -element countable set
{{QOE,S},{QOE}} is non empty finite V34() countable set
f9 is Element of the carrier of R
Class ((R),f9) is Element of bool the carrier of R
bool the carrier of R is non empty set
n is Element of the carrier of R
Class ((R),n) is Element of bool the carrier of R
f is non empty RelStr
the carrier of f is non empty set
bool the carrier of R is non empty set
{ [(Class ((R),b1)),(Class ((R),b2))] where b1, b2 is Element of the carrier of f : b1 <= b2 } is set
[:(Class (R)),(Class (R)):] is Relation-like bool the carrier of R -defined bool the carrier of R -valued Element of bool [:(bool the carrier of R),(bool the carrier of R):]
[:(bool the carrier of R),(bool the carrier of R):] is Relation-like non empty set
bool [:(bool the carrier of R),(bool the carrier of R):] is non empty set
f9 is set
n is Element of the carrier of f
Class ((R),n) is Element of bool the carrier of R
n1 is Element of the carrier of f
Class ((R),n1) is Element of bool the carrier of R
[(Class ((R),n)),(Class ((R),n1))] is V13() non empty Element of [:(bool the carrier of R),(bool the carrier of R):]
{(Class ((R),n)),(Class ((R),n1))} is non empty finite countable set
{(Class ((R),n))} is non empty trivial finite 1 -element countable set
{{(Class ((R),n)),(Class ((R),n1))},{(Class ((R),n))}} is non empty finite V34() countable set
f9 is Relation-like Class (R) -defined Class (R) -valued Element of bool [:(Class (R)),(Class (R)):]
n is set
n1 is set
[n,n1] is V13() non empty set
{n,n1} is non empty finite countable set
{n} is non empty trivial finite 1 -element countable set
{{n,n1},{n}} is non empty finite V34() countable set
l is Element of the carrier of R
Class ((R),l) is Element of bool the carrier of R
k is Element of the carrier of R
Class ((R),k) is Element of bool the carrier of R
[(Class ((R),l)),(Class ((R),k))] is V13() non empty Element of [:(bool the carrier of R),(bool the carrier of R):]
{(Class ((R),l)),(Class ((R),k))} is non empty finite countable set
{(Class ((R),l))} is non empty trivial finite 1 -element countable set
{{(Class ((R),l)),(Class ((R),k))},{(Class ((R),l))}} is non empty finite V34() countable set
a is Element of the carrier of R
b is Element of the carrier of R
S is Element of the carrier of R
Class ((R),S) is Element of bool the carrier of R
CP9 is Element of the carrier of R
Class ((R),CP9) is Element of bool the carrier of R
l is Element of the carrier of R
Class ((R),l) is Element of bool the carrier of R
k is Element of the carrier of R
Class ((R),k) is Element of bool the carrier of R
IR is Relation-like Class (R) -defined Class (R) -valued Element of bool [:(Class (R)),(Class (R)):]
CR is Relation-like Class (R) -defined Class (R) -valued Element of bool [:(Class (R)),(Class (R)):]
f is set
S is set
f9 is set
[S,f9] is V13() non empty set
{S,f9} is non empty finite countable set
{S} is non empty trivial finite 1 -element countable set
{{S,f9},{S}} is non empty finite V34() countable set
n is Element of the carrier of R
Class ((R),n) is Element of bool the carrier of R
bool the carrier of R is non empty set
n1 is Element of the carrier of R
Class ((R),n1) is Element of bool the carrier of R
S is set
f9 is set
[S,f9] is V13() non empty set
{S,f9} is non empty finite countable set
{S} is non empty trivial finite 1 -element countable set
{{S,f9},{S}} is non empty finite V34() countable set
n is Element of the carrier of R
Class ((R),n) is Element of bool the carrier of R
bool the carrier of R is non empty set
n1 is Element of the carrier of R
Class ((R),n1) is Element of bool the carrier of R
R is RelStr
(R) is Relation-like Class (R) -defined Class (R) -valued Element of bool [:(Class (R)),(Class (R)):]
the carrier of R is set
(R) is Relation-like the carrier of R -defined the carrier of R -valued V19( the carrier of R) V20( the carrier of R, the carrier of R) reflexive symmetric transitive Element of bool [: the carrier of R, the carrier of R:]
[: the carrier of R, the carrier of R:] is Relation-like set
bool [: the carrier of R, the carrier of R:] is non empty set
Class (R) is with_non-empty_elements a_partition of the carrier of R
[:(Class (R)),(Class (R)):] is Relation-like set
bool [:(Class (R)),(Class (R)):] is non empty set
the InternalRel of R is Relation-like the carrier of R -defined the carrier of R -valued Element of bool [: the carrier of R, the carrier of R:]
f is set
[f,f] is V13() non empty set
{f,f} is non empty finite countable set
{f} is non empty trivial finite 1 -element countable set
{{f,f},{f}} is non empty finite V34() countable set
QOE is set
Class ((R),QOE) is Element of bool the carrier of R
bool the carrier of R is non empty set
[QOE,QOE] is V13() non empty set
{QOE,QOE} is non empty finite countable set
{QOE} is non empty trivial finite 1 -element countable set
{{QOE,QOE},{QOE}} is non empty finite V34() countable set
S is Element of the carrier of R
f is set
QOE is set
S is set
[f,QOE] is V13() non empty set
{f,QOE} is non empty finite countable set
{f} is non empty trivial finite 1 -element countable set
{{f,QOE},{f}} is non empty finite V34() countable set
[QOE,S] is V13() non empty set
{QOE,S} is non empty finite countable set
{QOE} is non empty trivial finite 1 -element countable set
{{QOE,S},{QOE}} is non empty finite V34() countable set
[f,S] is V13() non empty set
{f,S} is non empty finite countable set
{{f,S},{f}} is non empty finite V34() countable set
f9 is Element of the carrier of R
Class ((R),f9) is Element of bool the carrier of R
bool the carrier of R is non empty set
n is Element of the carrier of R
Class ((R),n) is Element of bool the carrier of R
n1 is Element of the carrier of R
Class ((R),n1) is Element of bool the carrier of R
l is Element of the carrier of R
Class ((R),l) is Element of bool the carrier of R
[f9,n] is V13() non empty set
{f9,n} is non empty finite countable set
{f9} is non empty trivial finite 1 -element countable set
{{f9,n},{f9}} is non empty finite V34() countable set
[n1,l] is V13() non empty set
{n1,l} is non empty finite countable set
{n1} is non empty trivial finite 1 -element countable set
{{n1,l},{n1}} is non empty finite V34() countable set
k is set
Class ((R),k) is Element of bool the carrier of R
[n,n1] is V13() non empty set
{n,n1} is non empty finite countable set
{n} is non empty trivial finite 1 -element countable set
{{n,n1},{n}} is non empty finite V34() countable set
the InternalRel of R ~ is Relation-like the carrier of R -defined the carrier of R -valued Element of bool [: the carrier of R, the carrier of R:]
the InternalRel of R /\ ( the InternalRel of R ~) is Relation-like the carrier of R -defined the carrier of R -valued Element of bool [: the carrier of R, the carrier of R:]
[f9,n1] is V13() non empty set
{f9,n1} is non empty finite countable set
{{f9,n1},{f9}} is non empty finite V34() countable set
k is set
Class ((R),k) is Element of bool the carrier of R
[f9,l] is V13() non empty set
{f9,l} is non empty finite countable set
{{f9,l},{f9}} is non empty finite V34() countable set
k is set
Class ((R),k) is Element of bool the carrier of R
f is set
QOE is set
[f,QOE] is V13() non empty set
{f,QOE} is non empty finite countable set
{f} is non empty trivial finite 1 -element countable set
{{f,QOE},{f}} is non empty finite V34() countable set
[QOE,f] is V13() non empty set
{QOE,f} is non empty finite countable set
{QOE} is non empty trivial finite 1 -element countable set
{{QOE,f},{QOE}} is non empty finite V34() countable set
S is Element of the carrier of R
Class ((R),S) is Element of bool the carrier of R
bool the carrier of R is non empty set
f9 is Element of the carrier of R
Class ((R),f9) is Element of bool the carrier of R
n is Element of the carrier of R
Class ((R),n) is Element of bool the carrier of R
n1 is Element of the carrier of R
Class ((R),n1) is Element of bool the carrier of R
[S,f9] is V13() non empty set
{S,f9} is non empty finite countable set
{S} is non empty trivial finite 1 -element countable set
{{S,f9},{S}} is non empty finite V34() countable set
[n,n1] is V13() non empty set
{n,n1} is non empty finite countable set
{n} is non empty trivial finite 1 -element countable set
{{n,n1},{n}} is non empty finite V34() countable set
l is set
Class ((R),l) is Element of bool the carrier of R
l is set
Class ((R),l) is Element of bool the carrier of R
[S,n1] is V13() non empty set
{S,n1} is non empty finite countable set
{{S,n1},{S}} is non empty finite V34() countable set
l is set
Class ((R),l) is Element of bool the carrier of R
l is set
Class ((R),l) is Element of bool the carrier of R
[f9,n] is V13() non empty set
{f9,n} is non empty finite countable set
{f9} is non empty trivial finite 1 -element countable set
{{f9,n},{f9}} is non empty finite V34() countable set
the InternalRel of R ~ is Relation-like the carrier of R -defined the carrier of R -valued Element of bool [: the carrier of R, the carrier of R:]
the InternalRel of R /\ ( the InternalRel of R ~) is Relation-like the carrier of R -defined the carrier of R -valued Element of bool [: the carrier of R, the carrier of R:]
[n1,S] is V13() non empty set
{n1,S} is non empty finite countable set
{n1} is non empty trivial finite 1 -element countable set
{{n1,S},{n1}} is non empty finite V34() countable set
[f9,n1] is V13() non empty set
{f9,n1} is non empty finite countable set
{{f9,n1},{f9}} is non empty finite V34() countable set
l is set
Class ((R),l) is Element of bool the carrier of R
[f9,S] is V13() non empty set
{f9,S} is non empty finite countable set
{{f9,S},{f9}} is non empty finite V34() countable set
l is set
Class ((R),l) is Element of bool the carrier of R
R is non empty RelStr
(R) is Relation-like Class (R) -defined Class (R) -valued Element of bool [:(Class (R)),(Class (R)):]
the carrier of R is non empty set
(R) is Relation-like the carrier of R -defined the carrier of R -valued V19( the carrier of R) V20( the carrier of R, the carrier of R) reflexive symmetric transitive Element of bool [: the carrier of R, the carrier of R:]
[: the carrier of R, the carrier of R:] is Relation-like non empty set
bool [: the carrier of R, the carrier of R:] is non empty set
Class (R) is non empty with_non-empty_elements a_partition of the carrier of R
[:(Class (R)),(Class (R)):] is Relation-like non empty set
bool [:(Class (R)),(Class (R)):] is non empty set
CR is set
f is set
[CR,f] is V13() non empty set
{CR,f} is non empty finite countable set
{CR} is non empty trivial finite 1 -element countable set
{{CR,f},{CR}} is non empty finite V34() countable set
[f,CR] is V13() non empty set
{f,CR} is non empty finite countable set
{f} is non empty trivial finite 1 -element countable set
{{f,CR},{f}} is non empty finite V34() countable set
QOE is set
Class ((R),QOE) is Element of bool the carrier of R
bool the carrier of R is non empty set
S is set
Class ((R),S) is Element of bool the carrier of R
f9 is Element of the carrier of R
n is Element of the carrier of R
R is Relation-like set
R ~ is Relation-like set
R \ (R ~) is Relation-like Element of bool R
bool R is non empty set
R is Relation-like set
(R) is Relation-like set
R ~ is Relation-like set
R \ (R ~) is Relation-like Element of bool R
bool R is non empty set
IR is set
field (R) is set
CR is set
[IR,CR] is V13() non empty set
{IR,CR} is non empty finite countable set
{IR} is non empty trivial finite 1 -element countable set
{{IR,CR},{IR}} is non empty finite V34() countable set
[CR,IR] is V13() non empty set
{CR,IR} is non empty finite countable set
{CR} is non empty trivial finite 1 -element countable set
{{CR,IR},{CR}} is non empty finite V34() countable set
R is set
[:R,R:] is Relation-like set
bool [:R,R:] is non empty set
IR is Relation-like R -defined R -valued Element of bool [:R,R:]
(IR) is Relation-like asymmetric set
IR ~ is Relation-like set
IR \ (IR ~) is Relation-like R -defined R -valued Element of bool IR
bool IR is non empty set
IR ~ is Relation-like R -defined R -valued Element of bool [:R,R:]
IR \ (IR ~) is Relation-like R -defined R -valued Element of bool [:R,R:]
R is RelStr
the carrier of R is set
the InternalRel of R is Relation-like the carrier of R -defined the carrier of R -valued Element of bool [: the carrier of R, the carrier of R:]
[: the carrier of R, the carrier of R:] is Relation-like set
bool [: the carrier of R, the carrier of R:] is non empty set
( the carrier of R, the InternalRel of R) is Relation-like the carrier of R -defined the carrier of R -valued asymmetric Element of bool [: the carrier of R, the carrier of R:]
the InternalRel of R ~ is Relation-like set
the InternalRel of R \ ( the InternalRel of R ~) is Relation-like the carrier of R -defined the carrier of R -valued Element of bool the InternalRel of R
bool the InternalRel of R is non empty set
RelStr(# the carrier of R,( the carrier of R, the InternalRel of R) #) is strict RelStr
R is non empty RelStr
(R) is strict RelStr
the carrier of R is non empty set
the InternalRel of R is Relation-like the carrier of R -defined the carrier of R -valued Element of bool [: the carrier of R, the carrier of R:]
[: the carrier of R, the carrier of R:] is Relation-like non empty set
bool [: the carrier of R, the carrier of R:] is non empty set
( the carrier of R, the InternalRel of R) is Relation-like the carrier of R -defined the carrier of R -valued asymmetric Element of bool [: the carrier of R, the carrier of R:]
the InternalRel of R ~ is Relation-like set
the InternalRel of R \ ( the InternalRel of R ~) is Relation-like the carrier of R -defined the carrier of R -valued Element of bool the InternalRel of R
bool the InternalRel of R is non empty set
RelStr(# the carrier of R,( the carrier of R, the InternalRel of R) #) is non empty strict RelStr
R is transitive RelStr
(R) is strict RelStr
the carrier of R is set
the InternalRel of R is Relation-like the carrier of R -defined the carrier of R -valued Element of bool [: the carrier of R, the carrier of R:]
[: the carrier of R, the carrier of R:] is Relation-like set
bool [: the carrier of R, the carrier of R:] is non empty set
( the carrier of R, the InternalRel of R) is Relation-like the carrier of R -defined the carrier of R -valued asymmetric Element of bool [: the carrier of R, the carrier of R:]
the InternalRel of R ~ is Relation-like set
the InternalRel of R \ ( the InternalRel of R ~) is Relation-like the carrier of R -defined the carrier of R -valued Element of bool the InternalRel of R
bool the InternalRel of R is non empty set
RelStr(# the carrier of R,( the carrier of R, the InternalRel of R) #) is strict RelStr
the InternalRel of (R) is Relation-like the carrier of (R) -defined the carrier of (R) -valued Element of bool [: the carrier of (R), the carrier of (R):]
the carrier of (R) is set
[: the carrier of (R), the carrier of (R):] is Relation-like set
bool [: the carrier of (R), the carrier of (R):] is non empty set
S is set
f9 is set
n is set
[S,f9] is V13() non empty set
{S,f9} is non empty finite countable set
{S} is non empty trivial finite 1 -element countable set
{{S,f9},{S}} is non empty finite V34() countable set
[f9,n] is V13() non empty set
{f9,n} is non empty finite countable set
{f9} is non empty trivial finite 1 -element countable set
{{f9,n},{f9}} is non empty finite V34() countable set
the InternalRel of R ~ is Relation-like the carrier of R -defined the carrier of R -valued Element of bool [: the carrier of R, the carrier of R:]
[S,n] is V13() non empty set
{S,n} is non empty finite countable set
{{S,n},{S}} is non empty finite V34() countable set
[n,S] is V13() non empty set
{n,S} is non empty finite countable set
{n} is non empty trivial finite 1 -element countable set
{{n,S},{n}} is non empty finite V34() countable set
[f9,S] is V13() non empty set
{f9,S} is non empty finite countable set
{{f9,S},{f9}} is non empty finite V34() countable set
R is RelStr
(R) is strict RelStr
the carrier of R is set
the InternalRel of R is Relation-like the carrier of R -defined the carrier of R -valued Element of bool [: the carrier of R, the carrier of R:]
[: the carrier of R, the carrier of R:] is Relation-like set
bool [: the carrier of R, the carrier of R:] is non empty set
( the carrier of R, the InternalRel of R) is Relation-like the carrier of R -defined the carrier of R -valued asymmetric Element of bool [: the carrier of R, the carrier of R:]
the InternalRel of R ~ is Relation-like set
the InternalRel of R \ ( the InternalRel of R ~) is Relation-like the carrier of R -defined the carrier of R -valued Element of bool the InternalRel of R
bool the InternalRel of R is non empty set
RelStr(# the carrier of R,( the carrier of R, the InternalRel of R) #) is strict RelStr
the InternalRel of (R) is Relation-like the carrier of (R) -defined the carrier of (R) -valued Element of bool [: the carrier of (R), the carrier of (R):]
the carrier of (R) is set
[: the carrier of (R), the carrier of (R):] is Relation-like set
bool [: the carrier of (R), the carrier of (R):] is non empty set
QOE is set
S is set
[QOE,S] is V13() non empty set
{QOE,S} is non empty finite countable set
{QOE} is non empty trivial finite 1 -element countable set
{{QOE,S},{QOE}} is non empty finite V34() countable set
[S,QOE] is V13() non empty set
{S,QOE} is non empty finite countable set
{S} is non empty trivial finite 1 -element countable set
{{S,QOE},{S}} is non empty finite V34() countable set
the InternalRel of R ~ is Relation-like the carrier of R -defined the carrier of R -valued Element of bool [: the carrier of R, the carrier of R:]
R is non empty V81() reflexive transitive antisymmetric non void RelStr
the carrier of R is non empty set
(R) is Relation-like the carrier of R -defined the carrier of R -valued V19( the carrier of R) V20( the carrier of R, the carrier of R) reflexive symmetric transitive Element of bool [: the carrier of R, the carrier of R:]
[: the carrier of R, the carrier of R:] is Relation-like non empty set
bool [: the carrier of R, the carrier of R:] is non empty set
the InternalRel of R is Relation-like the carrier of R -defined the carrier of R -valued non empty V19( the carrier of R) V20( the carrier of R, the carrier of R) reflexive antisymmetric transitive Element of bool [: the carrier of R, the carrier of R:]
f is Element of the carrier of R
Class ((R),f) is Element of bool the carrier of R
bool the carrier of R is non empty set
{f} is non empty trivial finite 1 -element countable Element of bool the carrier of R
QOE is set
[QOE,f] is V13() non empty set
{QOE,f} is non empty finite countable set
{QOE} is non empty trivial finite 1 -element countable set
{{QOE,f},{QOE}} is non empty finite V34() countable set
the InternalRel of R ~ is Relation-like the carrier of R -defined the carrier of R -valued Element of bool [: the carrier of R, the carrier of R:]
the InternalRel of R /\ ( the InternalRel of R ~) is Relation-like the carrier of R -defined the carrier of R -valued Element of bool [: the carrier of R, the carrier of R:]
[f,QOE] is V13() non empty set
{f,QOE} is non empty finite countable set
{f} is non empty trivial finite 1 -element countable set
{{f,QOE},{f}} is non empty finite V34() countable set
dom the InternalRel of R is non empty Element of bool the carrier of R
R is Relation-like set
(R) is Relation-like asymmetric set
R ~ is Relation-like set
R \ (R ~) is Relation-like Element of bool R
bool R is non empty set
field R is set
IR is set
CR is set
[IR,CR] is V13() non empty set
{IR,CR} is non empty finite countable set
{IR} is non empty trivial finite 1 -element countable set
{{IR,CR},{IR}} is non empty finite V34() countable set
[CR,IR] is V13() non empty set
{CR,IR} is non empty finite countable set
{CR} is non empty trivial finite 1 -element countable set
{{CR,IR},{CR}} is non empty finite V34() countable set
R is Relation-like set
(R) is Relation-like asymmetric set
R ~ is Relation-like set
R \ (R ~) is Relation-like Element of bool R
bool R is non empty set
field R is set
IR is set
field (R) is set
CR is set
f is set
[IR,CR] is V13() non empty set
{IR,CR} is non empty finite countable set
{IR} is non empty trivial finite 1 -element countable set
{{IR,CR},{IR}} is non empty finite V34() countable set
[CR,f] is V13() non empty set
{CR,f} is non empty finite countable set
{CR} is non empty trivial finite 1 -element countable set
{{CR,f},{CR}} is non empty finite V34() countable set
[IR,f] is V13() non empty set
{IR,f} is non empty finite countable set
{{IR,f},{IR}} is non empty finite V34() countable set
[CR,IR] is V13() non empty set
{CR,IR} is non empty finite countable set
{{CR,IR},{CR}} is non empty finite V34() countable set
[f,IR] is V13() non empty set
{f,IR} is non empty finite countable set
{f} is non empty trivial finite 1 -element countable set
{{f,IR},{f}} is non empty finite V34() countable set
R is Relation-like set
(R) is Relation-like asymmetric set
R ~ is Relation-like set
R \ (R ~) is Relation-like Element of bool R
bool R is non empty set
IR is set
CR is set
[IR,CR] is V13() non empty set
{IR,CR} is non empty finite countable set
{IR} is non empty trivial finite 1 -element countable set
{{IR,CR},{IR}} is non empty finite V34() countable set
field R is set
field (R) is set
[CR,IR] is V13() non empty set
{CR,IR} is non empty finite countable set
{CR} is non empty trivial finite 1 -element countable set
{{CR,IR},{CR}} is non empty finite V34() countable set
R is RelStr
(R) is strict antisymmetric RelStr
the carrier of R is set
the InternalRel of R is Relation-like the carrier of R -defined the carrier of R -valued Element of bool [: the carrier of R, the carrier of R:]
[: the carrier of R, the carrier of R:] is Relation-like set
bool [: the carrier of R, the carrier of R:] is non empty set
( the carrier of R, the InternalRel of R) is Relation-like the carrier of R -defined the carrier of R -valued asymmetric Element of bool [: the carrier of R, the carrier of R:]
the InternalRel of R ~ is Relation-like set
the InternalRel of R \ ( the InternalRel of R ~) is Relation-like the carrier of R -defined the carrier of R -valued Element of bool the InternalRel of R
bool the InternalRel of R is non empty set
RelStr(# the carrier of R,( the carrier of R, the InternalRel of R) #) is strict RelStr
the InternalRel of (R) is Relation-like the carrier of (R) -defined the carrier of (R) -valued Element of bool [: the carrier of (R), the carrier of (R):]
the carrier of (R) is set
[: the carrier of (R), the carrier of (R):] is Relation-like set
bool [: the carrier of (R), the carrier of (R):] is non empty set
S is set
f9 is set
the InternalRel of R -Seg f9 is set
( the InternalRel of R -Seg f9) /\ S is set
n is set
the InternalRel of (R) -Seg n is set
( the InternalRel of (R) -Seg n) /\ S is set
n1 is set
n1 is set
[n1,n] is V13() non empty set
{n1,n} is non empty finite countable set
{n1} is non empty trivial finite 1 -element countable set
{{n1,n},{n1}} is non empty finite V34() countable set
the InternalRel of R -Seg n is set
R is RelStr
(R) is strict antisymmetric RelStr
the carrier of R is set
the InternalRel of R is Relation-like the carrier of R -defined the carrier of R -valued Element of bool [: the carrier of R, the carrier of R:]
[: the carrier of R, the carrier of R:] is Relation-like set
bool [: the carrier of R, the carrier of R:] is non empty set
( the carrier of R, the InternalRel of R) is Relation-like the carrier of R -defined the carrier of R -valued asymmetric Element of bool [: the carrier of R, the carrier of R:]
the InternalRel of R ~ is Relation-like set
the InternalRel of R \ ( the InternalRel of R ~) is Relation-like the carrier of R -defined the carrier of R -valued Element of bool the InternalRel of R
bool the InternalRel of R is non empty set
RelStr(# the carrier of R,( the carrier of R, the InternalRel of R) #) is strict RelStr
the InternalRel of (R) is Relation-like the carrier of (R) -defined the carrier of (R) -valued Element of bool [: the carrier of (R), the carrier of (R):]
the carrier of (R) is set
[: the carrier of (R), the carrier of (R):] is Relation-like set
bool [: the carrier of (R), the carrier of (R):] is non empty set
QOE is set
S is set
the InternalRel of (R) -Seg S is set
( the InternalRel of (R) -Seg S) /\ QOE is set
f9 is set
the InternalRel of R -Seg f9 is set
( the InternalRel of R -Seg f9) /\ QOE is set
n is set
[n,f9] is V13() non empty set
{n,f9} is non empty finite countable set
{n} is non empty trivial finite 1 -element countable set
{{n,f9},{n}} is non empty finite V34() countable set
[f9,n] is V13() non empty set
{f9,n} is non empty finite countable set
{f9} is non empty trivial finite 1 -element countable set
{{f9,n},{f9}} is non empty finite V34() countable set
the InternalRel of R ~ is Relation-like the carrier of R -defined the carrier of R -valued Element of bool [: the carrier of R, the carrier of R:]
the InternalRel of R \ ( the InternalRel of R ~) is Relation-like the carrier of R -defined the carrier of R -valued Element of bool [: the carrier of R, the carrier of R:]
the InternalRel of (R) -Seg f9 is set
R is RelStr
(R) is strict antisymmetric RelStr
the carrier of R is set
the InternalRel of R is Relation-like the carrier of R -defined the carrier of R -valued Element of bool [: the carrier of R, the carrier of R:]
[: the carrier of R, the carrier of R:] is Relation-like set
bool [: the carrier of R, the carrier of R:] is non empty set
( the carrier of R, the InternalRel of R) is Relation-like the carrier of R -defined the carrier of R -valued asymmetric Element of bool [: the carrier of R, the carrier of R:]
the InternalRel of R ~ is Relation-like set
the InternalRel of R \ ( the InternalRel of R ~) is Relation-like the carrier of R -defined the carrier of R -valued Element of bool the InternalRel of R
bool the InternalRel of R is non empty set
RelStr(# the carrier of R,( the carrier of R, the InternalRel of R) #) is strict RelStr
the carrier of (R) is set
the InternalRel of (R) is Relation-like the carrier of (R) -defined the carrier of (R) -valued Element of bool [: the carrier of (R), the carrier of (R):]
[: the carrier of (R), the carrier of (R):] is Relation-like set
bool [: the carrier of (R), the carrier of (R):] is non empty set
IR is set
CR is Element of the carrier of (R)
S is Element of the carrier of R
[S,CR] is V13() non empty set
{S,CR} is non empty finite countable set
{S} is non empty trivial finite 1 -element countable set
{{S,CR},{S}} is non empty finite V34() countable set
[CR,S] is V13() non empty set
{CR,S} is non empty finite countable set
{CR} is non empty trivial finite 1 -element countable set
{{CR,S},{CR}} is non empty finite V34() countable set
the InternalRel of R ~ is Relation-like the carrier of R -defined the carrier of R -valued Element of bool [: the carrier of R, the carrier of R:]
[CR,S] is V13() non empty set
{CR,S} is non empty finite countable set
{CR} is non empty trivial finite 1 -element countable set
{{CR,S},{CR}} is non empty finite V34() countable set
[CR,S] is V13() non empty set
{CR,S} is non empty finite countable set
{CR} is non empty trivial finite 1 -element countable set
{{CR,S},{CR}} is non empty finite V34() countable set
[CR,S] is V13() non empty set
{CR,S} is non empty finite countable set
{CR} is non empty trivial finite 1 -element countable set
{{CR,S},{CR}} is non empty finite V34() countable set
S is set
[S,CR] is V13() non empty set
{S,CR} is non empty finite countable set
{S} is non empty trivial finite 1 -element countable set
{{S,CR},{S}} is non empty finite V34() countable set
S is set
[S,CR] is V13() non empty set
{S,CR} is non empty finite countable set
{S} is non empty trivial finite 1 -element countable set
{{S,CR},{S}} is non empty finite V34() countable set
the InternalRel of R ~ is Relation-like the carrier of R -defined the carrier of R -valued Element of bool [: the carrier of R, the carrier of R:]
f9 is Element of the carrier of R
[f9,CR] is V13() non empty set
{f9,CR} is non empty finite countable set
{f9} is non empty trivial finite 1 -element countable set
{{f9,CR},{f9}} is non empty finite V34() countable set
[CR,f9] is V13() non empty set
{CR,f9} is non empty finite countable set
{{CR,f9},{CR}} is non empty finite V34() countable set
R is non empty RelStr
the carrier of R is non empty set
IR is non empty RelStr
the carrier of IR is non empty set
[: the carrier of R, the carrier of IR:] is Relation-like non empty set
bool [: the carrier of R, the carrier of IR:] is non empty set
(IR) is non empty strict antisymmetric RelStr
the InternalRel of IR is Relation-like the carrier of IR -defined the carrier of IR -valued Element of bool [: the carrier of IR, the carrier of IR:]
[: the carrier of IR, the carrier of IR:] is Relation-like non empty set
bool [: the carrier of IR, the carrier of IR:] is non empty set
( the carrier of IR, the InternalRel of IR) is Relation-like the carrier of IR -defined the carrier of IR -valued asymmetric Element of bool [: the carrier of IR, the carrier of IR:]
the InternalRel of IR ~ is Relation-like set
the InternalRel of IR \ ( the InternalRel of IR ~) is Relation-like the carrier of IR -defined the carrier of IR -valued Element of bool the InternalRel of IR
bool the InternalRel of IR is non empty set
RelStr(# the carrier of IR,( the carrier of IR, the InternalRel of IR) #) is non empty strict RelStr
(R) is Relation-like the carrier of R -defined the carrier of R -valued V19( the carrier of R) V20( the carrier of R, the carrier of R) reflexive symmetric transitive Element of bool [: the carrier of R, the carrier of R:]
[: the carrier of R, the carrier of R:] is Relation-like non empty set
bool [: the carrier of R, the carrier of R:] is non empty set
(R) is non empty strict antisymmetric RelStr
the InternalRel of R is Relation-like the carrier of R -defined the carrier of R -valued Element of bool [: the carrier of R, the carrier of R:]
( the carrier of R, the InternalRel of R) is Relation-like the carrier of R -defined the carrier of R -valued asymmetric Element of bool [: the carrier of R, the carrier of R:]
the InternalRel of R ~ is Relation-like set
the InternalRel of R \ ( the InternalRel of R ~) is Relation-like the carrier of R -defined the carrier of R -valued Element of bool the InternalRel of R
bool the InternalRel of R is non empty set
RelStr(# the carrier of R,( the carrier of R, the InternalRel of R) #) is non empty strict RelStr
CR is Relation-like the carrier of R -defined the carrier of IR -valued Function-like non empty V19( the carrier of R) V20( the carrier of R, the carrier of IR) Element of bool [: the carrier of R, the carrier of IR:]
the carrier of (R) is non empty set
[:NAT, the carrier of (R):] is Relation-like non empty non trivial non finite set
bool [:NAT, the carrier of (R):] is non empty non trivial non finite set
S is Relation-like NAT -defined the carrier of (R) -valued Function-like non empty V19( NAT ) V20( NAT , the carrier of (R)) Element of bool [:NAT, the carrier of (R):]
S is Relation-like NAT -defined the carrier of (R) -valued Function-like non empty V19( NAT ) V20( NAT , the carrier of (R)) Element of bool [:NAT, the carrier of (R):]
[:NAT, the carrier of R:] is Relation-like non empty non trivial non finite set
bool [:NAT, the carrier of R:] is non empty non trivial non finite set
f9 is Relation-like NAT -defined the carrier of R -valued Function-like non empty V19( NAT ) V20( NAT , the carrier of R) Element of bool [:NAT, the carrier of R:]
[:NAT, the carrier of IR:] is Relation-like non empty non trivial non finite set
bool [:NAT, the carrier of IR:] is non empty non trivial non finite set
n is Relation-like NAT -defined the carrier of IR -valued Function-like non empty V19( NAT ) V20( NAT , the carrier of IR) Element of bool [:NAT, the carrier of IR:]
the carrier of (IR) is non empty set
[:NAT, the carrier of (IR):] is Relation-like non empty non trivial non finite set
bool [:NAT, the carrier of (IR):] is non empty non trivial non finite set
l is V25() V29() finite cardinal countable ext-real non negative set
l + 1 is non empty V25() V29() finite cardinal countable V250() V251() ext-real positive non negative V255() V256() V267() V268() V269() V270() V271() V272() V281() V282() V283() V284() V285() Element of NAT
S . (l + 1) is Element of the carrier of (R)
S . l is Element of the carrier of (R)
[(S . (l + 1)),(S . l)] is V13() non empty Element of the carrier of [:(R),(R):]
[:(R),(R):] is non empty strict antisymmetric RelStr
the carrier of [:(R),(R):] is non empty set
{(S . (l + 1)),(S . l)} is non empty finite countable set
{(S . (l + 1))} is non empty trivial finite 1 -element countable set
{{(S . (l + 1)),(S . l)},{(S . (l + 1))}} is non empty finite V34() countable set
the InternalRel of (R) is Relation-like the carrier of (R) -defined the carrier of (R) -valued Element of bool [: the carrier of (R), the carrier of (R):]
[: the carrier of (R), the carrier of (R):] is Relation-like non empty set
bool [: the carrier of (R), the carrier of (R):] is non empty set
the InternalRel of R ~ is Relation-like the carrier of R -defined the carrier of R -valued Element of bool [: the carrier of R, the carrier of R:]
the InternalRel of R \ ( the InternalRel of R ~) is Relation-like the carrier of R -defined the carrier of R -valued Element of bool [: the carrier of R, the carrier of R:]
n1 is Relation-like NAT -defined the carrier of (IR) -valued Function-like non empty V19( NAT ) V20( NAT , the carrier of (IR)) Element of bool [:NAT, the carrier of (IR):]
k is V25() V29() finite cardinal countable V250() V251() ext-real non negative V255() V256() V267() V268() V269() V270() V271() V272() V283() V284() V285() Element of NAT
n1 . k is Element of the carrier of (IR)
S . k is Element of the carrier of (R)
CR . (S . k) is set
n1 . (l + 1) is Element of the carrier of (IR)
n1 . l is Element of the carrier of (IR)
CR . (S . (l + 1)) is set
CR . (S . l) is set
f9 . (l + 1) is Element of the carrier of R
f9 . l is Element of the carrier of R
[(f9 . (l + 1)),(f9 . l)] is V13() non empty Element of the carrier of [:R,R:]
[:R,R:] is non empty strict RelStr
the carrier of [:R,R:] is non empty set
{(f9 . (l + 1)),(f9 . l)} is non empty finite countable set
{(f9 . (l + 1))} is non empty trivial finite 1 -element countable set
{{(f9 . (l + 1)),(f9 . l)},{(f9 . (l + 1))}} is non empty finite V34() countable set
the InternalRel of R /\ ( the InternalRel of R ~) is Relation-like the carrier of R -defined the carrier of R -valued Element of bool [: the carrier of R, the carrier of R:]
a is Element of the carrier of R
b is Element of the carrier of R
n . (l + 1) is Element of the carrier of IR
CR . a is Element of the carrier of IR
n . k is Element of the carrier of IR
CR . b is Element of the carrier of IR
n . l is Element of the carrier of IR
[(n1 . (l + 1)),(n1 . l)] is V13() non empty Element of the carrier of [:(IR),(IR):]
[:(IR),(IR):] is non empty strict antisymmetric RelStr
the carrier of [:(IR),(IR):] is non empty set
{(n1 . (l + 1)),(n1 . l)} is non empty finite countable set
{(n1 . (l + 1))} is non empty trivial finite 1 -element countable set
{{(n1 . (l + 1)),(n1 . l)},{(n1 . (l + 1))}} is non empty finite V34() countable set
[(n1 . l),(n1 . (l + 1))] is V13() non empty Element of the carrier of [:(IR),(IR):]
{(n1 . l),(n1 . (l + 1))} is non empty finite countable set
{(n1 . l)} is non empty trivial finite 1 -element countable set
{{(n1 . l),(n1 . (l + 1))},{(n1 . l)}} is non empty finite V34() countable set
the InternalRel of IR ~ is Relation-like the carrier of IR -defined the carrier of IR -valued Element of bool [: the carrier of IR, the carrier of IR:]
the InternalRel of (IR) is Relation-like the carrier of (IR) -defined the carrier of (IR) -valued Element of bool [: the carrier of (IR), the carrier of (IR):]
[: the carrier of (IR), the carrier of (IR):] is Relation-like non empty set
bool [: the carrier of (IR), the carrier of (IR):] is non empty set
R is non empty RelStr
the carrier of R is non empty set
bool the carrier of R is non empty set
bool (bool the carrier of R) is non empty set
(R) is non empty strict antisymmetric RelStr
the InternalRel of R is Relation-like the carrier of R -defined the carrier of R -valued Element of bool [: the carrier of R, the carrier of R:]
[: the carrier of R, the carrier of R:] is Relation-like non empty set
bool [: the carrier of R, the carrier of R:] is non empty set
( the carrier of R, the InternalRel of R) is Relation-like the carrier of R -defined the carrier of R -valued asymmetric Element of bool [: the carrier of R, the carrier of R:]
the InternalRel of R ~ is Relation-like set
the InternalRel of R \ ( the InternalRel of R ~) is Relation-like the carrier of R -defined the carrier of R -valued Element of bool the InternalRel of R
bool the InternalRel of R is non empty set
RelStr(# the carrier of R,( the carrier of R, the InternalRel of R) #) is non empty strict RelStr
the carrier of (R) is non empty set
IR is Element of bool the carrier of R
the InternalRel of (R) is Relation-like the carrier of (R) -defined the carrier of (R) -valued Element of bool [: the carrier of (R), the carrier of (R):]
[: the carrier of (R), the carrier of (R):] is Relation-like non empty set
bool [: the carrier of (R), the carrier of (R):] is non empty set
(R) is Relation-like the carrier of R -defined the carrier of R -valued V19( the carrier of R) V20( the carrier of R, the carrier of R) reflexive symmetric transitive Element of bool [: the carrier of R, the carrier of R:]
Class (R) is non empty with_non-empty_elements a_partition of the carrier of R
{ (b1 /\ IR) where b1 is Element of Class (R) : ex b2 being Element of the carrier of (R) st
( b1 = Class ((R),b2) & b2 is_minimal_wrt IR, the InternalRel of (R) ) } is set
QOE is set
bool the carrier of R is non empty Element of bool (bool the carrier of R)
S is Element of Class (R)
S /\ IR is Element of bool the carrier of R
f9 is Element of the carrier of (R)
Class ((R),f9) is Element of bool the carrier of R
QOE is Element of bool (bool the carrier of R)
S is set
f9 is Element of Class (R)
f9 /\ IR is Element of bool the carrier of R
n is Element of the carrier of (R)
Class ((R),n) is Element of bool the carrier of R
f9 is Element of the carrier of (R)
Class ((R),f9) is Element of bool the carrier of R
(Class ((R),f9)) /\ IR is Element of bool the carrier of R
n is Element of the carrier of R
EqClass ((R),n) is Element of Class (R)
f is Element of bool (bool the carrier of R)
QOE is Element of bool (bool the carrier of R)
S is set
f9 is Element of the carrier of (R)
Class ((R),f9) is Element of bool the carrier of R
(Class ((R),f9)) /\ IR is Element of bool the carrier of R
f9 is Element of the carrier of (R)
Class ((R),f9) is Element of bool the carrier of R
(Class ((R),f9)) /\ IR is Element of bool the carrier of R
R is non empty RelStr
the carrier of R is non empty set
bool the carrier of R is non empty set
(R) is non empty strict antisymmetric RelStr
the InternalRel of R is Relation-like the carrier of R -defined the carrier of R -valued Element of bool [: the carrier of R, the carrier of R:]
[: the carrier of R, the carrier of R:] is Relation-like non empty set
bool [: the carrier of R, the carrier of R:] is non empty set
( the carrier of R, the InternalRel of R) is Relation-like the carrier of R -defined the carrier of R -valued asymmetric Element of bool [: the carrier of R, the carrier of R:]
the InternalRel of R ~ is Relation-like set
the InternalRel of R \ ( the InternalRel of R ~) is Relation-like the carrier of R -defined the carrier of R -valued Element of bool the InternalRel of R
bool the InternalRel of R is non empty set
RelStr(# the carrier of R,( the carrier of R, the InternalRel of R) #) is non empty strict RelStr
the carrier of (R) is non empty set
the InternalRel of (R) is Relation-like the carrier of (R) -defined the carrier of (R) -valued Element of bool [: the carrier of (R), the carrier of (R):]
[: the carrier of (R), the carrier of (R):] is Relation-like non empty set
bool [: the carrier of (R), the carrier of (R):] is non empty set
IR is Element of bool the carrier of R
(R,IR) is Element of bool (bool the carrier of R)
bool (bool the carrier of R) is non empty set
CR is set
f9 is Element of the carrier of (R)
(R) is Relation-like the carrier of R -defined the carrier of R -valued V19( the carrier of R) V20( the carrier of R, the carrier of R) reflexive symmetric transitive Element of bool [: the carrier of R, the carrier of R:]
n is Element of the carrier of (R)
Class ((R),n) is Element of bool the carrier of R
(Class ((R),n)) /\ IR is Element of bool the carrier of R
[f9,n] is V13() non empty Element of the carrier of [:(R),(R):]
[:(R),(R):] is non empty strict antisymmetric RelStr
the carrier of [:(R),(R):] is non empty set
{f9,n} is non empty finite countable set
{f9} is non empty trivial finite 1 -element countable set
{{f9,n},{f9}} is non empty finite V34() countable set
the InternalRel of R ~ is Relation-like the carrier of R -defined the carrier of R -valued Element of bool [: the carrier of R, the carrier of R:]
the InternalRel of R /\ ( the InternalRel of R ~) is Relation-like the carrier of R -defined the carrier of R -valued Element of bool [: the carrier of R, the carrier of R:]
n1 is set
[n1,f9] is V13() non empty set
{n1,f9} is non empty finite countable set
{n1} is non empty trivial finite 1 -element countable set
{{n1,f9},{n1}} is non empty finite V34() countable set
n1 is set
[n1,f9] is V13() non empty set
{n1,f9} is non empty finite countable set
{n1} is non empty trivial finite 1 -element countable set
{{n1,f9},{n1}} is non empty finite V34() countable set
[n1,n] is V13() non empty set
{n1,n} is non empty finite countable set
{{n1,n},{n1}} is non empty finite V34() countable set
[n,n1] is V13() non empty set
{n,n1} is non empty finite countable set
{n} is non empty trivial finite 1 -element countable set
{{n,n1},{n}} is non empty finite V34() countable set
[f9,n1] is V13() non empty set
{f9,n1} is non empty finite countable set
{{f9,n1},{f9}} is non empty finite V34() countable set
R is non empty RelStr
(R) is non empty strict antisymmetric RelStr
the carrier of R is non empty set
the InternalRel of R is Relation-like the carrier of R -defined the carrier of R -valued Element of bool [: the carrier of R, the carrier of R:]
[: the carrier of R, the carrier of R:] is Relation-like non empty set
bool [: the carrier of R, the carrier of R:] is non empty set
( the carrier of R, the InternalRel of R) is Relation-like the carrier of R -defined the carrier of R -valued asymmetric Element of bool [: the carrier of R, the carrier of R:]
the InternalRel of R ~ is Relation-like set
the InternalRel of R \ ( the InternalRel of R ~) is Relation-like the carrier of R -defined the carrier of R -valued Element of bool the InternalRel of R
bool the InternalRel of R is non empty set
RelStr(# the carrier of R,( the carrier of R, the InternalRel of R) #) is non empty strict RelStr
bool the carrier of R is non empty set
the InternalRel of (R) is Relation-like the carrier of (R) -defined the carrier of (R) -valued Element of bool [: the carrier of (R), the carrier of (R):]
the carrier of (R) is non empty set
[: the carrier of (R), the carrier of (R):] is Relation-like non empty set
bool [: the carrier of (R), the carrier of (R):] is non empty set
QOE is Element of bool the carrier of R
bool the carrier of (R) is non empty set
S is Element of bool the carrier of (R)
f9 is set
the InternalRel of (R) -Seg f9 is set
( the InternalRel of (R) -Seg f9) /\ S is Element of bool the carrier of (R)
(R) is Relation-like the carrier of R -defined the carrier of R -valued V19( the carrier of R) V20( the carrier of R, the carrier of R) reflexive symmetric transitive Element of bool [: the carrier of R, the carrier of R:]
n is Element of the carrier of (R)
Class ((R),n) is Element of bool the carrier of R
(Class ((R),n)) /\ QOE is Element of bool the carrier of