:: ARMSTRNG semantic presentation

REAL is non empty non trivial non finite set
NAT is non empty non trivial V29() V30() V31() non finite cardinal limit_cardinal countable denumerable Element of bool REAL
bool REAL is non empty non trivial non finite set
NAT is non empty non trivial V29() V30() V31() non finite cardinal limit_cardinal countable denumerable set
bool NAT 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
[:NAT,REAL:] is non empty non trivial Relation-like non finite set
bool [:NAT,REAL:] 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:] is non empty non trivial Relation-like non finite set
bool [:REAL,REAL:] 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:] is non empty non trivial Relation-like non finite set
bool [:INT,INT:] 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
BOOLEAN is non empty set
1 is non empty ext-real positive non negative V29() V30() V31() V35() finite cardinal V48() V49() countable Element of NAT
[:1,1:] is non empty Relation-like finite countable set
bool [:1,1:] is non empty finite V40() countable set
[:[:1,1:],1:] is non empty Relation-like finite countable set
bool [:[:1,1:],1:] is non empty finite V40() countable set
[:[:1,1:],REAL:] is non empty non trivial Relation-like non finite set
bool [:[:1,1:],REAL:] is non empty non trivial non finite set
2 is non empty ext-real positive non negative V29() V30() V31() V35() finite cardinal V48() V49() countable Element of NAT
[:2,2:] is non empty Relation-like finite countable set
[:[:2,2:],REAL:] is non empty non trivial Relation-like non finite set
bool [:[:2,2:],REAL:] is non empty non trivial non finite set
TOP-REAL 2 is V177() L15()
the carrier of (TOP-REAL 2) is set
{} is empty ext-real non positive non negative Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional Function-yielding V28() V29() V30() V31() V33() V34() V35() finite finite-yielding V40() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V48() V49() Cardinal-yielding with_common_domain countable FinSequence-yielding finite-support set
3 is non empty ext-real positive non negative V29() V30() V31() V35() finite cardinal V48() V49() countable Element of NAT
0 is empty ext-real non positive non negative Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional Function-yielding V28() V29() V30() V31() V33() V34() V35() finite finite-yielding V40() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V48() V49() Cardinal-yielding with_common_domain countable FinSequence-yielding finite-support Element of NAT
proj1 {} is empty ext-real non positive non negative Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional Function-yielding V28() V29() V30() V31() V33() V34() V35() finite finite-yielding V40() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V48() V49() Cardinal-yielding with_common_domain countable FinSequence-yielding finite-support set
proj2 {} is empty trivial with_non-empty_elements ext-real non positive non negative Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional Function-yielding V28() V29() V30() V31() V33() V34() V35() finite finite-yielding V40() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V48() V49() Cardinal-yielding with_common_domain countable FinSequence-yielding finite-support set
Seg 1 is non empty trivial finite 1 -element countable Element of bool NAT
FALSE is boolean Element of BOOLEAN
<*FALSE*> is non empty trivial Relation-like NAT -defined BOOLEAN -valued Function-like constant finite 1 -element FinSequence-like FinSubsequence-like countable finite-support FinSequence of BOOLEAN
<*1*> is non empty trivial Relation-like NAT -defined NAT -valued Function-like constant finite 1 -element FinSequence-like FinSubsequence-like Cardinal-yielding countable finite-support FinSequence of NAT
X is ext-real non negative V29() V30() V31() V35() finite cardinal V48() V49() countable Element of NAT
F is non empty set
K is Relation-like NAT -defined F -valued Function-like finite X -element FinSequence-like FinSubsequence-like countable finite-support FinSequence of F
len K is ext-real non negative V29() V30() V31() V35() finite cardinal V48() V49() countable Element of NAT
dom K is finite X -element countable Element of bool NAT
Seg X is finite X -element countable Element of bool NAT
F is non empty set
X is ext-real non negative V29() V30() V31() V35() finite cardinal V48() V49() countable Element of NAT
X -tuples_on F is non empty functional FinSequence-membered FinSequenceSet of F
F * is non empty functional FinSequence-membered FinSequenceSet of F
{ b₁ where b₁ is Relation-like NAT -defined F -valued Function-like finite FinSequence-like FinSubsequence-like countable finite-support Element of F * : len b₁ = X } is set
K is Relation-like NAT -defined F -valued Function-like finite X -element FinSequence-like FinSubsequence-like countable finite-support Element of X -tuples_on F
len K is ext-real non negative V29() V30() V31() V35() finite cardinal V48() V49() countable Element of NAT
dom K is finite X -element countable Element of bool NAT
Seg X is finite X -element countable Element of bool NAT
X is set
F is set
bool F is non empty set
bool (bool F) is non empty set
K is finite countable Element of bool (bool F)
Intersect K is Element of bool F
dcF is set
S is set
{dcF} is non empty trivial finite 1 -element countable set
S \/ {dcF} is non empty set
ck is Element of bool (bool F)
S is Element of bool (bool F)
ck \/ S is Element of bool (bool F)
Intersect (ck \/ S) is Element of bool F
Intersect ck is Element of bool F
Intersect S is Element of bool F
(Intersect ck) /\ (Intersect S) is Element of bool F
B is Element of bool F
(Intersect ck) /\ B is Element of bool F
m is Element of bool (bool F)
Intersect m is Element of bool F
dcF is Element of bool (bool F)
Intersect dcF is Element of bool F
[{},{}] is V21() set
{{},{}} is non empty functional finite V40() countable set
{{}} is non empty trivial functional finite V40() 1 -element with_common_domain countable set
{{{},{}},{{}}} is non empty finite V40() countable set
{[{},{}]} is non empty trivial Relation-like Function-like constant finite 1 -element countable finite-support set
F is Relation-like set
field F is set
K is set
[K,K] is V21() set
{K,K} is non empty finite countable set
{K} is non empty trivial finite 1 -element countable set
{{K,K},{K}} is non empty finite V40() countable set
K is set
dcF is set
[K,dcF] is V21() set
{K,dcF} is non empty finite countable set
{K} is non empty trivial finite 1 -element countable set
{{K,dcF},{K}} is non empty finite V40() countable set
[dcF,K] is V21() set
{dcF,K} is non empty finite countable set
{dcF} is non empty trivial finite 1 -element countable set
{{dcF,K},{dcF}} is non empty finite V40() countable set
K is set
dcF is set
S is set
[K,dcF] is V21() set
{K,dcF} is non empty finite countable set
{K} is non empty trivial finite 1 -element countable set
{{K,dcF},{K}} is non empty finite V40() countable set
[dcF,S] is V21() set
{dcF,S} is non empty finite countable set
{dcF} is non empty trivial finite 1 -element countable set
{{dcF,S},{dcF}} is non empty finite V40() countable set
[K,S] is V21() set
{K,S} is non empty finite countable set
{{K,S},{K}} is non empty finite V40() countable set
X is non empty Relation-like antisymmetric transitive set
field X is set
bool (field X) is non empty set
F is finite countable Element of bool (field X)
[:(field X),(field X):] is Relation-like set
bool [:(field X),(field X):] is non empty set
K is Relation-like field X -defined field X -valued Element of bool [:(field X),(field X):]
RelStr(# (field X),K #) is strict RelStr
the carrier of RelStr(# (field X),K #) is set
the InternalRel of RelStr(# (field X),K #) is Relation-like the carrier of RelStr(# (field X),K #) -defined the carrier of RelStr(# (field X),K #) -valued Element of bool [: the carrier of RelStr(# (field X),K #), the carrier of RelStr(# (field X),K #):]
[: the carrier of RelStr(# (field X),K #), the carrier of RelStr(# (field X),K #):] is Relation-like set
bool [: the carrier of RelStr(# (field X),K #), the carrier of RelStr(# (field X),K #):] is non empty set
ck is Element of the carrier of RelStr(# (field X),K #)
B is Element of the carrier of RelStr(# (field X),K #)
m is Element of the carrier of RelStr(# (field X),K #)
[B,m] is V21() set
{B,m} is non empty finite countable set
{B} is non empty trivial finite 1 -element countable set
{{B,m},{B}} is non empty finite V40() countable set
[ck,B] is V21() set
{ck,B} is non empty finite countable set
{ck} is non empty trivial finite 1 -element countable set
{{ck,B},{ck}} is non empty finite V40() countable set
[ck,m] is V21() set
{ck,m} is non empty finite countable set
{{ck,m},{ck}} is non empty finite V40() countable set
ck is Element of the carrier of RelStr(# (field X),K #)
B is Element of the carrier of RelStr(# (field X),K #)
[B,ck] is V21() set
{B,ck} is non empty finite countable set
{B} is non empty trivial finite 1 -element countable set
{{B,ck},{B}} is non empty finite V40() countable set
[ck,B] is V21() set
{ck,B} is non empty finite countable set
{ck} is non empty trivial finite 1 -element countable set
{{ck,B},{ck}} is non empty finite V40() countable set
bool the carrier of RelStr(# (field X),K #) is non empty set
ck is non empty transitive antisymmetric RelStr
the carrier of ck is non empty set
B is finite countable Element of bool the carrier of RelStr(# (field X),K #)
the InternalRel of ck is Relation-like the carrier of ck -defined the carrier of ck -valued Element of bool [: the carrier of ck, the carrier of ck:]
[: the carrier of ck, the carrier of ck:] is non empty Relation-like set
bool [: the carrier of ck, the carrier of ck:] is non empty set
m is Element of the carrier of ck
P is Element of F
x9 is set
[P,x9] is V21() set
{P,x9} is non empty finite countable set
{P} is non empty trivial finite 1 -element countable set
{{P,x9},{P}} is non empty finite V40() countable set
F₁() is set
bool F₁() is non empty set
X is Element of bool F₁()
F is Element of bool F₁()
K is set
X is set
bool X is non empty set
F is Relation-like set
K is set
dcF is set
dcF is Element of bool X
S is set
X is non empty set
bool X is non empty set
{ b₁ where b₁ is Element of X : (b₁,X) } is set
K is set
dcF is Element of X
K is Element of bool X
dcF is set
S is Element of X
F₁() is non empty finite countable set
{ b₁ where b₁ is Element of F₁() : a₁ c= b₁ } is set
X is set
{ b₁ where b₁ is Element of F₁() : X c= b₁ } is set
F is set
K is Element of F₁()
F is finite countable set
card F is ext-real non negative V29() V30() V31() V35() finite cardinal V48() V49() countable Element of NAT
dcF is ext-real non negative V29() V30() V31() V35() finite cardinal V48() V49() countable Element of NAT
K is Element of F₁()
{ b₁ where b₁ is Element of F₁() : K c= b₁ } is set
card H₁(K) is V29() V30() V31() cardinal set
K is ext-real non negative V29() V30() V31() V35() finite cardinal V48() V49() countable set
dcF is Element of F₁()
{ b₁ where b₁ is Element of F₁() : dcF c= b₁ } is set
card { b₁ where b₁ is Element of F₁() : dcF c= b₁ } is V29() V30() V31() cardinal set
dcF is Element of F₁()
{ b₁ where b₁ is Element of F₁() : dcF c= b₁ } is set
card H₁(dcF) is V29() V30() V31() cardinal set
S is set
S is Element of F₁()
S is set
ck is set
S /\ ck is set
{ b₁ where b₁ is Element of F₁() : S c= b₁ } is set
B is set
m is Element of F₁()
{ b₁ where b₁ is Element of F₁() : ck c= b₁ } is set
m is set
P is Element of F₁()
m is finite countable set
S is finite countable set
y9 is set
P is Element of F₁()
a is Element of F₁()
P is Element of F₁()
y9 is Element of F₁()
card S is ext-real non negative V29() V30() V31() V35() finite cardinal V48() V49() countable Element of NAT
card m is ext-real non negative V29() V30() V31() V35() finite cardinal V48() V49() countable Element of NAT
B is finite countable set
y9 is set
x9 is Element of F₁()
a is Element of F₁()
x9 is Element of F₁()
y9 is Element of F₁()
card B is ext-real non negative V29() V30() V31() V35() finite cardinal V48() V49() countable Element of NAT
X is non empty finite countable set
bool X is non empty finite V40() countable set
F is Element of X
K is set
dcF is set
S is non empty finite countable Element of bool X
meet S is set
S is non empty finite countable Element of bool X
meet S is set
S is non empty finite countable Element of bool X
meet S is set
S is non empty finite countable Element of bool X
meet S is set
S \/ S is non empty finite countable Element of bool X
ck is non empty finite countable Element of bool X
K /\ dcF is set
B is non empty finite countable Element of bool X
meet B is set
m is set
B is non empty finite countable Element of bool X
meet B is set
K is set
{K} is non empty trivial finite 1 -element countable set
dcF is non empty finite countable Element of bool X
meet dcF is set
S is set
X is set
bool X is non empty set
bool (bool X) is non empty set
X is set
bool X is non empty set
bool (bool X) is non empty set
{X} is non empty trivial finite 1 -element countable set
K is Element of bool (bool X)
dcF is set
S is set
dcF /\ S is set
X is set
bool X is non empty set
bool (bool X) is non empty set
F is non empty Element of bool (bool X)
K is Element of F
dcF is finite countable Element of bool (bool X)
Intersect dcF is Element of bool X
S is set
S is set
{S} is non empty trivial finite 1 -element countable set
S \/ {S} is non empty set
ck is Element of F
B is Element of F
ck /\ B is Element of bool X
ck is Element of bool (bool X)
Intersect ck is Element of bool X
ck is Element of bool (bool X)
Intersect ck is Element of bool X
{S} is non empty trivial finite 1 -element countable set
S \/ {S} is non empty set
B is Element of bool (bool X)
Intersect B is Element of bool X
meet B is Element of bool X
S \/ B is set
m is non empty Element of bool (bool X)
Intersect m is Element of bool X
meet m is Element of bool X
meet S is set
(meet S) /\ (meet B) is Element of bool X
meet ck is Element of bool X
ck is Element of F
B is Element of F
ck /\ B is Element of bool X
m is Element of bool (bool X)
Intersect m is Element of bool X
S is Element of F
S is Element of F
S /\ S is Element of bool X
ck is Element of bool (bool X)
Intersect ck is Element of bool X
X is non empty set
K is ext-real non negative V29() V30() V31() V35() finite cardinal V48() V49() countable Element of NAT
F is non empty set
K -tuples_on F is non empty functional FinSequence-membered FinSequenceSet of F
F * is non empty functional FinSequence-membered FinSequenceSet of F
{ b₁ where b₁ is Relation-like NAT -defined F -valued Function-like finite FinSequence-like FinSubsequence-like countable finite-support Element of F * : len b₁ = K } is set
[:X,(K -tuples_on F):] is non empty Relation-like set
bool [:X,(K -tuples_on F):] is non empty set
dcF is Relation-like X -defined K -tuples_on F -valued Function-like V24(X,K -tuples_on F) Function-yielding V28() Element of bool [:X,(K -tuples_on F):]
S is set
proj1 dcF is set
dcF . S is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like countable finite-support set
dom dcF is Element of bool X
bool X is non empty set
X is Relation-like Function-like Function-yielding V28() FinSequence-yielding set
F is set
X . F is Relation-like Function-like set
proj1 X is set
proj1 X is set
proj1 X is set
X is ext-real non negative V29() V30() V31() V35() finite cardinal V48() V49() countable Element of NAT
Seg X is finite X -element countable Element of bool NAT
F is Relation-like NAT -defined BOOLEAN -valued Function-like finite X -element FinSequence-like FinSubsequence-like countable finite-support FinSequence of BOOLEAN
K is Relation-like NAT -defined BOOLEAN -valued Function-like finite X -element FinSequence-like FinSubsequence-like countable finite-support FinSequence of BOOLEAN
dcF is Relation-like NAT -defined BOOLEAN -valued Function-like finite FinSequence-like FinSubsequence-like countable finite-support FinSequence of BOOLEAN
len dcF is ext-real non negative V29() V30() V31() V35() finite cardinal V48() V49() countable Element of NAT
dom dcF is finite countable Element of bool NAT
BOOLEAN * is non empty functional FinSequence-membered FinSequenceSet of BOOLEAN
X -tuples_on BOOLEAN is non empty functional FinSequence-membered FinSequenceSet of BOOLEAN
{ b₁ where b₁ is Relation-like NAT -defined BOOLEAN -valued Function-like finite FinSequence-like FinSubsequence-like countable finite-support Element of BOOLEAN * : len b₁ = X } is set
S is Relation-like NAT -defined BOOLEAN -valued Function-like finite X -element FinSequence-like FinSubsequence-like countable finite-support Element of X -tuples_on BOOLEAN
S is set
S . S is set
F /. S is boolean Element of BOOLEAN
K /. S is boolean Element of BOOLEAN
(F /. S) '&' (K /. S) is boolean Element of BOOLEAN
K161((F /. S),(K /. S)) is set
dcF is Relation-like NAT -defined BOOLEAN -valued Function-like finite X -element FinSequence-like FinSubsequence-like countable finite-support FinSequence of BOOLEAN
S is Relation-like NAT -defined BOOLEAN -valued Function-like finite X -element FinSequence-like FinSubsequence-like countable finite-support FinSequence of BOOLEAN
dom dcF is finite X -element countable Element of bool NAT
dom S is finite X -element countable Element of bool NAT
S is set
dcF . S is set
F /. S is boolean Element of BOOLEAN
K /. S is boolean Element of BOOLEAN
(F /. S) '&' (K /. S) is boolean Element of BOOLEAN
K161((F /. S),(K /. S)) is set
S . S is set
dcF is Relation-like NAT -defined BOOLEAN -valued Function-like finite X -element FinSequence-like FinSubsequence-like countable finite-support FinSequence of BOOLEAN
S is Relation-like NAT -defined BOOLEAN -valued Function-like finite X -element FinSequence-like FinSubsequence-like countable finite-support FinSequence of BOOLEAN
S is Relation-like NAT -defined BOOLEAN -valued Function-like finite X -element FinSequence-like FinSubsequence-like countable finite-support FinSequence of BOOLEAN
ck is set
dcF . ck is set
S /. ck is boolean Element of BOOLEAN
S /. ck is boolean Element of BOOLEAN
(S /. ck) '&' (S /. ck) is boolean Element of BOOLEAN
K161((S /. ck),(S /. ck)) is set
X is ext-real non negative V29() V30() V31() V35() finite cardinal V48() V49() countable Element of NAT
X -tuples_on BOOLEAN is non empty functional FinSequence-membered FinSequenceSet of BOOLEAN
BOOLEAN * is non empty functional FinSequence-membered FinSequenceSet of BOOLEAN
{ b₁ where b₁ is Relation-like NAT -defined BOOLEAN -valued Function-like finite FinSequence-like FinSubsequence-like countable finite-support Element of BOOLEAN * : len b₁ = X } is set
X -BinarySequence 0 is Relation-like NAT -defined BOOLEAN -valued Function-like finite X -element FinSequence-like FinSubsequence-like countable finite-support FinSequence of BOOLEAN
F is Relation-like NAT -defined BOOLEAN -valued Function-like finite X -element FinSequence-like FinSubsequence-like countable finite-support Element of X -tuples_on BOOLEAN
(X,(X -BinarySequence 0),F) is Relation-like NAT -defined BOOLEAN -valued Function-like finite X -element FinSequence-like FinSubsequence-like countable finite-support FinSequence of BOOLEAN
dom (X -BinarySequence 0) is finite X -element countable Element of bool NAT
Seg X is finite X -element countable Element of bool NAT
dom (X,(X -BinarySequence 0),F) is finite X -element countable Element of bool NAT
S is set
0* X is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like countable finite-support Element of REAL X
REAL X is functional FinSequence-membered FinSequenceSet of REAL
X |-> 0 is Relation-like empty-yielding NAT -defined NAT -valued Function-like Function-yielding V28() finite X -element FinSequence-like FinSubsequence-like Cardinal-yielding countable FinSequence-yielding finite-support Element of X -tuples_on NAT
X -tuples_on NAT is non empty functional FinSequence-membered FinSequenceSet of NAT
NAT * is non empty functional FinSequence-membered FinSequenceSet of NAT
{ b₁ where b₁ is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like countable finite-support Element of NAT * : len b₁ = X } is set
(Seg X) --> 0 is Relation-like Seg X -defined Seg X -defined NAT -valued {0} -valued Function-like constant total total V24( Seg X,{0}) Function-yielding V28() finite FinSequence-like FinSubsequence-like Cardinal-yielding countable finite-support Element of bool [:(Seg X),{0}:]
{0} is non empty trivial functional finite V40() 1 -element with_common_domain countable set
[:(Seg X),{0}:] is Relation-like finite countable set
bool [:(Seg X),{0}:] is non empty finite V40() countable set
(X -BinarySequence 0) . S is set
(X -BinarySequence 0) /. S is boolean Element of BOOLEAN
(X,(X -BinarySequence 0),F) . S is set
F /. S is boolean Element of BOOLEAN
FALSE '&' (F /. S) is boolean Element of BOOLEAN
K161(FALSE,(F /. S)) is set
X is ext-real non negative V29() V30() V31() V35() finite cardinal V48() V49() countable Element of NAT
X -BinarySequence 0 is Relation-like NAT -defined BOOLEAN -valued Function-like finite X -element FinSequence-like FinSubsequence-like countable finite-support FinSequence of BOOLEAN
'not' (X -BinarySequence 0) is Relation-like NAT -defined BOOLEAN -valued Function-like finite X -element FinSequence-like FinSubsequence-like countable finite-support FinSequence of BOOLEAN
F is Relation-like NAT -defined BOOLEAN -valued Function-like finite X -element FinSequence-like FinSubsequence-like countable finite-support FinSequence of BOOLEAN
(X,('not' (X -BinarySequence 0)),F) is Relation-like NAT -defined BOOLEAN -valued Function-like finite X -element FinSequence-like FinSubsequence-like countable finite-support FinSequence of BOOLEAN
dom (X -BinarySequence 0) is finite X -element countable Element of bool NAT
Seg X is finite X -element countable Element of bool NAT
dom (X,('not' (X -BinarySequence 0)),F) is finite X -element countable Element of bool NAT
dom F is finite X -element countable Element of bool NAT
S is set
0* X is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like countable finite-support Element of REAL X
REAL X is functional FinSequence-membered FinSequenceSet of REAL
X |-> 0 is Relation-like empty-yielding NAT -defined NAT -valued Function-like Function-yielding V28() finite X -element FinSequence-like FinSubsequence-like Cardinal-yielding countable FinSequence-yielding finite-support Element of X -tuples_on NAT
X -tuples_on NAT is non empty functional FinSequence-membered FinSequenceSet of NAT
NAT * is non empty functional FinSequence-membered FinSequenceSet of NAT
{ b₁ where b₁ is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like countable finite-support Element of NAT * : len b₁ = X } is set
(Seg X) --> 0 is Relation-like Seg X -defined Seg X -defined NAT -valued {0} -valued Function-like constant total total V24( Seg X,{0}) Function-yielding V28() finite FinSequence-like FinSubsequence-like Cardinal-yielding countable finite-support Element of bool [:(Seg X),{0}:]
{0} is non empty trivial functional finite V40() 1 -element with_common_domain countable set
[:(Seg X),{0}:] is Relation-like finite countable set
bool [:(Seg X),{0}:] is non empty finite V40() countable set
(X -BinarySequence 0) . S is set
(X -BinarySequence 0) /. S is boolean Element of BOOLEAN
('not' (X -BinarySequence 0)) /. S is boolean Element of BOOLEAN
ck is ext-real non negative V29() V30() V31() V35() finite cardinal V48() V49() countable Element of NAT
(X -BinarySequence 0) /. ck is boolean Element of BOOLEAN
'not' ((X -BinarySequence 0) /. ck) is boolean Element of BOOLEAN
K164(1,((X -BinarySequence 0) /. ck)) is set
TRUE is boolean Element of BOOLEAN
(X,('not' (X -BinarySequence 0)),F) . S is set
F /. S is boolean Element of BOOLEAN
TRUE '&' (F /. S) is boolean Element of BOOLEAN
K161(TRUE,(F /. S)) is set
F . S is set
X is ext-real non negative V29() V30() V31() V35() finite cardinal V48() V49() countable Element of NAT
F is ext-real non negative V29() V30() V31() V35() finite cardinal V48() V49() countable Element of NAT
2 to_power F is ext-real non negative V29() V30() V31() V35() finite cardinal V48() V49() countable Element of NAT
X -BinarySequence (2 to_power F) is Relation-like NAT -defined BOOLEAN -valued Function-like finite X -element FinSequence-like FinSubsequence-like countable finite-support FinSequence of BOOLEAN
F + 1 is non empty ext-real positive non negative V29() V30() V31() V35() finite cardinal V48() V49() countable Element of NAT
(X -BinarySequence (2 to_power F)) . (F + 1) is set
Seg X is finite X -element countable Element of bool NAT
TRUE is boolean Element of BOOLEAN
dcF is ext-real non negative V29() V30() V31() V35() finite cardinal V48() V49() countable Element of NAT
dcF -BinarySequence (2 to_power F) is Relation-like NAT -defined BOOLEAN -valued Function-like finite dcF -element FinSequence-like FinSubsequence-like countable finite-support FinSequence of BOOLEAN
H₁(dcF) . (F + 1) is set
dcF + 1 is non empty ext-real positive non negative V29() V30() V31() V35() finite cardinal V48() V49() countable Element of NAT
0* dcF is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like countable finite-support Element of REAL dcF
REAL dcF is functional FinSequence-membered FinSequenceSet of REAL
dcF |-> 0 is Relation-like empty-yielding NAT -defined NAT -valued Function-like Function-yielding V28() finite dcF -element FinSequence-like FinSubsequence-like Cardinal-yielding countable FinSequence-yielding finite-support Element of dcF -tuples_on NAT
dcF -tuples_on NAT is non empty functional FinSequence-membered FinSequenceSet of NAT
NAT * is non empty functional FinSequence-membered FinSequenceSet of NAT
{ b₁ where b₁ is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like countable finite-support Element of NAT * : len b₁ = dcF } is set
Seg dcF is finite dcF -element countable Element of bool NAT
(Seg dcF) --> 0 is Relation-like Seg dcF -defined Seg dcF -defined NAT -valued {0} -valued Function-like constant total total V24( Seg dcF,{0}) Function-yielding V28() finite FinSequence-like FinSubsequence-like Cardinal-yielding countable finite-support Element of bool [:(Seg dcF),{0}:]
{0} is non empty trivial functional finite V40() 1 -element with_common_domain countable set
[:(Seg dcF),{0}:] is Relation-like finite countable set
bool [:(Seg dcF),{0}:] is non empty finite V40() countable set
dom (0* dcF) is finite countable Element of bool NAT
len (0* dcF) is ext-real non negative V29() V30() V31() V35() finite cardinal V48() V49() countable Element of NAT
<*TRUE*> is non empty trivial Relation-like NAT -defined BOOLEAN -valued Function-like constant finite 1 -element FinSequence-like FinSubsequence-like countable finite-support Element of BOOLEAN *
BOOLEAN * is non empty functional FinSequence-membered FinSequenceSet of BOOLEAN
dom <*TRUE*> is non empty trivial finite 1 -element countable Element of bool NAT
(dcF + 1) -BinarySequence (2 to_power F) is Relation-like NAT -defined BOOLEAN -valued Function-like finite dcF + 1 -element FinSequence-like FinSubsequence-like countable finite-support FinSequence of BOOLEAN
H₁(dcF + 1) . (F + 1) is set
(0* dcF) ^ <*TRUE*> is non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like countable finite-support set
((0* dcF) ^ <*TRUE*>) . (F + 1) is set
<*TRUE*> . 1 is set
0* dcF is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like countable finite-support Element of REAL dcF
REAL dcF is functional FinSequence-membered FinSequenceSet of REAL
dcF |-> 0 is Relation-like empty-yielding NAT -defined NAT -valued Function-like Function-yielding V28() finite dcF -element FinSequence-like FinSubsequence-like Cardinal-yielding countable FinSequence-yielding finite-support Element of dcF -tuples_on NAT
dcF -tuples_on NAT is non empty functional FinSequence-membered FinSequenceSet of NAT
NAT * is non empty functional FinSequence-membered FinSequenceSet of NAT
{ b₁ where b₁ is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like countable finite-support Element of NAT * : len b₁ = dcF } is set
Seg dcF is finite dcF -element countable Element of bool NAT
(Seg dcF) --> 0 is Relation-like Seg dcF -defined Seg dcF -defined NAT -valued {0} -valued Function-like constant total total V24( Seg dcF,{0}) Function-yielding V28() finite FinSequence-like FinSubsequence-like Cardinal-yielding countable finite-support Element of bool [:(Seg dcF),{0}:]
{0} is non empty trivial functional finite V40() 1 -element with_common_domain countable set
[:(Seg dcF),{0}:] is Relation-like finite countable set
bool [:(Seg dcF),{0}:] is non empty finite V40() countable set
dom (0* dcF) is finite countable Element of bool NAT
len (0* dcF) is ext-real non negative V29() V30() V31() V35() finite cardinal V48() V49() countable Element of NAT
<*TRUE*> is non empty trivial Relation-like NAT -defined BOOLEAN -valued Function-like constant finite 1 -element FinSequence-like FinSubsequence-like countable finite-support Element of BOOLEAN *
BOOLEAN * is non empty functional FinSequence-membered FinSequenceSet of BOOLEAN
dom <*TRUE*> is non empty trivial finite 1 -element countable Element of bool NAT
(dcF + 1) -BinarySequence (2 to_power F) is Relation-like NAT -defined BOOLEAN -valued Function-like finite dcF + 1 -element FinSequence-like FinSubsequence-like countable finite-support FinSequence of BOOLEAN
H₁(dcF + 1) . (F + 1) is set
(0* dcF) ^ <*TRUE*> is non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like countable finite-support set
((0* dcF) ^ <*TRUE*>) . (F + 1) is set
<*TRUE*> . 1 is set
0 + 1 is non empty ext-real positive non negative V29() V30() V31() V35() finite cardinal V48() V49() countable Element of NAT
Seg dcF is finite dcF -element countable Element of bool NAT
dom H₁(dcF) is finite dcF -element countable Element of bool NAT
2 to_power dcF is ext-real non negative V29() V30() V31() V35() finite cardinal V48() V49() countable Element of NAT
(dcF + 1) -BinarySequence (2 to_power F) is Relation-like NAT -defined BOOLEAN -valued Function-like finite dcF + 1 -element FinSequence-like FinSubsequence-like countable finite-support FinSequence of BOOLEAN
H₁(dcF + 1) . (F + 1) is set
S is non empty ext-real positive non negative V29() V30() V31() V35() finite cardinal V48() V49() countable Element of NAT
S -BinarySequence (2 to_power F) is Relation-like NAT -defined BOOLEAN -valued Function-like finite S -element FinSequence-like FinSubsequence-like countable finite-support FinSequence of BOOLEAN
<*FALSE*> is non empty trivial Relation-like NAT -defined BOOLEAN -valued Function-like constant finite 1 -element FinSequence-like FinSubsequence-like countable finite-support Element of BOOLEAN *
BOOLEAN * is non empty functional FinSequence-membered FinSequenceSet of BOOLEAN
H₁(S) ^ <*FALSE*> is non empty Relation-like NAT -defined BOOLEAN -valued Function-like finite S + 1 -element K288(S,1) -element FinSequence-like FinSubsequence-like countable finite-support FinSequence of BOOLEAN
K288(S,1) is non empty ext-real positive non negative V29() V30() V31() V35() finite cardinal V48() V49() countable Element of NAT
S + 1 is non empty ext-real positive non negative V29() V30() V31() V35() finite cardinal V48() V49() countable Element of NAT
(H₁(S) ^ <*FALSE*>) . (F + 1) is set
(dcF + 1) -BinarySequence (2 to_power F) is Relation-like NAT -defined BOOLEAN -valued Function-like finite dcF + 1 -element FinSequence-like FinSubsequence-like countable finite-support FinSequence of BOOLEAN
H₁(dcF + 1) . (F + 1) is set
(dcF + 1) -BinarySequence (2 to_power F) is Relation-like NAT -defined BOOLEAN -valued Function-like finite dcF + 1 -element FinSequence-like FinSubsequence-like countable finite-support FinSequence of BOOLEAN
H₁(dcF + 1) . (F + 1) is set
0 -BinarySequence (2 to_power F) is empty proper ext-real non positive non negative Relation-like non-empty empty-yielding NAT -defined BOOLEAN -valued Function-like one-to-one constant functional Function-yielding V28() V29() V30() V31() V33() V34() V35() finite finite-yielding V40() cardinal 0 -element FinSequence-like FinSubsequence-like FinSequence-membered V48() V49() Cardinal-yielding with_common_domain countable FinSequence-yielding finite-support FinSequence of BOOLEAN
[:NAT,BOOLEAN:] is non empty non trivial Relation-like non finite set
H₁( 0 ) . (F + 1) is set
dcF is ext-real non negative V29() V30() V31() V35() finite cardinal V48() V49() countable Element of NAT
(X -BinarySequence (2 to_power F)) . dcF is set
S is ext-real non negative V29() V30() V31() V35() finite cardinal V48() V49() countable Element of NAT
S -BinarySequence (2 to_power F) is Relation-like NAT -defined BOOLEAN -valued Function-like finite S -element FinSequence-like FinSubsequence-like countable finite-support FinSequence of BOOLEAN
S + 1 is non empty ext-real positive non negative V29() V30() V31() V35() finite cardinal V48() V49() countable Element of NAT
0 + 1 is non empty ext-real positive non negative V29() V30() V31() V35() finite cardinal V48() V49() countable Element of NAT
S is ext-real non negative V29() V30() V31() V35() finite cardinal V48() V49() countable Element of NAT
(S + 1) -BinarySequence (2 to_power F) is Relation-like NAT -defined BOOLEAN -valued Function-like finite S + 1 -element FinSequence-like FinSubsequence-like countable finite-support FinSequence of BOOLEAN
dom H₁(S + 1) is finite S + 1 -element countable Element of bool NAT
Seg (S + 1) is non empty finite S + 1 -element S + 1 -element countable Element of bool NAT
S + 1 is non empty ext-real positive non negative V29() V30() V31() V35() finite cardinal V48() V49() countable Element of NAT
S + 1 is non empty ext-real positive non negative V29() V30() V31() V35() finite cardinal V48() V49() countable Element of NAT
H₁(S + 1) . (S + 1) is set
(S + 1) -BinarySequence (2 to_power F) is Relation-like NAT -defined BOOLEAN -valued Function-like finite S + 1 -element FinSequence-like FinSubsequence-like countable finite-support FinSequence of BOOLEAN
dom H₁(S + 1) is finite S + 1 -element countable Element of bool NAT
Seg (S + 1) is non empty finite S + 1 -element S + 1 -element countable Element of bool NAT
S + 1 is non empty ext-real positive non negative V29() V30() V31() V35() finite cardinal V48() V49() countable Element of NAT
S + 1 is non empty ext-real positive non negative V29() V30() V31() V35() finite cardinal V48() V49() countable Element of NAT
H₁(S + 1) . (S + 1) is set
2 to_power S is ext-real non negative V29() V30() V31() V35() finite cardinal V48() V49() countable Element of NAT
(S + 1) -BinarySequence (2 to_power F) is Relation-like NAT -defined BOOLEAN -valued Function-like finite S + 1 -element FinSequence-like FinSubsequence-like countable finite-support FinSequence of BOOLEAN
S + 1 is non empty ext-real positive non negative V29() V30() V31() V35() finite cardinal V48() V49() countable Element of NAT
H₁(S + 1) . (S + 1) is set
dom H₁(S + 1) is finite S + 1 -element countable Element of bool NAT
Seg (S + 1) is non empty finite S + 1 -element S + 1 -element countable Element of bool NAT
S + 1 is non empty ext-real positive non negative V29() V30() V31() V35() finite cardinal V48() V49() countable Element of NAT
dom H₁(S) is finite S -element countable Element of bool NAT
Seg S is finite S -element countable Element of bool NAT
len H₁(S) is ext-real non negative V29() V30() V31() V35() finite cardinal V48() V49() countable Element of NAT
<*FALSE*> is non empty trivial Relation-like NAT -defined BOOLEAN -valued Function-like constant finite 1 -element FinSequence-like FinSubsequence-like countable finite-support Element of BOOLEAN *
BOOLEAN * is non empty functional FinSequence-membered FinSequenceSet of BOOLEAN
dom <*FALSE*> is non empty trivial finite 1 -element countable Element of bool NAT
ck is non empty ext-real positive non negative V29() V30() V31() V35() finite cardinal V48() V49() countable Element of NAT
ck -BinarySequence (2 to_power F) is Relation-like NAT -defined BOOLEAN -valued Function-like finite ck -element FinSequence-like FinSubsequence-like countable finite-support FinSequence of BOOLEAN
H₁(ck) ^ <*FALSE*> is non empty Relation-like NAT -defined BOOLEAN -valued Function-like finite ck + 1 -element K288(ck,1) -element FinSequence-like FinSubsequence-like countable finite-support FinSequence of BOOLEAN
K288(ck,1) is non empty ext-real positive non negative V29() V30() V31() V35() finite cardinal V48() V49() countable Element of NAT
ck + 1 is non empty ext-real positive non negative V29() V30() V31() V35() finite cardinal V48() V49() countable Element of NAT
(H₁(ck) ^ <*FALSE*>) . (S + 1) is set
<*FALSE*> . 1 is set
Seg S is finite S -element countable Element of bool NAT
dom H₁(S) is finite S -element countable Element of bool NAT
ck is non empty ext-real positive non negative V29() V30() V31() V35() finite cardinal V48() V49() countable Element of NAT
ck -BinarySequence (2 to_power F) is Relation-like NAT -defined BOOLEAN -valued Function-like finite ck -element FinSequence-like FinSubsequence-like countable finite-support FinSequence of BOOLEAN
<*FALSE*> is non empty trivial Relation-like NAT -defined BOOLEAN -valued Function-like constant finite 1 -element FinSequence-like FinSubsequence-like countable finite-support Element of BOOLEAN *
BOOLEAN * is non empty functional FinSequence-membered FinSequenceSet of BOOLEAN
H₁(ck) ^ <*FALSE*> is non empty Relation-like NAT -defined BOOLEAN -valued Function-like finite ck + 1 -element K288(ck,1) -element FinSequence-like FinSubsequence-like countable finite-support FinSequence of BOOLEAN
K288(ck,1) is non empty ext-real positive non negative V29() V30() V31() V35() finite cardinal V48() V49() countable Element of NAT
ck + 1 is non empty ext-real positive non negative V29() V30() V31() V35() finite cardinal V48() V49() countable Element of NAT
(H₁(ck) ^ <*FALSE*>) . (S + 1) is set
H₁(S) . (S + 1) is set
(S + 1) -BinarySequence (2 to_power F) is Relation-like NAT -defined BOOLEAN -valued Function-like finite S + 1 -element FinSequence-like FinSubsequence-like countable finite-support FinSequence of BOOLEAN
(S + 1) -BinarySequence (2 to_power F) is Relation-like NAT -defined BOOLEAN -valued Function-like finite S + 1 -element FinSequence-like FinSubsequence-like countable finite-support FinSequence of BOOLEAN
S is ext-real non negative V29() V30() V31() V35() finite cardinal V48() V49() countable Element of NAT
S + 1 is non empty ext-real positive non negative V29() V30() V31() V35() finite cardinal V48() V49() countable Element of NAT
((S + 1) -BinarySequence (2 to_power F)) . (S + 1) is set
S is ext-real non negative V29() V30() V31() V35() finite cardinal V48() V49() countable Element of NAT
S + 1 is non empty ext-real positive non negative V29() V30() V31() V35() finite cardinal V48() V49() countable Element of NAT
(0 -BinarySequence (2 to_power F)) . (S + 1) is empty ext-real non positive non negative Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional Function-yielding V28() V29() V30() V31() V33() V34() V35() finite finite-yielding V40() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V48() V49() Cardinal-yielding with_common_domain countable FinSequence-yielding finite-support set
S is ext-real non negative V29() V30() V31() V35() finite cardinal V48() V49() countable Element of NAT
S -BinarySequence (2 to_power F) is Relation-like NAT -defined BOOLEAN -valued Function-like finite S -element FinSequence-like FinSubsequence-like countable finite-support FinSequence of BOOLEAN
S + 1 is non empty ext-real positive non negative V29() V30() V31() V35() finite cardinal V48() V49() countable Element of NAT
S is ext-real non negative V29() V30() V31() V35() finite cardinal V48() V49() countable Element of NAT
(S + 1) -BinarySequence (2 to_power F) is Relation-like NAT -defined BOOLEAN -valued Function-like finite S + 1 -element FinSequence-like FinSubsequence-like countable finite-support FinSequence of BOOLEAN
H₁(S + 1) . S is set
dom H₁(S) is finite S -element countable Element of bool NAT
Seg S is finite S -element countable Element of bool NAT
2 to_power S is ext-real non negative V29() V30() V31() V35() finite cardinal V48() V49() countable Element of NAT
(S + 1) -BinarySequence (2 to_power F) is Relation-like NAT -defined BOOLEAN -valued Function-like finite S + 1 -element FinSequence-like FinSubsequence-like countable finite-support FinSequence of BOOLEAN
H₁(S + 1) . S is set
ck is non empty ext-real positive non negative V29() V30() V31() V35() finite cardinal V48() V49() countable Element of NAT
ck -BinarySequence (2 to_power F) is Relation-like NAT -defined BOOLEAN -valued Function-like finite ck -element FinSequence-like FinSubsequence-like countable finite-support FinSequence of BOOLEAN
<*FALSE*> is non empty trivial Relation-like NAT -defined BOOLEAN -valued Function-like constant finite 1 -element FinSequence-like FinSubsequence-like countable finite-support Element of BOOLEAN *
BOOLEAN * is non empty functional FinSequence-membered FinSequenceSet of BOOLEAN
H₁(ck) ^ <*FALSE*> is non empty Relation-like NAT -defined BOOLEAN -valued Function-like finite ck + 1 -element K288(ck,1) -element FinSequence-like FinSubsequence-like countable finite-support FinSequence of BOOLEAN
K288(ck,1) is non empty ext-real positive non negative V29() V30() V31() V35() finite cardinal V48() V49() countable Element of NAT
ck + 1 is non empty ext-real positive non negative V29() V30() V31() V35() finite cardinal V48() V49() countable Element of NAT
(H₁(ck) ^ <*FALSE*>) . S is set
H₁(S) . S is set
Seg S is finite S -element countable Element of bool NAT
0* S is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like countable finite-support Element of REAL S
REAL S is functional FinSequence-membered FinSequenceSet of REAL
S |-> 0 is Relation-like empty-yielding NAT -defined NAT -valued Function-like Function-yielding V28() finite S -element FinSequence-like FinSubsequence-like Cardinal-yielding countable FinSequence-yielding finite-support Element of S -tuples_on NAT
S -tuples_on NAT is non empty functional FinSequence-membered FinSequenceSet of NAT
NAT * is non empty functional FinSequence-membered FinSequenceSet of NAT
{ b₁ where b₁ is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like countable finite-support Element of NAT * : len b₁ = S } is set
(Seg S) --> 0 is Relation-like Seg S -defined Seg S -defined NAT -valued {0} -valued Function-like constant total total V24( Seg S,{0}) Function-yielding V28() finite FinSequence-like FinSubsequence-like Cardinal-yielding countable finite-support Element of bool [:(Seg S),{0}:]
{0} is non empty trivial functional finite V40() 1 -element with_common_domain countable set
[:(Seg S),{0}:] is Relation-like finite countable set
bool [:(Seg S),{0}:] is non empty finite V40() countable set
dom (0* S) is finite countable Element of bool NAT
(S + 1) -BinarySequence (2 to_power F) is Relation-like NAT -defined BOOLEAN -valued Function-like finite S + 1 -element FinSequence-like FinSubsequence-like countable finite-support FinSequence of BOOLEAN
H₁(S + 1) . S is set
<*TRUE*> is non empty trivial Relation-like NAT -defined BOOLEAN -valued Function-like constant finite 1 -element FinSequence-like FinSubsequence-like countable finite-support Element of BOOLEAN *
BOOLEAN * is non empty functional FinSequence-membered FinSequenceSet of BOOLEAN
(0* S) ^ <*TRUE*> is non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like countable finite-support set
((0* S) ^ <*TRUE*>) . S is set
(0* S) . S is set
(S + 1) -BinarySequence (2 to_power F) is Relation-like NAT -defined BOOLEAN -valued Function-like finite S + 1 -element FinSequence-like FinSubsequence-like countable finite-support FinSequence of BOOLEAN
(S + 1) -BinarySequence (2 to_power F) is Relation-like NAT -defined BOOLEAN -valued Function-like finite S + 1 -element FinSequence-like FinSubsequence-like countable finite-support FinSequence of BOOLEAN
S is ext-real non negative V29() V30() V31() V35() finite cardinal V48() V49() countable Element of NAT
((S + 1) -BinarySequence (2 to_power F)) . S is set
S is ext-real non negative V29() V30() V31() V35() finite cardinal V48() V49() countable Element of NAT
(0 -BinarySequence (2 to_power F)) . S is empty ext-real non positive non negative Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional Function-yielding V28() V29() V30() V31() V33() V34() V35() finite finite-yielding V40() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V48() V49() Cardinal-yielding with_common_domain countable FinSequence-yielding finite-support set
S is ext-real non negative V29() V30() V31() V35() finite cardinal V48() V49() countable set
S + 1 is non empty ext-real positive non negative V29() V30() V31() V35() finite cardinal V48() V49() countable Element of NAT
S is ext-real non negative V29() V30() V31() V35() finite cardinal V48() V49() countable Element of NAT
S is ext-real non negative V29() V30() V31() V35() finite cardinal V48() V49() countable set
S + 1 is non empty ext-real positive non negative V29() V30() V31() V35() finite cardinal V48() V49() countable Element of NAT
S is ext-real non negative V29() V30() V31() V35() finite cardinal V48() V49() countable Element of NAT
2 to_power S is ext-real non negative V29() V30() V31() V35() finite cardinal V48() V49() countable Element of NAT
X is set
bool X is non empty Element of bool (bool X)
bool X is non empty set
bool (bool X) is non empty set
[:(bool X),(bool X):] is non empty Relation-like set
bool [:(bool X),(bool X):] is non empty set
[{},{}] is V21() set
{{},{}} is non empty functional finite V40() countable set
{{}} is non empty trivial functional finite V40() 1 -element with_common_domain countable set
{{{},{}},{{}}} is non empty finite V40() countable set
{[{},{}]} is non empty trivial Relation-like Function-like constant finite 1 -element countable finite-support set
F is Relation-like bool X -defined bool X -valued Element of bool [:(bool X),(bool X):]
X is set
bool X is non empty set
bool X is non empty Element of bool (bool X)
bool (bool X) is non empty set
[:(bool X),(bool X):] is non empty Relation-like bool X -defined bool X -valued Element of bool [:(bool X),(bool X):]
[:(bool X),(bool X):] is non empty Relation-like set
bool [:(bool X),(bool X):] is non empty set
[:(bool X),(bool X):] is non empty Relation-like set
bool [:(bool X),(bool X):] is non empty set
X is set
(X) is Relation-like bool X -defined bool X -valued Element of bool [:(bool X),(bool X):]
bool X is non empty Element of bool (bool X)
bool X is non empty set
bool (bool X) is non empty set
[:(bool X),(bool X):] is non empty Relation-like set
bool [:(bool X),(bool X):] is non empty set
[:(bool X),(bool X):] is non empty Relation-like bool X -defined bool X -valued Element of bool [:(bool X),(bool X):]
[:(bool X),(bool X):] is non empty Relation-like set
bool [:(bool X),(bool X):] is non empty set
X is set
bool X is non empty Element of bool (bool X)
bool X is non empty set
bool (bool X) is non empty set
[:(bool X),(bool X):] is non empty Relation-like set
bool [:(bool X),(bool X):] is non empty set
F is non empty Relation-like bool X -defined bool X -valued Element of bool [:(bool X),(bool X):]
(X) is non empty Relation-like bool X -defined bool X -valued Element of bool [:(bool X),(bool X):]
[:(bool X),(bool X):] is non empty Relation-like bool X -defined bool X -valued Element of bool [:(bool X),(bool X):]
[:(bool X),(bool X):] is non empty Relation-like set
bool [:(bool X),(bool X):] is non empty set
K is Element of F
X is set
(X) is non empty Relation-like bool X -defined bool X -valued Element of bool [:(bool X),(bool X):]
bool X is non empty Element of bool (bool X)
bool X is non empty set
bool (bool X) is non empty set
[:(bool X),(bool X):] is non empty Relation-like set
bool [:(bool X),(bool X):] is non empty set
[:(bool X),(bool X):] is non empty Relation-like bool X -defined bool X -valued Element of bool [:(bool X),(bool X):]
[:(bool X),(bool X):] is non empty Relation-like set
bool [:(bool X),(bool X):] is non empty set
F is set
K is set
dcF is set
[K,dcF] is V21() set
{K,dcF} is non empty finite countable set
{K} is non empty trivial finite 1 -element countable set
{{K,dcF},{K}} is non empty finite V40() countable set
S is Element of bool X
S is Element of bool X
ck is Element of bool X
B is Element of bool X
[ck,B] is V21() set
{ck,B} is non empty finite countable set
{ck} is non empty trivial finite 1 -element countable set
{{ck,B},{ck}} is non empty finite V40() countable set
K is Element of bool X
dcF is Element of bool X
[K,dcF] is V21() set
{K,dcF} is non empty finite countable set
{K} is non empty trivial finite 1 -element countable set
{{K,dcF},{K}} is non empty finite V40() countable set
X is set
bool X is non empty Element of bool (bool X)
bool X is non empty set
bool (bool X) is non empty set
[:(bool X),(bool X):] is non empty Relation-like set
bool [:(bool X),(bool X):] is non empty set
F is set
K is Relation-like bool X -defined bool X -valued Element of bool [:(bool X),(bool X):]
dcF is set
S is set
[dcF,S] is V21() set
{dcF,S} is non empty finite countable set
{dcF} is non empty trivial finite 1 -element countable set
{{dcF,S},{dcF}} is non empty finite V40() countable set
S is Element of bool X
ck is Element of bool X
[S,ck] is V21() set
{S,ck} is non empty finite countable set
{S} is non empty trivial finite 1 -element countable set
{{S,ck},{S}} is non empty finite V40() countable set
X is ()
the of X is non empty finite countable set
bool the of X is non empty finite V40() countable set
X is ()
the of X is non empty finite countable set
bool the of X is non empty finite V40() countable set
X is ()
the of X is non empty finite countable set
bool the of X is non empty finite V40() countable set
{ [b₁,b₂] where b₁, b₂ is finite countable Element of bool the of X : (X,b₁,b₂) } is set
bool the of X is non empty finite V40() countable Element of bool (bool the of X)
bool (bool the of X) is non empty finite V40() countable set
[:(bool the of X),(bool the of X):] is non empty Relation-like finite countable set
bool [:(bool the of X),(bool the of X):] is non empty finite V40() countable set
[:(bool the of X),(bool the of X):] is non empty Relation-like bool the of X -defined bool the of X -valued finite countable Element of bool [:(bool the of X),(bool the of X):]
[:(bool the of X),(bool the of X):] is non empty Relation-like finite countable set
bool [:(bool the of X),(bool the of X):] is non empty finite V40() countable set
dcF is set
S is finite countable Element of bool the of X
S is finite countable Element of bool the of X
[S,S] is V21() set
{S,S} is non empty finite V40() countable set
{S} is non empty trivial finite V40() 1 -element countable set
{{S,S},{S}} is non empty finite V40() countable set
X is ()
the of X is non empty finite countable set
bool the of X is non empty finite V40() countable set
(X) is Relation-like bool the of X -defined bool the of X -valued finite countable Element of bool [:(bool the of X),(bool the of X):]
bool the of X is non empty finite V40() countable Element of bool (bool the of X)
bool (bool the of X) is non empty finite V40() countable set
[:(bool the of X),(bool the of X):] is non empty Relation-like finite countable set
bool [:(bool the of X),(bool the of X):] is non empty finite V40() countable set
{ [b₁,b₂] where b₁, b₂ is finite countable Element of bool the of X : (X,b₁,b₂) } is set
F is finite countable Element of bool the of X
K is finite countable Element of bool the of X
[F,K] is V21() set
{F,K} is non empty finite V40() countable set
{F} is non empty trivial finite V40() 1 -element countable set
{{F,K},{F}} is non empty finite V40() countable set
S is finite countable Element of bool the of X
S is finite countable Element of bool the of X
[S,S] is V21() set
{S,S} is non empty finite V40() countable set
{S} is non empty trivial finite V40() 1 -element countable set
{{S,S},{S}} is non empty finite V40() countable set
X is set
(X) is non empty Relation-like bool X -defined bool X -valued Element of bool [:(bool X),(bool X):]
bool X is non empty Element of bool (bool X)
bool X is non empty set
bool (bool X) is non empty set
[:(bool X),(bool X):] is non empty Relation-like set
bool [:(bool X),(bool X):] is non empty set
[:(bool X),(bool X):] is non empty Relation-like bool X -defined bool X -valued Element of bool [:(bool X),(bool X):]
[:(bool X),(bool X):] is non empty Relation-like set
bool [:(bool X),(bool X):] is non empty set
dcF is Element of (X)
dcF `1 is set
S is Element of (X)
S `2 is set
X is set
(X) is non empty Relation-like bool X -defined bool X -valued Element of bool [:(bool X),(bool X):]
bool X is non empty Element of bool (bool X)
bool X is non empty set
bool (bool X) is non empty set
[:(bool X),(bool X):] is non empty Relation-like set
bool [:(bool X),(bool X):] is non empty set
[:(bool X),(bool X):] is non empty Relation-like bool X -defined bool X -valued Element of bool [:(bool X),(bool X):]
[:(bool X),(bool X):] is non empty Relation-like set
bool [:(bool X),(bool X):] is non empty set
X is set
(X) is non empty Relation-like bool X -defined bool X -valued Element of bool [:(bool X),(bool X):]
bool X is non empty Element of bool (bool X)
bool X is non empty set
bool (bool X) is non empty set
[:(bool X),(bool X):] is non empty Relation-like set
bool [:(bool X),(bool X):] is non empty set
[:(bool X),(bool X):] is non empty Relation-like bool X -defined bool X -valued Element of bool [:(bool X),(bool X):]
[:(bool X),(bool X):] is non empty Relation-like set
bool [:(bool X),(bool X):] is non empty set
K is Element of (X)
F is Element of (X)
K `1 is set
F `1 is set
F `2 is set
K `2 is set
[(F `1),(F `2)] is V21() set
{(F `1),(F `2)} is non empty finite countable set
{(F `1)} is non empty trivial finite 1 -element countable set
{{(F `1),(F `2)},{(F `1)}} is non empty finite V40() countable set
X is set
(X) is non empty Relation-like bool X -defined bool X -valued Element of bool [:(bool X),(bool X):]
bool X is non empty Element of bool (bool X)
bool X is non empty set
bool (bool X) is non empty set
[:(bool X),(bool X):] is non empty Relation-like set
bool [:(bool X),(bool X):] is non empty set
[:(bool X),(bool X):] is non empty Relation-like bool X -defined bool X -valued Element of bool [:(bool X),(bool X):]
[:(bool X),(bool X):] is non empty Relation-like set
bool [:(bool X),(bool X):] is non empty set
K is Element of (X)
F is Element of (X)
dcF is Element of (X)
K `2 is set
dcF `2 is set
F `2 is set
dcF `1 is set
K `1 is set
F `1 is set
X is set
bool X is non empty set
F is Element of bool X
K is Element of bool X
[F,K] is V21() set
{F,K} is non empty finite countable set
{F} is non empty trivial finite 1 -element countable set
{{F,K},{F}} is non empty finite V40() countable set
(X) is non empty Relation-like bool X -defined bool X -valued Element of bool [:(bool X),(bool X):]
bool X is non empty Element of bool (bool X)
bool (bool X) is non empty set
[:(bool X),(bool X):] is non empty Relation-like set
bool [:(bool X),(bool X):] is non empty set
[:(bool X),(bool X):] is non empty Relation-like bool X -defined bool X -valued Element of bool [:(bool X),(bool X):]
[:(bool X),(bool X):] is non empty Relation-like set
bool [:(bool X),(bool X):] is non empty set
X is set
bool X is non empty set
F is Element of bool X
K is Element of bool X
(X,F,K) is V21() Element of (X)
(X) is non empty Relation-like bool X -defined bool X -valued Element of bool [:(bool X),(bool X):]
bool X is non empty Element of bool (bool X)
bool (bool X) is non empty set
[:(bool X),(bool X):] is non empty Relation-like set
bool [:(bool X),(bool X):] is non empty set
[:(bool X),(bool X):] is non empty Relation-like bool X -defined bool X -valued Element of bool [:(bool X),(bool X):]
[:(bool X),(bool X):] is non empty Relation-like set
bool [:(bool X),(bool X):] is non empty set
{F,K} is non empty finite countable set
{F} is non empty trivial finite 1 -element countable set
{{F,K},{F}} is non empty finite V40() countable set
dcF is Element of bool X
S is Element of bool X
(X,dcF,S) is V21() Element of (X)
{dcF,S} is non empty finite countable set
{dcF} is non empty trivial finite 1 -element countable set
{{dcF,S},{dcF}} is non empty finite V40() countable set
(X,F,K) `2 is set
(X,dcF,S) `1 is set
(X,dcF,S) `2 is set
(X,F,K) `1 is set
X is set
(X) is non empty Relation-like bool X -defined bool X -valued Element of bool [:(bool X),(bool X):]
bool X is non empty Element of bool (bool X)
bool X is non empty set
bool (bool X) is non empty set
[:(bool X),(bool X):] is non empty Relation-like set
bool [:(bool X),(bool X):] is non empty set
[:(bool X),(bool X):] is non empty Relation-like bool X -defined bool X -valued Element of bool [:(bool X),(bool X):]
[:(bool X),(bool X):] is non empty Relation-like set
bool [:(bool X),(bool X):] is non empty set
{ [b₁,b₂] where b₁, b₂ is Element of (X) : (X,b₂,b₁) } is set
[:(X),(X):] is non empty Relation-like set
bool [:(X),(X):] is non empty set
[:(X),(X):] is non empty Relation-like [:(bool X),(bool X):] -defined [:(bool X),(bool X):] -valued Element of bool [:[:(bool X),(bool X):],[:(bool X),(bool X):]:]
[:[:(bool X),(bool X):],[:(bool X),(bool X):]:] is non empty Relation-like set
bool [:[:(bool X),(bool X):],[:(bool X),(bool X):]:] is non empty set
K is set
dcF is Element of (X)
S is Element of (X)
[dcF,S] is V21() set
{dcF,S} is non empty finite countable set
{dcF} is non empty trivial finite 1 -element countable set
{{dcF,S},{dcF}} is non empty finite V40() countable set
K is set
(K) is non empty Relation-like bool K -defined bool K -valued Element of bool [:(bool K),(bool K):]
bool K is non empty Element of bool (bool K)
bool K is non empty set
bool (bool K) is non empty set
[:(bool K),(bool K):] is non empty Relation-like set
bool [:(bool K),(bool K):] is non empty set
[:(bool K),(bool K):] is non empty Relation-like bool K -defined bool K -valued Element of bool [:(bool K),(bool K):]
[:(bool K),(bool K):] is non empty Relation-like set
bool [:(bool K),(bool K):] is non empty set
F is set
X is set
(X) is Relation-like (X) -defined (X) -valued Element of bool [:(X),(X):]
(X) is non empty Relation-like bool X -defined bool X -valued Element of bool [:(bool X),(bool X):]
bool X is non empty Element of bool (bool X)
bool X is non empty set
bool (bool X) is non empty set
[:(bool X),(bool X):] is non empty Relation-like set
bool [:(bool X),(bool X):] is non empty set
[:(bool X),(bool X):] is non empty Relation-like bool X -defined bool X -valued Element of bool [:(bool X),(bool X):]
[:(bool X),(bool X):] is non empty Relation-like set
bool [:(bool X),(bool X):] is non empty set
[:(X),(X):] is non empty Relation-like set
bool [:(X),(X):] is non empty set
{ [b₁,b₂] where b₁, b₂ is Element of (X) : (X,b₂,b₁) } is set
dcF is set
S is Element of (K)
S is Element of (K)
[S,S] is V21() set
{S,S} is non empty finite countable set
{S} is non empty trivial finite 1 -element countable set
{{S,S},{S}} is non empty finite V40() countable set
(K) is Relation-like (K) -defined (K) -valued Element of bool [:(K),(K):]
[:(K),(K):] is non empty Relation-like set
bool [:(K),(K):] is non empty set
{ [b₁,b₂] where b₁, b₂ is Element of (K) : (K,b₂,b₁) } is set
X is set
(X) is non empty Relation-like bool X -defined bool X -valued Element of bool [:(bool X),(bool X):]
bool X is non empty Element of bool (bool X)
bool X is non empty set
bool (bool X) is non empty set
[:(bool X),(bool X):] is non empty Relation-like set
bool [:(bool X),(bool X):] is non empty set
[:(bool X),(bool X):] is non empty Relation-like bool X -defined bool X -valued Element of bool [:(bool X),(bool X):]
[:(bool X),(bool X):] is non empty Relation-like set
bool [:(bool X),(bool X):] is non empty set
(X) is Relation-like (X) -defined (X) -valued Element of bool [:(X),(X):]
[:(X),(X):] is non empty Relation-like set
bool [:(X),(X):] is non empty set
{ [b₁,b₂] where b₁, b₂ is Element of (X) : (X,b₂,b₁) } is set
dom (X) is Relation-like bool X -defined bool X -valued Element of bool (X)
bool (X) is non empty set
F is set
K is Element of (X)
[K,K] is V21() set
{K,K} is non empty finite countable set
{K} is non empty trivial finite 1 -element countable set
{{K,K},{K}} is non empty finite V40() countable set
X is set
(X) is non empty Relation-like bool X -defined bool X -valued Element of bool [:(bool X),(bool X):]
bool X is non empty Element of bool (bool X)
bool X is non empty set
bool (bool X) is non empty set
[:(bool X),(bool X):] is non empty Relation-like set
bool [:(bool X),(bool X):] is non empty set
[:(bool X),(bool X):] is non empty Relation-like bool X -defined bool X -valued Element of bool [:(bool X),(bool X):]
[:(bool X),(bool X):] is non empty Relation-like set
bool [:(bool X),(bool X):] is non empty set
(X) is Relation-like (X) -defined (X) -valued Element of bool [:(X),(X):]
[:(X),(X):] is non empty Relation-like set
bool [:(X),(X):] is non empty set
{ [b₁,b₂] where b₁, b₂ is Element of (X) : (X,b₂,b₁) } is set
rng (X) is Relation-like bool X -defined bool X -valued Element of bool (X)
bool (X) is non empty set
F is set
K is Element of (X)
[K,K] is V21() set
{K,K} is non empty finite countable set
{K} is non empty trivial finite 1 -element countable set
{{K,K},{K}} is non empty finite V40() countable set
X is set
(X) is Relation-like (X) -defined (X) -valued Element of bool [:(X),(X):]
(X) is non empty Relation-like bool X -defined bool X -valued Element of bool [:(bool X),(bool X):]
bool X is non empty Element of bool (bool X)
bool X is non empty set
bool (bool X) is non empty set
[:(bool X),(bool X):] is non empty Relation-like set
bool [:(bool X),(bool X):] is non empty set
[:(bool X),(bool X):] is non empty Relation-like bool X -defined bool X -valued Element of bool [:(bool X),(bool X):]
[:(bool X),(bool X):] is non empty Relation-like set
bool [:(bool X),(bool X):] is non empty set
[:(X),(X):] is non empty Relation-like set
bool [:(X),(X):] is non empty set
{ [b₁,b₂] where b₁, b₂ is Element of (X) : (X,b₂,b₁) } is set
field (X) is set
dom (X) is Relation-like bool X -defined bool X -valued Element of bool (X)
bool (X) is non empty set
rng (X) is Relation-like bool X -defined bool X -valued Element of bool (X)
(dom (X)) \/ (rng (X)) is Relation-like bool X -defined bool X -valued Element of bool (X)
[:(bool X),(bool X):] \/ (rng (X)) is non empty Relation-like bool X -defined bool X -valued set
[:(bool X),(bool X):] \/ [:(bool X),(bool X):] is non empty Relation-like bool X -defined bool X -valued Element of bool [:(bool X),(bool X):]
X is set
(X) is Relation-like (X) -defined (X) -valued Element of bool [:(X),(X):]
(X) is non empty Relation-like bool X -defined bool X -valued Element of bool [:(bool X),(bool X):]
bool X is non empty Element of bool (bool X)
bool X is non empty set
bool (bool X) is non empty set
[:(bool X),(bool X):] is non empty Relation-like set
bool [:(bool X),(bool X):] is non empty set
[:(bool X),(bool X):] is non empty Relation-like bool X -defined bool X -valued Element of bool [:(bool X),(bool X):]
[:(bool X),(bool X):] is non empty Relation-like set
bool [:(bool X),(bool X):] is non empty set
[:(X),(X):] is non empty Relation-like set
bool [:(X),(X):] is non empty set
{ [b₁,b₂] where b₁, b₂ is Element of (X) : (X,b₂,b₁) } is set
dom (X) is non empty Relation-like bool X -defined bool X -valued Element of bool (X)
bool (X) is non empty set
dcF is set
S is (X,(X))
[dcF,dcF] is V21() set
{dcF,dcF} is non empty finite countable set
{dcF} is non empty trivial finite 1 -element countable set
{{dcF,dcF},{dcF}} is non empty finite V40() countable set
field (X) is set
rng (X) is non empty Relation-like bool X -defined bool X -valued Element of bool (X)
(X) \/ (rng (X)) is non empty Relation-like bool X -defined bool X -valued set
dcF is set
[dcF,dcF] is V21() set
{dcF,dcF} is non empty finite countable set
{dcF} is non empty trivial finite 1 -element countable set
{{dcF,dcF},{dcF}} is non empty finite V40() countable set
S is (X,(X))
dcF is set
S is set
[dcF,S] is V21() set
{dcF,S} is non empty finite countable set
{dcF} is non empty trivial finite 1 -element countable set
{{dcF,S},{dcF}} is non empty finite V40() countable set
[S,dcF] is V21() set
{S,dcF} is non empty finite countable set
{S} is non empty trivial finite 1 -element countable set
{{S,dcF},{S}} is non empty finite V40() countable set
S is (X,(X))
ck is (X,(X))
[S,ck] is V21() set
{S,ck} is non empty finite countable set
{S} is non empty trivial finite 1 -element countable set
{{S,ck},{S}} is non empty finite V40() countable set
B is (X,(X))
m is (X,(X))
[B,m] is V21() set
{B,m} is non empty finite countable set
{B} is non empty trivial finite 1 -element countable set
{{B,m},{B}} is non empty finite V40() countable set
dcF is set
S is set
S is set
[dcF,S] is V21() set
{dcF,S} is non empty finite countable set
{dcF} is non empty trivial finite 1 -element countable set
{{dcF,S},{dcF}} is non empty finite V40() countable set
[S,S] is V21() set
{S,S} is non empty finite countable set
{S} is non empty trivial finite 1 -element countable set
{{S,S},{S}} is non empty finite V40() countable set
[dcF,S] is V21() set
{dcF,S} is non empty finite countable set
{{dcF,S},{dcF}} is non empty finite V40() countable set
ck is (X,(X))
B is (X,(X))
[ck,B] is V21() set
{ck,B} is non empty finite countable set
{ck} is non empty trivial finite 1 -element countable set
{{ck,B},{ck}} is non empty finite V40() countable set
m is (X,(X))
P is (X,(X))
[m,P] is V21() set
{m,P} is non empty finite countable set
{m} is non empty trivial finite 1 -element countable set
{{m,P},{m}} is non empty finite V40() countable set
X is set
bool X is non empty Element of bool (bool X)
bool X is non empty set
bool (bool X) is non empty set
[:(bool X),(bool X):] is non empty Relation-like set
bool [:(bool X),(bool X):] is non empty set
X is set
bool X is non empty Element of bool (bool X)
bool X is non empty set
bool (bool X) is non empty set
[:(bool X),(bool X):] is non empty Relation-like set
bool [:(bool X),(bool X):] is non empty set
X is set
bool X is non empty Element of bool (bool X)
bool X is non empty set
bool (bool X) is non empty set
[:(bool X),(bool X):] is non empty Relation-like set
bool [:(bool X),(bool X):] is non empty set
X is set
bool X is non empty Element of bool (bool X)
bool X is non empty set
bool (bool X) is non empty set
[:(bool X),(bool X):] is non empty Relation-like set
bool [:(bool X),(bool X):] is non empty set
F is Relation-like bool X -defined bool X -valued Element of bool [:(bool X),(bool X):]
field F is set
K is Element of bool X
dcF is Element of bool X
(X,K,dcF) is V21() Element of (X)
(X) is non empty Relation-like bool X -defined bool X -valued Element of bool [:(bool X),(bool X):]
[:(bool X),(bool X):] is non empty Relation-like bool X -defined bool X -valued Element of bool [:(bool X),(bool X):]
[:(bool X),(bool X):] is non empty Relation-like set
bool [:(bool X),(bool X):] is non empty set
{K,dcF} is non empty finite countable set
{K} is non empty trivial finite 1 -element countable set
{{K,dcF},{K}} is non empty finite V40() countable set
S is Element of bool X
(X,dcF,S) is V21() Element of (X)
{dcF,S} is non empty finite countable set
{dcF} is non empty trivial finite 1 -element countable set
{{dcF,S},{dcF}} is non empty finite V40() countable set
(X,K,S) is V21() Element of (X)
{K,S} is non empty finite countable set
{{K,S},{K}} is non empty finite V40() countable set
K is set
dcF is set
S is set
[K,dcF] is V21() set
{K,dcF} is non empty finite countable set
{K} is non empty trivial finite 1 -element countable set
{{K,dcF},{K}} is non empty finite V40() countable set
[dcF,S] is V21() set
{dcF,S} is non empty finite countable set
{dcF} is non empty trivial finite 1 -element countable set
{{dcF,S},{dcF}} is non empty finite V40() countable set
[K,S] is V21() set
{K,S} is non empty finite countable set
{{K,S},{K}} is non empty finite V40() countable set
(bool X) \/ (bool X) is non empty Element of bool (bool X)
ck is Element of bool X
B is Element of bool X
(X,ck,B) is V21() Element of (X)
{ck,B} is non empty finite countable set
{ck} is non empty trivial finite 1 -element countable set
{{ck,B},{ck}} is non empty finite V40() countable set
S is Element of bool X
(X,S,ck) is V21() Element of (X)
{S,ck} is non empty finite countable set
{S} is non empty trivial finite 1 -element countable set
{{S,ck},{S}} is non empty finite V40() countable set
X is set
bool X is non empty Element of bool (bool X)
bool X is non empty set
bool (bool X) is non empty set
[:(bool X),(bool X):] is non empty Relation-like set
bool [:(bool X),(bool X):] is non empty set
X is set
(X) is non empty Relation-like bool X -defined bool X -valued Element of bool [:(bool X),(bool X):]
bool X is non empty Element of bool (bool X)
bool X is non empty set
bool (bool X) is non empty set
[:(bool X),(bool X):] is non empty Relation-like set
bool [:(bool X),(bool X):] is non empty set
[:(bool X),(bool X):] is non empty Relation-like bool X -defined bool X -valued Element of bool [:(bool X),(bool X):]
[:(bool X),(bool X):] is non empty Relation-like set
bool [:(bool X),(bool X):] is non empty set
K is Element of bool X
(X,K,K) is V21() Element of (X)
{K,K} is non empty finite countable set
{K} is non empty trivial finite 1 -element countable set
{{K,K},{K}} is non empty finite V40() countable set
nabla (bool X) is Relation-like bool X -defined bool X -valued total reflexive symmetric transitive Element of bool [:(bool X),(bool X):]
field (X) is set
K is set
dcF is set
S is set
[K,dcF] is V21() set
{K,dcF} is non empty finite countable set
{K} is non empty trivial finite 1 -element countable set
{{K,dcF},{K}} is non empty finite V40() countable set
[dcF,S] is V21() set
{dcF,S} is non empty finite countable set
{dcF} is non empty trivial finite 1 -element countable set
{{dcF,S},{dcF}} is non empty finite V40() countable set
[K,S] is V21() set
{K,S} is non empty finite countable set
{{K,S},{K}} is non empty finite V40() countable set
K is Element of bool X
dcF is Element of bool X
(X,K,dcF) is V21() Element of (X)
{K,dcF} is non empty finite countable set
{K} is non empty trivial finite 1 -element countable set
{{K,dcF},{K}} is non empty finite V40() countable set
S is Element of bool X
S is Element of bool X
(X,S,S) is V21() Element of (X)
{S,S} is non empty finite countable set
{S} is non empty trivial finite 1 -element countable set
{{S,S},{S}} is non empty finite V40() countable set
K is Element of bool X
dcF is Element of bool X
(X,K,dcF) is V21() Element of (X)
{K,dcF} is non empty finite countable set
{K} is non empty trivial finite 1 -element countable set
{{K,dcF},{K}} is non empty finite V40() countable set
S is Element of bool X
S is Element of bool X
(X,S,S) is V21() Element of (X)
{S,S} is non empty finite countable set
{S} is non empty trivial finite 1 -element countable set
{{S,S},{S}} is non empty finite V40() countable set
K \/ S is Element of bool X
dcF \/ S is Element of bool X
(X,(K \/ S),(dcF \/ S)) is V21() Element of (X)
{(K \/ S),(dcF \/ S)} is non empty finite countable set
{(K \/ S)} is non empty trivial finite 1 -element countable set
{{(K \/ S),(dcF \/ S)},{(K \/ S)}} is non empty finite V40() countable set
X is set
bool X is non empty Element of bool (bool X)
bool X is non empty set
bool (bool X) is non empty set
[:(bool X),(bool X):] is non empty Relation-like set
bool [:(bool X),(bool X):] is non empty set
(X) is non empty Relation-like bool X -defined bool X -valued Element of bool [:(bool X),(bool X):]
[:(bool X),(bool X):] is non empty Relation-like bool X -defined bool X -valued Element of bool [:(bool X),(bool X):]
[:(bool X),(bool X):] is non empty Relation-like set
bool [:(bool X),(bool X):] is non empty set
X is set
bool X is non empty Element of bool (bool X)
bool X is non empty set
bool (bool X) is non empty set
[:(bool X),(bool X):] is non empty Relation-like set
bool [:(bool X),(bool X):] is non empty set
X is set
bool X is non empty Element of bool (bool X)
bool X is non empty set
bool (bool X) is non empty set
[:(bool X),(bool X):] is non empty Relation-like set
bool [:(bool X),(bool X):] is non empty set
the non empty Relation-like bool X -defined bool X -valued transitive (X) (X) (X) Element of bool [:(bool X),(bool X):] is non empty Relation-like bool X -defined bool X -valued transitive (X) (X) (X) Element of bool [:(bool X),(bool X):]
X is finite countable set
bool X is non empty finite V40() countable Element of bool (bool X)
bool X is non empty finite V40() countable set
bool (bool X) is non empty finite V40() countable set
[:(bool X),(bool X):] is non empty Relation-like finite countable set
bool [:(bool X),(bool X):] is non empty finite V40() countable set
F is Relation-like bool X -defined bool X -valued finite countable Element of bool [:(bool X),(bool X):]
X is finite countable set
bool X is non empty finite V40() countable Element of bool (bool X)
bool X is non empty finite V40() countable set
bool (bool X) is non empty finite V40() countable set
[:(bool X),(bool X):] is non empty Relation-like finite countable set
bool [:(bool X),(bool X):] is non empty finite V40() countable set
the non empty Relation-like bool X -defined bool X -valued finite countable transitive (X) (X) (X) Element of bool [:(bool X),(bool X):] is non empty Relation-like bool X -defined bool X -valued finite countable transitive (X) (X) (X) Element of bool [:(bool X),(bool X):]
K is Relation-like bool X -defined bool X -valued finite countable (X) Element of bool [:(bool X),(bool X):]
F is Relation-like bool X -defined bool X -valued finite countable Element of bool [:(bool X),(bool X):]
X is set
bool X is non empty Element of bool (bool X)
bool X is non empty set
bool (bool X) is non empty set
[:(bool X),(bool X):] is non empty Relation-like set
bool [:(bool X),(bool X):] is non empty set
F is Relation-like bool X -defined bool X -valued Element of bool [:(bool X),(bool X):]
F is Relation-like bool X -defined bool X -valued Element of bool [:(bool X),(bool X):]
X is set
bool X is non empty Element of bool (bool X)
bool X is non empty set
bool (bool X) is non empty set
[:(bool X),(bool X):] is non empty Relation-like set
bool [:(bool X),(bool X):] is non empty set
X is set
bool X is non empty Element of bool (bool X)
bool X is non empty set
bool (bool X) is non empty set
[:(bool X),(bool X):] is non empty Relation-like set
bool [:(bool X),(bool X):] is non empty set
F is Relation-like bool X -defined bool X -valued Element of bool [:(bool X),(bool X):]
dcF is Element of bool X
K is Element of bool X
(X,K,dcF) is V21() Element of (X)
(X) is non empty Relation-like bool X -defined bool X -valued Element of bool [:(bool X),(bool X):]
[:(bool X),(bool X):] is non empty Relation-like bool X -defined bool X -valued Element of bool [:(bool X),(bool X):]
[:(bool X),(bool X):] is non empty Relation-like set
bool [:(bool X),(bool X):] is non empty set
{K,dcF} is non empty finite countable set
{K} is non empty trivial finite 1 -element countable set
{{K,dcF},{K}} is non empty finite V40() countable set
(X,K,K) is V21() Element of (X)
{K,K} is non empty finite countable set
{{K,K},{K}} is non empty finite V40() countable set
F is Relation-like bool X -defined bool X -valued Element of bool [:(bool X),(bool X):]
K is Element of bool X
(X,K,K) is V21() Element of (X)
(X) is non empty Relation-like bool X -defined bool X -valued Element of bool [:(bool X),(bool X):]
[:(bool X),(bool X):] is non empty Relation-like bool X -defined bool X -valued Element of bool [:(bool X),(bool X):]
[:(bool X),(bool X):] is non empty Relation-like set
bool [:(bool X),(bool X):] is non empty set
{K,K} is non empty finite countable set
{K} is non empty trivial finite 1 -element countable set
{{K,K},{K}} is non empty finite V40() countable set
K is Element of bool X
dcF is Element of bool X
(X,K,dcF) is V21() Element of (X)
(X) is non empty Relation-like bool X -defined bool X -valued Element of bool [:(bool X),(bool X):]
[:(bool X),(bool X):] is non empty Relation-like bool X -defined bool X -valued Element of bool [:(bool X),(bool X):]
[:(bool X),(bool X):] is non empty Relation-like set
bool [:(bool X),(bool X):] is non empty set
{K,dcF} is non empty finite countable set
{K} is non empty trivial finite 1 -element countable set
{{K,dcF},{K}} is non empty finite V40() countable set
S is Element of bool X
S is Element of bool X
(X,S,S) is V21() Element of (X)
{S,S} is non empty finite countable set
{S} is non empty trivial finite 1 -element countable set
{{S,S},{S}} is non empty finite V40() countable set
(X,S,K) is V21() Element of (X)
{S,K} is non empty finite countable set
{{S,K},{S}} is non empty finite V40() countable set
(X,S,dcF) is V21() Element of (X)
{S,dcF} is non empty finite countable set
{{S,dcF},{S}} is non empty finite V40() countable set
(X,dcF,S) is V21() Element of (X)
{dcF,S} is non empty finite countable set
{dcF} is non empty trivial finite 1 -element countable set
{{dcF,S},{dcF}} is non empty finite V40() countable set
X is set
bool X is non empty Element of bool (bool X)
bool X is non empty set
bool (bool X) is non empty set
[:(bool X),(bool X):] is non empty Relation-like set
bool [:(bool X),(bool X):] is non empty set
the non empty Relation-like bool X -defined bool X -valued transitive (X) (X) (X) (X) (X) Element of bool [:(bool X),(bool X):] is non empty Relation-like bool X -defined bool X -valued transitive (X) (X) (X) (X) (X) Element of bool [:(bool X),(bool X):]
X is set
bool X is non empty Element of bool (bool X)
bool X is non empty set
bool (bool X) is non empty set
[:(bool X),(bool X):] is non empty Relation-like set
bool [:(bool X),(bool X):] is non empty set
F is Relation-like bool X -defined bool X -valued Element of bool [:(bool X),(bool X):]
X is set
bool X is non empty Element of bool (bool X)
bool X is non empty set
bool (bool X) is non empty set
[:(bool X),(bool X):] is non empty Relation-like set
bool [:(bool X),(bool X):] is non empty set
F is Relation-like bool X -defined bool X -valued Element of bool [:(bool X),(bool X):]
X is set
bool X is non empty Element of bool (bool X)
bool X is non empty set
bool (bool X) is non empty set
[:(bool X),(bool X):] is non empty Relation-like set
bool [:(bool X),(bool X):] is non empty set
F is Relation-like bool X -defined bool X -valued Element of bool [:(bool X),(bool X):]
X is ()
the of X is non empty finite countable set
(X) is Relation-like bool the of X -defined bool the of X -valued finite countable Element of bool [:(bool the of X),(bool the of X):]
bool the of X is non empty finite V40() countable Element of bool (bool the of X)
bool the of X is non empty finite V40() countable set
bool (bool the of X) is non empty finite V40() countable set
[:(bool the of X),(bool the of X):] is non empty Relation-like finite countable set
bool [:(bool the of X),(bool the of X):] is non empty finite V40() countable set
{ [b₁,b₂] where b₁, b₂ is finite countable Element of bool the of X : (X,b₁,b₂) } is set
the of X is functional with_common_domain Element of bool (product the of X)
the of X is Relation-like non-empty the of X -defined Function-like total finite-support set
product the of X is non empty functional with_common_domain product-like set
bool (product the of X) is non empty set
S is finite countable Element of bool the of X
S is finite countable Element of bool the of X
( the of X,S,S) is V21() Element of ( the of X)
( the of X) is non empty Relation-like bool the of X -defined bool the of X -valued finite countable Element of bool [:(bool the of X),(bool the of X):]
[:(bool the of X),(bool the of X):] is non empty Relation-like bool the of X -defined bool the of X -valued finite countable Element of bool [:(bool the of X),(bool the of X):]
[:(bool the of X),(bool the of X):] is non empty Relation-like finite countable set
bool [:(bool the of X),(bool the of X):] is non empty finite V40() countable set
{S,S} is non empty finite V40() countable set
{S} is non empty trivial finite V40() 1 -element countable set
{{S,S},{S}} is non empty finite V40() countable set
ck is finite countable Element of bool the of X
( the of X,S,ck) is V21() Element of ( the of X)
{S,ck} is non empty finite V40() countable set
{S} is non empty trivial finite V40() 1 -element countable set
{{S,ck},{S}} is non empty finite V40() countable set
B is Relation-like Function-like Element of the of X
B | S is Relation-like Function-like finite countable finite-support set
m is Relation-like Function-like Element of the of X
m | S is Relation-like Function-like finite countable finite-support set
B | ck is Relation-like Function-like finite countable finite-support set
m | ck is Relation-like Function-like finite countable finite-support set
B | S is Relation-like Function-like finite countable finite-support set
m | S is Relation-like Function-like finite countable finite-support set
( the of X,S,ck) is V21() Element of ( the of X)
{S,ck} is non empty finite V40() countable set
{{S,ck},{S}} is non empty finite V40() countable set
S is finite countable Element of bool the of X
S is finite countable Element of bool the of X
( the of X,S,S) is V21() Element of ( the of X)
{S,S} is non empty finite V40() countable set
{S} is non empty trivial finite V40() 1 -element countable set
{{S,S},{S}} is non empty finite V40() countable set
ck is Relation-like Function-like Element of the of X
ck | S is Relation-like Function-like finite countable finite-support set
B is Relation-like Function-like Element of the of X
B | S is Relation-like Function-like finite countable finite-support set
ck | S is Relation-like Function-like finite countable finite-support set
B | S is Relation-like Function-like finite countable finite-support set
(ck | S) | S is Relation-like Function-like finite countable finite-support set
S is finite countable Element of bool the of X
S is finite countable Element of bool the of X
( the of X,S,S) is V21() Element of ( the of X)
{S,S} is non empty finite V40() countable set
{S} is non empty trivial finite V40() 1 -element countable set
{{S,S},{S}} is non empty finite V40() countable set
ck is finite countable Element of bool the of X
B is finite countable Element of bool the of X
( the of X,ck,B) is V21() Element of ( the of X)
{ck,B} is non empty finite V40() countable set
{ck} is non empty trivial finite V40() 1 -element countable set
{{ck,B},{ck}} is non empty finite V40() countable set
S \/ ck is finite countable Element of bool the of X
S \/ B is finite countable Element of bool the of X
( the of X,(S \/ ck),(S \/ B)) is V21() Element of ( the of X)
{(S \/ ck),(S \/ B)} is non empty finite V40() countable set
{(S \/ ck)} is non empty trivial finite V40() 1 -element countable set
{{(S \/ ck),(S \/ B)},{(S \/ ck)}} is non empty finite V40() countable set
m is Relation-like Function-like Element of the of X
m | (S \/ ck) is Relation-like Function-like finite countable finite-support set
P is Relation-like Function-like Element of the of X
P | (S \/ ck) is Relation-like Function-like finite countable finite-support set
m | (S \/ B) is Relation-like Function-like finite countable finite-support set
P | (S \/ B) is Relation-like Function-like finite countable finite-support set
m | ck is Relation-like Function-like finite countable finite-support set
(m | (S \/ ck)) | ck is Relation-like Function-like finite countable finite-support set
P | ck is Relation-like Function-like finite countable finite-support set
m | B is Relation-like Function-like finite countable finite-support set
P | B is Relation-like Function-like finite countable finite-support set
m | S is Relation-like Function-like finite countable finite-support set
(m | (S \/ ck)) | S is Relation-like Function-like finite countable finite-support set
P | S is Relation-like Function-like finite countable finite-support set
m | S is Relation-like Function-like finite countable finite-support set
P | S is Relation-like Function-like finite countable finite-support set
(m | S) \/ (m | B) is Relation-like finite countable set
X is set
bool X is non empty set
bool X is non empty Element of bool (bool X)
bool (bool X) is non empty set
[:(bool X),(bool X):] is non empty Relation-like set
bool [:(bool X),(bool X):] is non empty set
F is Element of bool X
{ (X,b₁,b₂) where b₁, b₂ is Element of bool X : ( F c= b₁ or b₂ c= b₁ ) } is set
[:(bool X),(bool X):] is non empty Relation-like bool X -defined bool X -valued Element of bool [:(bool X),(bool X):]
[:(bool X),(bool X):] is non empty Relation-like set
bool [:(bool X),(bool X):] is non empty set
dcF is set
S is Element of bool X
S is Element of bool X
(X,S,S) is V21() Element of (X)
(X) is non empty Relation-like bool X -defined bool X -valued Element of bool [:(bool X),(bool X):]
{S,S} is non empty finite countable set
{S} is non empty trivial finite 1 -element countable set
{{S,S},{S}} is non empty finite V40() countable set
dcF is Relation-like bool X -defined bool X -valued Element of bool [:(bool X),(bool X):]
S is Element of bool X
S is Element of bool X
(X,S,S) is V21() Element of (X)
(X) is non empty Relation-like bool X -defined bool X -valued Element of bool [:(bool X),(bool X):]
{S,S} is non empty finite countable set
{S} is non empty trivial finite 1 -element countable set
{{S,S},{S}} is non empty finite V40() countable set
ck is Element of bool X
B is Element of bool X
(X,ck,B) is V21() Element of (X)
{ck,B} is non empty finite countable set
{ck} is non empty trivial finite 1 -element countable set
{{ck,B},{ck}} is non empty finite V40() countable set
S \/ ck is Element of bool X
S \/ B is Element of bool X
(X,(S \/ ck),(S \/ B)) is V21() Element of (X)
{(S \/ ck),(S \/ B)} is non empty finite countable set
{(S \/ ck)} is non empty trivial finite 1 -element countable set
{{(S \/ ck),(S \/ B)},{(S \/ ck)}} is non empty finite V40() countable set
m is Element of bool X
P is Element of bool X
(X,m,P) is V21() Element of (X)
{m,P} is non empty finite countable set
{m} is non empty trivial finite 1 -element countable set
{{m,P},{m}} is non empty finite V40() countable set
x9 is Element of bool X
y9 is Element of bool X
(X,x9,y9) is V21() Element of (X)
{x9,y9} is non empty finite countable set
{x9} is non empty trivial finite 1 -element countable set
{{x9,y9},{x9}} is non empty finite V40() countable set
S is Element of bool X
S is Element of bool X
(X,S,S) is V21() Element of (X)
(X) is non empty Relation-like bool X -defined bool X -valued Element of bool [:(bool X),(bool X):]
{S,S} is non empty finite countable set
{S} is non empty trivial finite 1 -element countable set
{{S,S},{S}} is non empty finite V40() countable set
ck is Element of bool X
(X,S,ck) is V21() Element of (X)
{S,ck} is non empty finite countable set
{S} is non empty trivial finite 1 -element countable set
{{S,ck},{S}} is non empty finite V40() countable set
B is Element of bool X
m is Element of bool X
(X,B,m) is V21() Element of (X)
{B,m} is non empty finite countable set
{B} is non empty trivial finite 1 -element countable set
{{B,m},{B}} is non empty finite V40() countable set
P is Element of bool X
x9 is Element of bool X
(X,P,x9) is V21() Element of (X)
{P,x9} is non empty finite countable set
{P} is non empty trivial finite 1 -element countable set
{{P,x9},{P}} is non empty finite V40() countable set
(X,S,ck) is V21() Element of (X)
{S,ck} is non empty finite countable set
{{S,ck},{S}} is non empty finite V40() countable set
S is Element of bool X
S is Element of bool X
(X,S,S) is V21() Element of (X)
{S,S} is non empty finite countable set
{S} is non empty trivial finite 1 -element countable set
{{S,S},{S}} is non empty finite V40() countable set
X is set
bool X is non empty Element of bool (bool X)
bool X is non empty set
bool (bool X) is non empty set
[:(bool X),(bool X):] is non empty Relation-like set
bool [:(bool X),(bool X):] is non empty set
F is Relation-like bool X -defined bool X -valued Element of bool [:(bool X),(bool X):]
(X) is non empty Relation-like (X) -defined (X) -valued total reflexive antisymmetric transitive Element of bool [:(X),(X):]
(X) is non empty Relation-like bool X -defined bool X -valued Element of bool [:(bool X),(bool X):]
[:(bool X),(bool X):] is non empty Relation-like bool X -defined bool X -valued Element of bool [:(bool X),(bool X):]
[:(bool X),(bool X):] is non empty Relation-like set
bool [:(bool X),(bool X):] is non empty set
[:(X),(X):] is non empty Relation-like set
bool [:(X),(X):] is non empty set
{ [b₁,b₂] where b₁, b₂ is Element of (X) : (X,b₂,b₁) } is set
(F,(X)) is Relation-like bool X -defined bool X -valued Element of bool F
bool F is non empty set
X is set
bool X is non empty Element of bool (bool X)
bool X is non empty set
bool (bool X) is non empty set
[:(bool X),(bool X):] is non empty Relation-like set
bool [:(bool X),(bool X):] is non empty set
F is Relation-like bool X -defined bool X -valued Element of bool [:(bool X),(bool X):]
(X,F) is Relation-like bool X -defined bool X -valued Element of bool [:(bool X),(bool X):]
(X) is non empty Relation-like (X) -defined (X) -valued total reflexive antisymmetric transitive Element of bool [:(X),(X):]
(X) is non empty Relation-like bool X -defined bool X -valued Element of bool [:(bool X),(bool X):]
[:(bool X),(bool X):] is non empty Relation-like bool X -defined bool X -valued Element of bool [:(bool X),(bool X):]
[:(bool X),(bool X):] is non empty Relation-like set
bool [:(bool X),(bool X):] is non empty set
[:(X),(X):] is non empty Relation-like set
bool [:(X),(X):] is non empty set
{ [b₁,b₂] where b₁, b₂ is Element of (X) : (X,b₂,b₁) } is set
(F,(X)) is Relation-like bool X -defined bool X -valued Element of bool F
bool F is non empty set
X is set
bool X is non empty Element of bool (bool X)
bool X is non empty set
bool (bool X) is non empty set
[:(bool X),(bool X):] is non empty Relation-like set
bool [:(bool X),(bool X):] is non empty set
X is finite countable set
(X) is non empty Relation-like bool X -defined bool X -valued finite countable Element of bool [:(bool X),(bool X):]
bool X is non empty finite V40() countable Element of bool (bool X)
bool X is non empty finite V40() countable set
bool (bool X) is non empty finite V40() countable set
[:(bool X),(bool X):] is non empty Relation-like finite countable set
bool [:(bool X),(bool X):] is non empty finite V40() countable set
[:(bool X),(bool X):] is non empty Relation-like bool X -defined bool X -valued finite countable Element of bool [:(bool X),(bool X):]
[:(bool X),(bool X):] is non empty Relation-like finite countable set
bool [:(bool X),(bool X):] is non empty finite V40() countable set
F is Element of (X)
K is Relation-like bool X -defined bool X -valued finite countable Element of bool [:(bool X),(bool X):]
(X,K) is Relation-like bool X -defined bool X -valued finite countable Element of bool [:(bool X),(bool X):]
(X) is non empty Relation-like (X) -defined (X) -valued total finite countable reflexive antisymmetric transitive Element of bool [:(X),(X):]
[:(X),(X):] is non empty Relation-like finite countable set
bool [:(X),(X):] is non empty finite V40() countable set
{ [b₁,b₂] where b₁, b₂ is Element of (X) : (X,b₂,b₁) } is set
(K,(X)) is Relation-like bool X -defined bool X -valued finite countable Element of bool K
bool K is non empty finite V40() countable set
S is non empty Relation-like bool X -defined bool X -valued finite countable Element of bool [:(bool X),(bool X):]
{ b₁ where b₁ is (X,S) : (X,b₁,F) } is set
field (X) is finite countable set
S is set
ck is set
B is (X,S)
ck is Element of S
B is (X,S)
B is finite countable Element of bool X
m is finite countable Element of bool X
(X,B,m) is V21() Element of (X)
{B,m} is non empty finite V40() countable set
{B} is non empty trivial finite V40() 1 -element countable set
{{B,m},{B}} is non empty finite V40() countable set
P is (X,S)
P is set
[ck,P] is V21() set
{ck,P} is non empty finite countable set
{ck} is non empty trivial finite 1 -element countable set
{{ck,P},{ck}} is non empty finite V40() countable set
x9 is Element of (X)
y9 is Element of (X)
[x9,y9] is V21() set
{x9,y9} is non empty finite countable set
{x9} is non empty trivial finite 1 -element countable set
{{x9,y9},{x9}} is non empty finite V40() countable set
a is (X,S)
k is (X,S)
P is (X,S)
X is set
bool X is non empty Element of bool (bool X)
bool X is non empty set
bool (bool X) is non empty set
[:(bool X),(bool X):] is non empty Relation-like set
bool [:(bool X),(bool X):] is non empty set
F is Relation-like bool X -defined bool X -valued Element of bool [:(bool X),(bool X):]
K is Element of bool X
dcF is Element of bool X
(X,K,dcF) is V21() Element of (X)
(X) is non empty Relation-like bool X -defined bool X -valued Element of bool [:(bool X),(bool X):]
[:(bool X),(bool X):] is non empty Relation-like bool X -defined bool X -valued Element of bool [:(bool X),(bool X):]
[:(bool X),(bool X):] is non empty Relation-like set
bool [:(bool X),(bool X):] is non empty set
{K,dcF} is non empty finite countable set
{K} is non empty trivial finite 1 -element countable set
{{K,dcF},{K}} is non empty finite V40() countable set
(X) is non empty Relation-like (X) -defined (X) -valued total reflexive antisymmetric transitive Element of bool [:(X),(X):]
[:(X),(X):] is non empty Relation-like set
bool [:(X),(X):] is non empty set
{ [b₁,b₂] where b₁, b₂ is Element of (X) : (X,b₂,b₁) } is set
(X,F) is Relation-like bool X -defined bool X -valued Element of bool [:(bool X),(bool X):]
(F,(X)) is Relation-like bool X -defined bool X -valued Element of bool F
bool F is non empty set
S is Element of bool X
ck is Element of bool X
(X,S,ck) is V21() Element of (X)
{S,ck} is non empty finite countable set
{S} is non empty trivial finite 1 -element countable set
{{S,ck},{S}} is non empty finite V40() countable set
[(X,K,dcF),(X,S,ck)] is V21() set
{(X,K,dcF),(X,S,ck)} is non empty Relation-like finite countable set
{(X,K,dcF)} is non empty trivial Relation-like Function-like constant finite 1 -element countable finite-support set
{{(X,K,dcF),(X,S,ck)},{(X,K,dcF)}} is non empty finite V40() countable set
S is set
[(X,K,dcF),S] is V21() set
{(X,K,dcF),S} is non empty finite countable set
{{(X,K,dcF),S},{(X,K,dcF)}} is non empty finite V40() countable set
ck is set
B is set
[ck,B] is V21() set
{ck,B} is non empty finite countable set
{ck} is non empty trivial finite 1 -element countable set
{{ck,B},{ck}} is non empty finite V40() countable set
m is Element of (X)
P is Element of (X)
[m,P] is V21() set
{m,P} is non empty finite countable set
{m} is non empty trivial finite 1 -element countable set
{{m,P},{m}} is non empty finite V40() countable set
x9 is Element of bool X
y9 is Element of bool X
X is set
bool X is non empty Element of bool (bool X)
bool X is non empty set
bool (bool X) is non empty set
[:(bool X),(bool X):] is non empty Relation-like set
bool [:(bool X),(bool X):] is non empty set
X is non empty finite countable set
bool X is non empty finite V40() countable Element of bool (bool X)
bool X is non empty finite V40() countable set
bool (bool X) is non empty finite V40() countable set
[:(bool X),(bool X):] is non empty Relation-like finite countable set
bool [:(bool X),(bool X):] is non empty finite V40() countable set
F is non empty Relation-like bool X -defined bool X -valued finite countable transitive (X) (X) (X) (X) (X) Element of bool [:(bool X),(bool X):]
(X,F) is Relation-like bool X -defined bool X -valued finite countable Element of bool [:(bool X),(bool X):]
(X) is non empty Relation-like (X) -defined (X) -valued total finite countable reflexive antisymmetric transitive Element of bool [:(X),(X):]
(X) is non empty Relation-like bool X -defined bool X -valued finite countable Element of bool [:(bool X),(bool X):]
[:(bool X),(bool X):] is non empty Relation-like bool X -defined bool X -valued finite countable Element of bool [:(bool X),(bool X):]
[:(bool X),(bool X):] is non empty Relation-like finite countable set
bool [:(bool X),(bool X):] is non empty finite V40() countable set
[:(X),(X):] is non empty Relation-like finite countable set
bool [:(X),(X):] is non empty finite V40() countable set
{ [b₁,b₂] where b₁, b₂ is Element of (X) : (X,b₂,b₁) } is set
(F,(X)) is Relation-like bool X -defined bool X -valued finite countable Element of bool F
bool F is non empty finite V40() countable set
field (X) is finite countable set
S is finite countable Element of bool X
(X,S,S) is V21() Element of (X)
{S,S} is non empty finite V40() countable set
{S} is non empty trivial finite V40() 1 -element countable set
{{S,S},{S}} is non empty finite V40() countable set
S is set
ck is set
bool (field (X)) is non empty finite V40() countable set
ck is Element of S
B is set
m is set
[B,m] is V21() set
{B,m} is non empty finite countable set
{B} is non empty trivial finite 1 -element countable set
{{B,m},{B}} is non empty finite V40() countable set
P is finite countable Element of bool X
x9 is finite countable Element of bool X
(X,P,x9) is V21() Element of (X)
{P,x9} is non empty finite V40() countable set
{P} is non empty trivial finite V40() 1 -element countable set
{{P,x9},{P}} is non empty finite V40() countable set
y9 is Element of (X)
y9 is set
[ck,y9] is V21() set
{ck,y9} is non empty finite countable set
{ck} is non empty trivial finite 1 -element countable set
{{ck,y9},{ck}} is non empty finite V40() countable set
a is Element of (X)
k is Element of (X)
[a,k] is V21() set
{a,k} is non empty finite countable set
{a} is non empty trivial finite 1 -element countable set
{{a,k},{a}} is non empty finite V40() countable set
S is Element of (X)
S is finite countable Element of bool X
S is finite countable Element of bool X
(X,S,S) is V21() Element of (X)
{S,S} is non empty finite V40() countable set
{S} is non empty trivial finite V40() 1 -element countable set
{{S,S},{S}} is non empty finite V40() countable set
ck is finite countable Element of bool X
B is finite countable Element of bool X
(X,ck,B) is V21() Element of (X)
{ck,B} is non empty finite V40() countable set
{ck} is non empty trivial finite V40() 1 -element countable set
{{ck,B},{ck}} is non empty finite V40() countable set
[(X,ck,B),(X,S,S)] is V21() set
{(X,ck,B),(X,S,S)} is non empty Relation-like finite countable set
{(X,ck,B)} is non empty trivial Relation-like Function-like constant finite 1 -element countable finite-support set
{{(X,ck,B),(X,S,S)},{(X,ck,B)}} is non empty finite V40() countable set
S is finite countable Element of bool X
S is finite countable Element of bool X
(X,S,S) is V21() Element of (X)
{S,S} is non empty finite V40() countable set
{S} is non empty trivial finite V40() 1 -element countable set
{{S,S},{S}} is non empty finite V40() countable set
ck is finite countable Element of bool X
B is finite countable Element of bool X
(X,ck,B) is V21() Element of (X)
{ck,B} is non empty finite V40() countable set
{ck} is non empty trivial finite V40() 1 -element countable set
{{ck,B},{ck}} is non empty finite V40() countable set
(X,S,B) is V21() Element of (X)
{S,B} is non empty finite V40() countable set
{S} is non empty trivial finite V40() 1 -element countable set
{{S,B},{S}} is non empty finite V40() countable set
(X,S,B) is V21() Element of (X)
{S,B} is non empty finite V40() countable set
{{S,B},{S}} is non empty finite V40() countable set
S \/ B is finite countable Element of bool X
(X,S,(S \/ B)) is V21() Element of (X)
{S,(S \/ B)} is non empty finite V40() countable set
{{S,(S \/ B)},{S}} is non empty finite V40() countable set
S \/ S is finite countable Element of bool X
X is finite countable set
bool X is non empty finite V40() countable Element of bool (bool X)
bool X is non empty finite V40() countable set
bool (bool X) is non empty finite V40() countable set
[:(bool X),(bool X):] is non empty Relation-like finite countable set
bool [:(bool X),(bool X):] is non empty finite V40() countable set
F is Relation-like bool X -defined bool X -valued finite countable Element of bool [:(bool X),(bool X):]
{ (X,b₁,b₂) where b₁, b₂ is finite countable Element of bool X : ex b₃, b₄ being finite countable Element of bool X st
( (X,(X,b₃,b₄),(X,b₁,b₂)) & (X,b₃,b₄) in F ) } is set
K is Relation-like bool X -defined bool X -valued finite countable Element of bool [:(bool X),(bool X):]
(X,K) is Relation-like bool X -defined bool X -valued finite countable Element of bool [:(bool X),(bool X):]
(X) is non empty Relation-like (X) -defined (X) -valued total finite countable reflexive antisymmetric transitive Element of bool [:(X),(X):]
(X) is non empty Relation-like bool X -defined bool X -valued finite countable Element of bool [:(bool X),(bool X):]
[:(bool X),(bool X):] is non empty Relation-like bool X -defined bool X -valued finite countable Element of bool [:(bool X),(bool X):]
[:(bool X),(bool X):] is non empty Relation-like finite countable set
bool [:(bool X),(bool X):] is non empty finite V40() countable set
[:(X),(X):] is non empty Relation-like finite countable set
bool [:(X),(X):] is non empty finite V40() countable set
{ [b₁,b₂] where b₁, b₂ is Element of (X) : (X,b₂,b₁) } is set
(K,(X)) is Relation-like bool X -defined bool X -valued finite countable Element of bool K
bool K is non empty finite V40() countable set
dcF is finite countable Element of bool X
(X,dcF,dcF) is V21() Element of (X)
{dcF,dcF} is non empty finite V40() countable set
{dcF} is non empty trivial finite V40() 1 -element countable set
{{dcF,dcF},{dcF}} is non empty finite V40() countable set
S is finite countable Element of bool X
S is finite countable Element of bool X
(X,S,S) is V21() Element of (X)
{S,S} is non empty finite V40() countable set
{S} is non empty trivial finite V40() 1 -element countable set
{{S,S},{S}} is non empty finite V40() countable set
dcF is set
S is finite countable Element of bool X
S is finite countable Element of bool X
(X,S,S) is V21() Element of (X)
{S,S} is non empty finite V40() countable set
{S} is non empty trivial finite V40() 1 -element countable set
{{S,S},{S}} is non empty finite V40() countable set
ck is finite countable Element of bool X
B is finite countable Element of bool X
(X,ck,B) is V21() Element of (X)
{ck,B} is non empty finite V40() countable set
{ck} is non empty trivial finite V40() 1 -element countable set
{{ck,B},{ck}} is non empty finite V40() countable set
ck is finite countable Element of bool X
B is finite countable Element of bool X
(X,ck,B) is V21() Element of (X)
{ck,B} is non empty finite V40() countable set
{ck} is non empty trivial finite V40() 1 -element countable set
{{ck,B},{ck}} is non empty finite V40() countable set
m is finite countable Element of bool X
P is finite countable Element of bool X
(X,m,P) is V21() Element of (X)
{m,P} is non empty finite V40() countable set
{m} is non empty trivial finite V40() 1 -element countable set
{{m,P},{m}} is non empty finite V40() countable set
x9 is finite countable Element of bool X
y9 is finite countable Element of bool X
(X,x9,y9) is V21() Element of (X)
{x9,y9} is non empty finite V40() countable set
{x9} is non empty trivial finite V40() 1 -element countable set
{{x9,y9},{x9}} is non empty finite V40() countable set
dcF is finite countable Element of bool X
S is finite countable Element of bool X
(X,dcF,S) is V21() Element of (X)
{dcF,S} is non empty finite V40() countable set
{dcF} is non empty trivial finite V40() 1 -element countable set
{{dcF,S},{dcF}} is non empty finite V40() countable set
S is finite countable Element of bool X
ck is finite countable Element of bool X
(X,S,ck) is V21() Element of (X)
{S,ck} is non empty finite V40() countable set
{S} is non empty trivial finite V40() 1 -element countable set
{{S,ck},{S}} is non empty finite V40() countable set
B is finite countable Element of bool X
m is finite countable Element of bool X
(X,B,m) is V21() Element of (X)
{B,m} is non empty finite V40() countable set
{B} is non empty trivial finite V40() 1 -element countable set
{{B,m},{B}} is non empty finite V40() countable set
P is finite countable Element of bool X
x9 is finite countable Element of bool X
(X,P,x9) is V21() Element of (X)
{P,x9} is non empty finite V40() countable set
{P} is non empty trivial finite V40() 1 -element countable set
{{P,x9},{P}} is non empty finite V40() countable set
dcF is finite countable Element of bool X
S is finite countable Element of bool X
(X,dcF,S) is V21() Element of (X)
{dcF,S} is non empty finite V40() countable set
{dcF} is non empty trivial finite V40() 1 -element countable set
{{dcF,S},{dcF}} is non empty finite V40() countable set
S is finite countable Element of bool X
(X,S,S) is V21() Element of (X)
{S,S} is non empty finite V40() countable set
{S} is non empty trivial finite V40() 1 -element countable set
{{S,S},{S}} is non empty finite V40() countable set
ck is finite countable Element of bool X
B is finite countable Element of bool X
(X,ck,B) is V21() Element of (X)
{ck,B} is non empty finite V40() countable set
{ck} is non empty trivial finite V40() 1 -element countable set
{{ck,B},{ck}} is non empty finite V40() countable set
m is finite countable Element of bool X
P is finite countable Element of bool X
(X,m,P) is V21() Element of (X)
{m,P} is non empty finite V40() countable set
{m} is non empty trivial finite V40() 1 -element countable set
{{m,P},{m}} is non empty finite V40() countable set
(X,ck,P) is V21() Element of (X)
{ck,P} is non empty finite V40() countable set
{{ck,P},{ck}} is non empty finite V40() countable set
(X,dcF,S) is V21() Element of (X)
{dcF,S} is non empty finite V40() countable set
{{dcF,S},{dcF}} is non empty finite V40() countable set
dcF is finite countable Element of bool X
S is finite countable Element of bool X
(X,dcF,S) is V21() Element of (X)
{dcF,S} is non empty finite V40() countable set
{dcF} is non empty trivial finite V40() 1 -element countable set
{{dcF,S},{dcF}} is non empty finite V40() countable set
S is finite countable Element of bool X
ck is finite countable Element of bool X
(X,S,ck) is V21() Element of (X)
{S,ck} is non empty finite V40() countable set
{S} is non empty trivial finite V40() 1 -element countable set
{{S,ck},{S}} is non empty finite V40() countable set
dcF \/ S is finite countable Element of bool X
S \/ ck is finite countable Element of bool X
(X,(dcF \/ S),(S \/ ck)) is V21() Element of (X)
{(dcF \/ S),(S \/ ck)} is non empty finite V40() countable set
{(dcF \/ S)} is non empty trivial finite V40() 1 -element countable set
{{(dcF \/ S),(S \/ ck)},{(dcF \/ S)}} is non empty finite V40() countable set
B is finite countable Element of bool X
m is finite countable Element of bool X
(X,B,m) is V21() Element of (X)
{B,m} is non empty finite V40() countable set
{B} is non empty trivial finite V40() 1 -element countable set
{{B,m},{B}} is non empty finite V40() countable set
P is finite countable Element of bool X
x9 is finite countable Element of bool X
(X,P,x9) is V21() Element of (X)
{P,x9} is non empty finite V40() countable set
{P} is non empty trivial finite V40() 1 -element countable set
{{P,x9},{P}} is non empty finite V40() countable set
(X,(dcF \/ S),(dcF \/ S)) is V21() Element of (X)
{(dcF \/ S),(dcF \/ S)} is non empty finite V40() countable set
{{(dcF \/ S),(dcF \/ S)},{(dcF \/ S)}} is non empty finite V40() countable set
y9 is finite countable Element of bool X
a is finite countable Element of bool X
(X,y9,a) is V21() Element of (X)
{y9,a} is non empty finite V40() countable set
{y9} is non empty trivial finite V40() 1 -element countable set
{{y9,a},{y9}} is non empty finite V40() countable set
a \/ a is finite countable Element of bool X
S is set
S is finite countable Element of bool X
ck is finite countable Element of bool X
(X,S,ck) is V21() Element of (X)
{S,ck} is non empty finite V40() countable set
{S} is non empty trivial finite V40() 1 -element countable set
{{S,ck},{S}} is non empty finite V40() countable set
B is set
[S,B] is V21() set
{S,B} is non empty finite countable set
{S} is non empty trivial finite 1 -element countable set
{{S,B},{S}} is non empty finite V40() countable set
m is Element of (X)
P is Element of (X)
[m,P] is V21() set
{m,P} is non empty finite countable set
{m} is non empty trivial finite 1 -element countable set
{{m,P},{m}} is non empty finite V40() countable set
x9 is finite countable Element of bool X
y9 is finite countable Element of bool X
(X,x9,y9) is V21() Element of (X)
{x9,y9} is non empty finite V40() countable set
{x9} is non empty trivial finite V40() 1 -element countable set
{{x9,y9},{x9}} is non empty finite V40() countable set
a is finite countable Element of bool X
k is finite countable Element of bool X
(X,a,k) is V21() Element of (X)
{a,k} is non empty finite V40() countable set
{a} is non empty trivial finite V40() 1 -element countable set
{{a,k},{a}} is non empty finite V40() countable set
S is finite countable Element of bool X
ck is finite countable Element of bool X
(X,S,ck) is V21() Element of (X)
{S,ck} is non empty finite V40() countable set
{S} is non empty trivial finite V40() 1 -element countable set
{{S,ck},{S}} is non empty finite V40() countable set
B is finite countable Element of bool X
m is finite countable Element of bool X
(X,B,m) is V21() Element of (X)
{B,m} is non empty finite V40() countable set
{B} is non empty trivial finite V40() 1 -element countable set
{{B,m},{B}} is non empty finite V40() countable set
[(X,S,ck),(X,B,m)] is V21() set
{(X,S,ck),(X,B,m)} is non empty Relation-like finite countable set
{(X,S,ck)} is non empty trivial Relation-like Function-like constant finite 1 -element countable finite-support set
{{(X,S,ck),(X,B,m)},{(X,S,ck)}} is non empty finite V40() countable set
S is finite countable Element of bool X
S is finite countable Element of bool X
(X,S,S) is V21() Element of (X)
{S,S} is non empty finite V40() countable set
{S} is non empty trivial finite V40() 1 -element countable set
{{S,S},{S}} is non empty finite V40() countable set
ck is finite countable Element of bool X
B is finite countable Element of bool X
(X,ck,B) is V21() Element of (X)
{ck,B} is non empty finite V40() countable set
{ck} is non empty trivial finite V40() 1 -element countable set
{{ck,B},{ck}} is non empty finite V40() countable set
m is finite countable Element of bool X
P is finite countable Element of bool X
(X,m,P) is V21() Element of (X)
{m,P} is non empty finite V40() countable set
{m} is non empty trivial finite V40() 1 -element countable set
{{m,P},{m}} is non empty finite V40() countable set
S is non empty Relation-like bool X -defined bool X -valued finite countable transitive (X) (X) (X) (X) (X) Element of bool [:(bool X),(bool X):]
(X,S) is Relation-like bool X -defined bool X -valued finite countable Element of bool [:(bool X),(bool X):]
(S,(X)) is Relation-like bool X -defined bool X -valued finite countable Element of bool S
bool S is non empty finite V40() countable set
field (X) is finite countable set
S is set
ck is finite countable Element of bool X
B is finite countable Element of bool X
(X,ck,B) is V21() Element of (X)
{ck,B} is non empty finite V40() countable set
{ck} is non empty trivial finite V40() 1 -element countable set
{{ck,B},{ck}} is non empty finite V40() countable set
m is set
P is set
bool (field (X)) is non empty finite V40() countable set
P is Element of m
x9 is set
[P,x9] is V21() set
{P,x9} is non empty finite countable set
{P} is non empty trivial finite 1 -element countable set
{{P,x9},{P}} is non empty finite V40() countable set
y9 is Element of (X)
a is Element of (X)
[y9,a] is V21() set
{y9,a} is non empty finite countable set
{y9} is non empty trivial finite 1 -element countable set
{{y9,a},{y9}} is non empty finite V40() countable set
k is Element of (X)
x9 is Element of (X)
y9 is finite countable Element of bool X
a is finite countable Element of bool X
(X,y9,a) is V21() Element of (X)
{y9,a} is non empty finite V40() countable set
{y9} is non empty trivial finite V40() 1 -element countable set
{{y9,a},{y9}} is non empty finite V40() countable set
ck is finite countable Element of bool X
B is finite countable Element of bool X
(X,ck,B) is V21() Element of (X)
{ck,B} is non empty finite V40() countable set
{ck} is non empty trivial finite V40() 1 -element countable set
{{ck,B},{ck}} is non empty finite V40() countable set
m is finite countable Element of bool X
P is finite countable Element of bool X
(X,m,P) is V21() Element of (X)
{m,P} is non empty finite V40() countable set
{m} is non empty trivial finite V40() 1 -element countable set
{{m,P},{m}} is non empty finite V40() countable set
X is non empty finite countable set
bool X is non empty finite V40() countable Element of bool (bool X)
bool X is non empty finite V40() countable set
bool (bool X) is non empty finite V40() countable set
[:(bool X),(bool X):] is non empty Relation-like finite countable set
bool [:(bool X),(bool X):] is non empty finite V40() countable set
F is non empty Relation-like bool X -defined bool X -valued finite countable transitive (X) (X) (X) (X) (X) Element of bool [:(bool X),(bool X):]
(X,F) is Relation-like bool X -defined bool X -valued finite countable Element of bool [:(bool X),(bool X):]
(X) is non empty Relation-like (X) -defined (X) -valued total finite countable reflexive antisymmetric transitive Element of bool [:(X),(X):]
(X) is non empty Relation-like bool X -defined bool X -valued finite countable Element of bool [:(bool X),(bool X):]
[:(bool X),(bool X):] is non empty Relation-like bool X -defined bool X -valued finite countable Element of bool [:(bool X),(bool X):]
[:(bool X),(bool X):] is non empty Relation-like finite countable set
bool [:(bool X),(bool X):] is non empty finite V40() countable set
[:(X),(X):] is non empty Relation-like finite countable set
bool [:(X),(X):] is non empty finite V40() countable set
{ [b₁,b₂] where b₁, b₂ is Element of (X) : (X,b₂,b₁) } is set
(F,(X)) is Relation-like bool X -defined bool X -valued finite countable Element of bool F
bool F is non empty finite V40() countable set
[#] X is non empty non proper finite countable Element of bool X
(X,([#] X),([#] X)) is V21() Element of (X)
{([#] X),([#] X)} is non empty finite V40() countable set
{([#] X)} is non empty trivial finite V40() 1 -element countable set
{{([#] X),([#] X)},{([#] X)}} is non empty finite V40() countable set
dcF is finite countable Element of bool X
S is finite countable Element of bool X
(X,dcF,S) is V21() Element of (X)
{dcF,S} is non empty finite V40() countable set
{dcF} is non empty trivial finite V40() 1 -element countable set
{{dcF,S},{dcF}} is non empty finite V40() countable set
X is finite countable set
bool X is non empty finite V40() countable Element of bool (bool X)
bool X is non empty finite V40() countable set
bool (bool X) is non empty finite V40() countable set
[:(bool X),(bool X):] is non empty Relation-like finite countable set
bool [:(bool X),(bool X):] is non empty finite V40() countable set
F is Relation-like bool X -defined bool X -valued finite countable Element of bool [:(bool X),(bool X):]
(X,F) is Relation-like bool X -defined bool X -valued finite countable Element of bool [:(bool X),(bool X):]
(X) is non empty Relation-like (X) -defined (X) -valued total finite countable reflexive antisymmetric transitive Element of bool [:(X),(X):]
(X) is non empty Relation-like bool X -defined bool X -valued finite countable Element of bool [:(bool X),(bool X):]
[:(bool X),(bool X):] is non empty Relation-like bool X -defined bool X -valued finite countable Element of bool [:(bool X),(bool X):]
[:(bool X),(bool X):] is non empty Relation-like finite countable set
bool [:(bool X),(bool X):] is non empty finite V40() countable set
[:(X),(X):] is non empty Relation-like finite countable set
bool [:(X),(X):] is non empty finite V40() countable set
{ [b₁,b₂] where b₁, b₂ is Element of (X) : (X,b₂,b₁) } is set
(F,(X)) is Relation-like bool X -defined bool X -valued finite countable Element of bool F
bool F is non empty finite V40() countable set
K is finite countable Element of bool X
{ (X,b₁,b₂) where b₁, b₂ is finite countable Element of bool X : ( K c= b₁ or b₂ c= b₁ ) } is set
[K,X] is V21() set
{K,X} is non empty finite V40() countable set
{K} is non empty trivial finite V40() 1 -element countable set
{{K,X},{K}} is non empty finite V40() countable set
{[K,X]} is non empty trivial Relation-like Function-like constant finite 1 -element countable finite-support set
{ (X,b₁,b₁) where b₁ is finite countable Element of bool X : not K c= b₁ } is set
{[K,X]} \/ { (X,b₁,b₁) where b₁ is finite countable Element of bool X : not K c= b₁ } is non empty set
S is finite countable Element of bool X
(X,S,S) is V21() Element of (X)
{S,S} is non empty finite V40() countable set
{S} is non empty trivial finite V40() 1 -element countable set
{{S,S},{S}} is non empty finite V40() countable set
[#] X is non proper finite countable Element of bool X
S is set
S is finite countable Element of bool X
(X,S,S) is V21() Element of (X)
{S,S} is non empty finite V40() countable set
{S} is non empty trivial finite V40() 1 -element countable set
{{S,S},{S}} is non empty finite V40() countable set
S is finite countable Element of bool X
S is finite countable Element of bool X
(X,S,S) is V21() Element of (X)
{S,S} is non empty finite V40() countable set
{S} is non empty trivial finite V40() 1 -element countable set
{{S,S},{S}} is non empty finite V40() countable set
ck is finite countable Element of bool X
(X,ck,ck) is V21() Element of (X)
{ck,ck} is non empty finite V40() countable set
{ck} is non empty trivial finite V40() 1 -element countable set
{{ck,ck},{ck}} is non empty finite V40() countable set
S is Relation-like bool X -defined bool X -valued finite countable Element of bool [:(bool X),(bool X):]
{ (X,b₁,b₂) where b₁, b₂ is finite countable Element of bool X : ex b₃, b₄ being finite countable Element of bool X st
( (X,(X,b₃,b₄),(X,b₁,b₂)) & (X,b₃,b₄) in S ) } is set
ck is set
B is finite countable Element of bool X
m is finite countable Element of bool X
(X,B,m) is V21() Element of (X)
{B,m} is non empty finite V40() countable set
{B} is non empty trivial finite V40() 1 -element countable set
{{B,m},{B}} is non empty finite V40() countable set
P is finite countable Element of bool X
x9 is finite countable Element of bool X
(X,P,x9) is V21() Element of (X)
{P,x9} is non empty finite V40() countable set
{P} is non empty trivial finite V40() 1 -element countable set
{{P,x9},{P}} is non empty finite V40() countable set
ck is finite countable Element of bool X
B is finite countable Element of bool X
(X,ck,B) is V21() Element of (X)
{ck,B} is non empty finite V40() countable set
{ck} is non empty trivial finite V40() 1 -element countable set
{{ck,B},{ck}} is non empty finite V40() countable set
m is finite countable Element of bool X
P is finite countable Element of bool X
(X,m,P) is V21() Element of (X)
{m,P} is non empty finite V40() countable set
{m} is non empty trivial finite V40() 1 -element countable set
{{m,P},{m}} is non empty finite V40() countable set
B is set
m is finite countable Element of bool X
P is finite countable Element of bool X
(X,m,P) is V21() Element of (X)
{m,P} is non empty finite V40() countable set
{m} is non empty trivial finite V40() 1 -element countable set
{{m,P},{m}} is non empty finite V40() countable set
(X,K,([#] X)) is V21() Element of (X)
{K,([#] X)} is non empty finite V40() countable set
{{K,([#] X)},{K}} is non empty finite V40() countable set
ck is Relation-like bool X -defined bool X -valued finite countable Element of bool [:(bool X),(bool X):]
(X,m,m) is V21() Element of (X)
{m,m} is non empty finite V40() countable set
{{m,m},{m}} is non empty finite V40() countable set
ck is Relation-like bool X -defined bool X -valued finite countable Element of bool [:(bool X),(bool X):]
ck is Relation-like bool X -defined bool X -valued finite countable Element of bool [:(bool X),(bool X):]
ck is Relation-like bool X -defined bool X -valued finite countable Element of bool [:(bool X),(bool X):]
m is finite countable Element of bool X
P is finite countable Element of bool X
(X,m,P) is V21() Element of (X)
{m,P} is non empty finite V40() countable set
{m} is non empty trivial finite V40() 1 -element countable set
{{m,P},{m}} is non empty finite V40() countable set
x9 is finite countable Element of bool X
y9 is finite countable Element of bool X
(X,x9,y9) is V21() Element of (X)
{x9,y9} is non empty finite V40() countable set
{x9} is non empty trivial finite V40() 1 -element countable set
{{x9,y9},{x9}} is non empty finite V40() countable set
x9 is finite countable Element of bool X
y9 is finite countable Element of bool X
(X,x9,y9) is V21() Element of (X)
{x9,y9} is non empty finite V40() countable set
{x9} is non empty trivial finite V40() 1 -element countable set
{{x9,y9},{x9}} is non empty finite V40() countable set
a is finite countable Element of bool X
(X,a,a) is V21() Element of (X)
{a,a} is non empty finite V40() countable set
{a} is non empty trivial finite V40() 1 -element countable set
{{a,a},{a}} is non empty finite V40() countable set
B is finite countable Element of bool X
m is finite countable Element of bool X
(X,B,m) is V21() Element of (X)
{B,m} is non empty finite V40() countable set
{B} is non empty trivial finite V40() 1 -element countable set
{{B,m},{B}} is non empty finite V40() countable set
P is finite countable Element of bool X
x9 is finite countable Element of bool X
(X,P,x9) is V21() Element of (X)
{P,x9} is non empty finite V40() countable set
{P} is non empty trivial finite V40() 1 -element countable set
{{P,x9},{P}} is non empty finite V40() countable set
B is finite countable Element of bool X
(X,B,B) is V21() Element of (X)
{B,B} is non empty finite V40() countable set
{B} is non empty trivial finite V40() 1 -element countable set
{{B,B},{B}} is non empty finite V40() countable set
m is finite countable Element of bool X
P is non proper finite countable Element of bool X
(X,m,P) is V21() Element of (X)
{m,P} is non empty finite V40() countable set
{m} is non empty trivial finite V40() 1 -element countable set
{{m,P},{m}} is non empty finite V40() countable set
m is finite countable Element of bool X
P is finite countable Element of bool X
(X,m,P) is V21() Element of (X)
{m,P} is non empty finite V40() countable set
{m} is non empty trivial finite V40() 1 -element countable set
{{m,P},{m}} is non empty finite V40() countable set
(X,ck) is Relation-like bool X -defined bool X -valued finite countable Element of bool [:(bool X),(bool X):]
(ck,(X)) is Relation-like bool X -defined bool X -valued finite countable Element of bool ck
bool ck is non empty finite V40() countable set
X is set
bool X is non empty Element of bool (bool X)
bool X is non empty set
bool (bool X) is non empty set
[:(bool X),(bool X):] is non empty Relation-like set
bool [:(bool X),(bool X):] is non empty set
F is Relation-like bool X -defined bool X -valued Element of bool [:(bool X),(bool X):]
{ b₁ where b₁ is Element of bool X : not for b₂ being Element of bool X holds (X,F,b₂,b₁) } is set
dcF is set
S is Element of bool X
S is Element of bool X
X is set
bool X is non empty Element of bool (bool X)
bool X is non empty set
bool (bool X) is non empty set
[:(bool X),(bool X):] is non empty Relation-like set
bool [:(bool X),(bool X):] is non empty set
X is set
bool X is non empty Element of bool (bool X)
bool X is non empty set
bool (bool X) is non empty set
[:(bool X),(bool X):] is non empty Relation-like set
bool [:(bool X),(bool X):] is non empty set
F is Relation-like bool X -defined bool X -valued finite countable Element of bool [:(bool X),(bool X):]
(X,F) is Element of bool (bool X)
{ b₁ where b₁ is Element of bool X : not for b₂ being Element of bool X holds (X,F,b₂,b₁) } is set
dcF is set
S is Element of bool X
S is Element of bool X
(X,S,S) is V21() Element of (X)
(X) is non empty Relation-like bool X -defined bool X -valued Element of bool [:(bool X),(bool X):]
[:(bool X),(bool X):] is non empty Relation-like bool X -defined bool X -valued Element of bool [:(bool X),(bool X):]
[:(bool X),(bool X):] is non empty Relation-like set
bool [:(bool X),(bool X):] is non empty set
{S,S} is non empty finite countable set
{S} is non empty trivial finite 1 -element countable set
{{S,S},{S}} is non empty finite V40() countable set
B is set
ck is set
[ck,B] is V21() set
{ck,B} is non empty finite countable set
{ck} is non empty trivial finite 1 -element countable set
{{ck,B},{ck}} is non empty finite V40() countable set
[ck,B] `2 is set
dcF is Relation-like Function-like set
proj1 dcF is set
proj2 dcF is set
S is set
S is Element of bool X
ck is Element of bool X
ck is Element of bool X
(X,ck,S) is V21() Element of (X)
(X) is non empty Relation-like bool X -defined bool X -valued Element of bool [:(bool X),(bool X):]
[:(bool X),(bool X):] is non empty Relation-like bool X -defined bool X -valued Element of bool [:(bool X),(bool X):]
[:(bool X),(bool X):] is non empty Relation-like set
bool [:(bool X),(bool X):] is non empty set
{ck,S} is non empty finite countable set
{ck} is non empty trivial finite 1 -element countable set
{{ck,S},{ck}} is non empty finite V40() countable set
(X,F) is Relation-like bool X -defined bool X -valued Element of bool [:(bool X),(bool X):]
(X) is non empty Relation-like (X) -defined (X) -valued total reflexive antisymmetric transitive Element of bool [:(X),(X):]
[:(X),(X):] is non empty Relation-like set
bool [:(X),(X):] is non empty set
{ [b<sub>1</sub>,b<sub>2</sub>] where b<sub>1</sub>, b<sub>2</sub> is Element of (X) : (X,b<sub>2</sub>,b<sub>1</sub>) } is set
(F,(X)) is Relation-like bool X -defined bool X -valued finite countable Element of bool F
bool F is non empty finite V40() countable set
dcF . (X,ck,S) is set
(X,ck,S) `2 is set
B is set
m is set
[B,m] is V21() set
{B,m} is non empty finite countable set
{B} is non empty trivial finite 1 -element countable set
{{B,m},{B}} is non empty finite V40() countable set
[B,m] `2 is set
X is set
bool X is non empty Element of bool (bool X)
bool X is non empty set
bool (bool X) is non empty set
[:(bool X),(bool X):] is non empty Relation-like set
bool [:(bool X),(bool X):] is non empty set
F is set
K is Relation-like bool X -defined bool X -valued Element of bool [:(bool X),(bool X):]
(X,K) is Element of bool (bool X)
{ b<sub>1</sub> where b<sub>1</sub> is Element of bool X : not for b<sub>2</sub> being Element of bool X holds (X,K,b<sub>2</sub>,b<sub>1</sub>) } is set
dcF is Element of bool X
S is Element of bool X
S is Element of bool X
S is Element of bool X
ck is Element of bool X
dcF is Element of bool X
S is Element of bool X
X is non empty finite countable set
bool X is non empty finite V40() countable Element of bool (bool X)
bool X is non empty finite V40() countable set
bool (bool X) is non empty finite V40() countable set
[:(bool X),(bool X):] is non empty Relation-like finite countable set
bool [:(bool X),(bool X):] is non empty finite V40() countable set
F is non empty Relation-like bool X -defined bool X -valued finite countable transitive (X) (X) (X) (X) (X) Element of bool [:(bool X),(bool X):]
(X,F) is finite V40() countable Element of bool (bool X)
{ b<sub>1</sub> where b<sub>1</sub> is Element of bool X : not for b<sub>2</sub> being Element of bool X holds (X,F,b<sub>2</sub>,b<sub>1</sub>) } is set
(X,F) is non empty Relation-like bool X -defined bool X -valued finite countable Element of bool [:(bool X),(bool X):]
(X) is non empty Relation-like (X) -defined (X) -valued total finite countable reflexive antisymmetric transitive Element of bool [:(X),(X):]
(X) is non empty Relation-like bool X -defined bool X -valued finite countable Element of bool [:(bool X),(bool X):]
[:(bool X),(bool X):] is non empty Relation-like bool X -defined bool X -valued finite countable Element of bool [:(bool X),(bool X):]
[:(bool X),(bool X):] is non empty Relation-like finite countable set
bool [:(bool X),(bool X):] is non empty finite V40() countable set
[:(X),(X):] is non empty Relation-like finite countable set
bool [:(X),(X):] is non empty finite V40() countable set
{ [b<sub>1</sub>,b<sub>2</sub>] where b<sub>1</sub>, b<sub>2</sub> is Element of (X) : (X,b<sub>2</sub>,b<sub>1</sub>) } is set
(F,(X)) is Relation-like bool X -defined bool X -valued finite countable Element of bool F
bool F is non empty finite V40() countable set
[#] X is non empty non proper finite countable Element of bool X
(X,([#] X),([#] X)) is V21() Element of (X)
{([#] X),([#] X)} is non empty finite V40() countable set
{([#] X)} is non empty trivial finite V40() 1 -element countable set
{{([#] X),([#] X)},{([#] X)}} is non empty finite V40() countable set
dcF is finite countable Element of bool X
S is finite countable Element of bool X
(X,dcF,S) is V21() Element of (X)
{dcF,S} is non empty finite V40() countable set
{dcF} is non empty trivial finite V40() 1 -element countable set
{{dcF,S},{dcF}} is non empty finite V40() countable set
S is set
ck is set
S /\ ck is set
P is finite countable Element of bool X
x9 is finite countable Element of bool X
(X,x9,P) is V21() Element of (X)
{x9,P} is non empty finite V40() countable set
{x9} is non empty trivial finite V40() 1 -element countable set
{{x9,P},{x9}} is non empty finite V40() countable set
y9 is finite countable Element of bool X
a is finite countable Element of bool X
(X,a,y9) is V21() Element of (X)
{a,y9} is non empty finite V40() countable set
{a} is non empty trivial finite V40() 1 -element countable set
{{a,y9},{a}} is non empty finite V40() countable set
B is finite countable Element of bool X
m is finite countable Element of bool X
B /\ m is finite countable Element of bool X
(X,(B /\ m),(B /\ m)) is V21() Element of (X)
{(B /\ m),(B /\ m)} is non empty finite V40() countable set
{(B /\ m)} is non empty trivial finite V40() 1 -element countable set
{{(B /\ m),(B /\ m)},{(B /\ m)}} is non empty finite V40() countable set
k is finite countable Element of bool X
S is finite countable Element of bool X
(X,k,S) is V21() Element of (X)
{k,S} is non empty finite V40() countable set
{k} is non empty trivial finite V40() 1 -element countable set
{{k,S},{k}} is non empty finite V40() countable set
X is set
bool X is non empty set
F is set
{ (X,b<sub>1</sub>,b<sub>2</sub>) where b<sub>1</sub>, b<sub>2</sub> is Element of bool X : for b<sub>3</sub> being set holds
( not b<sub>3</sub> in F or not b<sub>1</sub> c= b<sub>3</sub> or b<sub>2</sub> c= b<sub>3</sub> ) } is set
bool X is non empty Element of bool (bool X)
bool (bool X) is non empty set
[:(bool X),(bool X):] is non empty Relation-like set
bool [:(bool X),(bool X):] is non empty set
[:(bool X),(bool X):] is non empty Relation-like bool X -defined bool X -valued Element of bool [:(bool X),(bool X):]
[:(bool X),(bool X):] is non empty Relation-like set
bool [:(bool X),(bool X):] is non empty set
dcF is set
S is Element of bool X
S is Element of bool X
(X,S,S) is V21() Element of (X)
(X) is non empty Relation-like bool X -defined bool X -valued Element of bool [:(bool X),(bool X):]
{S,S} is non empty finite countable set
{S} is non empty trivial finite 1 -element countable set
{{S,S},{S}} is non empty finite V40() countable set
X is set
bool X is non empty set
bool (bool X) is non empty set
bool X is non empty Element of bool (bool X)
[:(bool X),(bool X):] is non empty Relation-like set
bool [:(bool X),(bool X):] is non empty set
F is Element of bool (bool X)
(X,F) is Relation-like bool X -defined bool X -valued Element of bool [:(bool X),(bool X):]
{ (X,b<sub>1</sub>,b<sub>2</sub>) where b<sub>1</sub>, b<sub>2</sub> is Element of bool X : for b<sub>3</sub> being set holds
( not b<sub>3</sub> in F or not b<sub>1</sub> c= b<sub>3</sub> or b<sub>2</sub> c= b<sub>3</sub> ) } is set
S is set
(X) is non empty Relation-like bool X -defined bool X -valued Element of bool [:(bool X),(bool X):]
[:(bool X),(bool X):] is non empty Relation-like bool X -defined bool X -valued Element of bool [:(bool X),(bool X):]
[:(bool X),(bool X):] is non empty Relation-like set
bool [:(bool X),(bool X):] is non empty set
S is set
ck is set
[S,ck] is V21() set
{S,ck} is non empty finite countable set
{S} is non empty trivial finite 1 -element countable set
{{S,ck},{S}} is non empty finite V40() countable set
B is set
S is Element of bool X
(X,S,S) is V21() Element of (X)
(X) is non empty Relation-like bool X -defined bool X -valued Element of bool [:(bool X),(bool X):]
[:(bool X),(bool X):] is non empty Relation-like bool X -defined bool X -valued Element of bool [:(bool X),(bool X):]
[:(bool X),(bool X):] is non empty Relation-like set
bool [:(bool X),(bool X):] is non empty set
{S,S} is non empty finite countable set
{S} is non empty trivial finite 1 -element countable set
{{S,S},{S}} is non empty finite V40() countable set
S is non empty Element of bool (bool X)
ck is set
S is non empty Element of bool (bool X)
S is Element of bool X
ck is Element of bool X
(X,S,ck) is V21() Element of (X)
(X) is non empty Relation-like bool X -defined bool X -valued Element of bool [:(bool X),(bool X):]
[:(bool X),(bool X):] is non empty Relation-like bool X -defined bool X -valued Element of bool [:(bool X),(bool X):]
[:(bool X),(bool X):] is non empty Relation-like set
bool [:(bool X),(bool X):] is non empty set
{S,ck} is non empty finite countable set
{S} is non empty trivial finite 1 -element countable set
{{S,ck},{S}} is non empty finite V40() countable set
B is Element of S
m is Element of bool X
P is Element of bool X
(X,m,P) is V21() Element of (X)
{m,P} is non empty finite countable set
{m} is non empty trivial finite 1 -element countable set
{{m,P},{m}} is non empty finite V40() countable set
S is Element of bool X
ck is Element of bool X
(X,S,ck) is V21() Element of (X)
{S,ck} is non empty finite countable set
{S} is non empty trivial finite 1 -element countable set
{{S,ck},{S}} is non empty finite V40() countable set
B is Element of bool X
(X,ck,B) is V21() Element of (X)
{ck,B} is non empty finite countable set
{ck} is non empty trivial finite 1 -element countable set
{{ck,B},{ck}} is non empty finite V40() countable set
m is set
(X,S,B) is V21() Element of (X)
{S,B} is non empty finite countable set
{{S,B},{S}} is non empty finite V40() countable set
S is Element of bool X
ck is Element of bool X
(X,S,ck) is V21() Element of (X)
{S,ck} is non empty finite countable set
{S} is non empty trivial finite 1 -element countable set
{{S,ck},{S}} is non empty finite V40() countable set
B is Element of bool X
m is Element of bool X
(X,B,m) is V21() Element of (X)
{B,m} is non empty finite countable set
{B} is non empty trivial finite 1 -element countable set
{{B,m},{B}} is non empty finite V40() countable set
P is set
S is Element of bool X
ck is Element of bool X
(X,S,ck) is V21() Element of (X)
{S,ck} is non empty finite countable set
{S} is non empty trivial finite 1 -element countable set
{{S,ck},{S}} is non empty finite V40() countable set
B is Element of bool X
m is Element of bool X
(X,B,m) is V21() Element of (X)
{B,m} is non empty finite countable set
{B} is non empty trivial finite 1 -element countable set
{{B,m},{B}} is non empty finite V40() countable set
S \/ B is Element of bool X
ck \/ m is Element of bool X
(X,(S \/ B),(ck \/ m)) is V21() Element of (X)
{(S \/ B),(ck \/ m)} is non empty finite countable set
{(S \/ B)} is non empty trivial finite 1 -element countable set
{{(S \/ B),(ck \/ m)},{(S \/ B)}} is non empty finite V40() countable set
P is set
X is non empty finite countable set
bool X is non empty finite V40() countable set
bool (bool X) is non empty finite V40() countable set
F is finite V40() countable Element of bool (bool X)
(X,F) is Relation-like bool X -defined bool X -valued finite countable Element of bool [:(bool X),(bool X):]
bool X is non empty finite V40() countable Element of bool (bool X)
[:(bool X),(bool X):] is non empty Relation-like finite countable set
bool [:(bool X),(bool X):] is non empty finite V40() countable set
{ (X,b<sub>1</sub>,b<sub>2</sub>) where b<sub>1</sub>, b<sub>2</sub> is Element of bool X : for b<sub>3</sub> being set holds
( not b<sub>3</sub> in F or not b<sub>1</sub> c= b<sub>3</sub> or b<sub>2</sub> c= b<sub>3</sub> ) } is set
(X,(X,F)) is finite V40() countable Element of bool (bool X)
{ b<sub>1</sub> where b<sub>1</sub> is Element of bool X : not for b<sub>2</sub> being Element of bool X holds (X,(X,F),b<sub>2</sub>,b<sub>1</sub>) } is set
dcF is non empty Relation-like bool X -defined bool X -valued finite countable transitive (X) (X) (X) (X) (X) Element of bool [:(bool X),(bool X):]
(X,dcF) is non empty Relation-like bool X -defined bool X -valued finite countable Element of bool [:(bool X),(bool X):]
(X) is non empty Relation-like (X) -defined (X) -valued total finite countable reflexive antisymmetric transitive Element of bool [:(X),(X):]
(X) is non empty Relation-like bool X -defined bool X -valued finite countable Element of bool [:(bool X),(bool X):]
[:(bool X),(bool X):] is non empty Relation-like bool X -defined bool X -valued finite countable Element of bool [:(bool X),(bool X):]
[:(bool X),(bool X):] is non empty Relation-like finite countable set
bool [:(bool X),(bool X):] is non empty finite V40() countable set
[:(X),(X):] is non empty Relation-like finite countable set
bool [:(X),(X):] is non empty finite V40() countable set
{ [b<sub>1</sub>,b<sub>2</sub>] where b<sub>1</sub>, b<sub>2</sub> is Element of (X) : (X,b<sub>2</sub>,b<sub>1</sub>) } is set
(dcF,(X)) is Relation-like bool X -defined bool X -valued finite countable Element of bool dcF
bool dcF is non empty finite V40() countable set
S is set
B is finite countable Element of bool X
(X,B,B) is V21() Element of (X)
{B,B} is non empty finite V40() countable set
{B} is non empty trivial finite V40() 1 -element countable set
{{B,B},{B}} is non empty finite V40() countable set
m is finite countable Element of bool X
P is finite countable Element of bool X
(X,m,P) is V21() Element of (X)
{m,P} is non empty finite V40() countable set
{m} is non empty trivial finite V40() 1 -element countable set
{{m,P},{m}} is non empty finite V40() countable set
x9 is finite countable Element of bool X
y9 is finite countable Element of bool X
(X,x9,y9) is V21() Element of (X)
{x9,y9} is non empty finite V40() countable set
{x9} is non empty trivial finite V40() 1 -element countable set
{{x9,y9},{x9}} is non empty finite V40() countable set
ck is finite countable Element of F
X is non empty finite countable set
bool X is non empty finite V40() countable set
bool (bool X) is non empty finite V40() countable set
bool X is non empty finite V40() countable Element of bool (bool X)
[:(bool X),(bool X):] is non empty Relation-like finite countable set
bool [:(bool X),(bool X):] is non empty finite V40() countable set
F is finite V40() countable Element of bool (bool X)
(X,F) is Relation-like bool X -defined bool X -valued finite countable Element of bool [:(bool X),(bool X):]
{ (X,b<sub>1</sub>,b<sub>2</sub>) where b<sub>1</sub>, b<sub>2</sub> is Element of bool X : for b<sub>3</sub> being set holds
( not b<sub>3</sub> in F or not b<sub>1</sub> c= b<sub>3</sub> or b<sub>2</sub> c= b<sub>3</sub> ) } is set
(X,(X,F)) is finite V40() countable Element of bool (bool X)
{ b<sub>1</sub> where b<sub>1</sub> is Element of bool X : not for b<sub>2</sub> being Element of bool X holds (X,(X,F),b<sub>2</sub>,b<sub>1</sub>) } is set
dcF is non empty Relation-like bool X -defined bool X -valued finite countable transitive (X) (X) (X) (X) (X) Element of bool [:(bool X),(bool X):]
(X,dcF) is non empty Relation-like bool X -defined bool X -valued finite countable Element of bool [:(bool X),(bool X):]
(X) is non empty Relation-like (X) -defined (X) -valued total finite countable reflexive antisymmetric transitive Element of bool [:(X),(X):]
(X) is non empty Relation-like bool X -defined bool X -valued finite countable Element of bool [:(bool X),(bool X):]
[:(bool X),(bool X):] is non empty Relation-like bool X -defined bool X -valued finite countable Element of bool [:(bool X),(bool X):]
[:(bool X),(bool X):] is non empty Relation-like finite countable set
bool [:(bool X),(bool X):] is non empty finite V40() countable set
[:(X),(X):] is non empty Relation-like finite countable set
bool [:(X),(X):] is non empty finite V40() countable set
{ [b<sub>1</sub>,b<sub>2</sub>] where b<sub>1</sub>, b<sub>2</sub> is Element of (X) : (X,b<sub>2</sub>,b<sub>1</sub>) } is set
(dcF,(X)) is Relation-like bool X -defined bool X -valued finite countable Element of bool dcF
bool dcF is non empty finite V40() countable set
B is set
m is finite countable Element of bool X
P is finite countable Element of bool X
(X,P,m) is V21() Element of (X)
{P,m} is non empty finite V40() countable set
{P} is non empty trivial finite V40() 1 -element countable set
{{P,m},{P}} is non empty finite V40() countable set
x9 is finite countable Element of bool X
y9 is finite countable Element of bool X
(X,x9,y9) is V21() Element of (X)
{x9,y9} is non empty finite V40() countable set
{x9} is non empty trivial finite V40() 1 -element countable set
{{x9,y9},{x9}} is non empty finite V40() countable set
ck is non empty set
{ b<sub>1</sub> where b<sub>1</sub> is Element of ck : P c= b<sub>1</sub> } is set
k is set
S is Element of ck
k is set
S is Element of ck
k is finite V40() countable Element of bool (bool X)
Intersect k is finite countable Element of bool X
S is finite countable Element of bool X
m is set
P is set
x is Element of ck
meet k is finite countable Element of bool X
m is set
meet k is finite countable Element of bool X
(X,P,S) is V21() Element of (X)
{P,S} is non empty finite V40() countable set
{{P,S},{P}} is non empty finite V40() countable set
B is non empty Relation-like bool X -defined bool X -valued finite countable transitive (X) (X) (X) (X) (X) Element of bool [:(bool X),(bool X):]
(X,B) is finite V40() countable Element of bool (bool X)
{ b<sub>1</sub> where b<sub>1</sub> is Element of bool X : not for b<sub>2</sub> being Element of bool X holds (X,B,b<sub>2</sub>,b<sub>1</sub>) } is set
(X,B) is non empty Relation-like bool X -defined bool X -valued finite countable Element of bool [:(bool X),(bool X):]
(B,(X)) is Relation-like bool X -defined bool X -valued finite countable Element of bool B
bool B is non empty finite V40() countable set
P is set
x9 is (X,B)
y9 is Element of (X)
a is finite countable Element of bool X
k is finite countable Element of bool X
(X,a,k) is V21() Element of (X)
{a,k} is non empty finite V40() countable set
{a} is non empty trivial finite V40() 1 -element countable set
{{a,k},{a}} is non empty finite V40() countable set
S is finite countable Element of bool X
S is finite countable Element of bool X
(X,S,S) is V21() Element of (X)
{S,S} is non empty finite V40() countable set
{S} is non empty trivial finite V40() 1 -element countable set
{{S,S},{S}} is non empty finite V40() countable set
m is set
P is finite countable Element of bool X
x is finite countable Element of bool X
[x,m] is V21() set
{x,m} is non empty finite countable set
{x} is non empty trivial finite V40() 1 -element countable set
{{x,m},{x}} is non empty finite V40() countable set
x9 is finite countable Element of bool X
y9 is finite countable Element of bool X
(X,x9,y9) is V21() Element of (X)
{x9,y9} is non empty finite V40() countable set
{x9} is non empty trivial finite V40() 1 -element countable set
{{x9,y9},{x9}} is non empty finite V40() countable set
(X,x9,x9) is V21() Element of (X)
{x9,x9} is non empty finite V40() countable set
{{x9,x9},{x9}} is non empty finite V40() countable set
a is finite countable Element of bool X
k is finite countable Element of bool X
(X,a,k) is V21() Element of (X)
{a,k} is non empty finite V40() countable set
{a} is non empty trivial finite V40() 1 -element countable set
{{a,k},{a}} is non empty finite V40() countable set
X is set
bool X is non empty Element of bool (bool X)
bool X is non empty set
bool (bool X) is non empty set
[:(bool X),(bool X):] is non empty Relation-like set
bool [:(bool X),(bool X):] is non empty set
F is Relation-like bool X -defined bool X -valued Element of bool [:(bool X),(bool X):]
{ b<sub>1</sub> where b<sub>1</sub> is Element of bool X : for b<sub>2</sub>, b<sub>3</sub> being Element of bool X holds
( not (X,b<sub>2</sub>,b<sub>3</sub>) in F or not b<sub>2</sub> c= b<sub>1</sub> or b<sub>3</sub> c= b<sub>1</sub> ) } is set
dcF is set
S is Element of bool X
X is non empty finite countable set
bool X is non empty finite V40() countable Element of bool (bool X)
bool X is non empty finite V40() countable set
bool (bool X) is non empty finite V40() countable set
[:(bool X),(bool X):] is non empty Relation-like finite countable set
bool [:(bool X),(bool X):] is non empty finite V40() countable set
F is Relation-like bool X -defined bool X -valued finite countable Element of bool [:(bool X),(bool X):]
(X,F) is finite V40() countable Element of bool (bool X)
{ b<sub>1</sub> where b<sub>1</sub> is Element of bool X : for b<sub>2</sub>, b<sub>3</sub> being Element of bool X holds
( not (X,b<sub>2</sub>,b<sub>3</sub>) in F or not b<sub>2</sub> c= b<sub>1</sub> or b<sub>3</sub> c= b<sub>1</sub> ) } is set
dcF is finite countable Element of bool X
S is finite countable Element of bool X
(X,dcF,S) is V21() Element of (X)
(X) is non empty Relation-like bool X -defined bool X -valued finite countable Element of bool [:(bool X),(bool X):]
[:(bool X),(bool X):] is non empty Relation-like bool X -defined bool X -valued finite countable Element of bool [:(bool X),(bool X):]
[:(bool X),(bool X):] is non empty Relation-like finite countable set
bool [:(bool X),(bool X):] is non empty finite V40() countable set
{dcF,S} is non empty finite V40() countable set
{dcF} is non empty trivial finite V40() 1 -element countable set
{{dcF,S},{dcF}} is non empty finite V40() countable set
[#] X is non empty non proper finite countable Element of bool X
dcF is set
S is set
dcF /\ S is set
S is finite countable Element of bool X
ck is finite countable Element of bool X
ck /\ S is finite countable Element of bool X
m is finite countable Element of bool X
P is finite countable Element of bool X
(X,m,P) is V21() Element of (X)
(X) is non empty Relation-like bool X -defined bool X -valued finite countable Element of bool [:(bool X),(bool X):]
[:(bool X),(bool X):] is non empty Relation-like bool X -defined bool X -valued finite countable Element of bool [:(bool X),(bool X):]
[:(bool X),(bool X):] is non empty Relation-like finite countable set
bool [:(bool X),(bool X):] is non empty finite V40() countable set
{m,P} is non empty finite V40() countable set
{m} is non empty trivial finite V40() 1 -element countable set
{{m,P},{m}} is non empty finite V40() countable set
B is finite countable Element of bool X
X is non empty finite countable set
bool X is non empty finite V40() countable Element of bool (bool X)
bool X is non empty finite V40() countable set
bool (bool X) is non empty finite V40() countable set
[:(bool X),(bool X):] is non empty Relation-like finite countable set
bool [:(bool X),(bool X):] is non empty finite V40() countable set
F is Relation-like bool X -defined bool X -valued finite countable Element of bool [:(bool X),(bool X):]
(X,F) is finite V40() countable Element of bool (bool X)
{ b<sub>1</sub> where b<sub>1</sub> is Element of bool X : for b<sub>2</sub>, b<sub>3</sub> being Element of bool X holds
( not (X,b<sub>2</sub>,b<sub>3</sub>) in F or not b<sub>2</sub> c= b<sub>1</sub> or b<sub>3</sub> c= b<sub>1</sub> ) } is set
(X,(X,F)) is Relation-like bool X -defined bool X -valued finite countable Element of bool [:(bool X),(bool X):]
{ (X,b<sub>1</sub>,b<sub>2</sub>) where b<sub>1</sub>, b<sub>2</sub> is Element of bool X : for b<sub>3</sub> being set holds
( not b<sub>3</sub> in (X,F) or not b<sub>1</sub> c= b<sub>3</sub> or b<sub>2</sub> c= b<sub>3</sub> ) } is set
S is set
S is finite countable Element of bool X
ck is finite countable Element of bool X
(X,S,ck) is V21() Element of (X)
(X) is non empty Relation-like bool X -defined bool X -valued finite countable Element of bool [:(bool X),(bool X):]
[:(bool X),(bool X):] is non empty Relation-like bool X -defined bool X -valued finite countable Element of bool [:(bool X),(bool X):]
[:(bool X),(bool X):] is non empty Relation-like finite countable set
bool [:(bool X),(bool X):] is non empty finite V40() countable set
{S,ck} is non empty finite V40() countable set
{S} is non empty trivial finite V40() 1 -element countable set
{{S,ck},{S}} is non empty finite V40() countable set
B is set
m is finite countable Element of bool X
P is finite countable Element of bool X
S is Relation-like bool X -defined bool X -valued finite countable Element of bool [:(bool X),(bool X):]
(X,S) is finite V40() countable Element of bool (bool X)
{ b<sub>1</sub> where b<sub>1</sub> is Element of bool X : not for b<sub>2</sub> being Element of bool X holds (X,S,b<sub>2</sub>,b<sub>1</sub>) } is set
ck is set
{ (X,b<sub>1</sub>,b<sub>2</sub>) where b<sub>1</sub>, b<sub>2</sub> is finite countable Element of bool X : for b<sub>3</sub> being set holds
( not b<sub>3</sub> in (X,S) or not b<sub>1</sub> c= b<sub>3</sub> or b<sub>2</sub> c= b<sub>3</sub> ) } is set
(X,(X,S)) is Relation-like bool X -defined bool X -valued finite countable Element of bool [:(bool X),(bool X):]
(X,(X,(X,F))) is finite V40() countable Element of bool (bool X)
{ b<sub>1</sub> where b<sub>1</sub> is Element of bool X : not for b<sub>2</sub> being Element of bool X holds (X,(X,(X,F)),b<sub>2</sub>,b<sub>1</sub>) } is set
m is finite countable Element of bool X
P is finite countable Element of bool X
(X,m,P) is V21() Element of (X)
(X) is non empty Relation-like bool X -defined bool X -valued finite countable Element of bool [:(bool X),(bool X):]
[:(bool X),(bool X):] is non empty Relation-like bool X -defined bool X -valued finite countable Element of bool [:(bool X),(bool X):]
[:(bool X),(bool X):] is non empty Relation-like finite countable set
bool [:(bool X),(bool X):] is non empty finite V40() countable set
{m,P} is non empty finite V40() countable set
{m} is non empty trivial finite V40() 1 -element countable set
{{m,P},{m}} is non empty finite V40() countable set
x9 is set
y9 is finite countable Element of bool X
a is finite countable Element of bool X
k is finite countable Element of bool X
(X,a,k) is V21() Element of (X)
{a,k} is non empty finite V40() countable set
{a} is non empty trivial finite V40() 1 -element countable set
{{a,k},{a}} is non empty finite V40() countable set
S is finite countable Element of bool X
S is finite countable Element of bool X
(X,S,S) is V21() Element of (X)
{S,S} is non empty finite V40() countable set
{S} is non empty trivial finite V40() 1 -element countable set
{{S,S},{S}} is non empty finite V40() countable set
x9 is set
X is non empty finite countable set
bool X is non empty finite V40() countable Element of bool (bool X)
bool X is non empty finite V40() countable set
bool (bool X) is non empty finite V40() countable set
[:(bool X),(bool X):] is non empty Relation-like finite countable set
bool [:(bool X),(bool X):] is non empty finite V40() countable set
F is Relation-like bool X -defined bool X -valued finite countable Element of bool [:(bool X),(bool X):]
{ b<sub>1</sub> where b<sub>1</sub> is finite countable Element of bool X : for b<sub>2</sub>, b<sub>3</sub> being finite countable Element of bool X holds
( not (X,b<sub>2</sub>,b<sub>3</sub>) in F or not b<sub>2</sub> c= b<sub>1</sub> or b<sub>3</sub> c= b<sub>1</sub> ) } is set
(X,F) is finite V40() countable Element of bool (bool X)
dcF is set
S is finite countable Element of bool X
dcF is finite V40() countable Element of bool (bool X)
(X,dcF) is Relation-like bool X -defined bool X -valued finite countable Element of bool [:(bool X),(bool X):]
{ (X,b<sub>1</sub>,b<sub>2</sub>) where b<sub>1</sub>, b<sub>2</sub> is Element of bool X : for b<sub>3</sub> being set holds
( not b<sub>3</sub> in dcF or not b<sub>1</sub> c= b<sub>3</sub> or b<sub>2</sub> c= b<sub>3</sub> ) } is set
S is non empty Relation-like bool X -defined bool X -valued finite countable transitive (X) (X) (X) (X) (X) Element of bool [:(bool X),(bool X):]
ck is Relation-like bool X -defined bool X -valued finite countable Element of bool [:(bool X),(bool X):]
K is non empty Relation-like bool X -defined bool X -valued finite countable transitive (X) (X) (X) (X) (X) Element of bool [:(bool X),(bool X):]
dcF is non empty Relation-like bool X -defined bool X -valued finite countable transitive (X) (X) (X) (X) (X) Element of bool [:(bool X),(bool X):]
X is non empty finite countable set
bool X is non empty finite V40() countable Element of bool (bool X)
bool X is non empty finite V40() countable set
bool (bool X) is non empty finite V40() countable set
[:(bool X),(bool X):] is non empty Relation-like finite countable set
bool [:(bool X),(bool X):] is non empty finite V40() countable set
F is Relation-like bool X -defined bool X -valued finite countable Element of bool [:(bool X),(bool X):]
(X,F) is non empty Relation-like bool X -defined bool X -valued finite countable transitive (X) (X) (X) (X) (X) Element of bool [:(bool X),(bool X):]
(X,F) is finite V40() countable Element of bool (bool X)
{ b<sub>1</sub> where b<sub>1</sub> is Element of bool X : for b<sub>2</sub>, b<sub>3</sub> being Element of bool X holds
( not (X,b<sub>2</sub>,b<sub>3</sub>) in F or not b<sub>2</sub> c= b<sub>1</sub> or b<sub>3</sub> c= b<sub>1</sub> ) } is set
(X,(X,F)) is Relation-like bool X -defined bool X -valued finite countable Element of bool [:(bool X),(bool X):]
{ (X,b<sub>1</sub>,b<sub>2</sub>) where b<sub>1</sub>, b<sub>2</sub> is Element of bool X : for b<sub>3</sub> being set holds
( not b<sub>3</sub> in (X,F) or not b<sub>1</sub> c= b<sub>3</sub> or b<sub>2</sub> c= b<sub>3</sub> ) } is set
S is non empty Relation-like bool X -defined bool X -valued finite countable transitive (X) (X) (X) (X) (X) Element of bool [:(bool X),(bool X):]
S is Relation-like bool X -defined bool X -valued finite countable Element of bool [:(bool X),(bool X):]
X is set
bool X is non empty set
bool (bool X) is non empty set
{X} is non empty trivial finite 1 -element countable set
F is Element of bool X
{ b<sub>1</sub> where b<sub>1</sub> is Element of bool X : not F c= b<sub>1</sub> } is set
{X} \/ { b<sub>1</sub> where b<sub>1</sub> is Element of bool X : not F c= b<sub>1</sub> } is non empty set
K is Element of bool (bool X)
S is set
S is set
S /\ S is set
ck is Element of bool X
B is Element of bool X
ck /\ B is Element of bool X
ck is Element of bool X
B is Element of bool X
ck /\ B is Element of bool X
m is Element of bool X
ck is Element of bool X
B is Element of bool X
ck /\ B is Element of bool X
X is non empty finite countable set
bool X is non empty finite V40() countable Element of bool (bool X)
bool X is non empty finite V40() countable set
bool (bool X) is non empty finite V40() countable set
[:(bool X),(bool X):] is non empty Relation-like finite countable set
bool [:(bool X),(bool X):] is non empty finite V40() countable set
{X} is non empty trivial finite V40() 1 -element countable set
F is Relation-like bool X -defined bool X -valued finite countable Element of bool [:(bool X),(bool X):]
(X,F) is finite V40() countable Element of bool (bool X)
{ b<sub>1</sub> where b<sub>1</sub> is Element of bool X : not for b<sub>2</sub> being Element of bool X holds (X,F,b<sub>2</sub>,b<sub>1</sub>) } is set
K is finite countable Element of bool X
{ (X,b<sub>1</sub>,b<sub>2</sub>) where b<sub>1</sub>, b<sub>2</sub> is finite countable Element of bool X : ( K c= b<sub>1</sub> or b<sub>2</sub> c= b<sub>1</sub> ) } is set
{ b<sub>1</sub> where b<sub>1</sub> is finite countable Element of bool X : not K c= b<sub>1</sub> } is set
{X} \/ { b<sub>1</sub> where b<sub>1</sub> is finite countable Element of bool X : not K c= b<sub>1</sub> } is non empty set
S is set
S is finite countable Element of bool X
S is non empty finite V40() countable Element of bool (bool X)
{ (X,b<sub>1</sub>,b<sub>2</sub>) where b<sub>1</sub>, b<sub>2</sub> is finite countable Element of bool X : for b<sub>3</sub> being set holds
( not b<sub>3</sub> in S or not b<sub>1</sub> c= b<sub>3</sub> or b<sub>2</sub> c= b<sub>3</sub> ) } is set
(X,S) is Relation-like bool X -defined bool X -valued finite countable Element of bool [:(bool X),(bool X):]
ck is set
B is finite countable Element of bool X
m is finite countable Element of bool X
(X,B,m) is V21() Element of (X)
(X) is non empty Relation-like bool X -defined bool X -valued finite countable Element of bool [:(bool X),(bool X):]
[:(bool X),(bool X):] is non empty Relation-like bool X -defined bool X -valued finite countable Element of bool [:(bool X),(bool X):]
[:(bool X),(bool X):] is non empty Relation-like finite countable set
bool [:(bool X),(bool X):] is non empty finite V40() countable set
{B,m} is non empty finite V40() countable set
{B} is non empty trivial finite V40() 1 -element countable set
{{B,m},{B}} is non empty finite V40() countable set
P is set
x9 is finite countable Element of bool X
B is finite countable Element of bool X
m is finite countable Element of bool X
(X,B,m) is V21() Element of (X)
{B,m} is non empty finite V40() countable set
{B} is non empty trivial finite V40() 1 -element countable set
{{B,m},{B}} is non empty finite V40() countable set
X is finite countable set
bool X is non empty finite V40() countable Element of bool (bool X)
bool X is non empty finite V40() countable set
bool (bool X) is non empty finite V40() countable set
[:(bool X),(bool X):] is non empty Relation-like finite countable set
bool [:(bool X),(bool X):] is non empty finite V40() countable set
{X} is non empty trivial finite V40() 1 -element countable set
F is Relation-like bool X -defined bool X -valued finite countable Element of bool [:(bool X),(bool X):]
(X,F) is finite V40() countable Element of bool (bool X)
{ b<sub>1</sub> where b<sub>1</sub> is Element of bool X : not for b<sub>2</sub> being Element of bool X holds (X,F,b<sub>2</sub>,b<sub>1</sub>) } is set
K is finite countable Element of bool X
{ (X,b<sub>1</sub>,b<sub>2</sub>) where b<sub>1</sub>, b<sub>2</sub> is finite countable Element of bool X : ( K c= b<sub>1</sub> or b<sub>2</sub> c= b<sub>1</sub> ) } is set
{ b<sub>1</sub> where b<sub>1</sub> is finite countable Element of bool X : not K c= b<sub>1</sub> } is set
{X} \/ { b<sub>1</sub> where b<sub>1</sub> is finite countable Element of bool X : not K c= b<sub>1</sub> } is non empty set
[K,X] is V21() set
{K,X} is non empty finite V40() countable set
{K} is non empty trivial finite V40() 1 -element countable set
{{K,X},{K}} is non empty finite V40() countable set
{[K,X]} is non empty trivial Relation-like Function-like constant finite 1 -element countable finite-support set
{ (X,b<sub>1</sub>,b<sub>1</sub>) where b<sub>1</sub> is finite countable Element of bool X : not K c= b<sub>1</sub> } is set
{[K,X]} \/ { (X,b<sub>1</sub>,b<sub>1</sub>) where b<sub>1</sub> is finite countable Element of bool X : not K c= b<sub>1</sub> } is non empty set
(X,F) is Relation-like bool X -defined bool X -valued finite countable Element of bool [:(bool X),(bool X):]
(X) is non empty Relation-like (X) -defined (X) -valued total finite countable reflexive antisymmetric transitive Element of bool [:(X),(X):]
(X) is non empty Relation-like bool X -defined bool X -valued finite countable Element of bool [:(bool X),(bool X):]
[:(bool X),(bool X):] is non empty Relation-like bool X -defined bool X -valued finite countable Element of bool [:(bool X),(bool X):]
[:(bool X),(bool X):] is non empty Relation-like finite countable set
bool [:(bool X),(bool X):] is non empty finite V40() countable set
[:(X),(X):] is non empty Relation-like finite countable set
bool [:(X),(X):] is non empty finite V40() countable set
{ [b<sub>1</sub>,b<sub>2</sub>] where b<sub>1</sub>, b<sub>2</sub> is Element of (X) : (X,b<sub>2</sub>,b<sub>1</sub>) } is set
(F,(X)) is Relation-like bool X -defined bool X -valued finite countable Element of bool F
bool F is non empty finite V40() countable set
[#] X is non proper finite countable Element of bool X
ck is set
B is finite countable Element of bool X
(X,B,B) is V21() Element of (X)
{B,B} is non empty finite V40() countable set
{B} is non empty trivial finite V40() 1 -element countable set
{{B,B},{B}} is non empty finite V40() countable set
B is finite countable Element of bool X
m is finite countable Element of bool X
(X,m,B) is V21() Element of (X)
{m,B} is non empty finite V40() countable set
{m} is non empty trivial finite V40() 1 -element countable set
{{m,B},{m}} is non empty finite V40() countable set
{ b<sub>2</sub> where b<sub>1</sub> is finite countable Element of bool X : not K c= b<sub>2</sub> } is set
{X} \/ { b<sub>2</sub> where b<sub>1</sub> is finite countable Element of bool X : not K c= b<sub>2</sub> } is non empty set
P is finite countable Element of bool X
(X,P,P) is V21() Element of (X)
{P,P} is non empty finite V40() countable set
{P} is non empty trivial finite V40() 1 -element countable set
{{P,P},{P}} is non empty finite V40() countable set
{ b<sub>2</sub> where b<sub>1</sub> is finite countable Element of bool X : not K c= b<sub>2</sub> } is set
{X} \/ { b<sub>2</sub> where b<sub>1</sub> is finite countable Element of bool X : not K c= b<sub>2</sub> } is non empty set
{ b<sub>2</sub> where b<sub>1</sub> is finite countable Element of bool X : not K c= b<sub>2</sub> } is set
{X} \/ { b<sub>2</sub> where b<sub>1</sub> is finite countable Element of bool X : not K c= b<sub>2</sub> } is non empty set
X is set
bool X is non empty set
bool (bool X) is non empty set
X is non empty finite countable set
bool X is non empty finite V40() countable set
bool (bool X) is non empty finite V40() countable set
F is finite V40() countable Element of bool (bool X)
(X,F) is Relation-like bool X -defined bool X -valued finite countable Element of bool [:(bool X),(bool X):]
bool X is non empty finite V40() countable Element of bool (bool X)
[:(bool X),(bool X):] is non empty Relation-like finite countable set
bool [:(bool X),(bool X):] is non empty finite V40() countable set
{ (X,b<sub>1</sub>,b<sub>2</sub>) where b<sub>1</sub>, b<sub>2</sub> is Element of bool X : for b<sub>3</sub> being set holds
( not b<sub>3</sub> in F or not b<sub>1</sub> c= b<sub>3</sub> or b<sub>2</sub> c= b<sub>3</sub> ) } is set
(X,(X,F)) is finite V40() countable Element of bool (bool X)
{ b<sub>1</sub> where b<sub>1</sub> is Element of bool X : not for b<sub>2</sub> being Element of bool X holds (X,(X,F),b<sub>2</sub>,b<sub>1</sub>) } is set
{ (Intersect b<sub>1</sub>) where b<sub>1</sub> is finite V40() countable Element of bool (bool X) : b<sub>1</sub> c= F } is set
S is set
ck is finite countable Element of bool X
B is finite countable Element of bool X
(X,B,ck) is V21() Element of (X)
(X) is non empty Relation-like bool X -defined bool X -valued finite countable Element of bool [:(bool X),(bool X):]
[:(bool X),(bool X):] is non empty Relation-like bool X -defined bool X -valued finite countable Element of bool [:(bool X),(bool X):]
[:(bool X),(bool X):] is non empty Relation-like finite countable set
bool [:(bool X),(bool X):] is non empty finite V40() countable set
{B,ck} is non empty finite V40() countable set
{B} is non empty trivial finite V40() 1 -element countable set
{{B,ck},{B}} is non empty finite V40() countable set
(X,(X,F)) is Relation-like bool X -defined bool X -valued finite countable Element of bool [:(bool X),(bool X):]
(X) is non empty Relation-like (X) -defined (X) -valued total finite countable reflexive antisymmetric transitive Element of bool [:(X),(X):]
[:(X),(X):] is non empty Relation-like finite countable set
bool [:(X),(X):] is non empty finite V40() countable set
{ [b<sub>1</sub>,b<sub>2</sub>] where b<sub>1</sub>, b<sub>2</sub> is Element of (X) : (X,b<sub>2</sub>,b<sub>1</sub>) } is set
((X,F),(X)) is Relation-like bool X -defined bool X -valued finite countable Element of bool (X,F)
bool (X,F) is non empty finite V40() countable set
m is finite countable Element of bool X
P is finite countable Element of bool X
(X,m,P) is V21() Element of (X)
{m,P} is non empty finite V40() countable set
{m} is non empty trivial finite V40() 1 -element countable set
{{m,P},{m}} is non empty finite V40() countable set
{ b<sub>1</sub> where b<sub>1</sub> is finite countable Element of bool X : ( b<sub>1</sub> in F & m c= b<sub>1</sub> ) } is set
y9 is set
a is finite countable Element of bool X
a is set
y9 is finite V40() countable Element of bool (bool X)
k is finite countable Element of bool X
Intersect y9 is finite countable Element of bool X
k is set
S is finite countable Element of bool X
S is set
k is finite countable Element of bool X
(X,m,k) is V21() Element of (X)
{m,k} is non empty finite V40() countable set
{{m,k},{m}} is non empty finite V40() countable set
ck is finite V40() countable Element of bool (bool X)
Intersect ck is finite countable Element of bool X
X is non empty finite countable set
bool X is non empty finite V40() countable Element of bool (bool X)
bool X is non empty finite V40() countable set
bool (bool X) is non empty finite V40() countable set
[:(bool X),(bool X):] is non empty Relation-like finite countable set
bool [:(bool X),(bool X):] is non empty finite V40() countable set
F is non empty Relation-like bool X -defined bool X -valued finite countable transitive (X) (X) (X) (X) (X) Element of bool [:(bool X),(bool X):]
(X,F) is finite V40() countable Element of bool (bool X)
{ b<sub>1</sub> where b<sub>1</sub> is Element of bool X : not for b<sub>2</sub> being Element of bool X holds (X,F,b<sub>2</sub>,b<sub>1</sub>) } is set
(X,(X,F)) is Relation-like bool X -defined bool X -valued finite countable Element of bool [:(bool X),(bool X):]
{ (X,b<sub>1</sub>,b<sub>2</sub>) where b<sub>1</sub>, b<sub>2</sub> is Element of bool X : for b<sub>3</sub> being set holds
( not b<sub>3</sub> in (X,F) or not b<sub>1</sub> c= b<sub>3</sub> or b<sub>2</sub> c= b<sub>3</sub> ) } is set
{ (Intersect b<sub>1</sub>) where b<sub>1</sub> is finite V40() countable Element of bool (bool X) : b<sub>1</sub> c= (X,F) } is set
S is set
{S} is non empty trivial finite 1 -element countable set
ck is finite V40() countable Element of bool (bool X)
Intersect ck is finite countable Element of bool X
meet ck is finite countable Element of bool X
S is finite V40() countable Element of bool (bool X)
Intersect S is finite countable Element of bool X
X is set
bool X is non empty set
bool (bool X) is non empty set
F is non empty finite countable Element of bool (bool X)
(F) is finite countable Element of bool F
bool F is non empty finite V40() countable set
{ (Intersect b<sub>1</sub>) where b<sub>1</sub> is Element of bool (bool X) : b<sub>1</sub> c= (F) } is set
S is set
S is Element of F
ck is non empty finite countable Element of bool F
meet ck is set
B is non empty Element of bool (bool X)
m is set
Intersect B is Element of bool X
meet B is Element of bool X
S is Element of bool (bool X)
Intersect S is Element of bool X
X is set
bool X is non empty set
bool (bool X) is non empty set
F is set
{X} is non empty trivial finite 1 -element countable set
F \/ {X} is non empty set
K is non empty finite countable Element of bool (bool X)
(K) is finite countable Element of bool K
bool K is non empty finite V40() countable set
{ (Intersect b<sub>1</sub>) where b<sub>1</sub> is Element of bool (bool X) : b<sub>1</sub> c= F } is set
dcF is set
S is Element of K
S is Element of bool (bool X)
Intersect S is Element of bool X
X is non empty finite countable set
bool X is non empty finite V40() countable Element of bool (bool X)
bool X is non empty finite V40() countable set
bool (bool X) is non empty finite V40() countable set
[:(bool X),(bool X):] is non empty Relation-like finite countable set
bool [:(bool X),(bool X):] is non empty finite V40() countable set
F is non empty Relation-like bool X -defined bool X -valued finite countable transitive (X) (X) (X) (X) (X) Element of bool [:(bool X),(bool X):]
X --> INT is non empty Relation-like non-empty X -defined {INT} -valued Function-like constant total V24(X,{INT}) finite countable finite-support Element of bool [:X,{INT}:]
{INT} is non empty trivial finite 1 -element countable set
[:X,{INT}:] is non empty Relation-like finite countable set
bool [:X,{INT}:] is non empty finite V40() countable set
(X,F) is finite V40() countable Element of bool (bool X)
{ b<sub>1</sub> where b<sub>1</sub> is Element of bool X : not for b<sub>2</sub> being Element of bool X holds (X,F,b<sub>2</sub>,b<sub>1</sub>) } is set
dcF is finite V40() countable Element of bool (bool X)
(X,dcF) is Relation-like bool X -defined bool X -valued finite countable Element of bool [:(bool X),(bool X):]
{ (X,b<sub>1</sub>,b<sub>2</sub>) where b<sub>1</sub>, b<sub>2</sub> is Element of bool X : for b<sub>3</sub> being set holds
( not b<sub>3</sub> in dcF or not b<sub>1</sub> c= b<sub>3</sub> or b<sub>2</sub> c= b<sub>3</sub> ) } is set
S is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like countable finite-support set
proj2 S is finite countable set
K is Relation-like non-empty X -defined Function-like total finite-support set
dom K is finite countable Element of bool X
X --> 0 is non empty Relation-like X -defined NAT -valued Function-like constant total V24(X, NAT ) Function-yielding V28() finite Cardinal-yielding countable finite-support Element of bool [:X,NAT:]
[:X,NAT:] is non empty non trivial Relation-like non finite set
bool [:X,NAT:] is non empty non trivial non finite set
dom (X --> 0) is non empty finite countable Element of bool X
ck is set
(X --> 0) . ck is Relation-like Function-like set
K . ck is set
product K is non empty functional with_common_domain product-like set
{(X --> 0)} is non empty trivial functional finite V40() 1 -element with_common_domain countable set
B is set
bool (product K) is non empty set
B is non empty functional with_common_domain Element of bool (product K)
(X,K,B) is () ()
the of (X,K,B) is non empty finite countable set
the of (X,K,B) is Relation-like non-empty the of (X,K,B) -defined Function-like total finite-support set
((X,K,B)) is Relation-like bool the of (X,K,B) -defined bool the of (X,K,B) -valued finite countable Element of bool [:(bool the of (X,K,B)),(bool the of (X,K,B)):]
bool the of (X,K,B) is non empty finite V40() countable Element of bool (bool the of (X,K,B))
bool the of (X,K,B) is non empty finite V40() countable set
bool (bool the of (X,K,B)) is non empty finite V40() countable set
[:(bool the of (X,K,B)),(bool the of (X,K,B)):] is non empty Relation-like finite countable set
bool [:(bool the of (X,K,B)),(bool the of (X,K,B)):] is non empty finite V40() countable set
{ [b<sub>1</sub>,b<sub>2</sub>] where b<sub>1</sub>, b<sub>2</sub> is finite countable Element of bool the of (X,K,B) : ((X,K,B),b<sub>1</sub>,b<sub>2</sub>) } is set
P is Element of X
the of (X,K,B) . P is set
x9 is set
y9 is finite countable Element of bool X
a is finite countable Element of bool X
(X,y9,a) is V21() Element of (X)
(X) is non empty Relation-like bool X -defined bool X -valued finite countable Element of bool [:(bool X),(bool X):]
[:(bool X),(bool X):] is non empty Relation-like bool X -defined bool X -valued finite countable Element of bool [:(bool X),(bool X):]
[:(bool X),(bool X):] is non empty Relation-like finite countable set
bool [:(bool X),(bool X):] is non empty finite V40() countable set
{y9,a} is non empty finite V40() countable set
{y9} is non empty trivial finite V40() 1 -element countable set
{{y9,a},{y9}} is non empty finite V40() countable set
k is finite countable Element of bool the of (X,K,B)
S is finite countable Element of bool the of (X,K,B)
the of (X,K,B) is functional with_common_domain Element of bool (product the of (X,K,B))
product the of (X,K,B) is non empty functional with_common_domain product-like set
bool (product the of (X,K,B)) is non empty set
S is Relation-like Function-like Element of the of (X,K,B)
S | k is Relation-like Function-like finite countable finite-support set
m is Relation-like Function-like Element of the of (X,K,B)
m | k is Relation-like Function-like finite countable finite-support set
S | S is Relation-like Function-like finite countable finite-support set
m | S is Relation-like Function-like finite countable finite-support set
y9 is finite countable Element of bool the of (X,K,B)
a is finite countable Element of bool the of (X,K,B)
( the of (X,K,B),y9,a) is V21() Element of ( the of (X,K,B))
( the of (X,K,B)) is non empty Relation-like bool the of (X,K,B) -defined bool the of (X,K,B) -valued finite countable Element of bool [:(bool the of (X,K,B)),(bool the of (X,K,B)):]
[:(bool the of (X,K,B)),(bool the of (X,K,B)):] is non empty Relation-like bool the of (X,K,B) -defined bool the of (X,K,B) -valued finite countable Element of bool [:(bool the of (X,K,B)),(bool the of (X,K,B)):]
[:(bool the of (X,K,B)),(bool the of (X,K,B)):] is non empty Relation-like finite countable set
bool [:(bool the of (X,K,B)),(bool the of (X,K,B)):] is non empty finite V40() countable set
{y9,a} is non empty finite V40() countable set
{y9} is non empty trivial finite V40() 1 -element countable set
{{y9,a},{y9}} is non empty finite V40() countable set
k is set
S is Relation-like NAT -defined dcF -valued Function-like finite FinSequence-like FinSubsequence-like countable finite-support FinSequence of dcF
len S is ext-real non negative V29() V30() V31() V35() finite cardinal V48() V49() countable Element of NAT
ck is non empty ext-real positive non negative V29() V30() V31() V35() finite cardinal V48() V49() countable Element of NAT
ck -tuples_on BOOLEAN is non empty functional FinSequence-membered FinSequenceSet of BOOLEAN
BOOLEAN * is non empty functional FinSequence-membered FinSequenceSet of BOOLEAN
{ b<sub>1</sub> where b<sub>1</sub> is Relation-like NAT -defined BOOLEAN -valued Function-like finite FinSequence-like FinSubsequence-like countable finite-support Element of BOOLEAN * : len b<sub>1</sub> = ck } is set
Seg ck is non empty finite ck -element countable Element of bool NAT
B is Element of X
m is ext-real non negative V29() V30() V31() V35() finite cardinal V48() V49() countable set
S . m is set
P is boolean Element of BOOLEAN
TRUE is boolean Element of BOOLEAN
P is boolean Element of BOOLEAN
m is Relation-like NAT -defined BOOLEAN -valued Function-like finite FinSequence-like FinSubsequence-like countable finite-support FinSequence of BOOLEAN
dom m is finite countable Element of bool NAT
len m is ext-real non negative V29() V30() V31() V35() finite cardinal V48() V49() countable Element of NAT
P is Relation-like NAT -defined BOOLEAN -valued Function-like finite ck -element FinSequence-like FinSubsequence-like countable finite-support Element of ck -tuples_on BOOLEAN
x9 is Relation-like NAT -defined BOOLEAN -valued Function-like finite ck -element FinSequence-like FinSubsequence-like countable finite-support Element of ck -tuples_on BOOLEAN
y9 is ext-real non negative V29() V30() V31() V35() finite cardinal V48() V49() countable Element of NAT
S . y9 is set
x9 . y9 is set
[:X,(ck -tuples_on BOOLEAN):] is non empty Relation-like set
bool [:X,(ck -tuples_on BOOLEAN):] is non empty set
B is Relation-like X -defined ck -tuples_on BOOLEAN -valued Function-like V24(X,ck -tuples_on BOOLEAN) Function-yielding V28() finite countable FinSequence-yielding finite-support Element of bool [:X,(ck -tuples_on BOOLEAN):]
{ b<sub>1</sub> where b<sub>1</sub> is Relation-like X -defined Function-like K -compatible total finite-support Element of product K : ex b<sub>2</sub> being ext-real non negative V29() V30() V31() V35() finite cardinal V48() V49() countable Element of NAT st
for b<sub>3</sub> being Element of X holds b<sub>1</sub> . b<sub>3</sub> = Absval (ck,(ck -BinarySequence b<sub>2</sub>),(B . b<sub>3</sub>)) } is set
P is set
x9 is Relation-like X -defined Function-like K -compatible total finite-support Element of product K
y9 is ext-real non negative V29() V30() V31() V35() finite cardinal V48() V49() countable Element of NAT
ck -BinarySequence y9 is Relation-like NAT -defined BOOLEAN -valued Function-like finite ck -element FinSequence-like FinSubsequence-like countable finite-support FinSequence of BOOLEAN
P is empty ext-real non positive non negative Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional Function-yielding V28() V29() V30() V31() V33() V34() V35() finite finite-yielding V40() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V48() V49() Cardinal-yielding with_common_domain countable FinSequence-yielding finite-support Element of NAT
ck -BinarySequence P is Relation-like NAT -defined BOOLEAN -valued Function-like finite ck -element FinSequence-like FinSubsequence-like countable finite-support FinSequence of BOOLEAN
y9 is Element of X
B . y9 is Relation-like NAT -defined Function-like finite ck -element FinSequence-like FinSubsequence-like countable finite-support Element of ck -tuples_on BOOLEAN
(ck,(ck -BinarySequence P),(B . y9)) is Relation-like NAT -defined BOOLEAN -valued Function-like finite ck -element FinSequence-like FinSubsequence-like countable finite-support FinSequence of BOOLEAN
0* ck is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like countable finite-support Element of REAL ck
REAL ck is functional FinSequence-membered FinSequenceSet of REAL
(X --> 0) . y9 is ext-real non negative Relation-like Function-like V29() V30() V31() V35() finite cardinal V48() V49() countable finite-support Element of NAT
Absval (ck,(ck -BinarySequence P),(B . y9)) is ext-real non negative V29() V30() V31() V35() finite cardinal V48() V49() countable Element of NAT
P is empty ext-real non positive non negative Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional Function-yielding V28() V29() V30() V31() V33() V34() V35() finite finite-yielding V40() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V48() V49() Cardinal-yielding with_common_domain countable FinSequence-yielding finite-support Element of NAT
ck -BinarySequence P is Relation-like NAT -defined BOOLEAN -valued Function-like finite ck -element FinSequence-like FinSubsequence-like countable finite-support FinSequence of BOOLEAN
bool (product K) is non empty set
P is non empty functional with_common_domain Element of bool (product K)
(X,K,P) is () ()
the of (X,K,P) is non empty finite countable set
the of (X,K,P) is Relation-like non-empty the of (X,K,P) -defined Function-like total finite-support set
((X,K,P)) is Relation-like bool the of (X,K,P) -defined bool the of (X,K,P) -valued finite countable Element of bool [:(bool the of (X,K,P)),(bool the of (X,K,P)):]
bool the of (X,K,P) is non empty finite V40() countable Element of bool (bool the of (X,K,P))
bool the of (X,K,P) is non empty finite V40() countable set
bool (bool the of (X,K,P)) is non empty finite V40() countable set
[:(bool the of (X,K,P)),(bool the of (X,K,P)):] is non empty Relation-like finite countable set
bool [:(bool the of (X,K,P)),(bool the of (X,K,P)):] is non empty finite V40() countable set
{ [b<sub>1</sub>,b<sub>2</sub>] where b<sub>1</sub>, b<sub>2</sub> is finite countable Element of bool the of (X,K,P) : ((X,K,P),b<sub>1</sub>,b<sub>2</sub>) } is set
y9 is Element of X
the of (X,K,P) . y9 is set
dom S is finite countable Element of bool NAT
a is set
k is finite countable Element of bool X
S is finite countable Element of bool X
(X,k,S) is V21() Element of (X)
(X) is non empty Relation-like bool X -defined bool X -valued finite countable Element of bool [:(bool X),(bool X):]
[:(bool X),(bool X):] is non empty Relation-like bool X -defined bool X -valued finite countable Element of bool [:(bool X),(bool X):]
[:(bool X),(bool X):] is non empty Relation-like finite countable set
bool [:(bool X),(bool X):] is non empty finite V40() countable set
{k,S} is non empty finite V40() countable set
{k} is non empty trivial finite V40() 1 -element countable set
{{k,S},{k}} is non empty finite V40() countable set
S is finite countable Element of bool the of (X,K,P)
m is finite countable Element of bool the of (X,K,P)
the of (X,K,P) is functional with_common_domain Element of bool (product the of (X,K,P))
product the of (X,K,P) is non empty functional with_common_domain product-like set
bool (product the of (X,K,P)) is non empty set
P is Relation-like Function-like Element of the of (X,K,P)
P | S is Relation-like Function-like finite countable finite-support set
x is Relation-like Function-like Element of the of (X,K,P)
x | S is Relation-like Function-like finite countable finite-support set
P | m is Relation-like Function-like finite countable finite-support set
x | m is Relation-like Function-like finite countable finite-support set
y is Relation-like X -defined Function-like K -compatible total finite-support Element of product K
m is ext-real non negative V29() V30() V31() V35() finite cardinal V48() V49() countable Element of NAT
ck -BinarySequence m is Relation-like NAT -defined BOOLEAN -valued Function-like finite ck -element FinSequence-like FinSubsequence-like countable finite-support FinSequence of BOOLEAN
m is ext-real non negative V29() V30() V31() V35() finite cardinal V48() V49() countable Element of NAT
ck -BinarySequence m is Relation-like NAT -defined BOOLEAN -valued Function-like finite ck -element FinSequence-like FinSubsequence-like countable finite-support FinSequence of BOOLEAN
r0 is Relation-like X -defined Function-like K -compatible total finite-support Element of product K
r1 is ext-real non negative V29() V30() V31() V35() finite cardinal V48() V49() countable Element of NAT
ck -BinarySequence r1 is Relation-like NAT -defined BOOLEAN -valued Function-like finite ck -element FinSequence-like FinSubsequence-like countable finite-support FinSequence of BOOLEAN
r1 is ext-real non negative V29() V30() V31() V35() finite cardinal V48() V49() countable Element of NAT
ck -BinarySequence r1 is Relation-like NAT -defined BOOLEAN -valued Function-like finite ck -element FinSequence-like FinSubsequence-like countable finite-support FinSequence of BOOLEAN
proj1 x is set
proj1 P is set
x | S is Relation-like Function-like finite countable finite-support set
proj1 (x | S) is finite countable set
(proj1 P) /\ S is finite countable Element of bool X
x is set
g is Element of X
B . g is Relation-like NAT -defined Function-like finite ck -element FinSequence-like FinSubsequence-like countable finite-support Element of ck -tuples_on BOOLEAN
(ck,(ck -BinarySequence r1),(B . g)) is Relation-like NAT -defined BOOLEAN -valued Function-like finite ck -element FinSequence-like FinSubsequence-like countable finite-support FinSequence of BOOLEAN
(ck,(ck -BinarySequence m),(B . g)) is Relation-like NAT -defined BOOLEAN -valued Function-like finite ck -element FinSequence-like FinSubsequence-like countable finite-support FinSequence of BOOLEAN
dom (B . g) is finite ck -element countable Element of bool NAT
dom (ck,(ck -BinarySequence m),(B . g)) is finite ck -element countable Element of bool NAT
dom (ck,(ck -BinarySequence r1),(B . g)) is finite ck -element countable Element of bool NAT
bsi is set
S . bsi is set
bs0 is Relation-like NAT -defined BOOLEAN -valued Function-like finite ck -element FinSequence-like FinSubsequence-like countable finite-support Element of ck -tuples_on BOOLEAN
bs0 /. bsi is boolean Element of BOOLEAN
bs0 . bsi is set
(ck,(ck -BinarySequence m),(B . g)) . bsi is set
(ck -BinarySequence m) /. bsi is boolean Element of BOOLEAN
((ck -BinarySequence m) /. bsi) '&' (bs0 /. bsi) is boolean Element of BOOLEAN
K161(((ck -BinarySequence m) /. bsi),(bs0 /. bsi)) is set
(ck -BinarySequence r1) /. bsi is boolean Element of BOOLEAN
((ck -BinarySequence r1) /. bsi) '&' (bs0 /. bsi) is boolean Element of BOOLEAN
K161(((ck -BinarySequence r1) /. bsi),(bs0 /. bsi)) is set
(ck,(ck -BinarySequence r1),(B . g)) . bsi is set
S . bsi is set
(ck,(ck -BinarySequence m),(B . g)) . bsi is set
(ck,(ck -BinarySequence r1),(B . g)) . bsi is set
L is set
R is Element of X
P . R is set
x | k is Relation-like Function-like finite countable finite-support set
(x | k) . R is set
x . R is set
B . R is Relation-like NAT -defined Function-like finite ck -element FinSequence-like FinSubsequence-like countable finite-support Element of ck -tuples_on BOOLEAN
(ck,(ck -BinarySequence m),(B . R)) is Relation-like NAT -defined BOOLEAN -valued Function-like finite ck -element FinSequence-like FinSubsequence-like countable finite-support FinSequence of BOOLEAN
Absval (ck,(ck -BinarySequence m),(B . R)) is ext-real non negative V29() V30() V31() V35() finite cardinal V48() V49() countable Element of NAT
(ck,(ck -BinarySequence r1),(B . R)) is Relation-like NAT -defined BOOLEAN -valued Function-like finite ck -element FinSequence-like FinSubsequence-like countable finite-support FinSequence of BOOLEAN
Absval (ck,(ck -BinarySequence r1),(B . R)) is ext-real non negative V29() V30() V31() V35() finite cardinal V48() V49() countable Element of NAT
dom (B . R) is finite ck -element countable Element of bool NAT
Ma is Relation-like NAT -defined BOOLEAN -valued Function-like finite ck -element FinSequence-like FinSubsequence-like countable finite-support Element of ck -tuples_on BOOLEAN
Ma /. bsi is boolean Element of BOOLEAN
Ma . bsi is set
(ck -BinarySequence m) /. bsi is boolean Element of BOOLEAN
((ck -BinarySequence m) /. bsi) '&' (Ma /. bsi) is boolean Element of BOOLEAN
K161(((ck -BinarySequence m) /. bsi),(Ma /. bsi)) is set
(ck,(ck -BinarySequence m),(B . R)) . bsi is set
(ck,(ck -BinarySequence r1),(B . R)) . bsi is set
(ck -BinarySequence r1) /. bsi is boolean Element of BOOLEAN
((ck -BinarySequence r1) /. bsi) '&' (Ma /. bsi) is boolean Element of BOOLEAN
K161(((ck -BinarySequence r1) /. bsi),(Ma /. bsi)) is set
bs0 is Relation-like NAT -defined BOOLEAN -valued Function-like finite ck -element FinSequence-like FinSubsequence-like countable finite-support Element of ck -tuples_on BOOLEAN
bs0 /. bsi is boolean Element of BOOLEAN
((ck -BinarySequence m) /. bsi) '&' (bs0 /. bsi) is boolean Element of BOOLEAN
K161(((ck -BinarySequence m) /. bsi),(bs0 /. bsi)) is set
S . bsi is set
x . x is set
Absval (ck,(ck -BinarySequence m),(B . g)) is ext-real non negative V29() V30() V31() V35() finite cardinal V48() V49() countable Element of NAT
P . x is set
(x | S) . x is set
k is finite countable Element of bool the of (X,K,P)
S is finite countable Element of bool the of (X,K,P)
( the of (X,K,P),k,S) is V21() Element of ( the of (X,K,P))
( the of (X,K,P)) is non empty Relation-like bool the of (X,K,P) -defined bool the of (X,K,P) -valued finite countable Element of bool [:(bool the of (X,K,P)),(bool the of (X,K,P)):]
[:(bool the of (X,K,P)),(bool the of (X,K,P)):] is non empty Relation-like bool the of (X,K,P) -defined bool the of (X,K,P) -valued finite countable Element of bool [:(bool the of (X,K,P)),(bool the of (X,K,P)):]
[:(bool the of (X,K,P)),(bool the of (X,K,P)):] is non empty Relation-like finite countable set
bool [:(bool the of (X,K,P)),(bool the of (X,K,P)):] is non empty finite V40() countable set
{k,S} is non empty finite V40() countable set
{k} is non empty trivial finite V40() 1 -element countable set
{{k,S},{k}} is non empty finite V40() countable set
ck -BinarySequence 0 is Relation-like NAT -defined BOOLEAN -valued Function-like finite ck -element FinSequence-like FinSubsequence-like countable finite-support FinSequence of BOOLEAN
S is set
P is Relation-like X -defined NAT -valued Function-like V24(X, NAT ) finite countable finite-support Element of bool [:X,NAT:]
x is set
P . x is set
y is Element of X
B . y is Relation-like NAT -defined Function-like finite ck -element FinSequence-like FinSubsequence-like countable finite-support Element of ck -tuples_on BOOLEAN
(ck,(ck -BinarySequence 0),(B . y)) is Relation-like NAT -defined BOOLEAN -valued Function-like finite ck -element FinSequence-like FinSubsequence-like countable finite-support FinSequence of BOOLEAN
Absval (ck,(ck -BinarySequence 0),(B . y)) is ext-real non negative V29() V30() V31() V35() finite cardinal V48() V49() countable Element of NAT
P . y is ext-real non negative V29() V30() V31() V35() finite cardinal V48() V49() countable Element of NAT
K . x is set
dom P is finite countable Element of bool X
m is finite countable Element of dcF
y is ext-real non negative V29() V30() V31() V35() finite cardinal V48() V49() countable set
S . y is set
m is ext-real non negative V29() V30() V31() V35() finite cardinal V48() V49() countable set
m + 1 is non empty ext-real positive non negative V29() V30() V31() V35() finite cardinal V48() V49() countable Element of NAT
r0 is set
r1 is Element of X
B . r1 is Relation-like NAT -defined Function-like finite ck -element FinSequence-like FinSubsequence-like countable finite-support Element of ck -tuples_on BOOLEAN
x is Relation-like X -defined Function-like K -compatible total finite-support Element of product K
r0 is Relation-like NAT -defined BOOLEAN -valued Function-like finite ck -element FinSequence-like FinSubsequence-like countable finite-support Element of ck -tuples_on BOOLEAN
dom r0 is finite ck -element countable Element of bool NAT
r0 /. y is boolean Element of BOOLEAN
r0 . y is set
r1 is ext-real non negative V29() V30() V31() V35() finite cardinal V48() V49() countable Element of NAT
2 to_power r1 is ext-real non negative V29() V30() V31() V35() finite cardinal V48() V49() countable Element of NAT
ck -BinarySequence (2 to_power r1) is Relation-like NAT -defined BOOLEAN -valued Function-like finite ck -element FinSequence-like FinSubsequence-like countable finite-support FinSequence of BOOLEAN
x is Relation-like X -defined NAT -valued Function-like V24(X, NAT ) finite countable finite-support Element of bool [:X,NAT:]
g is set
x . g is set
bs0 is Element of X
B . bs0 is Relation-like NAT -defined Function-like finite ck -element FinSequence-like FinSubsequence-like countable finite-support Element of ck -tuples_on BOOLEAN
(ck,(ck -BinarySequence (2 to_power r1)),(B . bs0)) is Relation-like NAT -defined BOOLEAN -valued Function-like finite ck -element FinSequence-like FinSubsequence-like countable finite-support FinSequence of BOOLEAN
Absval (ck,(ck -BinarySequence (2 to_power r1)),(B . bs0)) is ext-real non negative V29() V30() V31() V35() finite cardinal V48() V49() countable Element of NAT
x . bs0 is ext-real non negative V29() V30() V31() V35() finite cardinal V48() V49() countable Element of NAT
K . g is set
dom x is finite countable Element of bool X
x | k is Relation-like k -defined X -defined Function-like K -compatible finite countable finite-support Element of sproduct K
sproduct K is non empty functional set
dom (x | k) is finite countable Element of bool k
bool k is non empty finite V40() countable set
g is Relation-like X -defined Function-like K -compatible total finite-support Element of product K
dom g is finite countable Element of bool X
(dom g) /\ k is finite countable Element of bool the of (X,K,P)
bs0 is set
bsi is Element of X
g . bsi is set
B . bsi is Relation-like NAT -defined Function-like finite ck -element FinSequence-like FinSubsequence-like countable finite-support Element of ck -tuples_on BOOLEAN
(ck,(ck -BinarySequence (2 to_power r1)),(B . bsi)) is Relation-like NAT -defined BOOLEAN -valued Function-like finite ck -element FinSequence-like FinSubsequence-like countable finite-support FinSequence of BOOLEAN
Absval (ck,(ck -BinarySequence (2 to_power r1)),(B . bsi)) is ext-real non negative V29() V30() V31() V35() finite cardinal V48() V49() countable Element of NAT
(ck,(ck -BinarySequence 0),(B . bsi)) is Relation-like NAT -defined BOOLEAN -valued Function-like finite ck -element FinSequence-like FinSubsequence-like countable finite-support FinSequence of BOOLEAN
dom (ck,(ck -BinarySequence 0),(B . bsi)) is finite ck -element countable Element of bool NAT
dom (ck,(ck -BinarySequence (2 to_power r1)),(B . bsi)) is finite ck -element countable Element of bool NAT
ck |-> 0 is Relation-like empty-yielding NAT -defined NAT -valued Function-like Function-yielding V28() finite ck -element FinSequence-like FinSubsequence-like Cardinal-yielding countable FinSequence-yielding finite-support Element of ck -tuples_on NAT
ck -tuples_on NAT is non empty functional FinSequence-membered FinSequenceSet of NAT
NAT * is non empty functional FinSequence-membered FinSequenceSet of NAT
{ b<sub>1</sub> where b<sub>1</sub> is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like countable finite-support Element of NAT * : len b<sub>1</sub> = ck } is set
(Seg ck) --> 0 is non empty Relation-like Seg ck -defined Seg ck -defined NAT -valued {0} -valued Function-like constant total total V24( Seg ck,{0}) Function-yielding V28() finite FinSequence-like FinSubsequence-like Cardinal-yielding countable finite-support Element of bool [:(Seg ck),{0}:]
{0} is non empty trivial functional finite V40() 1 -element with_common_domain countable set
[:(Seg ck),{0}:] is non empty Relation-like finite countable set
bool [:(Seg ck),{0}:] is non empty finite V40() countable set
j is set
dom (ck -BinarySequence 0) is finite ck -element countable Element of bool NAT
nj is ext-real non negative V29() V30() V31() V35() finite cardinal V48() V49() countable Element of NAT
(ck -BinarySequence 0) /. nj is boolean Element of BOOLEAN
(ck -BinarySequence 0) . nj is set
(ck,(ck -BinarySequence 0),(B . bsi)) . j is set
Ma is Relation-like NAT -defined BOOLEAN -valued Function-like finite ck -element FinSequence-like FinSubsequence-like countable finite-support Element of ck -tuples_on BOOLEAN
Ma /. nj is boolean Element of BOOLEAN
((ck -BinarySequence 0) /. nj) '&' (Ma /. nj) is boolean Element of BOOLEAN
K161(((ck -BinarySequence 0) /. nj),(Ma /. nj)) is set
dom (ck -BinarySequence (2 to_power r1)) is finite ck -element countable Element of bool NAT
(ck -BinarySequence (2 to_power r1)) /. nj is boolean Element of BOOLEAN
(ck -BinarySequence (2 to_power r1)) . nj is set
(ck,(ck -BinarySequence (2 to_power r1)),(B . bsi)) . j is set
((ck -BinarySequence (2 to_power r1)) /. nj) '&' (Ma /. nj) is boolean Element of BOOLEAN
K161(((ck -BinarySequence (2 to_power r1)) /. nj),(Ma /. nj)) is set
dom Ma is finite ck -element countable Element of bool NAT
Ma . y is set
(ck,(ck -BinarySequence (2 to_power r1)),(B . bsi)) . j is set
(ck -BinarySequence (2 to_power r1)) /. nj is boolean Element of BOOLEAN
((ck -BinarySequence (2 to_power r1)) /. nj) '&' (Ma /. nj) is boolean Element of BOOLEAN
K161(((ck -BinarySequence (2 to_power r1)) /. nj),(Ma /. nj)) is set
(x | k) . bsi is set
x . bsi is set
Absval (ck,(ck -BinarySequence 0),(B . bsi)) is ext-real non negative V29() V30() V31() V35() finite cardinal V48() V49() countable Element of NAT
(x | k) . bs0 is set
g . bs0 is set
g | k is Relation-like k -defined X -defined Function-like K -compatible finite countable finite-support Element of sproduct K
(ck -BinarySequence 0) /. y is boolean Element of BOOLEAN
(ck -BinarySequence 0) . y is set
dom (ck -BinarySequence (2 to_power r1)) is finite ck -element countable Element of bool NAT
(ck -BinarySequence (2 to_power r1)) /. y is boolean Element of BOOLEAN
(ck -BinarySequence (2 to_power r1)) . y is set
(ck,(ck -BinarySequence (2 to_power r1)),r0) is Relation-like NAT -defined BOOLEAN -valued Function-like finite ck -element FinSequence-like FinSubsequence-like countable finite-support FinSequence of BOOLEAN
(ck,(ck -BinarySequence (2 to_power r1)),r0) . y is set
((ck -BinarySequence (2 to_power r1)) /. y) '&' (r0 /. y) is boolean Element of BOOLEAN
K161(((ck -BinarySequence (2 to_power r1)) /. y),(r0 /. y)) is set
(ck,(ck -BinarySequence 0),r0) is Relation-like NAT -defined BOOLEAN -valued Function-like finite ck -element FinSequence-like FinSubsequence-like countable finite-support FinSequence of BOOLEAN
(ck,(ck -BinarySequence 0),r0) . y is set
((ck -BinarySequence 0) /. y) '&' (r0 /. y) is boolean Element of BOOLEAN
K161(((ck -BinarySequence 0) /. y),(r0 /. y)) is set
x | S is Relation-like S -defined X -defined Function-like K -compatible finite countable finite-support Element of sproduct K
g | S is Relation-like S -defined X -defined Function-like K -compatible finite countable finite-support Element of sproduct K
(ck,(ck -BinarySequence 0),(B . r1)) is Relation-like NAT -defined BOOLEAN -valued Function-like finite ck -element FinSequence-like FinSubsequence-like countable finite-support FinSequence of BOOLEAN
Absval (ck,(ck -BinarySequence 0),(B . r1)) is ext-real non negative V29() V30() V31() V35() finite cardinal V48() V49() countable Element of NAT
x . r1 is set
(x | S) . r1 is set
g . r1 is set
(ck,(ck -BinarySequence (2 to_power r1)),(B . r1)) is Relation-like NAT -defined BOOLEAN -valued Function-like finite ck -element FinSequence-like FinSubsequence-like countable finite-support FinSequence of BOOLEAN
Absval (ck,(ck -BinarySequence (2 to_power r1)),(B . r1)) is ext-real non negative V29() V30() V31() V35() finite cardinal V48() V49() countable Element of NAT
F is set
X is set
bool X is non empty set
K is set
{ (X,b<sub>1</sub>,b<sub>2</sub>) where b<sub>1</sub>, b<sub>2</sub> is Element of bool X : for b<sub>3</sub> being set holds
( not b<sub>3</sub> in K or not b<sub>1</sub> c= b<sub>3</sub> or b<sub>2</sub> c= b<sub>3</sub> ) } is set
dcF is Element of bool X
S is Element of bool X
(X,dcF,S) is V21() Element of (X)
(X) is non empty Relation-like bool X -defined bool X -valued Element of bool [:(bool X),(bool X):]
bool X is non empty Element of bool (bool X)
bool (bool X) is non empty set
[:(bool X),(bool X):] is non empty Relation-like set
bool [:(bool X),(bool X):] is non empty set
[:(bool X),(bool X):] is non empty Relation-like bool X -defined bool X -valued Element of bool [:(bool X),(bool X):]
[:(bool X),(bool X):] is non empty Relation-like set
bool [:(bool X),(bool X):] is non empty set
{dcF,S} is non empty finite countable set
{dcF} is non empty trivial finite 1 -element countable set
{{dcF,S},{dcF}} is non empty finite V40() countable set
S is Element of bool X
ck is Element of bool X
(X,S,ck) is V21() Element of (X)
{S,ck} is non empty finite countable set
{S} is non empty trivial finite 1 -element countable set
{{S,ck},{S}} is non empty finite V40() countable set
B is set
X is set
bool X is non empty Element of bool (bool X)
bool X is non empty set
bool (bool X) is non empty set
[:(bool X),(bool X):] is non empty Relation-like set
bool [:(bool X),(bool X):] is non empty set
F is Relation-like bool X -defined bool X -valued Element of bool [:(bool X),(bool X):]
(X,F) is Relation-like bool X -defined bool X -valued Element of bool [:(bool X),(bool X):]
(X) is non empty Relation-like (X) -defined (X) -valued total reflexive antisymmetric transitive Element of bool [:(X),(X):]
(X) is non empty Relation-like bool X -defined bool X -valued Element of bool [:(bool X),(bool X):]
[:(bool X),(bool X):] is non empty Relation-like bool X -defined bool X -valued Element of bool [:(bool X),(bool X):]
[:(bool X),(bool X):] is non empty Relation-like set
bool [:(bool X),(bool X):] is non empty set
[:(X),(X):] is non empty Relation-like set
bool [:(X),(X):] is non empty set
{ [b<sub>1</sub>,b<sub>2</sub>] where b<sub>1</sub>, b<sub>2</sub> is Element of (X) : (X,b<sub>2</sub>,b<sub>1</sub>) } is set
(F,(X)) is Relation-like bool X -defined bool X -valued Element of bool F
bool F is non empty set
{ b<sub>1</sub> where b<sub>1</sub> is Element of bool X : [b<sub>1</sub>,X] in (X,F) } is set
dcF is set
S is Element of bool X
[S,X] is V21() set
{S,X} is non empty finite countable set
{S} is non empty trivial finite 1 -element countable set
{{S,X},{S}} is non empty finite V40() countable set
X is finite countable set
bool X is non empty finite V40() countable Element of bool (bool X)
bool X is non empty finite V40() countable set
bool (bool X) is non empty finite V40() countable set
[:(bool X),(bool X):] is non empty Relation-like finite countable set
bool [:(bool X),(bool X):] is non empty finite V40() countable set
F is Relation-like bool X -defined bool X -valued finite countable Element of bool [:(bool X),(bool X):]
(X,F) is finite V40() countable Element of bool (bool X)
(X,F) is Relation-like bool X -defined bool X -valued finite countable Element of bool [:(bool X),(bool X):]
(X) is non empty Relation-like (X) -defined (X) -valued total finite countable reflexive antisymmetric transitive Element of bool [:(X),(X):]
(X) is non empty Relation-like bool X -defined bool X -valued finite countable Element of bool [:(bool X),(bool X):]
[:(bool X),(bool X):] is non empty Relation-like bool X -defined bool X -valued finite countable Element of bool [:(bool X),(bool X):]
[:(bool X),(bool X):] is non empty Relation-like finite countable set
bool [:(bool X),(bool X):] is non empty finite V40() countable set
[:(X),(X):] is non empty Relation-like finite countable set
bool [:(X),(X):] is non empty finite V40() countable set
{ [b<sub>1</sub>,b<sub>2</sub>] where b<sub>1</sub>, b<sub>2</sub> is Element of (X) : (X,b<sub>2</sub>,b<sub>1</sub>) } is set
(F,(X)) is Relation-like bool X -defined bool X -valued finite countable Element of bool F
bool F is non empty finite V40() countable set
{ b<sub>1</sub> where b<sub>1</sub> is Element of bool X : [b<sub>1</sub>,X] in (X,F) } is set
K is finite countable Element of bool X
{ (X,b<sub>1</sub>,b<sub>2</sub>) where b<sub>1</sub>, b<sub>2</sub> is finite countable Element of bool X : ( K c= b<sub>1</sub> or b<sub>2</sub> c= b<sub>1</sub> ) } is set
{K} is non empty trivial finite V40() 1 -element countable set
[K,X] is V21() set
{K,X} is non empty finite V40() countable set
{{K,X},{K}} is non empty finite V40() countable set
{[K,X]} is non empty trivial Relation-like Function-like constant finite 1 -element countable finite-support set
{ (X,b<sub>1</sub>,b<sub>1</sub>) where b<sub>1</sub> is finite countable Element of bool X : not K c= b<sub>1</sub> } is set
{[K,X]} \/ { (X,b<sub>1</sub>,b<sub>1</sub>) where b<sub>1</sub> is finite countable Element of bool X : not K c= b<sub>1</sub> } is non empty set
dcF is set
S is finite countable Element of bool X
[S,X] is V21() set
{S,X} is non empty finite V40() countable set
{S} is non empty trivial finite V40() 1 -element countable set
{{S,X},{S}} is non empty finite V40() countable set
S is finite countable Element of bool X
(X,S,S) is V21() Element of (X)
{S,S} is non empty finite V40() countable set
{S} is non empty trivial finite V40() 1 -element countable set
{{S,S},{S}} is non empty finite V40() countable set
X is ()
the of X is non empty finite countable set
(X) is Relation-like bool the of X -defined bool the of X -valued finite countable Element of bool [:(bool the of X),(bool the of X):]
bool the of X is non empty finite V40() countable Element of bool (bool the of X)
bool the of X is non empty finite V40() countable set
bool (bool the of X) is non empty finite V40() countable set
[:(bool the of X),(bool the of X):] is non empty Relation-like finite countable set
bool [:(bool the of X),(bool the of X):] is non empty finite V40() countable set
{ [b<sub>1</sub>,b<sub>2</sub>] where b<sub>1</sub>, b<sub>2</sub> is finite countable Element of bool the of X : (X,b<sub>1</sub>,b<sub>2</sub>) } is set
( the of X,(X)) is finite V40() countable Element of bool (bool the of X)
( the of X,(X)) is Relation-like bool the of X -defined bool the of X -valued finite countable Element of bool [:(bool the of X),(bool the of X):]
( the of X) is non empty Relation-like ( the of X) -defined ( the of X) -valued total finite countable reflexive antisymmetric transitive Element of bool [:( the of X),( the of X):]
( the of X) is non empty Relation-like bool the of X -defined bool the of X -valued finite countable Element of bool [:(bool the of X),(bool the of X):]
[:(bool the of X),(bool the of X):] is non empty Relation-like bool the of X -defined bool the of X -valued finite countable Element of bool [:(bool the of X),(bool the of X):]
[:(bool the of X),(bool the of X):] is non empty Relation-like finite countable set
bool [:(bool the of X),(bool the of X):] is non empty finite V40() countable set
[:( the of X),( the of X):] is non empty Relation-like finite countable set
bool [:( the of X),( the of X):] is non empty finite V40() countable set
{ [b<sub>1</sub>,b<sub>2</sub>] where b<sub>1</sub>, b<sub>2</sub> is Element of ( the of X) : ( the of X,b<sub>2</sub>,b<sub>1</sub>) } is set
((X),( the of X)) is Relation-like bool the of X -defined bool the of X -valued finite countable Element of bool (X)
bool (X) is non empty finite V40() countable set
{ b<sub>1</sub> where b<sub>1</sub> is Element of bool the of X : [b<sub>1</sub>, the of X] in ( the of X,(X)) } is set
( the of X,(X)) is finite V40() countable Element of bool (bool the of X)
{ b<sub>1</sub> where b<sub>1</sub> is Element of bool the of X : not for b<sub>2</sub> being Element of bool the of X holds ( the of X,(X),b<sub>2</sub>,b<sub>1</sub>) } is set
dcF is finite countable Element of bool the of X
S is finite countable Element of bool the of X
[S, the of X] is V21() set
{S, the of X} is non empty finite V40() countable set
{S} is non empty trivial finite V40() 1 -element countable set
{{S, the of X},{S}} is non empty finite V40() countable set
S is set
ck is set
B is finite countable Element of bool the of X
[B, the of X] is V21() set
{B, the of X} is non empty finite V40() countable set
{B} is non empty trivial finite V40() 1 -element countable set
{{B, the of X},{B}} is non empty finite V40() countable set
m is finite countable Element of bool the of X
[m, the of X] is V21() set
{m, the of X} is non empty finite V40() countable set
{m} is non empty trivial finite V40() 1 -element countable set
{{m, the of X},{m}} is non empty finite V40() countable set
[#] the of X is non empty non proper finite countable Element of bool the of X
( the of X,m,([#] the of X)) is V21() Element of ( the of X)
{m,([#] the of X)} is non empty finite V40() countable set
{{m,([#] the of X)},{m}} is non empty finite V40() countable set
( the of X,B,([#] the of X)) is V21() Element of ( the of X)
{B,([#] the of X)} is non empty finite V40() countable set
{{B,([#] the of X)},{B}} is non empty finite V40() countable set
X is finite countable set
bool X is non empty finite V40() countable set
bool (bool X) is non empty finite V40() countable set
bool X is non empty finite V40() countable Element of bool (bool X)
[:(bool X),(bool X):] is non empty Relation-like finite countable set
bool [:(bool X),(bool X):] is non empty finite V40() countable set
F is finite V40() countable Element of bool (bool X)
{ b<sub>1</sub> where b<sub>1</sub> is finite countable Element of bool X : for b<sub>2</sub> being finite countable Element of bool X holds
( not b<sub>2</sub> in F or not b<sub>2</sub> c= b<sub>1</sub> ) } is set
[#] X is non proper finite countable Element of bool X
dcF is set
S is finite countable Element of bool X
dcF is finite V40() countable Element of bool (bool X)
{ (X,b<sub>1</sub>,b<sub>2</sub>) where b<sub>1</sub>, b<sub>2</sub> is finite countable Element of bool X : for b<sub>3</sub> being set holds
( not b<sub>3</sub> in dcF or not b<sub>1</sub> c= b<sub>3</sub> or b<sub>2</sub> c= b<sub>3</sub> ) } is set
(X,dcF) is Relation-like bool X -defined bool X -valued finite countable Element of bool [:(bool X),(bool X):]
ck is set
m is set
B is finite countable Element of bool X
P is finite countable Element of bool X
[B,X] is V21() set
{B,X} is non empty finite V40() countable set
{B} is non empty trivial finite V40() 1 -element countable set
{{B,X},{B}} is non empty finite V40() countable set
S is non empty Relation-like bool X -defined bool X -valued finite countable transitive (X) (X) (X) (X) (X) Element of bool [:(bool X),(bool X):]
(X,S) is Relation-like bool X -defined bool X -valued finite countable Element of bool [:(bool X),(bool X):]
(X) is non empty Relation-like (X) -defined (X) -valued total finite countable reflexive antisymmetric transitive Element of bool [:(X),(X):]
(X) is non empty Relation-like bool X -defined bool X -valued finite countable Element of bool [:(bool X),(bool X):]
[:(bool X),(bool X):] is non empty Relation-like bool X -defined bool X -valued finite countable Element of bool [:(bool X),(bool X):]
[:(bool X),(bool X):] is non empty Relation-like finite countable set
bool [:(bool X),(bool X):] is non empty finite V40() countable set
[:(X),(X):] is non empty Relation-like finite countable set
bool [:(X),(X):] is non empty finite V40() countable set
{ [b<sub>1</sub>,b<sub>2</sub>] where b<sub>1</sub>, b<sub>2</sub> is Element of (X) : (X,b<sub>2</sub>,b<sub>1</sub>) } is set
(S,(X)) is Relation-like bool X -defined bool X -valued finite countable Element of bool S
bool S is non empty finite V40() countable set
(X,B,([#] X)) is V21() Element of (X)
{B,([#] X)} is non empty finite V40() countable set
{{B,([#] X)},{B}} is non empty finite V40() countable set
m is finite countable Element of bool X
P is finite countable Element of bool X
(X,m,P) is V21() Element of (X)
{m,P} is non empty finite V40() countable set
{m} is non empty trivial finite V40() 1 -element countable set
{{m,P},{m}} is non empty finite V40() countable set
[ck,X] is V21() set
{ck,X} is non empty finite countable set
{ck} is non empty trivial finite 1 -element countable set
{{ck,X},{ck}} is non empty finite V40() countable set
x9 is finite countable Element of bool X
(X,S) is finite V40() countable Element of bool (bool X)
{ b<sub>1</sub> where b<sub>1</sub> is Element of bool X : [b<sub>1</sub>,X] in (X,S) } is set
ck is set
[ck,X] is V21() set
{ck,X} is non empty finite countable set
{ck} is non empty trivial finite 1 -element countable set
{{ck,X},{ck}} is non empty finite V40() countable set
B is finite countable Element of bool X
[B,X] is V21() set
{B,X} is non empty finite V40() countable set
{B} is non empty trivial finite V40() 1 -element countable set
{{B,X},{B}} is non empty finite V40() countable set
m is finite countable Element of bool X
(X,m,([#] X)) is V21() Element of (X)
{m,([#] X)} is non empty finite V40() countable set
{m} is non empty trivial finite V40() 1 -element countable set
{{m,([#] X)},{m}} is non empty finite V40() countable set
(X,B,([#] X)) is V21() Element of (X)
{B,([#] X)} is non empty finite V40() countable set
{{B,([#] X)},{B}} is non empty finite V40() countable set
[m,X] is V21() set
{m,X} is non empty finite V40() countable set
{{m,X},{m}} is non empty finite V40() countable set
m is set
m is set
P is finite countable Element of bool X
X is finite countable set
bool X is non empty finite V40() countable set
bool (bool X) is non empty finite V40() countable set
F is finite V40() countable Element of bool (bool X)
{ b<sub>1</sub> where b<sub>1</sub> is finite countable Element of bool X : for b<sub>2</sub> being finite countable Element of bool X holds
( not b<sub>2</sub> in F or not b<sub>2</sub> c= b<sub>1</sub> ) } is set
K is set
(X,K) is Relation-like bool X -defined bool X -valued finite countable Element of bool [:(bool X),(bool X):]
bool X is non empty finite V40() countable Element of bool (bool X)
[:(bool X),(bool X):] is non empty Relation-like finite countable set
bool [:(bool X),(bool X):] is non empty finite V40() countable set
{ (X,b<sub>1</sub>,b<sub>2</sub>) where b<sub>1</sub>, b<sub>2</sub> is Element of bool X : for b<sub>3</sub> being set holds
( not b<sub>3</sub> in K or not b<sub>1</sub> c= b<sub>3</sub> or b<sub>2</sub> c= b<sub>3</sub> ) } is set
(X,(X,K)) is finite V40() countable Element of bool (bool X)
(X,(X,K)) is Relation-like bool X -defined bool X -valued finite countable Element of bool [:(bool X),(bool X):]
(X) is non empty Relation-like (X) -defined (X) -valued total finite countable reflexive antisymmetric transitive Element of bool [:(X),(X):]
(X) is non empty Relation-like bool X -defined bool X -valued finite countable Element of bool [:(bool X),(bool X):]
[:(bool X),(bool X):] is non empty Relation-like bool X -defined bool X -valued finite countable Element of bool [:(bool X),(bool X):]
[:(bool X),(bool X):] is non empty Relation-like finite countable set
bool [:(bool X),(bool X):] is non empty finite V40() countable set
[:(X),(X):] is non empty Relation-like finite countable set
bool [:(X),(X):] is non empty finite V40() countable set
{ [b<sub>1</sub>,b<sub>2</sub>] where b<sub>1</sub>, b<sub>2</sub> is Element of (X) : (X,b<sub>2</sub>,b<sub>1</sub>) } is set
((X,K),(X)) is Relation-like bool X -defined bool X -valued finite countable Element of bool (X,K)
bool (X,K) is non empty finite V40() countable set
{ b<sub>1</sub> where b<sub>1</sub> is Element of bool X : [b<sub>1</sub>,X] in (X,(X,K)) } is set
dcF is set
S is finite countable Element of bool X
[#] X is non proper finite countable Element of bool X
S is set
B is set
dcF is finite V40() countable Element of bool (bool X)
ck is finite countable Element of bool X
m is finite countable Element of bool X
[ck,X] is V21() set
{ck,X} is non empty finite V40() countable set
{ck} is non empty trivial finite V40() 1 -element countable set
{{ck,X},{ck}} is non empty finite V40() countable set
(X,ck,([#] X)) is V21() Element of (X)
{ck,([#] X)} is non empty finite V40() countable set
{{ck,([#] X)},{ck}} is non empty finite V40() countable set
B is finite countable Element of bool X
m is finite countable Element of bool X
(X,B,m) is V21() Element of (X)
{B,m} is non empty finite V40() countable set
{B} is non empty trivial finite V40() 1 -element countable set
{{B,m},{B}} is non empty finite V40() countable set
[S,X] is V21() set
{S,X} is non empty finite countable set
{S} is non empty trivial finite 1 -element countable set
{{S,X},{S}} is non empty finite V40() countable set
P is finite countable Element of bool X
S is set
[S,X] is V21() set
{S,X} is non empty finite countable set
{S} is non empty trivial finite 1 -element countable set
{{S,X},{S}} is non empty finite V40() countable set
ck is finite countable Element of bool X
[ck,X] is V21() set
{ck,X} is non empty finite V40() countable set
{ck} is non empty trivial finite V40() 1 -element countable set
{{ck,X},{ck}} is non empty finite V40() countable set
B is finite countable Element of bool X
(X,B,([#] X)) is V21() Element of (X)
{B,([#] X)} is non empty finite V40() countable set
{B} is non empty trivial finite V40() 1 -element countable set
{{B,([#] X)},{B}} is non empty finite V40() countable set
(X,ck,([#] X)) is V21() Element of (X)
{ck,([#] X)} is non empty finite V40() countable set
{{ck,([#] X)},{ck}} is non empty finite V40() countable set
[B,X] is V21() set
{B,X} is non empty finite V40() countable set
{{B,X},{B}} is non empty finite V40() countable set
B is set
B is set
m is finite countable Element of bool X
X is non empty finite countable set
bool X is non empty finite V40() countable set
bool (bool X) is non empty finite V40() countable set
F is finite V40() countable Element of bool (bool X)
bool X is non empty finite V40() countable Element of bool (bool X)
X --> (bool X) is non empty Relation-like non-empty X -defined bool (bool X) -valued Function-like constant total V24(X, bool (bool X)) finite countable finite-support Element of bool [:X,(bool (bool X)):]
[:X,(bool (bool X)):] is non empty Relation-like finite countable set
bool [:X,(bool (bool X)):] is non empty finite V40() countable set
{ b<sub>1</sub> where b<sub>1</sub> is finite countable Element of bool X : for b<sub>2</sub> being finite countable Element of bool X holds
( not b<sub>2</sub> in F or not b<sub>1</sub> /\ b<sub>2</sub> = {} ) } is set
{0} is non empty trivial functional finite V40() 1 -element with_common_domain countable set
{ b<sub>1</sub> where b<sub>1</sub> is finite countable Element of bool X : for b<sub>2</sub> being finite countable Element of bool X holds
( not b<sub>2</sub> in F or not b<sub>1</sub> /\ b<sub>2</sub> = {} ) } \/ {0} is non empty set
X --> 0 is non empty Relation-like X -defined NAT -valued Function-like constant total V24(X, NAT ) Function-yielding V28() finite Cardinal-yielding countable finite-support Element of bool [:X,NAT:]
[:X,NAT:] is non empty non trivial Relation-like non finite set
bool [:X,NAT:] is non empty non trivial non finite set
S is non empty set
{ ((X --> 0) +* (b<sub>1</sub> --> b<sub>1</sub>)) where b<sub>1</sub> is finite countable Element of bool X : b<sub>1</sub> in S } is set
K is Relation-like non-empty X -defined Function-like total finite-support set
product K is non empty functional with_common_domain product-like set
ck is set
dom K is finite countable Element of bool X
B is finite countable Element of bool X
B --> B is Relation-like B -defined bool X -valued Function-like constant total V24(B, bool X) finite countable finite-support Element of bool [:B,(bool X):]
[:B,(bool X):] is Relation-like finite countable set
bool [:B,(bool X):] is non empty finite V40() countable set
(X --> 0) +* (B --> B) is non empty Relation-like Function-like finite countable finite-support set
dom (B --> B) is finite countable Element of bool B
bool B is non empty finite V40() countable set
P is set
K . P is set
((X --> 0) +* (B --> B)) . P is set
(B --> B) . P is set
((X --> 0) +* (B --> B)) . P is set
(X --> 0) . P is Relation-like Function-like set
{} X is empty proper ext-real non positive non negative Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional Function-yielding V28() V29() V30() V31() V33() V34() V35() finite finite-yielding V40() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V48() V49() Cardinal-yielding with_common_domain countable FinSequence-yielding finite-support Element of bool X
proj1 ((X --> 0) +* (B --> B)) is non empty finite countable set
dom (X --> 0) is non empty finite countable Element of bool X
(dom (X --> 0)) \/ B is non empty finite countable Element of bool X
X \/ B is non empty finite countable set
{} X is empty proper ext-real non positive non negative Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional Function-yielding V28() V29() V30() V31() V33() V34() V35() finite finite-yielding V40() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V48() V49() Cardinal-yielding with_common_domain countable FinSequence-yielding finite-support Element of bool X
({} X) --> ({} X) is empty ext-real non positive non negative Relation-like non-empty empty-yielding {} X -defined bool X -valued Function-like one-to-one constant functional total V24( {} X, bool X) Function-yielding V28() V29() V30() V31() V33() V34() V35() finite finite-yielding V40() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V48() V49() Cardinal-yielding with_common_domain countable FinSequence-yielding finite-support Element of bool [:({} X),(bool X):]
[:({} X),(bool X):] is Relation-like finite countable set
bool [:({} X),(bool X):] is non empty finite V40() countable set
(X --> 0) +* (({} X) --> ({} X)) is non empty Relation-like Function-like Function-yielding V28() finite countable finite-support set
bool (product K) is non empty set
ck is non empty functional with_common_domain Element of bool (product K)
(X,K,ck) is () ()
B is () ()
the of B is non empty finite countable set
(B) is Relation-like bool the of B -defined bool the of B -valued finite countable Element of bool [:(bool the of B),(bool the of B):]
bool the of B is non empty finite V40() countable Element of bool (bool the of B)
bool the of B is non empty finite V40() countable set
bool (bool the of B) is non empty finite V40() countable set
[:(bool the of B),(bool the of B):] is non empty Relation-like finite countable set
bool [:(bool the of B),(bool the of B):] is non empty finite V40() countable set
{ [b<sub>1</sub>,b<sub>2</sub>] where b<sub>1</sub>, b<sub>2</sub> is finite countable Element of bool the of B : (B,b<sub>1</sub>,b<sub>2</sub>) } is set
( the of B,(B)) is finite V40() countable Element of bool (bool the of B)
( the of B,(B)) is Relation-like bool the of B -defined bool the of B -valued finite countable Element of bool [:(bool the of B),(bool the of B):]
( the of B) is non empty Relation-like ( the of B) -defined ( the of B) -valued total finite countable reflexive antisymmetric transitive Element of bool [:( the of B),( the of B):]
( the of B) is non empty Relation-like bool the of B -defined bool the of B -valued finite countable Element of bool [:(bool the of B),(bool the of B):]
[:(bool the of B),(bool the of B):] is non empty Relation-like bool the of B -defined bool the of B -valued finite countable Element of bool [:(bool the of B),(bool the of B):]
[:(bool the of B),(bool the of B):] is non empty Relation-like finite countable set
bool [:(bool the of B),(bool the of B):] is non empty finite V40() countable set
[:( the of B),( the of B):] is non empty Relation-like finite countable set
bool [:( the of B),( the of B):] is non empty finite V40() countable set
{ [b<sub>1</sub>,b<sub>2</sub>] where b<sub>1</sub>, b<sub>2</sub> is Element of ( the of B) : ( the of B,b<sub>2</sub>,b<sub>1</sub>) } is set
((B),( the of B)) is Relation-like bool the of B -defined bool the of B -valued finite countable Element of bool (B)
bool (B) is non empty finite V40() countable set
{ b<sub>1</sub> where b<sub>1</sub> is Element of bool the of B : [b<sub>1</sub>, the of B] in ( the of B,(B)) } is set
{ b<sub>1</sub> where b<sub>1</sub> is finite countable Element of bool X : [b<sub>1</sub>,X] in ( the of B,(B)) } is set
[#] X is non empty non proper finite countable Element of bool X
x9 is set
y9 is finite countable Element of bool X
the of B is functional with_common_domain Element of bool (product the of B)
the of B is Relation-like non-empty the of B -defined Function-like total finite-support set
product the of B is non empty functional with_common_domain product-like set
bool (product the of B) is non empty set
S is Relation-like Function-like Element of the of B
S | y9 is Relation-like Function-like finite countable finite-support set
S is Relation-like Function-like Element of the of B
S | y9 is Relation-like Function-like finite countable finite-support set
m is finite countable Element of bool X
m --> m is Relation-like m -defined bool X -valued Function-like constant total V24(m, bool X) finite countable finite-support Element of bool [:m,(bool X):]
[:m,(bool X):] is Relation-like finite countable set
bool [:m,(bool X):] is non empty finite V40() countable set
(X --> 0) +* (m --> m) is non empty Relation-like Function-like finite countable finite-support set
dom (m --> m) is finite countable Element of bool m
bool m is non empty finite V40() countable set
P is finite countable Element of bool X
P --> P is Relation-like P -defined bool X -valued Function-like constant total V24(P, bool X) finite countable finite-support Element of bool [:P,(bool X):]
[:P,(bool X):] is Relation-like finite countable set
bool [:P,(bool X):] is non empty finite V40() countable set
(X --> 0) +* (P --> P) is non empty Relation-like Function-like finite countable finite-support set
dom (P --> P) is finite countable Element of bool P
bool P is non empty finite V40() countable set
m /\ y9 is finite countable Element of bool X
x is finite countable Element of bool X
x is set
S . x is set
(P --> P) . x is set
(X --> 0) . x is Relation-like Function-like set
(S | y9) . x is set
(S | y9) . x is set
S . x is set
(m --> m) . x is set
S | X is Relation-like Function-like finite countable finite-support set
S | X is Relation-like Function-like finite countable finite-support set
m /\ y9 is finite countable Element of bool X
x is finite countable Element of bool X
x is set
(S | y9) . x is set
S . x is set
(X --> 0) +* {} is non empty Relation-like Function-like Function-yielding V28() finite countable finite-support set
((X --> 0) +* {}) . x is Relation-like Function-like set
(X --> 0) . x is Relation-like Function-like set
(S | y9) . x is set
S . x is set
(m --> m) . x is set
S | X is Relation-like Function-like finite countable finite-support set
S | X is Relation-like Function-like finite countable finite-support set
P /\ y9 is finite countable Element of bool X
x is finite countable Element of bool X
x is set
(S | y9) . x is set
S . x is set
(X --> 0) +* {} is non empty Relation-like Function-like Function-yielding V28() finite countable finite-support set
((X --> 0) +* {}) . x is Relation-like Function-like set
(X --> 0) . x is Relation-like Function-like set
(S | y9) . x is set
S . x is set
(P --> P) . x is set
S | X is Relation-like Function-like finite countable finite-support set
S | X is Relation-like Function-like finite countable finite-support set
S | X is Relation-like Function-like finite countable finite-support set
S | X is Relation-like Function-like finite countable finite-support set
a is finite countable Element of bool the of B
k is finite countable Element of bool the of B
[y9,X] is V21() set
{y9,X} is non empty finite V40() countable set
{y9} is non empty trivial finite V40() 1 -element countable set
{{y9,X},{y9}} is non empty finite V40() countable set
(X,y9,([#] X)) is V21() Element of (X)
(X) is non empty Relation-like bool X -defined bool X -valued finite countable Element of bool [:(bool X),(bool X):]
[:(bool X),(bool X):] is non empty Relation-like finite countable set
bool [:(bool X),(bool X):] is non empty finite V40() countable set
[:(bool X),(bool X):] is non empty Relation-like bool X -defined bool X -valued finite countable Element of bool [:(bool X),(bool X):]
[:(bool X),(bool X):] is non empty Relation-like finite countable set
bool [:(bool X),(bool X):] is non empty finite V40() countable set
{y9,([#] X)} is non empty finite V40() countable set
{{y9,([#] X)},{y9}} is non empty finite V40() countable set
S is finite countable Element of bool X
S is finite countable Element of bool X
(X,S,S) is V21() Element of (X)
{S,S} is non empty finite V40() countable set
{S} is non empty trivial finite V40() 1 -element countable set
{{S,S},{S}} is non empty finite V40() countable set
m is finite countable Element of bool the of B
P is finite countable Element of bool the of B
( the of B,m,P) is V21() Element of ( the of B)
{m,P} is non empty finite V40() countable set
{m} is non empty trivial finite V40() 1 -element countable set
{{m,P},{m}} is non empty finite V40() countable set
S ` is finite countable Element of bool X
X \ S is finite countable set
(S `) --> (S `) is Relation-like S ` -defined bool X -valued Function-like constant total V24(S ` , bool X) finite countable finite-support Element of bool [:(S `),(bool X):]
[:(S `),(bool X):] is Relation-like finite countable set
bool [:(S `),(bool X):] is non empty finite V40() countable set
(X --> 0) +* ((S `) --> (S `)) is non empty Relation-like Function-like finite countable finite-support set
m is set
r0 is finite countable Element of bool X
(S `) /\ r0 is finite countable Element of bool X
(X --> 0) +* {} is non empty Relation-like Function-like Function-yielding V28() finite countable finite-support set
r0 is Relation-like Function-like Element of the of B
r0 | X is Relation-like Function-like finite countable finite-support set
(r0 | X) . m is set
r0 . m is set
dom ((S `) --> (S `)) is finite countable Element of bool (S `)
bool (S `) is non empty finite V40() countable set
r1 is Relation-like Function-like Element of the of B
proj1 r1 is set
dom (X --> 0) is non empty finite countable Element of bool X
(dom (X --> 0)) \/ (dom ((S `) --> (S `))) is non empty finite countable set
X \/ (dom ((S `) --> (S `))) is non empty finite countable set
X \/ (S `) is non empty finite countable set
proj1 r0 is set
r0 | S is Relation-like Function-like finite countable finite-support set
proj1 (r0 | S) is finite countable set
(proj1 r1) /\ S is finite countable Element of bool X
r0 is set
(proj1 r0) /\ S is finite countable Element of bool X
S /\ (S `) is finite countable Element of bool X
(r0 | S) . r0 is set
(X --> 0) . r0 is Relation-like Function-like set
r1 . r0 is set
r1 | S is Relation-like Function-like finite countable finite-support set
r1 | X is Relation-like Function-like finite countable finite-support set
(r1 | X) . m is set
r1 . m is set
((S `) --> (S `)) . m is set
x9 is set
y9 is finite countable Element of bool X
[y9,X] is V21() set
{y9,X} is non empty finite V40() countable set
{y9} is non empty trivial finite V40() 1 -element countable set
{{y9,X},{y9}} is non empty finite V40() countable set
a is finite countable Element of bool the of B
k is finite countable Element of bool the of B
( the of B,a,k) is V21() Element of ( the of B)
{a,k} is non empty finite V40() countable set
{a} is non empty trivial finite V40() 1 -element countable set
{{a,k},{a}} is non empty finite V40() countable set
S is set
S is finite countable Element of bool X
[S,X] is V21() set
{S,X} is non empty finite V40() countable set
{S} is non empty trivial finite V40() 1 -element countable set
{{S,X},{S}} is non empty finite V40() countable set
P is finite countable Element of bool the of B
x is finite countable Element of bool the of B
( the of B,P,x) is V21() Element of ( the of B)
{P,x} is non empty finite V40() countable set
{P} is non empty trivial finite V40() 1 -element countable set
{{P,x},{P}} is non empty finite V40() countable set
m is finite countable Element of bool the of B
( the of B,m,x) is V21() Element of ( the of B)
{m,x} is non empty finite V40() countable set
{m} is non empty trivial finite V40() 1 -element countable set
{{m,x},{m}} is non empty finite V40() countable set
{ b₁ where b₁ is Element of X : ( not b₁ in y9 & ex b₂ being set st
( b₂ in F & b₁ in b₂ ) ) } is set
S is set
m is Element of X
P is set
S is set
m is finite countable Element of bool X
P is set
x is Element of X
y is set
m is finite countable Element of bool X
m --> m is Relation-like m -defined bool X -valued Function-like constant total V24(m, bool X) finite countable finite-support Element of bool [:m,(bool X):]
[:m,(bool X):] is Relation-like finite countable set
bool [:m,(bool X):] is non empty finite V40() countable set
(X --> 0) +* (m --> m) is non empty Relation-like Function-like finite countable finite-support set
r0 is finite countable Element of bool X
r1 is set
m /\ r0 is finite countable Element of bool X
dom (m --> m) is finite countable Element of bool m
bool m is non empty finite V40() countable set
r1 is Relation-like Function-like Element of the of B
proj1 r1 is set
(dom (X --> 0)) \/ (dom (m --> m)) is non empty finite countable set
X \/ (dom (m --> m)) is non empty finite countable set
X \/ m is non empty finite countable set
r0 is Relation-like Function-like Element of the of B
proj1 r0 is set
r0 | y9 is Relation-like Function-like finite countable finite-support set
proj1 (r0 | y9) is finite countable set
(proj1 r1) /\ y9 is finite countable Element of bool X
(proj1 r0) /\ y9 is finite countable Element of bool X
x is set
g is Element of X
bs0 is set
(r0 | y9) . x is set
(X --> 0) . x is Relation-like Function-like set
r1 . x is set
r1 | y9 is Relation-like Function-like finite countable finite-support set
r1 | X is Relation-like Function-like finite countable finite-support set
(r1 | X) . y is set
r1 . y is set
(m --> m) . y is set
r0 | X is Relation-like Function-like finite countable finite-support set
(r0 | X) . y is set
r0 . y is set
X is set
bool X is non empty Element of bool (bool X)
bool X is non empty set
bool (bool X) is non empty set
[:(bool X),(bool X):] is non empty Relation-like set
bool [:(bool X),(bool X):] is non empty set
X is set
bool X is non empty Element of bool (bool X)
bool X is non empty set
bool (bool X) is non empty set
[:(bool X),(bool X):] is non empty Relation-like set
bool [:(bool X),(bool X):] is non empty set
K is set
bool K is non empty Element of bool (bool K)
bool K is non empty set
bool (bool K) is non empty set
[:(bool K),(bool K):] is non empty Relation-like set
bool [:(bool K),(bool K):] is non empty set
F is Relation-like bool X -defined bool X -valued Element of bool [:(bool X),(bool X):]
dcF is Relation-like bool K -defined bool K -valued Element of bool [:(bool K),(bool K):]
X is set
bool X is non empty Element of bool (bool X)
bool X is non empty set
bool (bool X) is non empty set
[:(bool X),(bool X):] is non empty Relation-like set
bool [:(bool X),(bool X):] is non empty set
F is Relation-like bool X -defined bool X -valued Element of bool [:(bool X),(bool X):]
K is Element of bool X
dcF is Element of bool X
(X,K,dcF) is V21() Element of (X)
(X) is non empty Relation-like bool X -defined bool X -valued Element of bool [:(bool X),(bool X):]
[:(bool X),(bool X):] is non empty Relation-like bool X -defined bool X -valued Element of bool [:(bool X),(bool X):]
[:(bool X),(bool X):] is non empty Relation-like set
bool [:(bool X),(bool X):] is non empty set
{K,dcF} is non empty finite countable set
{K} is non empty trivial finite 1 -element countable set
{{K,dcF},{K}} is non empty finite V40() countable set
S is Element of bool X
(X,K,S) is V21() Element of (X)
{K,S} is non empty finite countable set
{{K,S},{K}} is non empty finite V40() countable set
dcF \/ S is Element of bool X
(X,K,(dcF \/ S)) is V21() Element of (X)
{K,(dcF \/ S)} is non empty finite countable set
{{K,(dcF \/ S)},{K}} is non empty finite V40() countable set
K \/ K is Element of bool X
(X,(K \/ K),(dcF \/ S)) is V21() Element of (X)
{(K \/ K),(dcF \/ S)} is non empty finite countable set
{(K \/ K)} is non empty trivial finite 1 -element countable set
{{(K \/ K),(dcF \/ S)},{(K \/ K)}} is non empty finite V40() countable set
K is Element of bool X
dcF is Element of bool X
(X,K,dcF) is V21() Element of (X)
(X) is non empty Relation-like bool X -defined bool X -valued Element of bool [:(bool X),(bool X):]
[:(bool X),(bool X):] is non empty Relation-like bool X -defined bool X -valued Element of bool [:(bool X),(bool X):]
[:(bool X),(bool X):] is non empty Relation-like set
bool [:(bool X),(bool X):] is non empty set
{K,dcF} is non empty finite countable set
{K} is non empty trivial finite 1 -element countable set
{{K,dcF},{K}} is non empty finite V40() countable set
S is Element of bool X
S is Element of bool X
(X,S,S) is V21() Element of (X)
{S,S} is non empty finite countable set
{S} is non empty trivial finite 1 -element countable set
{{S,S},{S}} is non empty finite V40() countable set
K \/ S is Element of bool X
dcF \/ S is Element of bool X
(X,(K \/ S),(dcF \/ S)) is V21() Element of (X)
{(K \/ S),(dcF \/ S)} is non empty finite countable set
{(K \/ S)} is non empty trivial finite 1 -element countable set
{{(K \/ S),(dcF \/ S)},{(K \/ S)}} is non empty finite V40() countable set
(X,(K \/ S),S) is V21() Element of (X)
{(K \/ S),S} is non empty finite countable set
{{(K \/ S),S},{(K \/ S)}} is non empty finite V40() countable set
(X,(K \/ S),S) is V21() Element of (X)
{(K \/ S),S} is non empty finite countable set
{{(K \/ S),S},{(K \/ S)}} is non empty finite V40() countable set
(X,(K \/ S),K) is V21() Element of (X)
{(K \/ S),K} is non empty finite countable set
{{(K \/ S),K},{(K \/ S)}} is non empty finite V40() countable set
(X,(K \/ S),dcF) is V21() Element of (X)
{(K \/ S),dcF} is non empty finite countable set
{{(K \/ S),dcF},{(K \/ S)}} is non empty finite V40() countable set
X is set
bool X is non empty Element of bool (bool X)
bool X is non empty set
bool (bool X) is non empty set
[:(bool X),(bool X):] is non empty Relation-like set
bool [:(bool X),(bool X):] is non empty set
F is Relation-like bool X -defined bool X -valued Element of bool [:(bool X),(bool X):]
K is Element of bool X
dcF is Element of bool X
(X,K,dcF) is V21() Element of (X)
(X) is non empty Relation-like bool X -defined bool X -valued Element of bool [:(bool X),(bool X):]
[:(bool X),(bool X):] is non empty Relation-like bool X -defined bool X -valued Element of bool [:(bool X),(bool X):]
[:(bool X),(bool X):] is non empty Relation-like set
bool [:(bool X),(bool X):] is non empty set
{K,dcF} is non empty finite countable set
{K} is non empty trivial finite 1 -element countable set
{{K,dcF},{K}} is non empty finite V40() countable set
S is Element of bool X
dcF \/ S is Element of bool X
S is Element of bool X
(X,(dcF \/ S),S) is V21() Element of (X)
{(dcF \/ S),S} is non empty finite countable set
{(dcF \/ S)} is non empty trivial finite 1 -element countable set
{{(dcF \/ S),S},{(dcF \/ S)}} is non empty finite V40() countable set
K \/ S is Element of bool X
(X,(K \/ S),S) is V21() Element of (X)
{(K \/ S),S} is non empty finite countable set
{(K \/ S)} is non empty trivial finite 1 -element countable set
{{(K \/ S),S},{(K \/ S)}} is non empty finite V40() countable set
(X,S,S) is V21() Element of (X)
{S,S} is non empty finite countable set
{S} is non empty trivial finite 1 -element countable set
{{S,S},{S}} is non empty finite V40() countable set
(X,(K \/ S),(dcF \/ S)) is V21() Element of (X)
{(K \/ S),(dcF \/ S)} is non empty finite countable set
{{(K \/ S),(dcF \/ S)},{(K \/ S)}} is non empty finite V40() countable set
K is Element of bool X
dcF is Element of bool X
(X,K,dcF) is V21() Element of (X)
(X) is non empty Relation-like bool X -defined bool X -valued Element of bool [:(bool X),(bool X):]
[:(bool X),(bool X):] is non empty Relation-like bool X -defined bool X -valued Element of bool [:(bool X),(bool X):]
[:(bool X),(bool X):] is non empty Relation-like set
bool [:(bool X),(bool X):] is non empty set
{K,dcF} is non empty finite countable set
{K} is non empty trivial finite 1 -element countable set
{{K,dcF},{K}} is non empty finite V40() countable set
S is Element of bool X
K \/ S is Element of bool X
(X,(K \/ S),dcF) is V21() Element of (X)
{(K \/ S),dcF} is non empty finite countable set
{(K \/ S)} is non empty trivial finite 1 -element countable set
{{(K \/ S),dcF},{(K \/ S)}} is non empty finite V40() countable set
(X,(K \/ S),K) is V21() Element of (X)
{(K \/ S),K} is non empty finite countable set
{{(K \/ S),K},{(K \/ S)}} is non empty finite V40() countable set
K is Element of bool X
dcF is Element of bool X
(X,K,dcF) is V21() Element of (X)
(X) is non empty Relation-like bool X -defined bool X -valued Element of bool [:(bool X),(bool X):]
[:(bool X),(bool X):] is non empty Relation-like bool X -defined bool X -valued Element of bool [:(bool X),(bool X):]
[:(bool X),(bool X):] is non empty Relation-like set
bool [:(bool X),(bool X):] is non empty set
{K,dcF} is non empty finite countable set
{K} is non empty trivial finite 1 -element countable set
{{K,dcF},{K}} is non empty finite V40() countable set
S is Element of bool X
(X,dcF,S) is V21() Element of (X)
{dcF,S} is non empty finite countable set
{dcF} is non empty trivial finite 1 -element countable set
{{dcF,S},{dcF}} is non empty finite V40() countable set
dcF \/ K is Element of bool X
(X,(dcF \/ K),S) is V21() Element of (X)
{(dcF \/ K),S} is non empty finite countable set
{(dcF \/ K)} is non empty trivial finite 1 -element countable set
{{(dcF \/ K),S},{(dcF \/ K)}} is non empty finite V40() countable set
K \/ K is Element of bool X
(X,(K \/ K),S) is V21() Element of (X)
{(K \/ K),S} is non empty finite countable set
{(K \/ K)} is non empty trivial finite 1 -element countable set
{{(K \/ K),S},{(K \/ K)}} is non empty finite V40() countable set
(X,K,S) is V21() Element of (X)
{K,S} is non empty finite countable set
{{K,S},{K}} is non empty finite V40() countable set
K is Element of bool X
dcF is Element of bool X
(X,K,dcF) is V21() Element of (X)
{K,dcF} is non empty finite countable set
{K} is non empty trivial finite 1 -element countable set
{{K,dcF},{K}} is non empty finite V40() countable set
S is Element of bool X
S is Element of bool X
(X,S,S) is V21() Element of (X)
{S,S} is non empty finite countable set
{S} is non empty trivial finite 1 -element countable set
{{S,S},{S}} is non empty finite V40() countable set
S \ K is Element of bool X
K \/ (S \ K) is Element of bool X
(X,S,dcF) is V21() Element of (X)
{S,dcF} is non empty finite countable set
{{S,dcF},{S}} is non empty finite V40() countable set
dcF \ S is Element of bool X
S \/ (dcF \ S) is Element of bool X
(X,S,S) is V21() Element of (X)
{S,S} is non empty finite countable set
{S} is non empty trivial finite 1 -element countable set
{{S,S},{S}} is non empty finite V40() countable set
(X,dcF,S) is V21() Element of (X)
{dcF,S} is non empty finite countable set
{dcF} is non empty trivial finite 1 -element countable set
{{dcF,S},{dcF}} is non empty finite V40() countable set
K is Element of bool X
dcF is Element of bool X
(X,K,dcF) is V21() Element of (X)
{K,dcF} is non empty finite countable set
{K} is non empty trivial finite 1 -element countable set
{{K,dcF},{K}} is non empty finite V40() countable set
S is Element of bool X
S is Element of bool X
(X,S,S) is V21() Element of (X)
{S,S} is non empty finite countable set
{S} is non empty trivial finite 1 -element countable set
{{S,S},{S}} is non empty finite V40() countable set
K \/ S is Element of bool X
dcF \/ S is Element of bool X
(X,(K \/ S),(dcF \/ S)) is V21() Element of (X)
{(K \/ S),(dcF \/ S)} is non empty finite countable set
{(K \/ S)} is non empty trivial finite 1 -element countable set
{{(K \/ S),(dcF \/ S)},{(K \/ S)}} is non empty finite V40() countable set
(X,(dcF \/ S),(dcF \/ S)) is V21() Element of (X)
{(dcF \/ S),(dcF \/ S)} is non empty finite countable set
{(dcF \/ S)} is non empty trivial finite 1 -element countable set
{{(dcF \/ S),(dcF \/ S)},{(dcF \/ S)}} is non empty finite V40() countable set
K \/ S is Element of bool X
(X,(K \/ S),(dcF \/ S)) is V21() Element of (X)
{(K \/ S),(dcF \/ S)} is non empty finite countable set
{(K \/ S)} is non empty trivial finite 1 -element countable set
{{(K \/ S),(dcF \/ S)},{(K \/ S)}} is non empty finite V40() countable set
X is set
bool X is non empty Element of bool (bool X)
bool X is non empty set
bool (bool X) is non empty set
[:(bool X),(bool X):] is non empty Relation-like set
bool [:(bool X),(bool X):] is non empty set
F is Relation-like bool X -defined bool X -valued Element of bool [:(bool X),(bool X):]
{ b₁ where b₁ is Element of bool X : ex b₂, b₃ being Element of bool X st
( (X,b₂,b₃) in F & b₂ c= b₁ & not b₃ c= b₁ ) } is set
X is set
bool X is non empty Element of bool (bool X)
bool X is non empty set
bool (bool X) is non empty set
[:(bool X),(bool X):] is non empty Relation-like set
bool [:(bool X),(bool X):] is non empty set
F is set
K is Relation-like bool X -defined bool X -valued Element of bool [:(bool X),(bool X):]
(X,K) is set
{ b₁ where b₁ is Element of bool X : ex b₂, b₃ being Element of bool X st
( (X,b₂,b₃) in K & b₂ c= b₁ & not b₃ c= b₁ ) } is set
dcF is Element of bool X
S is Element of bool X
S is Element of bool X
(X,S,S) is V21() Element of (X)
(X) is non empty Relation-like bool X -defined bool X -valued Element of bool [:(bool X),(bool X):]
[:(bool X),(bool X):] is non empty Relation-like bool X -defined bool X -valued Element of bool [:(bool X),(bool X):]
[:(bool X),(bool X):] is non empty Relation-like set
bool [:(bool X),(bool X):] is non empty set
{S,S} is non empty finite countable set
{S} is non empty trivial finite 1 -element countable set
{{S,S},{S}} is non empty finite V40() countable set
X is set
bool X is non empty set
bool X is non empty Element of bool (bool X)
bool (bool X) is non empty set
[:(bool X),(bool X):] is non empty Relation-like set
bool [:(bool X),(bool X):] is non empty set
dcF is Element of bool X
S is Element of bool X
(X,dcF,S) is V21() Element of (X)
(X) is non empty Relation-like bool X -defined bool X -valued Element of bool [:(bool X),(bool X):]
[:(bool X),(bool X):] is non empty Relation-like bool X -defined bool X -valued Element of bool [:(bool X),(bool X):]
[:(bool X),(bool X):] is non empty Relation-like set
bool [:(bool X),(bool X):] is non empty set
{dcF,S} is non empty finite countable set
{dcF} is non empty trivial finite 1 -element countable set
{{dcF,S},{dcF}} is non empty finite V40() countable set
K is Relation-like bool X -defined bool X -valued Element of bool [:(bool X),(bool X):]
F is Element of bool X
(X,K) is set
{ b₁ where b₁ is Element of bool X : ex b₂, b₃ being Element of bool X st
( (X,b₂,b₃) in K & b₂ c= b₁ & not b₃ c= b₁ ) } is set
X is non empty finite countable set
bool X is non empty finite V40() countable Element of bool (bool X)
bool X is non empty finite V40() countable set
bool (bool X) is non empty finite V40() countable set
[:(bool X),(bool X):] is non empty Relation-like finite countable set
bool [:(bool X),(bool X):] is non empty finite V40() countable set
F is Relation-like bool X -defined bool X -valued finite countable Element of bool [:(bool X),(bool X):]
(X,F) is non empty Relation-like bool X -defined bool X -valued finite countable transitive (X) (X) (X) (X) (X) Element of bool [:(bool X),(bool X):]
(X,F) is set
{ b₁ where b₁ is Element of bool X : ex b₂, b₃ being Element of bool X st
( (X,b₂,b₃) in F & b₂ c= b₁ & not b₃ c= b₁ ) } is set
(X,(X,F)) is finite V40() countable Element of bool (bool X)
{ b₁ where b₁ is Element of bool X : not for b₂ being Element of bool X holds (X,(X,F),b₂,b₁) } is set
(bool X) \ (X,F) is finite V40() countable Element of bool (bool X)
{ b₁ where b₁ is finite countable Element of bool X : for b₂, b₃ being finite countable Element of bool X holds
( not (X,b₂,b₃) in F or not b₂ c= b₁ or b₃ c= b₁ ) } is set
S is set
ck is finite countable Element of bool X
B is finite countable Element of bool X
(X,ck,B) is V21() Element of (X)
(X) is non empty Relation-like bool X -defined bool X -valued finite countable Element of bool [:(bool X),(bool X):]
[:(bool X),(bool X):] is non empty Relation-like bool X -defined bool X -valued finite countable Element of bool [:(bool X),(bool X):]
[:(bool X),(bool X):] is non empty Relation-like finite countable set
bool [:(bool X),(bool X):] is non empty finite V40() countable set
{ck,B} is non empty finite V40() countable set
{ck} is non empty trivial finite V40() 1 -element countable set
{{ck,B},{ck}} is non empty finite V40() countable set
ck is finite countable Element of bool X
(X,F) is finite V40() countable Element of bool (bool X)
S is finite V40() countable Element of bool (bool X)
{ (X,b₁,b₂) where b₁, b₂ is finite countable Element of bool X : for b₃ being set holds
( not b₃ in S or not b₁ c= b₃ or b₂ c= b₃ ) } is set
(X,S) is Relation-like bool X -defined bool X -valued finite countable Element of bool [:(bool X),(bool X):]
B is Relation-like bool X -defined bool X -valued finite countable Element of bool [:(bool X),(bool X):]
m is finite countable Element of bool X
P is finite countable Element of bool X
(X,m,P) is V21() Element of (X)
(X) is non empty Relation-like bool X -defined bool X -valued finite countable Element of bool [:(bool X),(bool X):]
[:(bool X),(bool X):] is non empty Relation-like bool X -defined bool X -valued finite countable Element of bool [:(bool X),(bool X):]
[:(bool X),(bool X):] is non empty Relation-like finite countable set
bool [:(bool X),(bool X):] is non empty finite V40() countable set
{m,P} is non empty finite V40() countable set
{m} is non empty trivial finite V40() 1 -element countable set
{{m,P},{m}} is non empty finite V40() countable set
x9 is finite countable Element of bool X
y9 is finite countable Element of bool X
(X,x9,y9) is V21() Element of (X)
{x9,y9} is non empty finite V40() countable set
{x9} is non empty trivial finite V40() 1 -element countable set
{{x9,y9},{x9}} is non empty finite V40() countable set
a is finite countable Element of bool X
x9 is set
y9 is finite countable Element of bool X
m is finite countable Element of bool X
P is finite countable Element of bool X
(X,m,P) is V21() Element of (X)
{m,P} is non empty finite V40() countable set
{m} is non empty trivial finite V40() 1 -element countable set
{{m,P},{m}} is non empty finite V40() countable set
[#] X is non empty non proper finite countable Element of bool X
X is non empty finite countable set
bool X is non empty finite V40() countable Element of bool (bool X)
bool X is non empty finite V40() countable set
bool (bool X) is non empty finite V40() countable set
[:(bool X),(bool X):] is non empty Relation-like finite countable set
bool [:(bool X),(bool X):] is non empty finite V40() countable set
F is Relation-like bool X -defined bool X -valued finite countable Element of bool [:(bool X),(bool X):]
(X,F) is set
{ b₁ where b₁ is Element of bool X : ex b₂, b₃ being Element of bool X st
( (X,b₂,b₃) in F & b₂ c= b₁ & not b₃ c= b₁ ) } is set
K is Relation-like bool X -defined bool X -valued finite countable Element of bool [:(bool X),(bool X):]
(X,K) is set
{ b₁ where b₁ is Element of bool X : ex b₂, b₃ being Element of bool X st
( (X,b₂,b₃) in K & b₂ c= b₁ & not b₃ c= b₁ ) } is set
(X,F) is non empty Relation-like bool X -defined bool X -valued finite countable transitive (X) (X) (X) (X) (X) Element of bool [:(bool X),(bool X):]
(X,K) is non empty Relation-like bool X -defined bool X -valued finite countable transitive (X) (X) (X) (X) (X) Element of bool [:(bool X),(bool X):]
S is set
ck is finite countable Element of bool X
B is finite countable Element of bool X
(X,ck,B) is V21() Element of (X)
(X) is non empty Relation-like bool X -defined bool X -valued finite countable Element of bool [:(bool X),(bool X):]
[:(bool X),(bool X):] is non empty Relation-like bool X -defined bool X -valued finite countable Element of bool [:(bool X),(bool X):]
[:(bool X),(bool X):] is non empty Relation-like finite countable set
bool [:(bool X),(bool X):] is non empty finite V40() countable set
{ck,B} is non empty finite V40() countable set
{ck} is non empty trivial finite V40() 1 -element countable set
{{ck,B},{ck}} is non empty finite V40() countable set
m is finite countable Element of bool X
ck is finite countable Element of bool X
B is finite countable Element of bool X
(X,ck,B) is V21() Element of (X)
{ck,B} is non empty finite V40() countable set
{ck} is non empty trivial finite V40() 1 -element countable set
{{ck,B},{ck}} is non empty finite V40() countable set
m is finite countable Element of bool X
X is non empty finite countable set
bool X is non empty finite V40() countable Element of bool (bool X)
bool X is non empty finite V40() countable set
bool (bool X) is non empty finite V40() countable set
[:(bool X),(bool X):] is non empty Relation-like finite countable set
bool [:(bool X),(bool X):] is non empty finite V40() countable set
F is Relation-like bool X -defined bool X -valued finite countable Element of bool [:(bool X),(bool X):]
(X,F) is set
{ b₁ where b₁ is Element of bool X : ex b₂, b₃ being Element of bool X st
( (X,b₂,b₃) in F & b₂ c= b₁ & not b₃ c= b₁ ) } is set
(X,F) is non empty Relation-like bool X -defined bool X -valued finite countable transitive (X) (X) (X) (X) (X) Element of bool [:(bool X),(bool X):]
(X,(X,F)) is set
{ b₁ where b₁ is Element of bool X : ex b₂, b₃ being Element of bool X st
( (X,b₂,b₃) in (X,F) & b₂ c= b₁ & not b₃ c= b₁ ) } is set
{ b₁ where b₁ is finite countable Element of bool X : for b₂, b₃ being finite countable Element of bool X holds
( not (X,b₂,b₃) in F or not b₂ c= b₁ or b₃ c= b₁ ) } is set
S is set
S is finite countable Element of bool X
ck is finite countable Element of bool X
(X,S,ck) is V21() Element of (X)
(X) is non empty Relation-like bool X -defined bool X -valued finite countable Element of bool [:(bool X),(bool X):]
[:(bool X),(bool X):] is non empty Relation-like bool X -defined bool X -valued finite countable Element of bool [:(bool X),(bool X):]
[:(bool X),(bool X):] is non empty Relation-like finite countable set
bool [:(bool X),(bool X):] is non empty finite V40() countable set
{S,ck} is non empty finite V40() countable set
{S} is non empty trivial finite V40() 1 -element countable set
{{S,ck},{S}} is non empty finite V40() countable set
S is finite countable Element of bool X
ck is finite countable Element of bool X
(X,S,ck) is V21() Element of (X)
(X) is non empty Relation-like bool X -defined bool X -valued finite countable Element of bool [:(bool X),(bool X):]
[:(bool X),(bool X):] is non empty Relation-like bool X -defined bool X -valued finite countable Element of bool [:(bool X),(bool X):]
[:(bool X),(bool X):] is non empty Relation-like finite countable set
bool [:(bool X),(bool X):] is non empty finite V40() countable set
{S,ck} is non empty finite V40() countable set
{S} is non empty trivial finite V40() 1 -element countable set
{{S,ck},{S}} is non empty finite V40() countable set
B is finite countable Element of bool X
m is finite countable Element of bool X
(X,B,m) is V21() Element of (X)
{B,m} is non empty finite V40() countable set
{B} is non empty trivial finite V40() 1 -element countable set
{{B,m},{B}} is non empty finite V40() countable set
(X,F) is finite V40() countable Element of bool (bool X)
(X, { b₁ where b₁ is finite countable Element of bool X : for b₂, b₃ being finite countable Element of bool X holds
( not (X,b₂,b₃) in F or not b₂ c= b₁ or b₃ c= b₁ ) } ) is Relation-like bool X -defined bool X -valued finite countable Element of bool [:(bool X),(bool X):]
{ (X,b₁,b₂) where b₁, b₂ is Element of bool X : for b₃ being set holds
( not b₃ in { b₁ where b₄ is finite countable Element of bool X : for b₅, b₆ being finite countable Element of bool X holds
( not (X,b₂,b₃) in F or not b₂ c= b₁ or b₃ c= b₁ ) } or not b₁ c= b₃ or b₂ c= b₃ ) } is set
B is finite countable Element of bool X
m is finite countable Element of bool X
(X,B,m) is V21() Element of (X)
{B,m} is non empty finite V40() countable set
{B} is non empty trivial finite V40() 1 -element countable set
{{B,m},{B}} is non empty finite V40() countable set
X is set
bool X is non empty Element of bool (bool X)
bool X is non empty set
bool (bool X) is non empty set
[:(bool X),(bool X):] is non empty Relation-like set
bool [:(bool X),(bool X):] is non empty set
X is non empty finite countable set
bool X is non empty finite V40() countable Element of bool (bool X)
bool X is non empty finite V40() countable set
bool (bool X) is non empty finite V40() countable set
[:(bool X),(bool X):] is non empty Relation-like finite countable set
bool [:(bool X),(bool X):] is non empty finite V40() countable set
F is Relation-like bool X -defined bool X -valued finite countable Element of bool [:(bool X),(bool X):]
(X,F) is non empty Relation-like bool X -defined bool X -valued finite countable transitive (X) (X) (X) (X) (X) Element of bool [:(bool X),(bool X):]
(X,(X,F)) is finite V40() countable Element of bool (bool X)
(X,(X,F)) is non empty Relation-like bool X -defined bool X -valued finite countable Element of bool [:(bool X),(bool X):]
(X) is non empty Relation-like (X) -defined (X) -valued total finite countable reflexive antisymmetric transitive Element of bool [:(X),(X):]
(X) is non empty Relation-like bool X -defined bool X -valued finite countable Element of bool [:(bool X),(bool X):]
[:(bool X),(bool X):] is non empty Relation-like bool X -defined bool X -valued finite countable Element of bool [:(bool X),(bool X):]
[:(bool X),(bool X):] is non empty Relation-like finite countable set
bool [:(bool X),(bool X):] is non empty finite V40() countable set
[:(X),(X):] is non empty Relation-like finite countable set
bool [:(X),(X):] is non empty finite V40() countable set
{ [b₁,b₂] where b₁, b₂ is Element of (X) : (X,b₂,b₁) } is set
((X,F),(X)) is Relation-like bool X -defined bool X -valued finite countable Element of bool (X,F)
bool (X,F) is non empty finite V40() countable set
{ b₁ where b₁ is Element of bool X : [b₁,X] in (X,(X,F)) } is set
K is finite countable Element of bool X
{ b₁ where b₁ is finite countable Element of bool X : (X,K,b₁) in (X,F) } is set
S is set
ck is finite countable Element of bool X
(X,K,ck) is V21() Element of (X)
{K,ck} is non empty finite V40() countable set
{K} is non empty trivial finite V40() 1 -element countable set
{{K,ck},{K}} is non empty finite V40() countable set
{ b₁ where b₁ is finite countable Element of bool X : for b₂, b₃ being finite countable Element of bool X holds
( not (X,b₂,b₃) in F or not b₂ c= b₁ or b₃ c= b₁ ) } is set
(X,K,K) is V21() Element of (X)
{K,K} is non empty finite V40() countable set
{K} is non empty trivial finite V40() 1 -element countable set
{{K,K},{K}} is non empty finite V40() countable set
S is finite V40() countable Element of bool (bool X)
m is set
(X,F) is finite V40() countable Element of bool (bool X)
(X, { b₁ where b₁ is finite countable Element of bool X : for b₂, b₃ being finite countable Element of bool X holds
( not (X,b₂,b₃) in F or not b₂ c= b₁ or b₃ c= b₁ ) } ) is Relation-like bool X -defined bool X -valued finite countable Element of bool [:(bool X),(bool X):]
{ (X,b₁,b₂) where b₁, b₂ is Element of bool X : for b₃ being set holds
( not b₃ in { b₁ where b₄ is finite countable Element of bool X : for b₅, b₆ being finite countable Element of bool X holds
( not (X,b₂,b₃) in F or not b₂ c= b₁ or b₃ c= b₁ ) } or not b₁ c= b₃ or b₂ c= b₃ ) } is set
P is finite countable Element of bool X
[P,X] is V21() set
{P,X} is non empty finite V40() countable set
{P} is non empty trivial finite V40() 1 -element countable set
{{P,X},{P}} is non empty finite V40() countable set
[#] X is non empty non proper finite countable Element of bool X
(X,P,([#] X)) is V21() Element of (X)
{P,([#] X)} is non empty finite V40() countable set
{{P,([#] X)},{P}} is non empty finite V40() countable set
x9 is finite countable Element of bool X
y9 is finite countable Element of bool X
(X,x9,y9) is V21() Element of (X)
{x9,y9} is non empty finite V40() countable set
{x9} is non empty trivial finite V40() 1 -element countable set
{{x9,y9},{x9}} is non empty finite V40() countable set
a is finite countable Element of bool X
(X,F) is set
{ b₁ where b₁ is Element of bool X : ex b₂, b₃ being Element of bool X st
( (X,b₂,b₃) in F & b₂ c= b₁ & not b₃ c= b₁ ) } is set
k is finite countable Element of bool X
S is finite countable Element of bool X
(X,k,S) is V21() Element of (X)
{k,S} is non empty finite V40() countable set
{k} is non empty trivial finite V40() 1 -element countable set
{{k,S},{k}} is non empty finite V40() countable set
a is set
k is finite countable Element of bool X
{ b₁ where b₁ is finite countable Element of bool X : (X,k,b₁) in (X,F) } is set
S is set
m is finite countable Element of bool X
(X,k,m) is V21() Element of (X)
{k,m} is non empty finite V40() countable set
{k} is non empty trivial finite V40() 1 -element countable set
{{k,m},{k}} is non empty finite V40() countable set
(X,k,k) is V21() Element of (X)
{k,k} is non empty finite V40() countable set
{k} is non empty trivial finite V40() 1 -element countable set
{{k,k},{k}} is non empty finite V40() countable set
S is finite V40() countable Element of bool (bool X)
m is set
P is finite countable Element of bool X
(X,k,P) is V21() Element of (X)
{k,P} is non empty finite V40() countable set
{{k,P},{k}} is non empty finite V40() countable set
k \/ k is finite countable Element of bool X
k \/ P is finite countable Element of bool X
(X,(k \/ k),(k \/ P)) is V21() Element of (X)
{(k \/ k),(k \/ P)} is non empty finite V40() countable set
{(k \/ k)} is non empty trivial finite V40() 1 -element countable set
{{(k \/ k),(k \/ P)},{(k \/ k)}} is non empty finite V40() countable set
(X,k,([#] X)) is V21() Element of (X)
{k,([#] X)} is non empty finite V40() countable set
{{k,([#] X)},{k}} is non empty finite V40() countable set
(X,(X,F)) is set
{ b₁ where b₁ is Element of bool X : ex b₂, b₃ being Element of bool X st
( (X,b₂,b₃) in (X,F) & b₂ c= b₁ & not b₃ c= b₁ ) } is set
x is finite countable Element of bool X
y is finite countable Element of bool X
(X,x,y) is V21() Element of (X)
{x,y} is non empty finite V40() countable set
{x} is non empty trivial finite V40() 1 -element countable set
{{x,y},{x}} is non empty finite V40() countable set
(X,(k \/ P),(k \/ P)) is V21() Element of (X)
{(k \/ P),(k \/ P)} is non empty finite V40() countable set
{(k \/ P)} is non empty trivial finite V40() 1 -element countable set
{{(k \/ P),(k \/ P)},{(k \/ P)}} is non empty finite V40() countable set
x \/ (k \/ P) is finite countable Element of bool X
y \/ (k \/ P) is finite countable Element of bool X
(X,(x \/ (k \/ P)),(y \/ (k \/ P))) is V21() Element of (X)
{(x \/ (k \/ P)),(y \/ (k \/ P))} is non empty finite V40() countable set
{(x \/ (k \/ P))} is non empty trivial finite V40() 1 -element countable set
{{(x \/ (k \/ P)),(y \/ (k \/ P))},{(x \/ (k \/ P))}} is non empty finite V40() countable set
(X,(k \/ P),(y \/ (k \/ P))) is V21() Element of (X)
{(k \/ P),(y \/ (k \/ P))} is non empty finite V40() countable set
{{(k \/ P),(y \/ (k \/ P))},{(k \/ P)}} is non empty finite V40() countable set
(X,k,(y \/ (k \/ P))) is V21() Element of (X)
{k,(y \/ (k \/ P))} is non empty finite V40() countable set
{{k,(y \/ (k \/ P))},{k}} is non empty finite V40() countable set
(X,K,([#] X)) is V21() Element of (X)
{K,([#] X)} is non empty finite V40() countable set
{{K,([#] X)},{K}} is non empty finite V40() countable set
P is finite countable Element of bool X
(X,K,P) is V21() Element of (X)
{K,P} is non empty finite V40() countable set
{{K,P},{K}} is non empty finite V40() countable set
K \/ K is finite countable Element of bool X
K \/ P is finite countable Element of bool X
(X,(K \/ K),(K \/ P)) is V21() Element of (X)
{(K \/ K),(K \/ P)} is non empty finite V40() countable set
{(K \/ K)} is non empty trivial finite V40() 1 -element countable set
{{(K \/ K),(K \/ P)},{(K \/ K)}} is non empty finite V40() countable set
(X,K,([#] X)) is V21() Element of (X)
{K,([#] X)} is non empty finite V40() countable set
{{K,([#] X)},{K}} is non empty finite V40() countable set
(X,F) is set
{ b₁ where b₁ is Element of bool X : ex b₂, b₃ being Element of bool X st
( (X,b₂,b₃) in F & b₂ c= b₁ & not b₃ c= b₁ ) } is set
(X,(X,F)) is set
{ b₁ where b₁ is Element of bool X : ex b₂, b₃ being Element of bool X st
( (X,b₂,b₃) in (X,F) & b₂ c= b₁ & not b₃ c= b₁ ) } is set
x9 is finite countable Element of bool X
y9 is finite countable Element of bool X
(X,x9,y9) is V21() Element of (X)
{x9,y9} is non empty finite V40() countable set
{x9} is non empty trivial finite V40() 1 -element countable set
{{x9,y9},{x9}} is non empty finite V40() countable set
(X,(K \/ P),(K \/ P)) is V21() Element of (X)
{(K \/ P),(K \/ P)} is non empty finite V40() countable set
{(K \/ P)} is non empty trivial finite V40() 1 -element countable set
{{(K \/ P),(K \/ P)},{(K \/ P)}} is non empty finite V40() countable set
x9 \/ (K \/ P) is finite countable Element of bool X
y9 \/ (K \/ P) is finite countable Element of bool X
(X,(x9 \/ (K \/ P)),(y9 \/ (K \/ P))) is V21() Element of (X)
{(x9 \/ (K \/ P)),(y9 \/ (K \/ P))} is non empty finite V40() countable set
{(x9 \/ (K \/ P))} is non empty trivial finite V40() 1 -element countable set
{{(x9 \/ (K \/ P)),(y9 \/ (K \/ P))},{(x9 \/ (K \/ P))}} is non empty finite V40() countable set
(X,(K \/ P),(y9 \/ (K \/ P))) is V21() Element of (X)
{(K \/ P),(y9 \/ (K \/ P))} is non empty finite V40() countable set
{{(K \/ P),(y9 \/ (K \/ P))},{(K \/ P)}} is non empty finite V40() countable set
(X,K,(y9 \/ (K \/ P))) is V21() Element of (X)
{K,(y9 \/ (K \/ P))} is non empty finite V40() countable set
{{K,(y9 \/ (K \/ P))},{K}} is non empty finite V40() countable set
x9 is finite countable Element of bool X
y9 is finite countable Element of bool X
(X,x9,y9) is V21() Element of (X)
{x9,y9} is non empty finite V40() countable set
{x9} is non empty trivial finite V40() 1 -element countable set
{{x9,y9},{x9}} is non empty finite V40() countable set
(X,F) is set
{ b₁ where b₁ is Element of bool X : ex b₂, b₃ being Element of bool X st
( (X,b₂,b₃) in F & b₂ c= b₁ & not b₃ c= b₁ ) } is set
a is finite countable Element of bool X
(X,(X,F)) is set
{ b₁ where b₁ is Element of bool X : ex b₂, b₃ being Element of bool X st
( (X,b₂,b₃) in (X,F) & b₂ c= b₁ & not b₃ c= b₁ ) } is set
[K,X] is V21() set
{K,X} is non empty finite V40() countable set
{{K,X},{K}} is non empty finite V40() countable set