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

F

{ F

card F

card F

{ F

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

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

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

{ { {b

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

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

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

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

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