:: DICKSON semantic presentation

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

F

F

{ F

{ F

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

F

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),b

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

{ (b

( b

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