:: DILWORTH semantic presentation

REAL is non empty non trivial non finite set
NAT is non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal Element of bool REAL
bool REAL is non empty non trivial non finite set
omega is non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal set
bool omega is non empty non trivial non finite set
bool NAT is non empty non trivial non finite set
COMPLEX is non empty non trivial non finite set
RAT is non empty non trivial non finite set
INT is non empty non trivial non finite set
{} is empty trivial Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional ext-real non positive non negative epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural finite finite-yielding with_finite-elements cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V49() real V51() complex-valued ext-real-valued real-valued natural-valued increasing decreasing non-decreasing non-increasing set
the empty trivial Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional ext-real non positive non negative epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural finite finite-yielding with_finite-elements cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V49() real V51() complex-valued ext-real-valued real-valued natural-valued increasing decreasing non-decreasing non-increasing set is empty trivial Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional ext-real non positive non negative epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural finite finite-yielding with_finite-elements cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V49() real V51() complex-valued ext-real-valued real-valued natural-valued increasing decreasing non-decreasing non-increasing set
2 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() Element of NAT
1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() Element of NAT
{{},1} is non empty finite with_finite-elements set
K266(NAT) is V83() set
[:NAT,REAL:] is non empty non trivial Relation-like non finite set
bool [:NAT,REAL:] is non empty non trivial non finite set
1 -tuples_on NAT is non empty functional FinSequence-membered FinSequenceSet of NAT
[:REAL,REAL:] is non empty non trivial Relation-like non finite set
bool [:REAL,REAL:] is non empty non trivial non finite set
K662() is set
bool K662() is non empty set
K663() is Element of bool K662()
[:INT,INT:] is non empty non trivial Relation-like non finite set
bool [:INT,INT:] is non empty non trivial non finite set
[:COMPLEX,COMPLEX:] is non empty non trivial Relation-like non finite set
bool [:COMPLEX,COMPLEX:] is non empty non trivial non finite set
[:[:COMPLEX,COMPLEX:],COMPLEX:] is non empty non trivial Relation-like non finite set
bool [:[:COMPLEX,COMPLEX:],COMPLEX:] is non empty non trivial non finite set
[:[:REAL,REAL:],REAL:] is non empty non trivial Relation-like non finite set
bool [:[:REAL,REAL:],REAL:] is non empty non trivial non finite set
[:RAT,RAT:] is non empty non trivial Relation-like non finite set
bool [:RAT,RAT:] is non empty non trivial non finite set
[:[:RAT,RAT:],RAT:] is non empty non trivial Relation-like non finite set
bool [:[:RAT,RAT:],RAT:] is non empty non trivial non finite set
[:[:INT,INT:],INT:] is non empty non trivial Relation-like non finite set
bool [:[:INT,INT:],INT:] is non empty non trivial non finite set
[:NAT,NAT:] is non empty non trivial Relation-like non finite set
[:[:NAT,NAT:],NAT:] is non empty non trivial Relation-like non finite set
bool [:[:NAT,NAT:],NAT:] is non empty non trivial non finite set
3 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() Element of NAT
0 is empty trivial Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional ext-real non positive non negative epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural finite finite-yielding with_finite-elements cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V49() real V51() complex-valued ext-real-valued real-valued natural-valued increasing decreasing non-decreasing non-increasing Element of NAT
union {} is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() set
dom {} is empty trivial Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional ext-real non positive non negative epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural finite finite-yielding with_finite-elements cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V49() real V51() complex-valued ext-real-valued real-valued natural-valued increasing decreasing non-decreasing non-increasing set
rng {} is empty trivial Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional ext-real non positive non negative V24() V25() V26() V27() V29() epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural finite finite-yielding with_finite-elements cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V49() real V51() complex-valued ext-real-valued real-valued natural-valued increasing decreasing non-decreasing non-increasing with_non-empty_elements set
F₂() is finite set
F₁() is non empty finite set
{ F₃(b₁) where b₁ is Element of F₁() : P₁[b₁] } is set
card F₂() is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() Element of omega
card F₁() is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() Element of omega
{ F₃(b₁) where b₁ is Element of F₁() : b₁ in F₁() } is set
n is finite set
card n is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() Element of omega
cP is set
iP is Element of F₁()
F₃(iP) is set
cP is set
f is set
n is set
{cP} is non empty trivial finite 1 -element set
n \/ {cP} is non empty set
f \ (n \/ {cP}) is Element of bool f
bool f is non empty set
f \ n is Element of bool f
(f \ n) \ {cP} is Element of bool f
f is set
bool f is non empty set
bool (bool f) is non empty set
n is set
bool n is non empty set
bool (bool n) is non empty set
f \/ n is set
bool (f \/ n) is non empty set
bool (bool (f \/ n)) is non empty set
cP is Element of bool (bool f)
iP is Element of bool (bool n)
cP \/ iP is set
(bool f) \/ (bool n) is non empty set
f is set
n is set
f \/ n is set
cP is with_non-empty_elements a_partition of f
iP is with_non-empty_elements a_partition of n
cP \/ iP is set
bool (f \/ n) is non empty set
bool (bool (f \/ n)) is non empty set
union (cP \/ iP) is set
union cP is Element of bool f
bool f is non empty set
union iP is Element of bool n
bool n is non empty set
(union cP) \/ (union iP) is set
f \/ (union iP) is set
A is Element of bool (f \/ n)
g is Element of bool (f \/ n)
n is set
f is set
bool f is non empty set
f \ n is Element of bool f
{(f \ n)} is non empty trivial finite 1 -element Element of bool (bool f)
bool (bool f) is non empty set
cP is with_non-empty_elements a_partition of n
cP \/ {(f \ n)} is non empty set
n \/ (f \ n) is set
f is non empty non trivial non finite set
bool f is non empty non trivial non finite set
n is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() set
[:NAT,f:] is non empty non trivial Relation-like non finite set
bool [:NAT,f:] is non empty non trivial non finite set
cP is non empty Relation-like NAT -defined f -valued Function-like V17( NAT ) quasi_total Element of bool [:NAT,f:]
n + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() set
Seg (n + 1) is non empty finite n + 1 -element Element of bool NAT
[:(Seg (n + 1)),f:] is non empty non trivial Relation-like non finite set
bool [:(Seg (n + 1)),f:] is non empty non trivial non finite set
cP | (Seg (n + 1)) is Relation-like NAT -defined Seg (n + 1) -defined NAT -defined f -valued Function-like finite Element of bool [:NAT,f:]
P is non empty Relation-like Seg (n + 1) -defined f -valued Function-like V17( Seg (n + 1)) quasi_total finite Element of bool [:(Seg (n + 1)),f:]
card P is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() Element of omega
rng P is non empty finite set
card (rng P) is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() Element of omega
dom P is non empty finite Element of bool (Seg (n + 1))
bool (Seg (n + 1)) is non empty finite with_finite-elements set
card (dom P) is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() Element of omega
P is finite Element of bool f
card P is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() Element of omega
f is RelStr
the carrier of f is set
bool the carrier of f is non empty set
f is RelStr
the carrier of f is set
bool the carrier of f is non empty set
f is RelStr
the carrier of f is set
bool the carrier of f is non empty set
n is Element of bool the carrier of f
cP is set
iP is set
[cP,iP] is non empty set
{cP,iP} is non empty finite set
{cP} is non empty trivial finite 1 -element set
{{cP,iP},{cP}} is non empty finite with_finite-elements set
the InternalRel of f is Relation-like the carrier of f -defined the carrier of f -valued Element of bool [: the carrier of f, the carrier of f:]
[: the carrier of f, the carrier of f:] is Relation-like set
bool [: the carrier of f, the carrier of f:] is non empty set
[iP,cP] is non empty set
{iP,cP} is non empty finite set
{iP} is non empty trivial finite 1 -element set
{{iP,cP},{iP}} is non empty finite with_finite-elements set
f is RelStr
the carrier of f is set
bool the carrier of f is non empty set
{} f is empty trivial Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional ext-real non positive non negative epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural finite finite-yielding with_finite-elements cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V49() real V51() complex-valued ext-real-valued real-valued natural-valued increasing decreasing non-decreasing non-increasing strongly_connected (f) Element of bool the carrier of f
n is set
cP is set
[n,cP] is non empty set
{n,cP} is non empty finite set
{n} is non empty trivial finite 1 -element set
{{n,cP},{n}} is non empty finite with_finite-elements set
the InternalRel of f is Relation-like the carrier of f -defined the carrier of f -valued Element of bool [: the carrier of f, the carrier of f:]
[: the carrier of f, the carrier of f:] is Relation-like set
bool [: the carrier of f, the carrier of f:] is non empty set
[cP,n] is non empty set
{cP,n} is non empty finite set
{cP} is non empty trivial finite 1 -element set
{{cP,n},{cP}} is non empty finite with_finite-elements set
f is RelStr
the carrier of f is set
bool the carrier of f is non empty set
n is Element of bool the carrier of f
the InternalRel of f is Relation-like the carrier of f -defined the carrier of f -valued Element of bool [: the carrier of f, the carrier of f:]
[: the carrier of f, the carrier of f:] is Relation-like set
bool [: the carrier of f, the carrier of f:] is non empty set
iP is Element of the carrier of f
P is Element of the carrier of f
[iP,P] is non empty set
{iP,P} is non empty finite set
{iP} is non empty trivial finite 1 -element set
{{iP,P},{iP}} is non empty finite with_finite-elements set
[P,iP] is non empty set
{P,iP} is non empty finite set
{P} is non empty trivial finite 1 -element set
{{P,iP},{P}} is non empty finite with_finite-elements set
iP is set
P is set
[iP,P] is non empty set
{iP,P} is non empty finite set
{iP} is non empty trivial finite 1 -element set
{{iP,P},{iP}} is non empty finite with_finite-elements set
[P,iP] is non empty set
{P,iP} is non empty finite set
{P} is non empty trivial finite 1 -element set
{{P,iP},{P}} is non empty finite with_finite-elements set
P is Element of the carrier of f
A is Element of the carrier of f
f is RelStr
the carrier of f is set
bool the carrier of f is non empty set
{} f is empty trivial Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional ext-real non positive non negative epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural finite finite-yielding with_finite-elements cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V49() real V51() complex-valued ext-real-valued real-valued natural-valued increasing decreasing non-decreasing non-increasing strongly_connected (f) Element of bool the carrier of f
f is V139() reflexive RelStr
the carrier of f is set
bool the carrier of f is non empty set
n is Element of bool the carrier of f
the InternalRel of f is Relation-like the carrier of f -defined the carrier of f -valued V17( the carrier of f) quasi_total reflexive Element of bool [: the carrier of f, the carrier of f:]
[: the carrier of f, the carrier of f:] is Relation-like set
bool [: the carrier of f, the carrier of f:] is non empty set
P is set
P is set
[P,P] is non empty set
{P,P} is non empty finite set
{P} is non empty trivial finite 1 -element set
{{P,P},{P}} is non empty finite with_finite-elements set
[P,P] is non empty set
{P,P} is non empty finite set
{P} is non empty trivial finite 1 -element set
{{P,P},{P}} is non empty finite with_finite-elements set
f is non empty RelStr
the carrier of f is non empty set
bool the carrier of f is non empty set
the Element of the carrier of f is Element of the carrier of f
{ the Element of the carrier of f} is non empty trivial finite 1 -element (f) Element of bool the carrier of f
f is non empty RelStr
the carrier of f is non empty set
bool the carrier of f is non empty set
n is Element of the carrier of f
cP is Element of the carrier of f
{n,cP} is non empty finite Element of bool the carrier of f
f is non empty RelStr
the carrier of f is non empty set
bool the carrier of f is non empty set
n is Element of the carrier of f
cP is Element of the carrier of f
{n,cP} is non empty finite Element of bool the carrier of f
iP is Element of the carrier of f
P is Element of the carrier of f
f is RelStr
the carrier of f is set
bool the carrier of f is non empty set
n is (f) Element of bool the carrier of f
bool n is non empty set
cP is Element of bool n
the InternalRel of f is Relation-like the carrier of f -defined the carrier of f -valued Element of bool [: the carrier of f, the carrier of f:]
[: the carrier of f, the carrier of f:] is Relation-like set
bool [: the carrier of f, the carrier of f:] is non empty set
P is set
P is set
[P,P] is non empty set
{P,P} is non empty finite set
{P} is non empty trivial finite 1 -element set
{{P,P},{P}} is non empty finite with_finite-elements set
[P,P] is non empty set
{P,P} is non empty finite set
{P} is non empty trivial finite 1 -element set
{{P,P},{P}} is non empty finite with_finite-elements set
f is RelStr
the carrier of f is set
bool the carrier of f is non empty set
n is finite (f) Element of bool the carrier of f
card n is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() Element of omega
cP is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() set
bool n is non empty finite with_finite-elements set
iP is finite Element of bool n
card iP is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() Element of omega
P is finite (f) Element of bool the carrier of f
card P is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() Element of omega
f is transitive RelStr
the carrier of f is set
bool the carrier of f is non empty set
n is (f) Element of bool the carrier of f
cP is Element of the carrier of f
iP is Element of the carrier of f
{iP} is non empty trivial finite 1 -element set
n \/ {iP} is non empty set
P is set
P is Element of the carrier of f
A is Element of the carrier of f
f is transitive RelStr
the carrier of f is set
bool the carrier of f is non empty set
n is (f) Element of bool the carrier of f
cP is Element of the carrier of f
iP is Element of the carrier of f
{iP} is non empty trivial finite 1 -element set
n \/ {iP} is non empty set
P is set
P is Element of the carrier of f
A is Element of the carrier of f
f is RelStr
the carrier of f is set
bool the carrier of f is non empty set
f is RelStr
the carrier of f is set
bool the carrier of f is non empty set
n is Element of bool the carrier of f
cP is Element of the carrier of f
iP is Element of the carrier of f
f is RelStr
the carrier of f is set
bool the carrier of f is non empty set
n is Element of bool the carrier of f
cP is Element of the carrier of f
iP is Element of the carrier of f
f is RelStr
the carrier of f is set
bool the carrier of f is non empty set
{} f is empty trivial Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional ext-real non positive non negative epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural finite finite-yielding with_finite-elements cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V49() real V51() complex-valued ext-real-valued real-valued natural-valued increasing decreasing non-decreasing non-increasing strongly_connected (f) (f) Element of bool the carrier of f
f is non empty RelStr
the carrier of f is non empty set
bool the carrier of f is non empty set
the Element of the carrier of f is Element of the carrier of f
{ the Element of the carrier of f} is non empty trivial finite 1 -element (f) (f) Element of bool the carrier of f
f is non empty RelStr
the carrier of f is non empty set
bool the carrier of f is non empty set
n is Element of the carrier of f
cP is Element of the carrier of f
{n,cP} is non empty finite Element of bool the carrier of f
f is non empty RelStr
the carrier of f is non empty set
bool the carrier of f is non empty set
n is Element of the carrier of f
cP is Element of the carrier of f
{n,cP} is non empty finite Element of bool the carrier of f
P is Element of the carrier of f
P is Element of the carrier of f
f is RelStr
the carrier of f is set
bool the carrier of f is non empty set
n is (f) Element of bool the carrier of f
cP is (f) Element of bool the carrier of f
iP is set
P is set
P is Element of the carrier of f
A is Element of the carrier of f
f is RelStr
the carrier of f is set
bool the carrier of f is non empty set
n is (f) Element of bool the carrier of f
bool n is non empty set
cP is Element of bool n
iP is Element of bool the carrier of f
P is Element of the carrier of f
P is Element of the carrier of f
f is RelStr
the carrier of f is set
bool the carrier of f is non empty set
n is finite (f) Element of bool the carrier of f
card n is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() Element of omega
cP is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() set
bool n is non empty finite with_finite-elements set
iP is finite Element of bool n
card iP is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() Element of omega
P is finite (f) Element of bool the carrier of f
card P is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() Element of omega
f is RelStr
the carrier of f is set
bool the carrier of f is non empty set
n is finite RelStr
card n is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() set
the carrier of n is finite set
card the carrier of n is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() set
iP is finite (f) Element of bool the carrier of f
card iP is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() Element of omega
cP is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() set
{} f is empty trivial Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional ext-real non positive non negative epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural finite finite-yielding with_finite-elements cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V49() real V51() complex-valued ext-real-valued real-valued natural-valued increasing decreasing non-decreasing non-increasing strongly_connected (f) (f) Element of bool the carrier of f
card ({} f) is empty trivial Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional ext-real non positive non negative epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural finite finite-yielding with_finite-elements cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V49() real V51() complex-valued ext-real-valued real-valued natural-valued increasing decreasing non-decreasing non-increasing Element of omega
cP is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() set
iP is finite (f) Element of bool the carrier of f
card iP is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() Element of omega
iP is finite (f) Element of bool the carrier of f
card iP is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() Element of omega
P is finite (f) Element of bool the carrier of f
card P is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() Element of omega
f is () RelStr
the carrier of f is set
bool the carrier of f is non empty set
n is (f) Element of bool the carrier of f
cP is finite (f) Element of bool the carrier of f
card cP is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() Element of omega
bool n is non empty set
iP is finite Element of bool n
card iP is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() Element of omega
f is () RelStr
the carrier of f is set
bool the carrier of f is non empty set
n is finite (f) Element of bool the carrier of f
card n is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() Element of omega
cP is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() Element of omega
iP is finite (f) Element of bool the carrier of f
card iP is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() Element of omega
n is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() set
cP is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() set
iP is finite (f) Element of bool the carrier of f
card iP is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() Element of omega
iP is finite (f) Element of bool the carrier of f
card iP is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() Element of omega
P is finite (f) Element of bool the carrier of f
card P is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() Element of omega
P is finite (f) Element of bool the carrier of f
card P is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() Element of omega
f is empty trivial finite {} -element () RelStr
(f) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() set
the carrier of f is empty trivial Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional ext-real non positive non negative epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural finite finite-yielding with_finite-elements cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V49() real V51() complex-valued ext-real-valued real-valued natural-valued increasing decreasing non-decreasing non-increasing set
bool the carrier of f is non empty finite with_finite-elements set
{} f is empty trivial non proper Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional ext-real non positive non negative epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural finite finite-yielding with_finite-elements cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V49() real V51() complex-valued ext-real-valued real-valued natural-valued increasing decreasing non-decreasing non-increasing strongly_connected (f) (f) Element of bool the carrier of f
card ({} f) is empty trivial Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional ext-real non positive non negative epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural finite finite-yielding with_finite-elements cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V49() real V51() complex-valued ext-real-valued real-valued natural-valued increasing decreasing non-decreasing non-increasing Element of omega
n is empty trivial non proper Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional ext-real non positive non negative epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural finite finite-yielding with_finite-elements cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V49() real V51() complex-valued ext-real-valued real-valued natural-valued increasing decreasing non-decreasing non-increasing strongly_connected (f) (f) Element of bool the carrier of f
card n is empty trivial Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional ext-real non positive non negative epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural finite finite-yielding with_finite-elements cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V49() real V51() complex-valued ext-real-valued real-valued natural-valued increasing decreasing non-decreasing non-increasing Element of omega
f is non empty () RelStr
(f) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() set
the carrier of f is non empty set
the Element of the carrier of f is Element of the carrier of f
{ the Element of the carrier of f} is non empty trivial finite 1 -element (f) (f) Element of bool the carrier of f
bool the carrier of f is non empty set
card { the Element of the carrier of f} is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() Element of omega
f is non empty () RelStr
[#] f is non empty non proper Element of bool the carrier of f
the carrier of f is non empty set
bool the carrier of f is non empty set
(f) is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() set
0 + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() set
n is finite (f) Element of bool the carrier of f
card n is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() Element of omega
cP is set
iP is set
f is () RelStr
(f) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() set
[#] f is non proper Element of bool the carrier of f
the carrier of f is set
bool the carrier of f is non empty set
cP is Element of the carrier of f
iP is Element of the carrier of f
{cP,iP} is non empty finite set
card {cP,iP} is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() Element of omega
f is RelStr
n is finite () RelStr
the carrier of n is finite set
bool the carrier of n is non empty finite with_finite-elements set
card n is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() set
card the carrier of n is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() set
iP is finite (n) Element of bool the carrier of n
card iP is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() Element of omega
cP is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() set
{} f is empty trivial Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional ext-real non positive non negative epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural finite finite-yielding with_finite-elements cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V49() real V51() complex-valued ext-real-valued real-valued natural-valued increasing decreasing non-decreasing non-increasing strongly_connected (f) (f) Element of bool the carrier of f
the carrier of f is set
bool the carrier of f is non empty set
card {} is empty trivial Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional ext-real non positive non negative epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural finite finite-yielding with_finite-elements cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V49() real V51() complex-valued ext-real-valued real-valued natural-valued increasing decreasing non-decreasing non-increasing Element of omega
cP is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() set
iP is finite (n) Element of bool the carrier of n
card iP is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() Element of omega
iP is finite (f) Element of bool the carrier of f
card iP is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() Element of omega
P is finite (f) Element of bool the carrier of f
card P is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() Element of omega
f is () RelStr
the carrier of f is set
bool the carrier of f is non empty set
n is finite (f) Element of bool the carrier of f
card n is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() Element of omega
cP is (f) Element of bool the carrier of f
bool cP is non empty set
iP is finite Element of bool cP
card iP is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() Element of omega
f is () RelStr
the carrier of f is set
bool the carrier of f is non empty set
n is finite (f) Element of bool the carrier of f
card n is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() Element of omega
cP is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() Element of omega
iP is finite (f) Element of bool the carrier of f
card iP is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() Element of omega
n is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() set
cP is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() set
iP is finite (f) Element of bool the carrier of f
card iP is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() Element of omega
iP is finite (f) Element of bool the carrier of f
card iP is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() Element of omega
P is finite (f) Element of bool the carrier of f
card P is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() Element of omega
P is finite (f) Element of bool the carrier of f
card P is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() Element of omega
f is empty trivial finite {} -element () () RelStr
(f) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() set
the carrier of f is empty trivial Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional ext-real non positive non negative epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural finite finite-yielding with_finite-elements cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V49() real V51() complex-valued ext-real-valued real-valued natural-valued increasing decreasing non-decreasing non-increasing set
bool the carrier of f is non empty finite with_finite-elements set
{} f is empty trivial non proper Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional ext-real non positive non negative epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural finite finite-yielding with_finite-elements cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V49() real V51() complex-valued ext-real-valued real-valued natural-valued increasing decreasing non-decreasing non-increasing strongly_connected (f) (f) Element of bool the carrier of f
card ({} f) is empty trivial Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional ext-real non positive non negative epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural finite finite-yielding with_finite-elements cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V49() real V51() complex-valued ext-real-valued real-valued natural-valued increasing decreasing non-decreasing non-increasing Element of omega
n is empty trivial non proper Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional ext-real non positive non negative epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural finite finite-yielding with_finite-elements cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V49() real V51() complex-valued ext-real-valued real-valued natural-valued increasing decreasing non-decreasing non-increasing strongly_connected (f) (f) Element of bool the carrier of f
card n is empty trivial Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional ext-real non positive non negative epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural finite finite-yielding with_finite-elements cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V49() real V51() complex-valued ext-real-valued real-valued natural-valued increasing decreasing non-decreasing non-increasing Element of omega
f is non empty () RelStr
(f) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() set
the carrier of f is non empty set
the Element of the carrier of f is Element of the carrier of f
{ the Element of the carrier of f} is non empty trivial finite 1 -element (f) (f) Element of bool the carrier of f
bool the carrier of f is non empty set
card { the Element of the carrier of f} is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() Element of omega
f is non empty () RelStr
[#] f is non empty non proper Element of bool the carrier of f
the carrier of f is non empty set
bool the carrier of f is non empty set
(f) is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() set
0 + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() set
n is finite (f) Element of bool the carrier of f
card n is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() Element of omega
cP is set
iP is set
f is () RelStr
(f) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() set
[#] f is non proper Element of bool the carrier of f
the carrier of f is set
bool the carrier of f is non empty set
cP is Element of the carrier of f
iP is Element of the carrier of f
{cP,iP} is non empty finite set
card {cP,iP} is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() Element of omega
f is RelStr
n is () () RelStr
the carrier of n is set
bool the carrier of n is non empty set
(n) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() set
cP is finite (n) Element of bool the carrier of n
card cP is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() Element of omega
(n) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() set
iP is finite (n) Element of bool the carrier of n
card iP is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() Element of omega
0 + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() set
[#] n is non proper Element of bool the carrier of n
g is finite Element of bool the carrier of n
card g is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() Element of omega
g is finite Element of bool the carrier of n
card g is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() Element of omega
max ((n),(n)) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() set
(max ((n),(n))) + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() set
g is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() set
g is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() set
g is finite Element of bool the carrier of n
card g is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() Element of omega
g \/ iP is finite Element of bool the carrier of n
(g \/ iP) \/ cP is finite Element of bool the carrier of n
e1 is finite Element of bool the carrier of n
card e1 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() Element of omega
{ {b₁,b₂} where b₁, b₂ is Element of the carrier of n : ( not b₁ = b₂ & b₁ in e1 & b₂ in e1 & ( b₁ <= b₂ or b₂ <= b₁ ) ) } is set
{ {b₁,b₂} where b₁, b₂ is Element of the carrier of n : ( not b₁ = b₂ & b₁ in e1 & b₂ in e1 & not b₁ <= b₂ & not b₂ <= b₁ ) } is set
the_subsets_of_card (2,e1) is finite with_finite-elements Element of bool (bool e1)
bool e1 is non empty finite with_finite-elements set
bool (bool e1) is non empty finite with_finite-elements set
{ b₁ where b₁ is Element of bool e1 : card b₁ = 2 } is set
{ { {b₁,b₂} where b₁, b₂ is Element of the carrier of n : ( not b₁ = b₂ & b₁ in e1 & b₂ in e1 & ( b₁ <= b₂ or b₂ <= b₁ ) ) } , { {b₁,b₂} where b₁, b₂ is Element of the carrier of n : ( not b₁ = b₂ & b₁ in e1 & b₂ in e1 & not b₁ <= b₂ & not b₂ <= b₁ ) } } is non empty finite set
j is set
r is Element of the carrier of n
s is Element of the carrier of n
{r,s} is non empty finite set
card j is epsilon-transitive epsilon-connected ordinal cardinal set
j is set
r is Element of the carrier of n
s is Element of the carrier of n
{r,s} is non empty finite set
card j is epsilon-transitive epsilon-connected ordinal cardinal set
j is set
r is set
s is Element of the carrier of n
Sp is Element of the carrier of n
{s,Sp} is non empty finite set
Sp is Element of the carrier of n
Sp is Element of the carrier of n
{Sp,Sp} is non empty finite set
bool (the_subsets_of_card (2,e1)) is non empty finite with_finite-elements set
j is set
union { { {b₁,b₂} where b₁, b₂ is Element of the carrier of n : ( not b₁ = b₂ & b₁ in e1 & b₂ in e1 & ( b₁ <= b₂ or b₂ <= b₁ ) ) } , { {b₁,b₂} where b₁, b₂ is Element of the carrier of n : ( not b₁ = b₂ & b₁ in e1 & b₂ in e1 & not b₁ <= b₂ & not b₂ <= b₁ ) } } is set
j is set
r is set
j is set
r is finite Element of bool e1
card r is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() Element of omega
s is set
Sp is set
{s,Sp} is non empty finite set
Sp is Element of the carrier of n
Sp is Element of the carrier of n
{Sp,Sp} is non empty finite set
j is finite with_finite-elements Element of bool (the_subsets_of_card (2,e1))
r is set
s is set
Sp is Element of the carrier of n
Sp is Element of the carrier of n
{Sp,Sp} is non empty finite set
r is set
s is set
Sp is Element of the carrier of n
Sp is Element of the carrier of n
{Sp,Sp} is non empty finite set
r is finite with_finite-elements Element of bool (the_subsets_of_card (2,e1))
{ {b₁,b₂} where b₁, b₂ is Element of the carrier of n : ( not b₁ = b₂ & b₁ in e1 & b₂ in e1 & ( b₁ <= b₂ or b₂ <= b₁ ) ) } /\ { {b₁,b₂} where b₁, b₂ is Element of the carrier of n : ( not b₁ = b₂ & b₁ in e1 & b₂ in e1 & not b₁ <= b₂ & not b₂ <= b₁ ) } is set
s is set
Sp is Element of the carrier of n
Sp is Element of the carrier of n
{Sp,Sp} is non empty finite set
Sp is Element of the carrier of n
cc is Element of the carrier of n
{Sp,cc} is non empty finite set
j is finite with_finite-elements with_non-empty_elements a_partition of the_subsets_of_card (2,e1)
card j is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() Element of omega
r is finite Element of bool e1
card r is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() Element of omega
s is finite Element of bool the carrier of n
card s is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() Element of omega
the_subsets_of_card (2,s) is finite with_finite-elements Element of bool (bool s)
bool s is non empty finite with_finite-elements set
bool (bool s) is non empty finite with_finite-elements set
{ b₁ where b₁ is Element of bool s : card b₁ = 2 } is set
Sp is finite Element of j
Sp is Element of the carrier of n
Sp is Element of the carrier of n
{Sp,Sp} is non empty finite set
card {Sp,Sp} is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() Element of omega
cc is Element of the carrier of n
d is Element of the carrier of n
{cc,d} is non empty finite set
Sp is Element of the carrier of n
Sp is Element of the carrier of n
{Sp,Sp} is non empty finite set
card {Sp,Sp} is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() Element of omega
cc is Element of the carrier of n
d is Element of the carrier of n
{cc,d} is non empty finite set
f is RelStr
the carrier of f is set
bool the carrier of f is non empty set
n is Element of bool the carrier of f
downarrow n is Element of bool the carrier of f
n \/ (downarrow n) is Element of bool the carrier of f
uparrow n is Element of bool the carrier of f
n \/ (uparrow n) is Element of bool the carrier of f
f is transitive antisymmetric RelStr
the carrier of f is set
bool the carrier of f is non empty set
n is (f) Element of bool the carrier of f
(f,n) is Element of bool the carrier of f
uparrow n is Element of bool the carrier of f
n \/ (uparrow n) is Element of bool the carrier of f
(f,n) is Element of bool the carrier of f
downarrow n is Element of bool the carrier of f
n \/ (downarrow n) is Element of bool the carrier of f
cP is set
iP is Element of the carrier of f
P is Element of the carrier of f
P is Element of the carrier of f
A is Element of the carrier of f
f is () RelStr
the carrier of f is set
bool the carrier of f is non empty set
(f) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() set
[#] f is non proper Element of bool the carrier of f
n is finite (f) Element of bool the carrier of f
card n is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() Element of omega
(f,n) is Element of bool the carrier of f
uparrow n is Element of bool the carrier of f
n \/ (uparrow n) is Element of bool the carrier of f
(f,n) is Element of bool the carrier of f
downarrow n is Element of bool the carrier of f
n \/ (downarrow n) is Element of bool the carrier of f
(f,n) \/ (f,n) is Element of bool the carrier of f
iP is set
P is Element of the carrier of f
{P} is non empty trivial finite 1 -element set
n \/ {P} is non empty finite set
A is Element of the carrier of f
g is Element of the carrier of f
card (n \/ {P}) is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() Element of omega
(card n) + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() set
f is transitive RelStr
the carrier of f is set
bool the carrier of f is non empty set
[#] f is non proper Element of bool the carrier of f
n is Element of the carrier of f
cP is Element of bool the carrier of f
(f,cP) is Element of bool the carrier of f
downarrow cP is Element of bool the carrier of f
cP \/ (downarrow cP) is Element of bool the carrier of f
P is Element of the carrier of f
P is Element of the carrier of f
f is transitive RelStr
the carrier of f is set
bool the carrier of f is non empty set
[#] f is non proper Element of bool the carrier of f
n is Element of the carrier of f
cP is Element of bool the carrier of f
(f,cP) is Element of bool the carrier of f
uparrow cP is Element of bool the carrier of f
cP \/ (uparrow cP) is Element of bool the carrier of f
P is Element of the carrier of f
P is Element of the carrier of f
f is RelStr
the carrier of f is set
bool the carrier of f is non empty set
[#] f is non proper Element of bool the carrier of f
cP is set
iP is set
iP is Element of bool the carrier of f
P is Element of the carrier of f
P is Element of bool the carrier of f
A is Element of the carrier of f
iP is Element of bool the carrier of f
P is Element of bool the carrier of f
iP is Element of bool the carrier of f
P is Element of bool the carrier of f
cP is Element of bool the carrier of f
iP is Element of bool the carrier of f
P is set
P is Element of the carrier of f
P is Element of the carrier of f
P is Element of the carrier of f
A is Element of the carrier of f
g is Element of the carrier of f
cP is set
iP is set
iP is Element of bool the carrier of f
P is Element of the carrier of f
P is Element of bool the carrier of f
A is Element of the carrier of f
iP is Element of bool the carrier of f
P is Element of bool the carrier of f
iP is Element of bool the carrier of f
P is Element of bool the carrier of f
cP is Element of bool the carrier of f
iP is Element of bool the carrier of f
P is set
P is Element of the carrier of f
P is Element of the carrier of f
P is Element of the carrier of f
A is Element of the carrier of f
g is Element of the carrier of f
f is non empty transitive antisymmetric () RelStr
(f) is Element of bool the carrier of f
the carrier of f is non empty set
bool the carrier of f is non empty set
the InternalRel of f is Relation-like the carrier of f -defined the carrier of f -valued Element of bool [: the carrier of f, the carrier of f:]
[: the carrier of f, the carrier of f:] is non empty Relation-like set
bool [: the carrier of f, the carrier of f:] is non empty set
iP is finite (f) Element of bool the carrier of f
card iP is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() Element of omega
the Element of the carrier of f is Element of the carrier of f
{ the Element of the carrier of f} is non empty trivial finite 1 -element (f) (f) Element of bool the carrier of f
card { the Element of the carrier of f} is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() Element of omega
P is Element of the carrier of f
[#] f is non empty non proper Element of bool the carrier of f
P is Element of the carrier of f
{P} is non empty trivial finite 1 -element (f) (f) Element of bool the carrier of f
iP \/ {P} is non empty finite Element of bool the carrier of f
g is finite (f) Element of bool the carrier of f
card g is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() Element of omega
(card iP) + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() set
(card iP) + 0 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() set
(f) is Element of bool the carrier of f
the InternalRel of f is Relation-like the carrier of f -defined the carrier of f -valued Element of bool [: the carrier of f, the carrier of f:]
[: the carrier of f, the carrier of f:] is non empty Relation-like set
bool [: the carrier of f, the carrier of f:] is non empty set
iP is finite (f) Element of bool the carrier of f
card iP is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() Element of omega
the Element of the carrier of f is Element of the carrier of f
{ the Element of the carrier of f} is non empty trivial finite 1 -element (f) (f) Element of bool the carrier of f
card { the Element of the carrier of f} is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() Element of omega
P is Element of the carrier of f
[#] f is non empty non proper Element of bool the carrier of f
P is Element of the carrier of f
{P} is non empty trivial finite 1 -element (f) (f) Element of bool the carrier of f
iP \/ {P} is non empty finite Element of bool the carrier of f
g is finite (f) Element of bool the carrier of f
card g is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() Element of omega
(card iP) + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() set
(card iP) + 0 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() set
f is RelStr
(f) is Element of bool the carrier of f
the carrier of f is set
bool the carrier of f is non empty set
cP is Element of the carrier of f
iP is Element of the carrier of f
[#] f is non proper Element of bool the carrier of f
(f) is Element of bool the carrier of f
cP is Element of the carrier of f
iP is Element of the carrier of f
[#] f is non proper Element of bool the carrier of f
f is RelStr
the carrier of f is set
bool the carrier of f is non empty set
(f) is (f) Element of bool the carrier of f
n is (f) Element of bool the carrier of f
(f,n) is Element of bool the carrier of f
uparrow n is Element of bool the carrier of f
n \/ (uparrow n) is Element of bool the carrier of f
cP is set
[#] f is non proper Element of bool the carrier of f
iP is Element of the carrier of f
P is Element of the carrier of f
f is RelStr
the carrier of f is set
bool the carrier of f is non empty set
(f) is (f) Element of bool the carrier of f
n is (f) Element of bool the carrier of f
(f,n) is Element of bool the carrier of f
downarrow n is Element of bool the carrier of f
n \/ (downarrow n) is Element of bool the carrier of f
cP is set
[#] f is non proper Element of bool the carrier of f
iP is Element of the carrier of f
P is Element of the carrier of f
f is RelStr
the carrier of f is set
bool the carrier of f is non empty set
n is finite Element of bool the carrier of f
subrelstr n is strict V147(f) SubRelStr of f
f is RelStr
the carrier of f is set
bool the carrier of f is non empty set
n is Element of bool the carrier of f
subrelstr n is strict V147(f) SubRelStr of f
the carrier of (subrelstr n) is set
bool the carrier of (subrelstr n) is non empty set
cP is ( subrelstr n) Element of bool the carrier of (subrelstr n)
iP is Element of the carrier of f
P is Element of the carrier of f
P is Element of the carrier of (subrelstr n)
A is Element of the carrier of (subrelstr n)
f is RelStr
the carrier of f is set
bool the carrier of f is non empty set
n is Element of bool the carrier of f
subrelstr n is strict V147(f) SubRelStr of f
the carrier of (subrelstr n) is set
bool the carrier of (subrelstr n) is non empty set
cP is (f) Element of bool the carrier of f
cP /\ n is Element of bool the carrier of f
P is Element of the carrier of (subrelstr n)
A is Element of the carrier of (subrelstr n)
g is Element of the carrier of f
g is Element of the carrier of f
f is RelStr
the carrier of f is set
bool the carrier of f is non empty set
n is Element of bool the carrier of f
subrelstr n is strict V147(f) SubRelStr of f
the carrier of (subrelstr n) is set
bool the carrier of (subrelstr n) is non empty set
cP is ( subrelstr n) Element of bool the carrier of (subrelstr n)
{} f is empty trivial Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional ext-real non positive non negative epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural finite finite-yielding with_finite-elements cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V49() real V51() complex-valued ext-real-valued real-valued natural-valued increasing decreasing non-decreasing non-increasing strongly_connected (f) (f) Element of bool the carrier of f
{} f is empty trivial Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional ext-real non positive non negative epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural finite finite-yielding with_finite-elements cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V49() real V51() complex-valued ext-real-valued real-valued natural-valued increasing decreasing non-decreasing non-increasing strongly_connected (f) (f) Element of bool the carrier of f
P is Element of bool the carrier of f
P is Element of the carrier of f
A is Element of the carrier of f
g is Element of the carrier of (subrelstr n)
g is Element of the carrier of (subrelstr n)
f is RelStr
the carrier of f is set
bool the carrier of f is non empty set
n is Element of bool the carrier of f
subrelstr n is strict V147(f) SubRelStr of f
the carrier of (subrelstr n) is set
bool the carrier of (subrelstr n) is non empty set
cP is (f) Element of bool the carrier of f
cP /\ n is Element of bool the carrier of f
{} (subrelstr n) is empty trivial Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional ext-real non positive non negative epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural finite finite-yielding with_finite-elements cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V49() real V51() complex-valued ext-real-valued real-valued natural-valued increasing decreasing non-decreasing non-increasing strongly_connected ( subrelstr n) ( subrelstr n) Element of bool the carrier of (subrelstr n)
{} (subrelstr n) is empty trivial Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional ext-real non positive non negative epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural finite finite-yielding with_finite-elements cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V49() real V51() complex-valued ext-real-valued real-valued natural-valued increasing decreasing non-decreasing non-increasing strongly_connected ( subrelstr n) ( subrelstr n) Element of bool the carrier of (subrelstr n)
P is Element of bool the carrier of (subrelstr n)
A is Element of the carrier of (subrelstr n)
g is Element of the carrier of (subrelstr n)
g is Element of the carrier of f
g is Element of the carrier of f
f is RelStr
the carrier of f is set
bool the carrier of f is non empty set
n is Element of bool the carrier of f
subrelstr n is strict V147(f) SubRelStr of f
the carrier of (subrelstr n) is set
bool the carrier of (subrelstr n) is non empty set
cP is Element of bool the carrier of (subrelstr n)
iP is Element of the carrier of (subrelstr n)
P is Element of the carrier of f
P is Element of the carrier of f
A is Element of the carrier of (subrelstr n)
f is RelStr
the carrier of f is set
bool the carrier of f is non empty set
n is Element of bool the carrier of f
subrelstr n is strict V147(f) SubRelStr of f
the carrier of (subrelstr n) is set
bool the carrier of (subrelstr n) is non empty set
cP is Element of bool the carrier of (subrelstr n)
iP is Element of the carrier of (subrelstr n)
P is Element of the carrier of f
P is Element of the carrier of f
A is Element of the carrier of (subrelstr n)
f is transitive RelStr
the carrier of f is set
bool the carrier of f is non empty set
n is (f) Element of bool the carrier of f
(f,n) is Element of bool the carrier of f
downarrow n is Element of bool the carrier of f
n \/ (downarrow n) is Element of bool the carrier of f
subrelstr (f,n) is strict transitive V147(f) SubRelStr of f
the carrier of (subrelstr (f,n)) is set
bool the carrier of (subrelstr (f,n)) is non empty set
cP is ( subrelstr (f,n)) Element of bool the carrier of (subrelstr (f,n))
iP is Element of the carrier of f
P is Element of the carrier of f
g is Element of the carrier of (subrelstr (f,n))
g is Element of the carrier of f
A is Element of the carrier of (subrelstr (f,n))
A is Element of the carrier of (subrelstr (f,n))
A is Element of the carrier of (subrelstr (f,n))
f is transitive RelStr
the carrier of f is set
bool the carrier of f is non empty set
n is (f) Element of bool the carrier of f
(f,n) is Element of bool the carrier of f
uparrow n is Element of bool the carrier of f
n \/ (uparrow n) is Element of bool the carrier of f
subrelstr (f,n) is strict transitive V147(f) SubRelStr of f
the carrier of (subrelstr (f,n)) is set
bool the carrier of (subrelstr (f,n)) is non empty set
cP is ( subrelstr (f,n)) Element of bool the carrier of (subrelstr (f,n))
iP is Element of the carrier of f
P is Element of the carrier of f
g is Element of the carrier of (subrelstr (f,n))
g is Element of the carrier of f
A is Element of the carrier of (subrelstr (f,n))
A is Element of the carrier of (subrelstr (f,n))
A is Element of the carrier of (subrelstr (f,n))
f is () RelStr
the carrier of f is set
bool the carrier of f is non empty set
n is Element of bool the carrier of f
subrelstr n is strict V147(f) SubRelStr of f
cP is finite (f) Element of bool the carrier of f
card cP is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() Element of omega
the carrier of (subrelstr n) is set
bool the carrier of (subrelstr n) is non empty set
P is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() set
P is finite ( subrelstr n) Element of bool the carrier of (subrelstr n)
card P is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() Element of omega
P is finite ( subrelstr n) Element of bool the carrier of (subrelstr n)
card P is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() Element of omega
{} (subrelstr n) is empty trivial Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional ext-real non positive non negative epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural finite finite-yielding with_finite-elements cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V49() real V51() complex-valued ext-real-valued real-valued natural-valued increasing decreasing non-decreasing non-increasing strongly_connected ( subrelstr n) ( subrelstr n) Element of bool the carrier of (subrelstr n)
card ({} (subrelstr n)) is empty trivial Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional ext-real non positive non negative epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural finite finite-yielding with_finite-elements cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V49() real V51() complex-valued ext-real-valued real-valued natural-valued increasing decreasing non-decreasing non-increasing Element of omega
P is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() set
P is finite ( subrelstr n) Element of bool the carrier of (subrelstr n)
card P is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() Element of omega
P is finite ( subrelstr n) Element of bool the carrier of (subrelstr n)
card P is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() Element of omega
A is finite ( subrelstr n) Element of bool the carrier of (subrelstr n)
card A is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() Element of omega
f is () RelStr
the carrier of f is set
bool the carrier of f is non empty set
n is Element of bool the carrier of f
subrelstr n is strict V147(f) SubRelStr of f
cP is finite (f) Element of bool the carrier of f
card cP is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() Element of omega
the carrier of (subrelstr n) is set
bool the carrier of (subrelstr n) is non empty set
{} (subrelstr n) is empty trivial Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional ext-real non positive non negative epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural finite finite-yielding with_finite-elements cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V49() real V51() complex-valued ext-real-valued real-valued natural-valued increasing decreasing non-decreasing non-increasing strongly_connected ( subrelstr n) ( subrelstr n) Element of bool the carrier of (subrelstr n)
iP is finite ( subrelstr n) Element of bool the carrier of (subrelstr n)
card iP is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() Element of omega
iP is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() set
iP + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() set
P is finite ( subrelstr n) Element of bool the carrier of (subrelstr n)
card P is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() Element of omega
P is finite ( subrelstr n) Element of bool the carrier of (subrelstr n)
card P is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() Element of omega
P is finite Element of bool the carrier of (subrelstr n)
card P is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() Element of omega
A is finite ( subrelstr n) Element of bool the carrier of (subrelstr n)
card A is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() Element of omega
g is finite ( subrelstr n) Element of bool the carrier of (subrelstr n)
card g is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() Element of omega
iP is finite ( subrelstr n) Element of bool the carrier of (subrelstr n)
card iP is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() Element of omega
P is finite ( subrelstr n) Element of bool the carrier of (subrelstr n)
card P is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() Element of omega
P is finite ( subrelstr n) Element of bool the carrier of (subrelstr n)
card P is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() Element of omega
f is non empty transitive antisymmetric () RelStr
the carrier of f is non empty set
[#] f is non empty non proper Element of bool the carrier of f
bool the carrier of f is non empty set
n is Element of the carrier of f
{n} is non empty trivial finite 1 -element (f) (f) Element of bool the carrier of f
(f,{n}) is Element of bool the carrier of f
downarrow {n} is Element of bool the carrier of f
{n} \/ (downarrow {n}) is non empty Element of bool the carrier of f
subrelstr (f,{n}) is strict transitive antisymmetric V147(f) () SubRelStr of f
P is non empty transitive antisymmetric () RelStr
(P) is non empty (P) Element of bool the carrier of P
the carrier of P is non empty set
bool the carrier of P is non empty set
P is set
[#] P is non empty non proper Element of bool the carrier of P
A is Element of the carrier of P
g is Element of the carrier of f
downarrow n is Element of bool the carrier of f
f is transitive antisymmetric () RelStr
(f) is (f) Element of bool the carrier of f
the carrier of f is set
bool the carrier of f is non empty set
(f,(f)) is Element of bool the carrier of f
uparrow (f) is Element of bool the carrier of f
(f) \/ (uparrow (f)) is Element of bool the carrier of f
[#] f is non proper Element of bool the carrier of f
iP is set
P is Element of the carrier of f
P is Element of the carrier of f
f is non empty transitive antisymmetric () RelStr
the carrier of f is non empty set
[#] f is non empty non proper Element of bool the carrier of f
bool the carrier of f is non empty set
n is Element of the carrier of f
{n} is non empty trivial finite 1 -element (f) (f) Element of bool the carrier of f
(f,{n}) is Element of bool the carrier of f
uparrow {n} is Element of bool the carrier of f
{n} \/ (uparrow {n}) is non empty Element of bool the carrier of f
subrelstr (f,{n}) is strict transitive antisymmetric V147(f) () SubRelStr of f
P is non empty transitive antisymmetric () RelStr
(P) is non empty (P) Element of bool the carrier of P
the carrier of P is non empty set
bool the carrier of P is non empty set
P is set
[#] P is non empty non proper Element of bool the carrier of P
A is Element of the carrier of P
g is Element of the carrier of f
uparrow n is Element of bool the carrier of f
f is transitive antisymmetric () RelStr
(f) is (f) Element of bool the carrier of f
the carrier of f is set
bool the carrier of f is non empty set
(f,(f)) is Element of bool the carrier of f
downarrow (f) is Element of bool the carrier of f
(f) \/ (downarrow (f)) is Element of bool the carrier of f
[#] f is non proper Element of bool the carrier of f
iP is set
P is Element of the carrier of f
P is Element of the carrier of f
f is transitive antisymmetric () RelStr
the carrier of f is set
bool the carrier of f is non empty set
(f) is (f) Element of bool the carrier of f
n is (f) Element of bool the carrier of f
cP is set
[#] f is non proper Element of bool the carrier of f
iP is Element of the carrier of f
P is Element of the carrier of f
f is transitive antisymmetric () RelStr
the carrier of f is set
bool the carrier of f is non empty set
(f) is (f) Element of bool the carrier of f
n is (f) Element of bool the carrier of f
cP is set
[#] f is non proper Element of bool the carrier of f
iP is Element of the carrier of f
P is Element of the carrier of f
f is () RelStr
the carrier of f is set
bool the carrier of f is non empty set
(f) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() set
n is Element of bool the carrier of f
subrelstr n is strict V147(f) () SubRelStr of f
((subrelstr n)) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() set
the carrier of (subrelstr n) is set
bool the carrier of (subrelstr n) is non empty set
iP is finite ( subrelstr n) Element of bool the carrier of (subrelstr n)
card iP is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() Element of omega
f is () RelStr
the carrier of f is set
bool the carrier of f is non empty set
(f) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() set
n is finite (f) Element of bool the carrier of f
card n is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() Element of omega
cP is Element of bool the carrier of f
subrelstr cP is strict V147(f) () SubRelStr of f
((subrelstr cP)) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() set
n /\ cP is finite Element of bool the carrier of f
the carrier of (subrelstr cP) is set
bool the carrier of (subrelstr cP) is non empty set
iP is finite ( subrelstr cP) Element of bool the carrier of (subrelstr cP)
card iP is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() Element of omega
f is () RelStr
the carrier of f is set
bool the carrier of f is non empty set
(f) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() set
n is Element of bool the carrier of f
subrelstr n is strict V147(f) () SubRelStr of f
((subrelstr n)) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() set
the carrier of (subrelstr n) is set
bool the carrier of (subrelstr n) is non empty set
cP is finite ( subrelstr n) Element of bool the carrier of (subrelstr n)
card cP is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() Element of omega
f is () RelStr
the carrier of f is set
bool the carrier of f is non empty set
(f) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() set
n is finite (f) Element of bool the carrier of f
card n is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() Element of omega
cP is Element of bool the carrier of f
subrelstr cP is strict V147(f) () SubRelStr of f
((subrelstr cP)) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() set
n /\ cP is finite Element of bool the carrier of f
the carrier of (subrelstr cP) is set
bool the carrier of (subrelstr cP) is non empty set
iP is finite ( subrelstr cP) Element of bool the carrier of (subrelstr cP)
card iP is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() Element of omega
f is RelStr
the carrier of f is set
f is RelStr
the carrier of f is set
cP is with_non-empty_elements a_partition of the carrier of f
bool the carrier of f is non empty set
iP is set
SmallestPartition the carrier of f is with_non-empty_elements a_partition of the carrier of f
cP is with_non-empty_elements a_partition of the carrier of f
iP is set
bool the carrier of f is non empty set
{ {b₁} where b₁ is Element of the carrier of f : verum } is set
P is Element of the carrier of f
{P} is non empty trivial finite 1 -element set
f is empty trivial finite {} -element () () RelStr
the carrier of f is empty trivial Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional ext-real non positive non negative epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural finite finite-yielding with_finite-elements cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V49() real V51() complex-valued ext-real-valued real-valued natural-valued increasing decreasing non-decreasing