:: DILWORTH semantic presentation

REAL is non empty non trivial non finite set

bool REAL is non empty non trivial non finite 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

{{},1} is non empty finite with_finite-elements set
K266(NAT) is V83() set
is non empty non trivial Relation-like non finite set
bool is non empty non trivial non finite set

is non empty non trivial Relation-like non finite set
bool is non empty non trivial non finite set
K662() is set
bool K662() is non empty set
K663() is Element of bool K662()
is non empty non trivial Relation-like non finite set
bool is non empty non trivial non finite set
is non empty non trivial Relation-like non finite set
bool is non empty non trivial non finite set
is non empty non trivial Relation-like non finite set
bool is non empty non trivial non finite set
is non empty non trivial Relation-like non finite set
bool is non empty non trivial non finite set
is non empty non trivial Relation-like non finite set
bool is non empty non trivial non finite set
is non empty non trivial Relation-like non finite set
bool is non empty non trivial non finite set
is non empty non trivial Relation-like non finite set
bool is non empty non trivial non finite set
is non empty non trivial Relation-like non finite set
is non empty non trivial Relation-like non finite set
bool is non empty non trivial non finite set

F2() is finite set
F1() is non empty finite set
{ F3(b1) where b1 is Element of F1() : P1[b1] } is set

{ F3(b1) where b1 is Element of F1() : b1 in F1() } is set
n is finite set

cP is set
iP is Element of F1()
F3(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 \/ 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 \/ {(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

[:NAT,f:] is non empty non trivial Relation-like non finite set
bool [:NAT,f:] is non empty non trivial non finite 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:]

rng P is non empty finite set

dom P is non empty finite Element of bool (Seg (n + 1))
bool (Seg (n + 1)) is non empty finite with_finite-elements set

P is finite Element of bool 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
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

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

iP is finite Element of bool n

P is finite (f) Element of bool the carrier of f

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

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

iP is finite Element of bool n

P is finite (f) 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
n is finite RelStr

the carrier of n is finite set

iP is finite (f) Element of bool the carrier of f

iP is finite (f) Element of bool the carrier of f

iP is finite (f) Element of bool the carrier of f

P is finite (f) 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
n is (f) Element of bool the carrier of f
cP is finite (f) Element of bool the carrier of f

bool n is non empty set
iP is finite Element of bool n

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

iP is finite (f) Element of bool the carrier of f

iP is finite (f) Element of bool the carrier of f

iP is finite (f) Element of bool the carrier of f

P is finite (f) Element of bool the carrier of f

P is finite (f) Element of bool the carrier of f

bool the carrier of f is non empty finite with_finite-elements set

f is non empty () RelStr

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

n is finite (f) Element of bool the carrier of f

cP is set
iP is set
f is () RelStr

[#] 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

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

iP is finite (n) Element of bool the carrier of n

the carrier of f is set
bool the carrier of f is non empty set

iP is finite (n) Element of bool the carrier of n

iP is finite (f) Element of bool the carrier of f

P is finite (f) 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
n is finite (f) Element of bool the carrier of f

cP is (f) Element of bool the carrier of f
bool cP is non empty set
iP is finite Element of bool cP

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

iP is finite (f) Element of bool the carrier of f

iP is finite (f) Element of bool the carrier of f

iP is finite (f) Element of bool the carrier of f

P is finite (f) Element of bool the carrier of f

P is finite (f) Element of bool the carrier of f

bool the carrier of f is non empty finite with_finite-elements set

f is non empty () RelStr

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

n is finite (f) Element of bool the carrier of f

cP is set
iP is set
f is () RelStr

[#] 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

f is RelStr
n is () () RelStr
the carrier of n is set
bool the carrier of n is non empty set

cP is finite (n) Element of bool the carrier of n

iP is finite (n) Element of bool the carrier of n

[#] n is non proper Element of bool the carrier of n
g is finite Element of bool the carrier of n

g is finite Element of bool the carrier of n

(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 finite Element of bool the carrier of n

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

{ {b1,b2} where b1, b2 is Element of the carrier of n : ( not b1 = b2 & b1 in e1 & b2 in e1 & ( b1 <= b2 or b2 <= b1 ) ) } is set
{ {b1,b2} where b1, b2 is Element of the carrier of n : ( not b1 = b2 & b1 in e1 & b2 in e1 & not b1 <= b2 & not b2 <= b1 ) } 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
{ b1 where b1 is Element of bool e1 : card b1 = 2 } is set
{ { {b1,b2} where b1, b2 is Element of the carrier of n : ( not b1 = b2 & b1 in e1 & b2 in e1 & ( b1 <= b2 or b2 <= b1 ) ) } , { {b1,b2} where b1, b2 is Element of the carrier of n : ( not b1 = b2 & b1 in e1 & b2 in e1 & not b1 <= b2 & not b2 <= b1 ) } } 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

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

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 { { {b1,b2} where b1, b2 is Element of the carrier of n : ( not b1 = b2 & b1 in e1 & b2 in e1 & ( b1 <= b2 or b2 <= b1 ) ) } , { {b1,b2} where b1, b2 is Element of the carrier of n : ( not b1 = b2 & b1 in e1 & b2 in e1 & not b1 <= b2 & not b2 <= b1 ) } } is set
j is set
r is set
j is set
r is finite Element of bool e1

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))
{ {b1,b2} where b1, b2 is Element of the carrier of n : ( not b1 = b2 & b1 in e1 & b2 in e1 & ( b1 <= b2 or b2 <= b1 ) ) } /\ { {b1,b2} where b1, b2 is Element of the carrier of n : ( not b1 = b2 & b1 in e1 & b2 in e1 & not b1 <= b2 & not b2 <= b1 ) } 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

r is finite Element of bool e1

s is finite Element of bool the carrier of n

bool (bool s) is non empty finite with_finite-elements set
{ b1 where b1 is Element of bool s : card b1 = 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

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

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 \/ () is Element of bool the carrier of f
uparrow n is Element of bool the carrier of f
n \/ () is Element of bool the carrier of f

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 \/ () 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 \/ () 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 non proper Element of bool the carrier of f
n is finite (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 \/ () 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 \/ () 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

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 \/ () is Element of bool the carrier of f
P is Element of the carrier of f
P is Element of the carrier of f

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

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

(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

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

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 \/ () 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 \/ () 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 () is set
bool the carrier of () is non empty set
cP is ( subrelstr n) Element of bool the carrier of ()
iP is Element of the carrier of f
P is Element of the carrier of f
P is Element of the carrier of ()
A is Element of the carrier of ()
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 () is set
bool the carrier of () 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 ()
A is Element of the carrier of ()
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 () is set
bool the carrier of () is non empty set
cP is ( subrelstr n) Element of bool the carrier of ()

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 ()
g is Element of the carrier of ()
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 () is set
bool the carrier of () 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 bool the carrier of ()
A is Element of the carrier of ()
g is Element of the carrier of ()
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 () is set
bool the carrier of () is non empty set
cP is Element of bool the carrier of ()
iP is Element of the carrier of ()
P is Element of the carrier of f
P is Element of the carrier of f
A is Element of the carrier of ()
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 () is set
bool the carrier of () is non empty set
cP is Element of bool the carrier of ()
iP is Element of the carrier of ()
P is Element of the carrier of f
P is Element of the carrier of f
A is Element of the carrier of ()

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 \/ () 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))

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 \/ () 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

the carrier of () is set
bool the carrier of () is non empty set

P is finite ( subrelstr n) Element of bool the carrier of ()

P is finite ( subrelstr n) Element of bool the carrier of ()

P is finite ( subrelstr n) Element of bool the carrier of ()

P is finite ( subrelstr n) Element of bool the carrier of ()

A is finite ( subrelstr n) Element of bool the carrier of ()

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

the carrier of () is set
bool the carrier of () is non empty set

iP is finite ( subrelstr n) Element of bool the carrier of ()

P is finite ( subrelstr n) Element of bool the carrier of ()

P is finite ( subrelstr n) Element of bool the carrier of ()

P is finite Element of bool the carrier of ()

A is finite ( subrelstr n) Element of bool the carrier of ()

g is finite ( subrelstr n) Element of bool the carrier of ()

iP is finite ( subrelstr n) Element of bool the carrier of ()

P is finite ( subrelstr n) Element of bool the carrier of ()

P is finite ( subrelstr n) Element of bool the carrier of ()

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} \/ () 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 (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} \/ () 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 (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

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

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

n is Element of bool the carrier of f
subrelstr n is strict V147(f) () SubRelStr of f

the carrier of () is set
bool the carrier of () is non empty set
iP is finite ( subrelstr n) Element of bool the carrier of ()

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

cP is Element of bool the carrier of f
subrelstr cP is strict V147(f) () SubRelStr of f

n /\ cP is finite Element of bool the carrier of f
the carrier of () is set
bool the carrier of () is non empty set
iP is finite ( subrelstr cP) Element of bool the carrier of ()

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 () is set
bool the carrier of () is non empty set
cP is finite ( subrelstr n) Element of bool the carrier of ()

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

cP is Element of bool the carrier of f
subrelstr cP is strict V147(f) () SubRelStr of f

n /\ cP is finite Element of bool the carrier of f
the carrier of () is set
bool the carrier of () is non empty set
iP is finite ( subrelstr cP) Element of bool the carrier of ()

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
{ {b1} where b1 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