:: MMLQUERY semantic presentation

REAL is set
NAT is non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal Element of bool REAL
bool REAL is non empty set
omega is non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal set
bool omega is non empty non trivial non finite set
bool NAT is non empty non trivial non finite set
[:NAT,REAL:] is set
bool [:NAT,REAL:] is non empty set
bool (bool REAL) is non empty set
{} is set
the empty functional epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural finite V37() cardinal {} -element FinSequence-membered ext-real non positive non negative V67() set is empty functional epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural finite V37() cardinal {} -element FinSequence-membered ext-real non positive non negative V67() set
1 is non empty epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() Element of NAT
2 is non empty epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() Element of NAT
3 is non empty epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() Element of NAT
dom {} is set
rng {} is set
0 is epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() Element of NAT
X is Relation-like set
A is Relation-like set
c1 is set
Im (X,c1) is set
{c1} is non empty trivial finite 1 -element set
X .: {c1} is set
Im (A,c1) is set
A .: {c1} is set
c2 is set
z is set
[z,c2] is set
{z,c2} is finite set
{z} is non empty trivial finite 1 -element set
{{z,c2},{z}} is finite V37() set
c1 is set
c2 is set
[c1,c2] is set
{c1,c2} is finite set
{c1} is non empty trivial finite 1 -element set
{{c1,c2},{c1}} is finite V37() set
Im (X,c1) is set
X .: {c1} is set
Im (A,c1) is set
A .: {c1} is set
X is set
[:X,X:] is set
bool [:X,X:] is non empty set
X is set
[:X,X:] is set
bool [:X,X:] is non empty set
A is Relation-like X -defined X -valued Element of bool [:X,X:]
c1 is Element of X
Im (A,c1) is set
{c1} is non empty trivial finite 1 -element set
A .: {c1} is set
bool X is non empty set
A .: {c1} is Element of bool X
X is set
[:X,X:] is set
bool [:X,X:] is non empty set
A is Element of X
c1 is Relation-like X -defined X -valued Element of bool [:X,X:]
(X,c1,A) is Element of bool X
bool X is non empty set
{A} is non empty trivial finite 1 -element set
c1 .: {A} is set
c2 is Element of X
[A,c2] is set
{A,c2} is finite set
{{A,c2},{A}} is finite V37() set
X is set
[:X,X:] is set
bool [:X,X:] is non empty set
bool X is non empty set
X is set
[:X,X:] is set
bool [:X,X:] is non empty set
bool X is non empty set
A is Relation-like X -defined X -valued Element of bool [:X,X:]
c1 is Element of bool X
A .: c1 is set
A .: c1 is Element of bool X
{ (X,A,b₁) where b₁ is Element of X : b₁ in c1 } is set
union { (X,A,b₁) where b₁ is Element of X : b₁ in c1 } is set
c2 is set
z is set
x is Element of X
(X,A,x) is Element of bool X
{x} is non empty trivial finite 1 -element set
A .: {x} is set
[x,c2] is set
{x,c2} is finite set
{{x,c2},{x}} is finite V37() set
c2 is set
z is set
[z,c2] is set
{z,c2} is finite set
{z} is non empty trivial finite 1 -element set
{{z,c2},{z}} is finite V37() set
x is Element of X
(X,A,x) is Element of bool X
{x} is non empty trivial finite 1 -element set
A .: {x} is set
c2 is Element of bool X
z is Element of bool X
meet { (X,A,b₁) where b₁ is Element of X : b₁ in c1 } is set
c2 is set
z is set
x is Element of X
(X,A,x) is Element of bool X
{x} is non empty trivial finite 1 -element set
A .: {x} is set
{ b₁ where b₁ is Element of X : ex b₂ being Element of X st
( (b₁,b₂,A) & b₁ in c1 ) } is set
c2 is set
z is Element of X
x is Element of X
c2 is Relation-like X -defined X -valued Element of bool [:X,X:]
{ b₁ where b₁ is Element of X : ( card (X,A,b₁) = card (X,c2,b₁) & b₁ in c1 ) } is set
z is set
x is Element of X
(X,A,x) is Element of bool X
{x} is non empty trivial finite 1 -element set
A .: {x} is set
card (X,A,x) is epsilon-transitive epsilon-connected ordinal cardinal set
(X,c2,x) is Element of bool X
c2 .: {x} is set
card (X,c2,x) is epsilon-transitive epsilon-connected ordinal cardinal set
{ b₁ where b₁ is Element of X : ( card (X,A,b₁) c= card (X,c2,b₁) & b₁ in c1 ) } is set
z is set
x is Element of X
(X,A,x) is Element of bool X
{x} is non empty trivial finite 1 -element set
A .: {x} is set
card (X,A,x) is epsilon-transitive epsilon-connected ordinal cardinal set
(X,c2,x) is Element of bool X
c2 .: {x} is set
card (X,c2,x) is epsilon-transitive epsilon-connected ordinal cardinal set
{ b₁ where b₁ is Element of X : ( card (X,c2,b₁) c= card (X,A,b₁) & b₁ in c1 ) } is set
z is set
x is Element of X
(X,c2,x) is Element of bool X
{x} is non empty trivial finite 1 -element set
c2 .: {x} is set
card (X,c2,x) is epsilon-transitive epsilon-connected ordinal cardinal set
(X,A,x) is Element of bool X
A .: {x} is set
card (X,A,x) is epsilon-transitive epsilon-connected ordinal cardinal set
{ b₁ where b₁ is Element of X : ( card (X,A,b₁) in card (X,c2,b₁) & b₁ in c1 ) } is set
z is set
x is Element of X
(X,A,x) is Element of bool X
{x} is non empty trivial finite 1 -element set
A .: {x} is set
card (X,A,x) is epsilon-transitive epsilon-connected ordinal cardinal set
(X,c2,x) is Element of bool X
c2 .: {x} is set
card (X,c2,x) is epsilon-transitive epsilon-connected ordinal cardinal set
{ b₁ where b₁ is Element of X : ( card (X,c2,b₁) in card (X,A,b₁) & b₁ in c1 ) } is set
z is set
x is Element of X
(X,c2,x) is Element of bool X
{x} is non empty trivial finite 1 -element set
c2 .: {x} is set
card (X,c2,x) is epsilon-transitive epsilon-connected ordinal cardinal set
(X,A,x) is Element of bool X
A .: {x} is set
card (X,A,x) is epsilon-transitive epsilon-connected ordinal cardinal set
X is set
bool X is non empty set
[:X,X:] is set
bool [:X,X:] is non empty set
c1 is Relation-like X -defined X -valued Element of bool [:X,X:]
c2 is epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() set
A is Element of bool X
{ b₁ where b₁ is Element of X : ( card (X,c1,b₁) = c2 & b₁ in A ) } is set
z is set
x is Element of X
(X,c1,x) is Element of bool X
{x} is non empty trivial finite 1 -element set
c1 .: {x} is set
card (X,c1,x) is epsilon-transitive epsilon-connected ordinal cardinal set
{ b₁ where b₁ is Element of X : ( card (X,c1,b₁) c= c2 & b₁ in A ) } is set
z is set
x is Element of X
(X,c1,x) is Element of bool X
{x} is non empty trivial finite 1 -element set
c1 .: {x} is set
card (X,c1,x) is epsilon-transitive epsilon-connected ordinal cardinal set
{ b₁ where b₁ is Element of X : ( c2 c= card (X,c1,b₁) & b₁ in A ) } is set
z is set
x is Element of X
(X,c1,x) is Element of bool X
{x} is non empty trivial finite 1 -element set
c1 .: {x} is set
card (X,c1,x) is epsilon-transitive epsilon-connected ordinal cardinal set
{ b₁ where b₁ is Element of X : ( card (X,c1,b₁) in c2 & b₁ in A ) } is set
z is set
x is Element of X
(X,c1,x) is Element of bool X
{x} is non empty trivial finite 1 -element set
c1 .: {x} is set
card (X,c1,x) is epsilon-transitive epsilon-connected ordinal cardinal set
{ b₁ where b₁ is Element of X : ( c2 in card (X,c1,b₁) & b₁ in A ) } is set
z is set
x is Element of X
(X,c1,x) is Element of bool X
{x} is non empty trivial finite 1 -element set
c1 .: {x} is set
card (X,c1,x) is epsilon-transitive epsilon-connected ordinal cardinal set
X is set
bool X is non empty set
[:X,X:] is set
bool [:X,X:] is non empty set
A is Element of bool X
c1 is Element of X
c2 is Relation-like X -defined X -valued Element of bool [:X,X:]
(X,c2,A) is Element of bool X
{ b₁ where b₁ is Element of X : ex b₂ being Element of X st
( (b₁,b₂,c2) & b₁ in A ) } is set
(X,c2,c1) is Element of bool X
{c1} is non empty trivial finite 1 -element set
c2 .: {c1} is set
z is Element of X
x is Element of X
the Element of (X,c2,c1) is Element of (X,c2,c1)
x is Element of X
X is set
bool X is non empty set
[:X,X:] is set
bool [:X,X:] is non empty set
A is Element of bool X
c1 is Relation-like X -defined X -valued Element of bool [:X,X:]
(X,c1,A) is Element of bool X
{ b₁ where b₁ is Element of X : ex b₂ being Element of X st
( (b₁,b₂,c1) & b₁ in A ) } is set
c2 is set
X is set
bool X is non empty set
[:X,X:] is set
bool [:X,X:] is non empty set
A is Element of bool X
c1 is Relation-like X -defined X -valued Element of bool [:X,X:]
dom c1 is Element of bool X
(X,c1,A) is Element of bool X
{ b₁ where b₁ is Element of X : ex b₂ being Element of X st
( (b₁,b₂,c1) & b₁ in A ) } is set
c2 is set
z is Element of X
(X,c1,z) is Element of bool X
{z} is non empty trivial finite 1 -element set
c1 .: {z} is set
X is set
bool X is non empty set
[:X,X:] is set
bool [:X,X:] is non empty set
A is Element of bool X
c1 is Element of bool X
c2 is Relation-like X -defined X -valued Element of bool [:X,X:]
(X,c2,c1) is Element of bool X
{ b₁ where b₁ is Element of X : ex b₂ being Element of X st
( (b₁,b₂,c2) & b₁ in c1 ) } is set
z is epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() set
(X,A,c2,z) is Element of bool X
{ b₁ where b₁ is Element of X : ( z c= card (X,c2,b₁) & b₁ in A ) } is set
x is set
s is Element of X
(X,c2,s) is Element of bool X
{s} is non empty trivial finite 1 -element set
c2 .: {s} is set
card (X,c2,s) is epsilon-transitive epsilon-connected ordinal cardinal set
X is set
bool X is non empty set
[:X,X:] is set
bool [:X,X:] is non empty set
A is Element of bool X
c1 is Relation-like X -defined X -valued Element of bool [:X,X:]
(X,A,c1,1) is Element of bool X
{ b₁ where b₁ is Element of X : ( 1 c= card (X,c1,b₁) & b₁ in A ) } is set
(X,c1,A) is Element of bool X
{ b₁ where b₁ is Element of X : ex b₂ being Element of X st
( (b₁,b₂,c1) & b₁ in A ) } is set
c2 is set
z is Element of X
(X,c1,z) is Element of bool X
{z} is non empty trivial finite 1 -element set
c1 .: {z} is set
succ 0 is non empty epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() set
card (X,c1,z) is epsilon-transitive epsilon-connected ordinal cardinal set
X is set
bool X is non empty set
[:X,X:] is set
bool [:X,X:] is non empty set
A is Element of bool X
c1 is Element of bool X
c2 is Relation-like X -defined X -valued Element of bool [:X,X:]
(X,c2,c1) is Element of bool X
{ b₁ where b₁ is Element of X : ex b₂ being Element of X st
( (b₁,b₂,c2) & b₁ in c1 ) } is set
z is epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() set
(X,A,c2,z) is Element of bool X
{ b₁ where b₁ is Element of X : ( z in card (X,c2,b₁) & b₁ in A ) } is set
x is set
s is Element of X
(X,c2,s) is Element of bool X
{s} is non empty trivial finite 1 -element set
c2 .: {s} is set
card (X,c2,s) is epsilon-transitive epsilon-connected ordinal cardinal set
X is set
bool X is non empty set
[:X,X:] is set
bool [:X,X:] is non empty set
A is Element of bool X
c1 is Relation-like X -defined X -valued Element of bool [:X,X:]
(X,A,c1,0) is Element of bool X
{ b₁ where b₁ is Element of X : ( 0 in card (X,c1,b₁) & b₁ in A ) } is set
(X,c1,A) is Element of bool X
{ b₁ where b₁ is Element of X : ex b₂ being Element of X st
( (b₁,b₂,c1) & b₁ in A ) } is set
c2 is set
z is Element of X
(X,c1,z) is Element of bool X
{z} is non empty trivial finite 1 -element set
c1 .: {z} is set
card (X,c1,z) is epsilon-transitive epsilon-connected ordinal cardinal set
X is set
bool X is non empty set
[:X,X:] is set
bool [:X,X:] is non empty set
A is Element of bool X
c1 is Element of bool X
c2 is Relation-like X -defined X -valued Element of bool [:X,X:]
(X,c2,c1) is Element of bool X
{ b₁ where b₁ is Element of X : ex b₂ being Element of X st
( (b₁,b₂,c2) & b₁ in c1 ) } is set
z is epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() set
(X,A,c2,z) is Element of bool X
{ b₁ where b₁ is Element of X : ( card (X,c2,b₁) = z & b₁ in A ) } is set
x is set
s is Element of X
(X,c2,s) is Element of bool X
{s} is non empty trivial finite 1 -element set
c2 .: {s} is set
card (X,c2,s) is epsilon-transitive epsilon-connected ordinal cardinal set
X is set
bool X is non empty set
[:X,X:] is set
bool [:X,X:] is non empty set
A is Element of bool X
c1 is Relation-like X -defined X -valued Element of bool [:X,X:]
c2 is epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() set
c2 + 1 is epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() Element of NAT
(X,A,c1,(c2 + 1)) is Element of bool X
{ b₁ where b₁ is Element of X : ( c2 + 1 c= card (X,c1,b₁) & b₁ in A ) } is set
(X,A,c1,c2) is Element of bool X
{ b₁ where b₁ is Element of X : ( c2 in card (X,c1,b₁) & b₁ in A ) } is set
z is set
x is Element of X
(X,c1,x) is Element of bool X
{x} is non empty trivial finite 1 -element set
c1 .: {x} is set
card (X,c1,x) is epsilon-transitive epsilon-connected ordinal cardinal set
succ c2 is non empty epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() set
z is set
x is Element of X
(X,c1,x) is Element of bool X
{x} is non empty trivial finite 1 -element set
c1 .: {x} is set
card (X,c1,x) is epsilon-transitive epsilon-connected ordinal cardinal set
succ c2 is non empty epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() set
X is set
bool X is non empty set
[:X,X:] is set
bool [:X,X:] is non empty set
A is Element of bool X
c1 is Relation-like X -defined X -valued Element of bool [:X,X:]
c2 is epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() set
(X,A,c1,c2) is Element of bool X
{ b₁ where b₁ is Element of X : ( card (X,c1,b₁) c= c2 & b₁ in A ) } is set
c2 + 1 is epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() Element of NAT
(X,A,c1,(c2 + 1)) is Element of bool X
{ b₁ where b₁ is Element of X : ( card (X,c1,b₁) in c2 + 1 & b₁ in A ) } is set
z is set
x is Element of X
(X,c1,x) is Element of bool X
{x} is non empty trivial finite 1 -element set
c1 .: {x} is set
card (X,c1,x) is epsilon-transitive epsilon-connected ordinal cardinal set
succ c2 is non empty epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() set
z is set
x is Element of X
(X,c1,x) is Element of bool X
{x} is non empty trivial finite 1 -element set
c1 .: {x} is set
card (X,c1,x) is epsilon-transitive epsilon-connected ordinal cardinal set
succ c2 is non empty epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() set
X is set
bool X is non empty set
[:X,X:] is set
bool [:X,X:] is non empty set
A is Element of bool X
c1 is Element of bool X
c2 is Relation-like X -defined X -valued Element of bool [:X,X:]
z is Relation-like X -defined X -valued Element of bool [:X,X:]
x is epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() set
(X,c1,z,x) is Element of bool X
{ b₁ where b₁ is Element of X : ( x c= card (X,z,b₁) & b₁ in c1 ) } is set
s is epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() set
(X,A,c2,s) is Element of bool X
{ b₁ where b₁ is Element of X : ( s c= card (X,c2,b₁) & b₁ in A ) } is set
s is set
x is Element of X
(X,c2,x) is Element of bool X
{x} is non empty trivial finite 1 -element set
c2 .: {x} is set
card (X,c2,x) is epsilon-transitive epsilon-connected ordinal cardinal set
(X,z,x) is Element of bool X
z .: {x} is set
card (X,z,x) is epsilon-transitive epsilon-connected ordinal cardinal set
X is set
bool X is non empty set
[:X,X:] is set
bool [:X,X:] is non empty set
A is Element of bool X
c1 is Element of bool X
c2 is Relation-like X -defined X -valued Element of bool [:X,X:]
z is Relation-like X -defined X -valued Element of bool [:X,X:]
x is epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() set
(X,c1,z,x) is Element of bool X
{ b₁ where b₁ is Element of X : ( x in card (X,z,b₁) & b₁ in c1 ) } is set
s is epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() set
(X,A,c2,s) is Element of bool X
{ b₁ where b₁ is Element of X : ( s in card (X,c2,b₁) & b₁ in A ) } is set
s is set
x is Element of X
(X,c2,x) is Element of bool X
{x} is non empty trivial finite 1 -element set
c2 .: {x} is set
card (X,c2,x) is epsilon-transitive epsilon-connected ordinal cardinal set
(X,z,x) is Element of bool X
z .: {x} is set
card (X,z,x) is epsilon-transitive epsilon-connected ordinal cardinal set
X is set
bool X is non empty set
[:X,X:] is set
bool [:X,X:] is non empty set
A is Element of bool X
c1 is Element of bool X
c2 is Relation-like X -defined X -valued Element of bool [:X,X:]
z is Relation-like X -defined X -valued Element of bool [:X,X:]
x is epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() set
(X,A,z,x) is Element of bool X
{ b₁ where b₁ is Element of X : ( card (X,z,b₁) c= x & b₁ in A ) } is set
s is epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() set
(X,c1,c2,s) is Element of bool X
{ b₁ where b₁ is Element of X : ( card (X,c2,b₁) c= s & b₁ in c1 ) } is set
s is set
x is Element of X
(X,z,x) is Element of bool X
{x} is non empty trivial finite 1 -element set
z .: {x} is set
card (X,z,x) is epsilon-transitive epsilon-connected ordinal cardinal set
(X,c2,x) is Element of bool X
c2 .: {x} is set
card (X,c2,x) is epsilon-transitive epsilon-connected ordinal cardinal set
X is set
bool X is non empty set
[:X,X:] is set
bool [:X,X:] is non empty set
A is Element of bool X
c1 is Element of bool X
c2 is Relation-like X -defined X -valued Element of bool [:X,X:]
z is Relation-like X -defined X -valued Element of bool [:X,X:]
x is epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() set
(X,A,z,x) is Element of bool X
{ b₁ where b₁ is Element of X : ( card (X,z,b₁) in x & b₁ in A ) } is set
s is epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() set
(X,c1,c2,s) is Element of bool X
{ b₁ where b₁ is Element of X : ( card (X,c2,b₁) in s & b₁ in c1 ) } is set
s is set
x is Element of X
(X,z,x) is Element of bool X
{x} is non empty trivial finite 1 -element set
z .: {x} is set
card (X,z,x) is epsilon-transitive epsilon-connected ordinal cardinal set
(X,c2,x) is Element of bool X
c2 .: {x} is set
card (X,c2,x) is epsilon-transitive epsilon-connected ordinal cardinal set
X is set
bool X is non empty set
[:X,X:] is set
bool [:X,X:] is non empty set
A is Element of bool X
c1 is Element of bool X
c2 is Relation-like X -defined X -valued Element of bool [:X,X:]
z is Relation-like X -defined X -valued Element of bool [:X,X:]
x is Relation-like X -defined X -valued Element of bool [:X,X:]
(X,x,A,z) is Element of bool X
{ b₁ where b₁ is Element of X : ( card (X,z,b₁) c= card (X,x,b₁) & b₁ in A ) } is set
s is Relation-like X -defined X -valued Element of bool [:X,X:]
(X,s,c1,c2) is Element of bool X
{ b₁ where b₁ is Element of X : ( card (X,c2,b₁) c= card (X,s,b₁) & b₁ in c1 ) } is set
s is set
x is Element of X
(X,z,x) is Element of bool X
{x} is non empty trivial finite 1 -element set
z .: {x} is set
card (X,z,x) is epsilon-transitive epsilon-connected ordinal cardinal set
(X,x,x) is Element of bool X
x .: {x} is set
card (X,x,x) is epsilon-transitive epsilon-connected ordinal cardinal set
(X,c2,x) is Element of bool X
c2 .: {x} is set
card (X,c2,x) is epsilon-transitive epsilon-connected ordinal cardinal set
(X,s,x) is Element of bool X
s .: {x} is set
card (X,s,x) is epsilon-transitive epsilon-connected ordinal cardinal set
X is set
bool X is non empty set
[:X,X:] is set
bool [:X,X:] is non empty set
A is Element of bool X
c1 is Element of bool X
c2 is Relation-like X -defined X -valued Element of bool [:X,X:]
z is Relation-like X -defined X -valued Element of bool [:X,X:]
x is Relation-like X -defined X -valued Element of bool [:X,X:]
(X,x,A,z) is Element of bool X
{ b₁ where b₁ is Element of X : ( card (X,z,b₁) in card (X,x,b₁) & b₁ in A ) } is set
s is Relation-like X -defined X -valued Element of bool [:X,X:]
(X,s,c1,c2) is Element of bool X
{ b₁ where b₁ is Element of X : ( card (X,c2,b₁) in card (X,s,b₁) & b₁ in c1 ) } is set
s is set
x is Element of X
(X,z,x) is Element of bool X
{x} is non empty trivial finite 1 -element set
z .: {x} is set
card (X,z,x) is epsilon-transitive epsilon-connected ordinal cardinal set
(X,x,x) is Element of bool X
x .: {x} is set
card (X,x,x) is epsilon-transitive epsilon-connected ordinal cardinal set
(X,c2,x) is Element of bool X
c2 .: {x} is set
(X,s,x) is Element of bool X
s .: {x} is set
card (X,c2,x) is epsilon-transitive epsilon-connected ordinal cardinal set
card (X,s,x) is epsilon-transitive epsilon-connected ordinal cardinal set
X is set
bool X is non empty set
[:X,X:] is set
bool [:X,X:] is non empty set
A is Element of bool X
c1 is Element of bool X
c2 is Relation-like X -defined X -valued Element of bool [:X,X:]
z is Relation-like X -defined X -valued Element of bool [:X,X:]
x is Relation-like X -defined X -valued Element of bool [:X,X:]
(X,x,c1,z) is Element of bool X
{ b₁ where b₁ is Element of X : ( card (X,x,b₁) c= card (X,z,b₁) & b₁ in c1 ) } is set
s is Relation-like X -defined X -valued Element of bool [:X,X:]
(X,s,A,c2) is Element of bool X
{ b₁ where b₁ is Element of X : ( card (X,s,b₁) c= card (X,c2,b₁) & b₁ in A ) } is set
s is set
x is Element of X
(X,s,x) is Element of bool X
{x} is non empty trivial finite 1 -element set
s .: {x} is set
card (X,s,x) is epsilon-transitive epsilon-connected ordinal cardinal set
(X,c2,x) is Element of bool X
c2 .: {x} is set
card (X,c2,x) is epsilon-transitive epsilon-connected ordinal cardinal set
(X,z,x) is Element of bool X
z .: {x} is set
card (X,z,x) is epsilon-transitive epsilon-connected ordinal cardinal set
(X,x,x) is Element of bool X
x .: {x} is set
card (X,x,x) is epsilon-transitive epsilon-connected ordinal cardinal set
X is set
bool X is non empty set
[:X,X:] is set
bool [:X,X:] is non empty set
A is Element of bool X
c1 is Element of bool X
c2 is Relation-like X -defined X -valued Element of bool [:X,X:]
z is Relation-like X -defined X -valued Element of bool [:X,X:]
x is Relation-like X -defined X -valued Element of bool [:X,X:]
(X,x,c1,z) is Element of bool X
{ b₁ where b₁ is Element of X : ( card (X,x,b₁) in card (X,z,b₁) & b₁ in c1 ) } is set
s is Relation-like X -defined X -valued Element of bool [:X,X:]
(X,s,A,c2) is Element of bool X
{ b₁ where b₁ is Element of X : ( card (X,s,b₁) in card (X,c2,b₁) & b₁ in A ) } is set
s is set
x is Element of X
(X,s,x) is Element of bool X
{x} is non empty trivial finite 1 -element set
s .: {x} is set
card (X,s,x) is epsilon-transitive epsilon-connected ordinal cardinal set
(X,c2,x) is Element of bool X
c2 .: {x} is set
card (X,c2,x) is epsilon-transitive epsilon-connected ordinal cardinal set
(X,z,x) is Element of bool X
z .: {x} is set
card (X,z,x) is epsilon-transitive epsilon-connected ordinal cardinal set
(X,x,x) is Element of bool X
x .: {x} is set
card (X,x,x) is epsilon-transitive epsilon-connected ordinal cardinal set
X is set
bool X is non empty set
[:X,X:] is set
bool [:X,X:] is non empty set
A is Element of bool X
c1 is Relation-like X -defined X -valued Element of bool [:X,X:]
(X,c1,A) is Element of bool X
{ b₁ where b₁ is Element of X : ex b₂ being Element of X st
( (b₁,b₂,c1) & b₁ in A ) } is set
c2 is Relation-like X -defined X -valued Element of bool [:X,X:]
(X,c1,A,c2) is Element of bool X
{ b₁ where b₁ is Element of X : ( card (X,c2,b₁) in card (X,c1,b₁) & b₁ in A ) } is set
z is set
x is Element of X
(X,c2,x) is Element of bool X
{x} is non empty trivial finite 1 -element set
c2 .: {x} is set
card (X,c2,x) is epsilon-transitive epsilon-connected ordinal cardinal set
(X,c1,x) is Element of bool X
c1 .: {x} is set
card (X,c1,x) is epsilon-transitive epsilon-connected ordinal cardinal set
X is set
bool X is non empty set
[:X,X:] is set
bool [:X,X:] is non empty set
A is Element of bool X
c1 is Element of bool X
c2 is Relation-like X -defined X -valued Element of bool [:X,X:]
(X,c2,A) is Element of bool X
{ b₁ where b₁ is Element of X : ex b₂ being Element of X st
( (b₁,b₂,c2) & b₁ in A ) } is set
z is Relation-like X -defined X -valued Element of bool [:X,X:]
(X,z,c1) is Element of bool X
{ b₁ where b₁ is Element of X : ex b₂ being Element of X st
( (b₁,b₂,z) & b₁ in c1 ) } is set
x is set
s is Element of X
(X,c2,s) is Element of bool X
{s} is non empty trivial finite 1 -element set
c2 .: {s} is set
(X,z,s) is Element of bool X
z .: {s} is set
X is set
bool X is non empty set
[:X,X:] is set
bool [:X,X:] is non empty set
A is Element of bool X
c1 is Relation-like X -defined X -valued Element of bool [:X,X:]
(X,c1,A) is Element of bool X
{ (X,c1,b₁) where b₁ is Element of X : b₁ in A } is set
union { (X,c1,b₁) where b₁ is Element of X : b₁ in A } is set
c2 is Element of X
z is set
[z,c2] is set
{z,c2} is finite set
{z} is non empty trivial finite 1 -element set
{{z,c2},{z}} is finite V37() set
x is Element of X
s is Element of X
(X,c1,s) is Element of bool X
{s} is non empty trivial finite 1 -element set
c1 .: {s} is set
z is Element of X
(X,c1,z) is Element of bool X
{z} is non empty trivial finite 1 -element set
c1 .: {z} is set
[z,c2] is set
{z,c2} is finite set
{{z,c2},{z}} is finite V37() set
X is set
bool X is non empty set
X is set
bool X is non empty set
A is Element of bool X
c1 is Element of bool X
A /\ c1 is set
A /\ c1 is Element of bool X
A \/ c1 is set
A \/ c1 is Element of bool X
A \ c1 is set
A \ c1 is Element of bool X
X is set
bool X is non empty set
[:X,X:] is set
bool [:X,X:] is non empty set
A is Element of bool X
c1 is Element of bool X
(X,A,c1) is Element of bool X
c2 is Relation-like X -defined X -valued Element of bool [:X,X:]
(X,c2,(X,A,c1)) is Element of bool X
{ (X,c2,b₁) where b₁ is Element of X : b₁ in (X,A,c1) } is set
meet { (X,c2,b₁) where b₁ is Element of X : b₁ in (X,A,c1) } is set
(X,c2,A) is Element of bool X
{ (X,c2,b₁) where b₁ is Element of X : b₁ in A } is set
meet { (X,c2,b₁) where b₁ is Element of X : b₁ in A } is set
(X,c2,c1) is Element of bool X
{ (X,c2,b₁) where b₁ is Element of X : b₁ in c1 } is set
meet { (X,c2,b₁) where b₁ is Element of X : b₁ in c1 } is set
(X,(X,c2,A),(X,c2,c1)) is Element of bool X
z is set
the Element of A is Element of A
s is Element of X
(X,c2,s) is Element of bool X
{s} is non empty trivial finite 1 -element set
c2 .: {s} is set
s is set
x is Element of X
(X,c2,x) is Element of bool X
{x} is non empty trivial finite 1 -element set
c2 .: {x} is set
the Element of c1 is Element of c1
s is Element of X
(X,c2,s) is Element of bool X
{s} is non empty trivial finite 1 -element set
c2 .: {s} is set
s is set
x is Element of X
(X,c2,x) is Element of bool X
{x} is non empty trivial finite 1 -element set
c2 .: {x} is set
z is set
the Element of c1 is Element of c1
s is Element of X
(X,c2,s) is Element of bool X
{s} is non empty trivial finite 1 -element set
c2 .: {s} is set
s is set
x is Element of X
(X,c2,x) is Element of bool X
{x} is non empty trivial finite 1 -element set
c2 .: {x} is set
X is set
bool X is non empty set
[:X,X:] is set
bool [:X,X:] is non empty set
A is Element of bool X
c1 is Element of bool X
c2 is Relation-like X -defined X -valued Element of bool [:X,X:]
(X,c2,A) is Element of bool X
{ (X,c2,b₁) where b₁ is Element of X : b₁ in A } is set
union { (X,c2,b₁) where b₁ is Element of X : b₁ in A } is set
z is Relation-like X -defined X -valued Element of bool [:X,X:]
(X,z,c1) is Element of bool X
{ (X,z,b₁) where b₁ is Element of X : b₁ in c1 } is set
union { (X,z,b₁) where b₁ is Element of X : b₁ in c1 } is set
(X,c2,c1) is Element of bool X
{ (X,c2,b₁) where b₁ is Element of X : b₁ in c1 } is set
union { (X,c2,b₁) where b₁ is Element of X : b₁ in c1 } is set
X is set
bool X is non empty set
[:X,X:] is set
bool [:X,X:] is non empty set
A is Element of bool X
c1 is Relation-like X -defined X -valued Element of bool [:X,X:]
(X,c1,A) is Element of bool X
{ (X,c1,b₁) where b₁ is Element of X : b₁ in A } is set
meet { (X,c1,b₁) where b₁ is Element of X : b₁ in A } is set
c2 is Relation-like X -defined X -valued Element of bool [:X,X:]
(X,c2,A) is Element of bool X
{ (X,c2,b₁) where b₁ is Element of X : b₁ in A } is set
meet { (X,c2,b₁) where b₁ is Element of X : b₁ in A } is set
z is set
x is set
s is Element of X
(X,c1,s) is Element of bool X
{s} is non empty trivial finite 1 -element set
c1 .: {s} is set
(X,c2,s) is Element of bool X
c2 .: {s} is set
s is set
x is Element of X
(X,c2,x) is Element of bool X
{x} is non empty trivial finite 1 -element set
c2 .: {x} is set
(X,c1,x) is Element of bool X
c1 .: {x} is set
X is set
bool X is non empty set
[:X,X:] is set
bool [:X,X:] is non empty set
A is Element of bool X
c1 is Relation-like X -defined X -valued Element of bool [:X,X:]
(X,c1,A) is Element of bool X
{ (X,c1,b₁) where b₁ is Element of X : b₁ in A } is set
meet { (X,c1,b₁) where b₁ is Element of X : b₁ in A } is set
c2 is Relation-like X -defined X -valued Element of bool [:X,X:]
([:X,X:],c1,c2) is Relation-like X -defined X -valued Element of bool [:X,X:]
(X,([:X,X:],c1,c2),A) is Element of bool X
{ (X,([:X,X:],c1,c2),b₁) where b₁ is Element of X : b₁ in A } is set
meet { (X,([:X,X:],c1,c2),b₁) where b₁ is Element of X : b₁ in A } is set
(X,c2,A) is Element of bool X
{ (X,c2,b₁) where b₁ is Element of X : b₁ in A } is set
meet { (X,c2,b₁) where b₁ is Element of X : b₁ in A } is set
(X,(X,c1,A),(X,c2,A)) is Element of bool X
z is set
the Element of A is Element of A
s is set
x is Element of X
(X,c1,x) is Element of bool X
{x} is non empty trivial finite 1 -element set
c1 .: {x} is set
(X,([:X,X:],c1,c2),x) is Element of bool X
([:X,X:],c1,c2) .: {x} is set
Y is set
x is Element of X
(X,([:X,X:],c1,c2),x) is Element of bool X
{x} is non empty trivial finite 1 -element set
([:X,X:],c1,c2) .: {x} is set
(X,c1,x) is Element of bool X
c1 .: {x} is set
(X,c2,x) is Element of bool X
c2 .: {x} is set
(X,(X,c1,x),(X,c2,x)) is Element of bool X
X is set
bool X is non empty set
[:X,X:] is set
bool [:X,X:] is non empty set
A is Element of bool X
c1 is Element of bool X
c2 is Relation-like X -defined X -valued Element of bool [:X,X:]
(X,c2,c1) is Element of bool X
{ (X,c2,b₁) where b₁ is Element of X : b₁ in c1 } is set
meet { (X,c2,b₁) where b₁ is Element of X : b₁ in c1 } is set
(X,c2,A) is Element of bool X
{ (X,c2,b₁) where b₁ is Element of X : b₁ in A } is set
meet { (X,c2,b₁) where b₁ is Element of X : b₁ in A } is set
z is set
the Element of A is Element of A
s is Element of X
(X,c2,s) is Element of bool X
{s} is non empty trivial finite 1 -element set
c2 .: {s} is set
s is set
x is Element of X
(X,c2,x) is Element of bool X
{x} is non empty trivial finite 1 -element set
c2 .: {x} is set
X is set
[:X,X:] is set
bool [:X,X:] is non empty set
A is Relation-like X -defined X -valued Element of bool [:X,X:]
c1 is Relation-like X -defined X -valued Element of bool [:X,X:]
c2 is set
z is set
[c2,z] is set
{c2,z} is finite set
{c2} is non empty trivial finite 1 -element set
{{c2,z},{c2}} is finite V37() set
s is Element of X
x is Element of X
(X,A,x) is Element of bool X
bool X is non empty set
{x} is non empty trivial finite 1 -element set
A .: {x} is set
(X,c1,x) is Element of bool X
c1 .: {x} is set
bool X is non empty set
x is Element of X
{x} is non empty trivial finite 1 -element set
s is Element of X
(X,c1,x) is Element of bool X
c1 .: {x} is set
(X,A,x) is Element of bool X
A .: {x} is set
X is set
[:X,X:] is set
bool [:X,X:] is non empty set
bool X is non empty set
A is Relation-like X -defined X -valued Element of bool [:X,X:]
c1 is Relation-like X -defined X -valued Element of bool [:X,X:]
c2 is Element of X
{c2} is non empty trivial finite 1 -element set
(X,A,c2) is Element of bool X
A .: {c2} is set
z is Element of bool X
(X,A,z) is Element of bool X
{ (X,A,b₁) where b₁ is Element of X : b₁ in z } is set
union { (X,A,b₁) where b₁ is Element of X : b₁ in z } is set
(X,c1,c2) is Element of bool X
c1 .: {c2} is set
c2 is Element of X
(X,A,c2) is Element of bool X
{c2} is non empty trivial finite 1 -element set
A .: {c2} is set
(X,c1,c2) is Element of bool X
c1 .: {c2} is set
X is set
[:X,X:] is set
bool [:X,X:] is non empty set
bool X is non empty set
A is Relation-like X -defined X -valued Element of bool [:X,X:]
c1 is Relation-like set
c2 is set
z is set
[c2,z] is set
{c2,z} is finite set
{c2} is non empty trivial finite 1 -element set
{{c2,z},{c2}} is finite V37() set
c2 is Relation-like X -defined X -valued Element of bool [:X,X:]
z is Element of bool X
(X,c2,z) is Element of bool X
{ (X,c2,b₁) where b₁ is Element of X : b₁ in z } is set
union { (X,c2,b₁) where b₁ is Element of X : b₁ in z } is set
{ (IFEQ ((X,A,b₁),{},{b₁},{})) where b₁ is Element of X : b₁ in z } is set
union { (IFEQ ((X,A,b₁),{},{b₁},{})) where b₁ is Element of X : b₁ in z } is set
x is set
s is Element of X
(X,c2,s) is Element of bool X
{s} is non empty trivial finite 1 -element set
c2 .: {s} is set
[s,x] is set
{s,x} is finite set
{{s,x},{s}} is finite V37() set
(X,A,s) is Element of bool X
A .: {s} is set
IFEQ ((X,A,s),{},{s},{}) is set
x is set
s is set
s is Element of X
(X,A,s) is Element of bool X
{s} is non empty trivial finite 1 -element set
A .: {s} is set
IFEQ ((X,A,s),{},{s},{}) is set
[s,x] is set
{s,x} is finite set
{{s,x},{s}} is finite V37() set
c1 is Relation-like X -defined X -valued Element of bool [:X,X:]
c2 is Relation-like X -defined X -valued Element of bool [:X,X:]
z is Element of bool X
(X,c1,z) is Element of bool X
{ (X,c1,b₁) where b₁ is Element of X : b₁ in z } is set
union { (X,c1,b₁) where b₁ is Element of X : b₁ in z } is set
{ (IFEQ ((X,A,b₁),{},{b₁},{})) where b₁ is Element of X : b₁ in z } is set
union { (IFEQ ((X,A,b₁),{},{b₁},{})) where b₁ is Element of X : b₁ in z } is set
(X,c2,z) is Element of bool X
{ (X,c2,b₁) where b₁ is Element of X : b₁ in z } is set
union { (X,c2,b₁) where b₁ is Element of X : b₁ in z } is set
X is set
[:X,X:] is set
bool [:X,X:] is non empty set
X is set
[:X,X:] is set
bool [:X,X:] is non empty set
A is Relation-like X -defined X -valued Element of bool [:X,X:]
c1 is Relation-like X -defined X -valued Element of bool [:X,X:]
A /\ c1 is X -defined X -valued set
A /\ c1 is Relation-like X -defined X -valued Element of bool [:X,X:]
bool X is non empty set
c2 is Relation-like X -defined X -valued Element of bool [:X,X:]
A /\ c1 is Relation-like X -defined X -valued Element of bool [:X,X:]
z is Element of bool X
(X,c2,z) is Element of bool X
{ (X,c2,b₁) where b₁ is Element of X : b₁ in z } is set
union { (X,c2,b₁) where b₁ is Element of X : b₁ in z } is set
{ (X,(X,A,b₁),(X,c1,b₁)) where b₁ is Element of X : b₁ in z } is set
union { (X,(X,A,b₁),(X,c1,b₁)) where b₁ is Element of X : b₁ in z } is set
x is set
s is set
[s,x] is set
{s,x} is finite set
{s} is non empty trivial finite 1 -element set
{{s,x},{s}} is finite V37() set
s is Element of X
x is Element of X
[s,x] is set
{s,x} is finite set
{s} is non empty trivial finite 1 -element set
{{s,x},{s}} is finite V37() set
(X,A,s) is Element of bool X
A .: {s} is set
(X,c1,s) is Element of bool X
c1 .: {s} is set
(X,(X,A,s),(X,c1,s)) is Element of bool X
x is set
s is set
s is Element of X
(X,A,s) is Element of bool X
{s} is non empty trivial finite 1 -element set
A .: {s} is set
(X,c1,s) is Element of bool X
c1 .: {s} is set
(X,(X,A,s),(X,c1,s)) is Element of bool X
x is Element of X
[s,x] is set
{s,x} is finite set
{{s,x},{s}} is finite V37() set
c2 is Relation-like X -defined X -valued Element of bool [:X,X:]
z is Element of bool X
(X,c2,z) is Element of bool X
{ (X,c2,b₁) where b₁ is Element of X : b₁ in z } is set
union { (X,c2,b₁) where b₁ is Element of X : b₁ in z } is set
{ (X,(X,A,b₁),(X,c1,b₁)) where b₁ is Element of X : b₁ in z } is set
union { (X,(X,A,b₁),(X,c1,b₁)) where b₁ is Element of X : b₁ in z } is set
z is Element of bool X
(X,c2,z) is Element of bool X
{ (X,c2,b₁) where b₁ is Element of X : b₁ in z } is set
union { (X,c2,b₁) where b₁ is Element of X : b₁ in z } is set
{ (X,(X,A,b₁),(X,c1,b₁)) where b₁ is Element of X : b₁ in z } is set
union { (X,(X,A,b₁),(X,c1,b₁)) where b₁ is Element of X : b₁ in z } is set
A /\ c1 is Relation-like X -defined X -valued Element of bool [:X,X:]
(X,(A /\ c1),z) is Element of bool X
{ (X,(A /\ c1),b₁) where b₁ is Element of X : b₁ in z } is set
union { (X,(A /\ c1),b₁) where b₁ is Element of X : b₁ in z } is set
A \/ c1 is X -defined X -valued set
A \/ c1 is Relation-like X -defined X -valued Element of bool [:X,X:]
c2 is Relation-like X -defined X -valued Element of bool [:X,X:]
A \/ c1 is Relation-like X -defined X -valued Element of bool [:X,X:]
z is Element of bool X
(X,c2,z) is Element of bool X
{ (X,c2,b₁) where b₁ is Element of X : b₁ in z } is set
union { (X,c2,b₁) where b₁ is Element of X : b₁ in z } is set
{ (X,(X,A,b₁),(X,c1,b₁)) where b₁ is Element of X : b₁ in z } is set
union { (X,(X,A,b₁),(X,c1,b₁)) where b₁ is Element of X : b₁ in z } is set
x is set
s is set
[s,x] is set
{s,x} is finite set
{s} is non empty trivial finite 1 -element set
{{s,x},{s}} is finite V37() set
s is Element of X
x is Element of X
[s,x] is set
{s,x} is finite set
{s} is non empty trivial finite 1 -element set
{{s,x},{s}} is finite V37() set
(X,A,s) is Element of bool X
A .: {s} is set
(X,c1,s) is Element of bool X
c1 .: {s} is set
(X,(X,A,s),(X,c1,s)) is Element of bool X
x is set
s is set
s is Element of X
(X,A,s) is Element of bool X
{s} is non empty trivial finite 1 -element set
A .: {s} is set
(X,c1,s) is Element of bool X
c1 .: {s} is set
(X,(X,A,s),(X,c1,s)) is Element of bool X
x is Element of X
[s,x] is set
{s,x} is finite set
{{s,x},{s}} is finite V37() set
c2 is Relation-like X -defined X -valued Element of bool [:X,X:]
z is Element of bool X
(X,c2,z) is Element of bool X
{ (X,c2,b₁) where b₁ is Element of X : b₁ in z } is set
union { (X,c2,b₁) where b₁ is Element of X : b₁ in z } is set
{ (X,(X,A,b₁),(X,c1,b₁)) where b₁ is Element of X : b₁ in z } is set
union { (X,(X,A,b₁),(X,c1,b₁)) where b₁ is Element of X : b₁ in z } is set
z is Element of bool X
(X,c2,z) is Element of bool X
{ (X,c2,b₁) where b₁ is Element of X : b₁ in z } is set
union { (X,c2,b₁) where b₁ is Element of X : b₁ in z } is set
{ (X,(X,A,b₁),(X,c1,b₁)) where b₁ is Element of X : b₁ in z } is set
union { (X,(X,A,b₁),(X,c1,b₁)) where b₁ is Element of X : b₁ in z } is set
A \/ c1 is Relation-like X -defined X -valued Element of bool [:X,X:]
(X,(A \/ c1),z) is Element of bool X
{ (X,(A \/ c1),b₁) where b₁ is Element of X : b₁ in z } is set
union { (X,(A \/ c1),b₁) where b₁ is Element of X : b₁ in z } is set
A \ c1 is X -defined X -valued set
A \ c1 is Relation-like X -defined X -valued Element of bool [:X,X:]
c2 is Relation-like X -defined X -valued Element of bool [:X,X:]
A \ c1 is Relation-like X -defined X -valued Element of bool [:X,X:]
z is Element of bool X
(X,c2,z) is Element of bool X
{ (X,c2,b₁) where b₁ is Element of X : b₁ in z } is set
union { (X,c2,b₁) where b₁ is Element of X : b₁ in z } is set
{ (X,(X,A,b₁),(X,c1,b₁)) where b₁ is Element of X : b₁ in z } is set
union { (X,(X,A,b₁),(X,c1,b₁)) where b₁ is Element of X : b₁ in z } is set
x is set
s is set
[s,x] is set
{s,x} is finite set
{s} is non empty trivial finite 1 -element set
{{s,x},{s}} is finite V37() set
s is Element of X
x is Element of X
[s,x] is set
{s,x} is finite set
{s} is non empty trivial finite 1 -element set
{{s,x},{s}} is finite V37() set
(X,A,s) is Element of bool X
A .: {s} is set
(X,c1,s) is Element of bool X
c1 .: {s} is set
(X,(X,A,s),(X,c1,s)) is Element of bool X
x is set
s is set
s is Element of X
(X,A,s) is Element of bool X
{s} is non empty trivial finite 1 -element set
A .: {s} is set
(X,c1,s) is Element of bool X
c1 .: {s} is set
(X,(X,A,s),(X,c1,s)) is Element of bool X
x is Element of X
[s,x] is set
{s,x} is finite set
{{s,x},{s}} is finite V37() set
c2 is Relation-like X -defined X -valued Element of bool [:X,X:]
z is Element of bool X
(X,c2,z) is Element of bool X
{ (X,c2,b₁) where b₁ is Element of X : b₁ in z } is set
union { (X,c2,b₁) where b₁ is Element of X : b₁ in z } is set
{ (X,(X,A,b₁),(X,c1,b₁)) where b₁ is Element of X : b₁ in z } is set
union { (X,(X,A,b₁),(X,c1,b₁)) where b₁ is Element of X : b₁ in z } is set
z is Element of bool X
(X,c2,z) is Element of bool X
{ (X,c2,b₁) where b₁ is Element of X : b₁ in z } is set
union { (X,c2,b₁) where b₁ is Element of X : b₁ in z } is set
{ (X,(X,A,b₁),(X,c1,b₁)) where b₁ is Element of X : b₁ in z } is set
union { (X,(X,A,b₁),(X,c1,b₁)) where b₁ is Element of X : b₁ in z } is set
A \ c1 is Relation-like X -defined X -valued Element of bool [:X,X:]
(X,(A \ c1),z) is Element of bool X
{ (X,(A \ c1),b₁) where b₁ is Element of X : b₁ in z } is set
union { (X,(A \ c1),b₁) where b₁ is Element of X : b₁ in z } is set
A * c1 is Relation-like set
A * c1 is Relation-like X -defined X -valued Element of bool [:X,X:]
c2 is Relation-like X -defined X -valued Element of bool [:X,X:]
z is Element of bool X
(X,c2,z) is Element of bool X
{ (X,c2,b₁) where b₁ is Element of X : b₁ in z } is set
union { (X,c2,b₁) where b₁ is Element of X : b₁ in z } is set
(X,A,z) is Element of bool X
{ (X,A,b₁) where b₁ is Element of X : b₁ in z } is set
union { (X,A,b₁) where b₁ is Element of X : b₁ in z } is set
(X,c1,(X,A,z)) is Element of bool X
{ (X,c1,b₁) where b₁ is Element of X : b₁ in (X,A,z) } is set
union { (X,c1,b₁) where b₁ is Element of X : b₁ in (X,A,z) } is set
z is Element of bool X
(X,c2,z) is Element of bool X
{ (X,c2,b₁) where b₁ is Element of X : b₁ in z } is set
union { (X,c2,b₁) where b₁ is Element of X : b₁ in z } is set
(X,A,z) is Element of bool X
{ (X,A,b₁) where b₁ is Element of X : b₁ in z } is set
union { (X,A,b₁) where b₁ is Element of X : b₁ in z } is set
(X,c1,(X,A,z)) is Element of bool X
{ (X,c1,b₁) where b₁ is Element of X : b₁ in (X,A,z) } is set
union { (X,c1,b₁) where b₁ is Element of X : b₁ in (X,A,z) } is set
A * c1 is Relation-like X -defined X -valued Element of bool [:X,X:]
(X,(A * c1),z) is Element of bool X
{ (X,(A * c1),b₁) where b₁ is Element of X : b₁ in z } is set
union { (X,(A * c1),b₁) where b₁ is Element of X : b₁ in z } is set
c2 is Relation-like set
z is set
x is set
[z,x] is set
{z,x} is finite set
{z} is non empty trivial finite 1 -element set
{{z,x},{z}} is finite V37() set
z is Relation-like X -defined X -valued Element of bool [:X,X:]
x is Element of bool X
(X,z,x) is Element of bool X
{ (X,z,b₁) where b₁ is Element of X : b₁ in x } is set
union { (X,z,b₁) where b₁ is Element of X : b₁ in x } is set
{ (X,c1,(X,A,b₁)) where b₁ is Element of X : b₁ in x } is set
union { (X,c1,(X,A,b₁)) where b₁ is Element of X : b₁ in x } is set
s is set
s is Element of X
(X,z,s) is Element of bool X
{s} is non empty trivial finite 1 -element set
z .: {s} is set
[s,s] is set
{s,s} is finite set
{{s,s},{s}} is finite V37() set
(X,A,s) is Element of bool X
A .: {s} is set
(X,c1,(X,A,s)) is Element of bool X
{ (X,c1,b₁) where b₁ is Element of X : b₁ in (X,A,s) } is set
meet { (X,c1,b₁) where b₁ is Element of X : b₁ in (X,A,s) } is set
x is Element of X
(X,A,x) is Element of bool X
{x} is non empty trivial finite 1 -element set
A .: {x} is set
(X,c1,(X,A,x)) is Element of bool X
{ (X,c1,b₁) where b₁ is Element of X : b₁ in (X,A,x) } is set
meet { (X,c1,b₁) where b₁ is Element of X : b₁ in (X,A,x) } is set
s is set
s is set
x is Element of X
(X,A,x) is Element of bool X
{x} is non empty trivial finite 1 -element set
A .: {x} is set
(X,c1,(X,A,x)) is Element of bool X
{ (X,c1,b₁) where b₁ is Element of X : b₁ in (X,A,x) } is set
meet { (X,c1,b₁) where b₁ is Element of X : b₁ in (X,A,x) } is set
[x,s] is set
{x,s} is finite set
{{x,s},{x}} is finite V37() set
c2 is Relation-like X -defined X -valued Element of bool [:X,X:]
z is Relation-like X -defined X -valued Element of bool [:X,X:]
x is Element of bool X
(X,c2,x) is Element of bool X
{ (X,c2,b₁) where b₁ is Element of X : b₁ in x } is set
union { (X,c2,b₁) where b₁ is Element of X : b₁ in x } is set
{ (X,c1,(X,A,b₁)) where b₁ is Element of X : b₁ in x } is set
union { (X,c1,(X,A,b₁)) where b₁ is Element of X : b₁ in x } is set
(X,z,x) is Element of bool X
{ (X,z,b₁) where b₁ is Element of X : b₁ in x } is set
union { (X,z,b₁) where b₁ is Element of X : b₁ in x } is set
X is set
[:X,X:] is set
bool [:X,X:] is non empty set
c1 is Relation-like X -defined X -valued Element of bool [:X,X:]
c2 is Relation-like X -defined X -valued Element of bool [:X,X:]
(X,c1,c2) is Relation-like X -defined X -valued Element of bool [:X,X:]
A is Element of X
(X,(X,c1,c2),A) is Element of bool X
bool X is non empty set
{A} is non empty trivial finite 1 -element set
(X,c1,c2) .: {A} is set
(X,c1,A) is Element of bool X
c1 .: {A} is set
(X,c2,A) is Element of bool X
c2 .: {A} is set
(X,(X,c1,A),(X,c2,A)) is Element of bool X
X is set
[:X,X:] is set
bool [:X,X:] is non empty set
c1 is Relation-like X -defined X -valued Element of bool [:X,X:]
c2 is Relation-like X -defined X -valued Element of bool [:X,X:]
(X,c1,c2) is Relation-like X -defined X -valued Element of bool [:X,X:]
A is Element of X
(X,(X,c1,c2),A) is Element of bool X
bool X is non empty set
{A} is non empty trivial finite 1 -element set
(X,c1,c2) .: {A} is set
(X,c1,A) is Element of bool X
c1 .: {A} is set
(X,c2,A) is Element of bool X
c2 .: {A} is set
(X,(X,c1,A),(X,c2,A)) is Element of bool X
X is set
[:X,X:] is set
bool [:X,X:] is non empty set
c1 is Relation-like X -defined X -valued Element of bool [:X,X:]
c2 is Relation-like X -defined X -valued Element of bool [:X,X:]
(X,c1,c2) is Relation-like X -defined X -valued Element of bool [:X,X:]
A is Element of X
(X,(X,c1,c2),A) is Element of bool X
bool X is non empty set
{A} is non empty trivial finite 1 -element set
(X,c1,c2) .: {A} is set
(X,c1,A) is Element of bool X
c1 .: {A} is set
(X,c2,A) is Element of bool X
c2 .: {A} is set
(X,(X,c1,A),(X,c2,A)) is Element of bool X
X is set
[:X,X:] is set
bool [:X,X:] is non empty set
c1 is Relation-like X -defined X -valued Element of bool [:X,X:]
c2 is Relation-like X -defined X -valued Element of bool [:X,X:]
(X,c1,c2) is Relation-like X -defined X -valued Element of bool [:X,X:]
A is Element of X
(X,(X,c1,c2),A) is Element of bool X
bool X is non empty set
{A} is non empty trivial finite 1 -element set
(X,c1,c2) .: {A} is set
(X,c1,A) is Element of bool X
c1 .: {A} is set
(X,c2,(X,c1,A)) is Element of bool X
{ (X,c2,b₁) where b₁ is Element of X : b₁ in (X,c1,A) } is set
union { (X,c2,b₁) where b₁ is Element of X : b₁ in (X,c1,A) } is set
X is set
[:X,X:] is set
bool [:X,X:] is non empty set
A is Element of X
c1 is Relation-like X -defined X -valued Element of bool [:X,X:]
(X,c1,A) is Element of bool X
bool X is non empty set
{A} is non empty trivial finite 1 -element set
c1 .: {A} is set
c2 is Relation-like X -defined X -valued Element of bool [:X,X:]
(X,c1,c2) is Relation-like X -defined X -valued Element of bool [:X,X:]
(X,(X,c1,c2),A) is Element of bool X
(X,c1,c2) .: {A} is set
(X,c2,(X,c1,A)) is Element of bool X
{ (X,c2,b₁) where b₁ is Element of X : b₁ in (X,c1,A) } is set
meet { (X,c2,b₁) where b₁ is Element of X : b₁ in (X,c1,A) } is set
z is Element of bool X
{ (X,c2,(X,c1,b₁)) where b₁ is Element of X : b₁ in z } is set
{(X,c2,(X,c1,A))} is non empty trivial finite 1 -element set
x is set
s is Element of X
(X,c1,s) is Element of bool X
{s} is non empty trivial finite 1 -element set
c1 .: {s} is set
(X,c2,(X,c1,s)) is Element of bool X
{ (X,c2,b₁) where b₁ is Element of X : b₁ in (X,c1,s) } is set
meet { (X,c2,b₁) where b₁ is Element of X : b₁ in (X,c1,s) } is set
x is set
union { (X,c2,(X,c1,b₁)) where b₁ is Element of X : b₁ in z } is set
X is set
A is set
[X,A] is set
{X,A} is finite set
{X} is non empty trivial finite 1 -element set
{{X,A},{X}} is finite V37() set
c1 is set
[:c1,c1:] is set
bool [:c1,c1:] is non empty set
c2 is Relation-like c1 -defined c1 -valued Element of bool [:c1,c1:]
(c1,c2) is Relation-like c1 -defined c1 -valued Element of bool [:c1,c1:]
dom c2 is Element of bool c1
bool c1 is non empty set
Im ((c1,c2),X) is set
(c1,c2) .: {X} is set
(c1,c2) .: {X} is Element of bool c1
{ (IFEQ ((c1,c2,b₁),{},{b₁},{})) where b₁ is Element of c1 : b₁ in {X} } is set
union { (IFEQ ((c1,c2,b₁),{},{b₁},{})) where b₁ is Element of c1 : b₁ in {X} } is set
z is set
x is Element of c1
(c1,c2,x) is Element of bool c1
{x} is non empty trivial finite 1 -element set
c2 .: {x} is set
IFEQ ((c1,c2,x),{},{x},{}) is set
s is set
[x,s] is set
{x,s} is finite set
{{x,s},{x}} is finite V37() set
z is Element of c1
(c1,c2,z) is Element of bool c1
{z} is non empty trivial finite 1 -element set
c2 .: {z} is set
x is set
[z,x] is set
{z,x} is finite set
{{z,x},{z}} is finite V37() set
IFEQ ((c1,c2,z),{},{z},{}) is set
{ (IFEQ ((c1,c2,b₁),{},{b₁},{})) where b₁ is Element of c1 : b₁ in {z} } is set
union { (IFEQ ((c1,c2,b₁),{},{b₁},{})) where b₁ is Element of c1 : b₁ in {z} } is set
x is Element of bool c1
(c1,(c1,c2),x) is Element of bool c1
{ (c1,(c1,c2),b₁) where b₁ is Element of c1 : b₁ in x } is set
union { (c1,(c1,c2),b₁) where b₁ is Element of c1 : b₁ in x } is set
(c1,(c1,c2),z) is Element of bool c1
(c1,c2) .: {z} is set
X is set
[:X,X:] is set
bool [:X,X:] is non empty set
A is Relation-like X -defined X -valued Element of bool [:X,X:]
(X,A) is Relation-like X -defined X -valued Element of bool [:X,X:]
dom A is Element of bool X
bool X is non empty set
X \ (dom A) is Element of bool X
id (X \ (dom A)) is Relation-like set
c1 is set
c2 is set
[c1,c2] is set
{c1,c2} is finite set
{c1} is non empty trivial finite 1 -element set
{{c1,c2},{c1}} is finite V37() set
X is set
[:X,X:] is set
bool [:X,X:] is non empty set
A is Relation-like X -defined X -valued Element of bool [:X,X:]
(X,A) is Relation-like X -defined X -valued Element of bool [:X,X:]
(X,(X,A)) is Relation-like X -defined X -valued Element of bool [:X,X:]
dom (X,(X,A)) is Element of bool X
bool X is non empty set
dom A is Element of bool X
dom (X,A) is Element of bool X
X \ (dom (X,A)) is Element of bool X
id (X \ (dom (X,A))) is Relation-like set
dom (id (X \ (dom (X,A)))) is set
X \ (dom A) is Element of bool X
id (X \ (dom A)) is Relation-like set
dom (id (X \ (dom A))) is set
X \ (dom (id (X \ (dom A)))) is Element of bool X
X \ (X \ (dom A)) is Element of bool X
X /\ (dom A) is Element of bool X
X is set
bool X is non empty set
[:X,X:] is set
bool [:X,X:] is non empty set
A is Element of bool X
c1 is Relation-like X -defined X -valued Element of bool [:X,X:]
(X,c1) is Relation-like X -defined X -valued Element of bool [:X,X:]
(X,(X,c1)) is Relation-like X -defined X -valued Element of bool [:X,X:]
(X,(X,(X,c1)),A) is Element of bool X
{ b₁ where b₁ is Element of X : ex b₂ being Element of X st
( (b₁,b₂,(X,(X,c1))) & b₁ in A ) } is set
(X,c1,A) is Element of bool X
{ b₁ where b₁ is Element of X : ex b₂ being Element of X st
( (b₁,b₂,c1) & b₁ in A ) } is set
c2 is set
z is Element of X
(X,(X,(X,c1)),z) is Element of bool X
{z} is non empty trivial finite 1 -element set
(X,(X,c1)) .: {z} is set
dom (X,(X,c1)) is Element of bool X
dom c1 is Element of bool X
(X,c1,z) is Element of bool X
c1 .: {z} is set
c2 is set
z is Element of X
(X,c1,z) is Element of bool X
{z} is non empty trivial finite 1 -element set
c1 .: {z} is set
dom c1 is Element of bool X
dom (X,(X,c1)) is Element of bool X
(X,(X,(X,c1)),z) is Element of bool X
(X,(X,c1)) .: {z} is set
X is set
bool X is non empty set
[:X,X:] is set
bool [:X,X:] is non empty set
A is Element of bool X
c1 is Relation-like X -defined X -valued Element of bool [:X,X:]
(X,A,c1,0) is Element of bool X
{ b₁ where b₁ is Element of X : ( card (X,c1,b₁) = 0 & b₁ in A ) } is set
(X,c1) is Relation-like X -defined X -valued Element of bool [:X,X:]
(X,(X,c1),A) is Element of bool X
{ b₁ where b₁ is Element of X : ex b₂ being Element of X st
( (b₁,b₂,(X,c1)) & b₁ in A ) } is set
c2 is set
z is Element of X
(X,c1,z) is Element of bool X
{z} is non empty trivial finite 1 -element set
c1 .: {z} is set
card (X,c1,z) is epsilon-transitive epsilon-connected ordinal cardinal set
dom c1 is Element of bool X
[z,z] is set
{z,z} is finite set
{{z,z},{z}} is finite V37() set
c2 is set
z is Element of X
x is Element of X
x is Element of X
[z,x] is set
{z,x} is finite set
{z} is non empty trivial finite 1 -element set
{{z,x},{z}} is finite V37() set
dom c1 is Element of bool X
(X,c1,z) is Element of bool X
c1 .: {z} is set
card (X,c1,z) is epsilon-transitive epsilon-connected ordinal cardinal set
s is Element of X
X is set
[:X,X:] is set
bool [:X,X:] is non empty set
A is Relation-like X -defined X -valued Element of bool [:X,X:]
(X,A) is Relation-like X -defined X -valued Element of bool [:X,X:]
(X,(X,A)) is Relation-like X -defined X -valued Element of bool [:X,X:]
(X,(X,(X,A))) is Relation-like X -defined X -valued Element of bool [:X,X:]
dom (X,(X,A)) is Element of bool X
bool X is non empty set
X \ (dom (X,(X,A))) is Element of bool X
id (X \ (dom (X,(X,A)))) is Relation-like set
dom A is Element of bool X
X \ (dom A) is Element of bool X
id (X \ (dom A)) is Relation-like set
X is set
[:X,X:] is set
bool [:X,X:] is non empty set
A is Relation-like X -defined X -valued Element of bool [:X,X:]
(X,A) is Relation-like X -defined X -valued Element of bool [:X,X:]
c1 is Relation-like X -defined X -valued Element of bool [:X,X:]
(X,c1) is Relation-like X -defined X -valued Element of bool [:X,X:]
(X,(X,A),(X,c1)) is Relation-like X -defined X -valued Element of bool [:X,X:]
(X,A,c1) is Relation-like X -defined X -valued Element of bool [:X,X:]
(X,(X,A,c1)) is Relation-like X -defined X -valued Element of bool [:X,X:]
c2 is set
z is set
[c2,z] is set
{c2,z} is finite set
{c2} is non empty trivial finite 1 -element set
{{c2,z},{c2}} is finite V37() set
dom A is Element of bool X
bool X is non empty set
dom c1 is Element of bool X
(dom A) /\ (dom c1) is Element of bool X
dom (X,A,c1) is Element of bool X
X is set
[:X,X:] is set
bool [:X,X:] is non empty set
A is Relation-like X -defined X -valued Element of bool [:X,X:]
(X,A) is Relation-like X -defined X -valued Element of bool [:X,X:]
c1 is Relation-like X -defined X -valued Element of bool [:X,X:]
(X,A,c1) is Relation-like X -defined X -valued Element of bool [:X,X:]
(X,(X,A,c1)) is Relation-like X -defined X -valued Element of bool [:X,X:]
(X,c1) is Relation-like X -defined X -valued Element of bool [:X,X:]
(X,(X,A),(X,c1)) is Relation-like X -defined X -valued Element of bool [:X,X:]
c2 is set
z is set
[c2,z] is set
{c2,z} is finite set
{c2} is non empty trivial finite 1 -element set
{{c2,z},{c2}} is finite V37() set
dom (X,A,c1) is Element of bool X
bool X is non empty set
dom A is Element of bool X
dom c1 is Element of bool X
(dom A) \/ (dom c1) is Element of bool X
dom A is Element of bool X
bool X is non empty set
dom c1 is Element of bool X
(dom A) \/ (dom c1) is Element of bool X
dom (X,A,c1) is Element of bool X
X is set
[:X,X:] is set
bool [:X,X:] is non empty set
A is Relation-like X -defined X -valued Element of bool [:X,X:]
dom A is Element of bool X
bool X is non empty set
c1 is Relation-like X -defined X -valued Element of bool [:X,X:]
dom c1 is Element of bool X
(X,A,c1) is Relation-like X -defined X -valued Element of bool [:X,X:]
c2 is Relation-like X -defined X -valued Element of bool [:X,X:]
(X,(X,A,c1),c2) is Relation-like X -defined X -valued Element of bool [:X,X:]
(X,A,c2) is Relation-like X -defined X -valued Element of bool [:X,X:]
(X,c1,c2) is Relation-like X -defined X -valued Element of bool [:X,X:]
(X,(X,A,c2),(X,c1,c2)) is Relation-like X -defined X -valued Element of bool [:X,X:]
z is set
x is set
[z,x] is set
{z,x} is finite set
{z} is non empty trivial finite 1 -element set
{{z,x},{z}} is finite V37() set
s is Element of X
s is Element of X
(X,(X,(X,A,c1),c2),s) is Element of bool X
{s} is non empty trivial finite 1 -element set
(X,(X,A,c1),c2) .: {s} is set
(X,(X,A,c1),s) is Element of bool X
(X,A,c1) .: {s} is set
(X,c2,(X,(X,A,c1),s)) is Element of bool X
{ (X,c2,b₁) where b₁ is Element of X : b₁ in (X,(X,A,c1),s) } is set
meet { (X,c2,b₁) where b₁ is Element of X : b₁ in (X,(X,A,c1),s) } is set
(X,A,s) is Element of bool X
A .: {s} is set
(X,c1,s) is Element of bool X
c1 .: {s} is set
(X,(X,A,s),(X,c1,s)) is Element of bool X
(X,c2,(X,(X,A,s),(X,c1,s))) is Element of bool X
{ (X,c2,b₁) where b₁ is Element of X : b₁ in (X,(X,A,s),(X,c1,s)) } is set
meet { (X,c2,b₁) where b₁ is Element of X : b₁ in (X,(X,A,s),(X,c1,s)) } is set
(X,c2,(X,A,s)) is Element of bool X
{ (X,c2,b₁) where b₁ is Element of X : b₁ in (X,A,s) } is set
meet { (X,c2,b₁) where b₁ is Element of X : b₁ in (X,A,s) } is set
(X,c2,(X,c1,s)) is Element of bool X
{ (X,c2,b₁) where b₁ is Element of X : b₁ in (X,c1,s) } is set
meet { (X,c2,b₁) where b₁ is Element of X : b₁ in (X,c1,s) } is set
(X,(X,c2,(X,A,s)),(X,c2,(X,c1,s))) is Element of bool X
(X,(X,A,c2),s) is Element of bool X
(X,A,c2) .: {s} is set
(X,(X,(X,A,c2),s),(X,c2,(X,c1,s))) is Element of bool X
(X,(X,c1,c2),s) is Element of bool X
(X,c1,c2) .: {s} is set
(X,(X,(X,A,c2),s),(X,(X,c1,c2),s)) is Element of bool X
(X,(X,(X,A,c2),(X,c1,c2)),s) is Element of bool X
(X,(X,A,c2),(X,c1,c2)) .: {s} is set
s is Element of X
s is Element of X
(X,(X,(X,A,c2),(X,c1,c2)),s) is Element of bool X
{s} is non empty trivial finite 1 -element set
(X,(X,A,c2),(X,c1,c2)) .: {s} is set
(X,(X,A,c2),s) is Element of bool X
(X,A,c2) .: {s} is set
(X,(X,c1,c2),s) is Element of bool X
(X,c1,c2) .: {s} is set
(X,(X,(X,A,c2),s),(X,(X,c1,c2),s)) is Element of bool X
(X,c1,s) is Element of bool X
c1 .: {s} is set
(X,c2,(X,c1,s)) is Element of bool X
{ (X,c2,b₁) where b₁ is Element of X : b₁ in (X,c1,s) } is set
meet { (X,c2,b₁) where b₁ is Element of X : b₁ in (X,c1,s) } is set
(X,(X,(X,A,c2),s),(X,c2,(X,c1,s))) is Element of bool X
(X,A,s) is Element of bool X
A .: {s} is set
(X,c2,(X,A,s)) is Element of bool X
{ (X,c2,b₁) where b₁ is Element of X : b₁ in (X,A,s) } is set
meet { (X,c2,b₁) where b₁ is Element of X : b₁ in (X,A,s) } is set
(X,(X,c2,(X,A,s)),(X,c2,(X,c1,s))) is Element of bool X
(X,(X,A,s),(X,c1,s)) is Element of bool X
(X,c2,(X,(X,A,s),(X,c1,s))) is Element of bool X
{ (X,c2,b₁) where b₁ is Element of X : b₁ in (X,(X,A,s),(X,c1,s)) } is set
meet { (X,c2,b₁) where b₁ is Element of X : b₁ in (X,(X,A,s),(X,c1,s)) } is set
(X,(X,A,c1),s) is Element of bool X
(X,A,c1) .: {s} is set
(X,c2,(X,(X,A,c1),s)) is Element of bool X
{ (X,c2,b₁) where b₁ is Element of X : b₁ in (X,(X,A,c1),s) } is set
meet { (X,c2,b₁) where b₁ is Element of X : b₁ in (X,(X,A,c1),s) } is set
(X,(X,(X,A,c1),c2),s) is Element of bool X
(X,(X,A,c1),c2) .: {s} is set
X is set
[:X,X:] is set
bool [:X,X:] is non empty set
X is set
[:X,X:] is set
bool [:X,X:] is non empty set
A is Relation-like X -defined X -valued Element of bool [:X,X:]
dom A is Element of bool X
bool X is non empty set
id (dom A) is Relation-like set
id X is Relation-like set
c1 is set
c2 is set
[c1,c2] is set
{c1,c2} is finite set
{c1} is non empty trivial finite 1 -element set
{{c1,c2},{c1}} is finite V37() set
z is set
[c1,z] is set
{c1,z} is finite set
{{c1,z},{c1}} is finite V37() set
id X is Relation-like set
X is set
[:X,X:] is set
bool [:X,X:] is non empty set
A is Relation-like X -defined X -valued Element of bool [:X,X:]
(X,A) is Relation-like X -defined X -valued Element of bool [:X,X:]
dom A is Element of bool X
bool X is non empty set
X \ (dom A) is Element of bool X
id (X \ (dom A)) is Relation-like set
id X is Relation-like set
X is set
[:X,X:] is set
bool [:X,X:] is non empty set
the Relation-like X -defined X -valued Element of bool [:X,X:] is Relation-like X -defined X -valued Element of bool [:X,X:]
(X, the Relation-like X -defined X -valued Element of bool [:X,X:]) is Relation-like X -defined X -valued (X) Element of bool [:X,X:]
X is set
[:X,X:] is set
bool [:X,X:] is non empty set
A is Relation-like X -defined X -valued (X) Element of bool [:X,X:]
c1 is Relation-like X -defined X -valued Element of bool [:X,X:]
(X,A,c1) is Relation-like X -defined X -valued Element of bool [:X,X:]
c2 is Relation-like X -defined X -valued Element of bool [:X,X:]
id X is Relation-like set
(X,c1,A) is Relation-like X -defined X -valued (X) Element of bool [:X,X:]
c2 is Relation-like X -defined X -valued Element of bool [:X,X:]
(X,A,c1) is Relation-like X -defined X -valued Element of bool [:X,X:]
c2 is Relation-like X -defined X -valued Element of bool [:X,X:]
id X is Relation-like set
X is set
[:X,X:] is set
bool [:X,X:] is non empty set
A is Relation-like X -defined X -valued (X) Element of bool [:X,X:]
c1 is Relation-like X -defined X -valued (X) Element of bool [:X,X:]
(X,A,c1) is Relation-like X -defined X -valued Element of bool [:X,X:]
c2 is Relation-like X -defined X -valued Element of bool [:X,X:]
id X is Relation-like set
X is set
[:X,X:] is set
bool [:X,X:] is non empty set
A is set
c1 is Element of X
c2 is Relation-like X -defined X -valued (X) Element of bool [:X,X:]
(X,c2,c1) is Element of bool X
bool X is non empty set
{c1} is non empty trivial finite 1 -element set
c2 .: {c1} is set
[c1,A] is set
{c1,A} is finite set
{{c1,A},{c1}} is finite V37() set
id X is Relation-like set
X is set
bool X is non empty set
[:X,X:] is set
bool [:X,X:] is non empty set
A is Element of bool X
c1 is Relation-like X -defined X -valued (X) Element of bool [:X,X:]
(X,c1,A) is Element of bool X
{ (X,c1,b₁) where b₁ is Element of X : b₁ in A } is set
union { (X,c1,b₁) where b₁ is Element of X : b₁ in A } is set
(X,c1,A) is Element of bool X
{ b₁ where b₁ is Element of X : ex b₂ being Element of X st
( (b₁,b₂,c1) & b₁ in A ) } is set
c2 is set
z is Element of X
(X,c1,z) is Element of bool X
{z} is non empty trivial finite 1 -element set
c1 .: {z} is set
c2 is set
z is Element of X
(X,c1,z) is Element of bool X
{z} is non empty trivial finite 1 -element set
c1 .: {z} is set
the Element of (X,c1,z) is Element of (X,c1,z)
[z, the Element of (X,c1,z)] is set
{z, the Element of (X,c1,z)} is finite set
{{z, the Element of (X,c1,z)},{z}} is finite V37() set
id X is Relation-like set
X is set
[:X,X:] is set
bool [:X,X:] is non empty set
A is Relation-like X -defined X -valued (X) Element of bool [:X,X:]
(X,A) is Relation-like X -defined X -valued (X) Element of bool [:X,X:]
(X,(X,A)) is Relation-like X -defined X -valued (X) Element of bool [:X,X:]
dom (X,A) is Element of bool X
bool X is non empty set
X \ (dom (X,A)) is Element of bool X
id (X \ (dom (X,A))) is Relation-like set
dom A is Element of bool X
X \ (dom A) is Element of bool X
id (X \ (dom A)) is Relation-like set
dom (id (X \ (dom A))) is set
X \ (dom (id (X \ (dom A)))) is Element of bool X
id (X \ (dom (id (X \ (dom A))))) is Relation-like set
X \ (X \ (dom A)) is Element of bool X
id (X \ (X \ (dom A))) is Relation-like set
X /\ (dom A) is Element of bool X
id (X /\ (dom A)) is Relation-like set
id (dom A) is Relation-like set
X is set
[:X,X:] is set
bool [:X,X:] is non empty set
A is Relation-like X -defined X -valued (X) Element of bool [:X,X:]
(X,A) is Relation-like X -defined X -valued (X) Element of bool [:X,X:]
c1 is Relation-like X -defined X -valued (X) Element of bool [:X,X:]
(X,A,c1) is Relation-like X -defined X -valued (X) Element of bool [:X,X:]
(X,(X,A,c1)) is Relation-like X -defined X -valued (X) Element of bool [:X,X:]
(X,c1) is Relation-like X -defined X -valued (X) Element of bool [:X,X:]
(X,(X,A),(X,c1)) is Relation-like X -defined X -valued (X) Element of bool [:X,X:]
dom A is Element of bool X
bool X is non empty set
id (dom A) is Relation-like set
dom c1 is Element of bool X
id (dom c1) is Relation-like set
dom (X,A,c1) is Element of bool X
X \ (dom (X,A,c1)) is Element of bool X
id (X \ (dom (X,A,c1))) is Relation-like set
(X,(dom A),(dom c1)) is Element of bool X
id (X,(dom A),(dom c1)) is Relation-like set
dom (id (X,(dom A),(dom c1))) is set
X \ (dom (id (X,(dom A),(dom c1)))) is Element of bool X
id (X \ (dom (id (X,(dom A),(dom c1))))) is Relation-like set
X \ (X,(dom A),(dom c1)) is Element of bool X
id (X \ (X,(dom A),(dom c1))) is Relation-like set
X \ (dom A) is Element of bool X
X \ (dom c1) is Element of bool X
(X \ (dom A)) \/ (X \ (dom c1)) is Element of bool X
id ((X \ (dom A)) \/ (X \ (dom c1))) is Relation-like set
id (X \ (dom A)) is Relation-like set
id (X \ (dom c1)) is Relation-like set
(id (X \ (dom A))) \/ (id (X \ (dom c1))) is set
(X,A) \/ (id (X \ (dom c1))) is set
X is set
[:X,X:] is set
bool [:X,X:] is non empty set
A is Relation-like X -defined X -valued Element of bool [:X,X:]
(X,A) is Relation-like X -defined X -valued (X) Element of bool [:X,X:]
(X,A,(X,A)) is Relation-like X -defined X -valued Element of bool [:X,X:]
dom (X,A,(X,A)) is Element of bool X
bool X is non empty set
dom A is Element of bool X
dom (X,A) is Element of bool X
(X,(dom A),(dom (X,A))) is Element of bool X
X \ (dom A) is Element of bool X
id (X \ (dom A)) is Relation-like set
dom (id (X \ (dom A))) is set
(dom A) \/ (dom (id (X \ (dom A)))) is set
(X,(dom A),(X \ (dom A))) is Element of bool X
(dom A) \/ X is set
X is set
[:X,X:] is set
bool [:X,X:] is non empty set
id X is Relation-like set
A is Relation-like X -defined X -valued (X) Element of bool [:X,X:]
(X,A) is Relation-like X -defined X -valued (X) Element of bool [:X,X:]
(X,A,(X,A)) is Relation-like X -defined X -valued (X) Element of bool [:X,X:]
dom (X,A,(X,A)) is Element of bool X
bool X is non empty set
X is set
[:X,X:] is set
bool [:X,X:] is non empty set
A is Relation-like X -defined X -valued Element of bool [:X,X:]
(X,A) is Relation-like X -defined X -valued (X) Element of bool [:X,X:]
(X,A,(X,A)) is Relation-like X -defined X -valued (X) Element of bool [:X,X:]
dom (X,A,(X,A)) is Element of bool X
bool X is non empty set
dom A is Element of bool X
X \ (dom A) is Element of bool X
id (X \ (dom A)) is Relation-like set
A /\ (id (X \ (dom A))) is Relation-like X -defined X -valued Element of bool [:X,X:]
dom (A /\ (id (X \ (dom A)))) is Element of bool X
dom (id (X \ (dom A))) is set
(dom A) /\ (dom (id (X \ (dom A)))) is Element of bool X
(dom A) /\ (X \ (dom A)) is Element of bool X
(dom A) /\ X is Element of bool X
((dom A) /\ X) \ (dom A) is Element of bool X
(dom A) \ (dom A) is Element of bool X
X is set
[:X,X:] is set
bool [:X,X:] is non empty set
A is Relation-like X -defined X -valued Element of bool [:X,X:]
(X,A) is Relation-like X -defined X -valued (X) Element of bool [:X,X:]
c1 is Relation-like X -defined X -valued Element of bool [:X,X:]
(X,A,c1) is Relation-like X -defined X -valued Element of bool [:X,X:]
(X,(X,A,c1),(X,A)) is Relation-like X -defined X -valued (X) Element of bool [:X,X:]
(X,A,(X,A)) is Relation-like X -defined X -valued (X) Element of bool [:X,X:]
(X,c1,(X,A)) is Relation-like X -defined X -valued (X) Element of bool [:X,X:]
(X,(X,A,(X,A)),(X,c1,(X,A))) is Relation-like X -defined X -valued (X) Element of bool [:X,X:]
{} \/ (X,c1,(X,A)) is set
X is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
dom X is finite Element of bool NAT
A is set
{ b₁ where b₁ is epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() Element of NAT : ( b₁ in dom X & A in X . b₁ ) } is set
card { b₁ where b₁ is epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() Element of NAT : ( b₁ in dom X & A in X . b₁ ) } is epsilon-transitive epsilon-connected ordinal cardinal set
c1 is set
c2 is epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() Element of NAT
X . c2 is set
X is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
len X is epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() Element of NAT
A is set
(X,A) is epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() set
dom X is finite Element of bool NAT
{ b₁ where b₁ is epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() Element of NAT : ( b₁ in dom X & A in X . b₁ ) } is set
card { b₁ where b₁ is epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() Element of NAT : ( b₁ in dom X & A in X . b₁ ) } is epsilon-transitive epsilon-connected ordinal cardinal set
c1 is set
c2 is epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() Element of NAT
X . c2 is set
card (dom X) is epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() Element of omega
Seg (len X) is finite len X -element Element of bool NAT
card (Seg (len X)) is epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() Element of omega
X is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
len X is epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() Element of NAT
rng X is finite set
meet (rng X) is set
A is set
(X,A) is epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() set
dom X is finite Element of bool NAT
{ b₁ where b₁ is epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() Element of NAT : ( b₁ in dom X & A in X . b₁ ) } is set
card { b₁ where b₁ is epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() Element of NAT : ( b₁ in dom X & A in X . b₁ ) } is epsilon-transitive epsilon-connected ordinal cardinal set
c1 is set
c2 is epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() Element of NAT
X . c2 is set
Seg (len X) is finite len X -element Element of bool NAT
card (Seg (len X)) is epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() Element of omega
c1 is set
c2 is set
X . c2 is set
z is epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() Element of NAT
X . z is set
c1 is set
X . c1 is set
X is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
len X is epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() Element of NAT
A is set
(X,A) is epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() set
dom X is finite Element of bool NAT
{ b₁ where b₁ is epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() Element of NAT : ( b₁ in dom X & A in X . b₁ ) } is set
card { b₁ where b₁ is epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() Element of NAT : ( b₁ in dom X & A in X . b₁ ) } is epsilon-transitive epsilon-connected ordinal cardinal set
A is epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() set
c1 is set
(X,c1) is epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() set
dom X is finite Element of bool NAT
{ b₁ where b₁ is epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() Element of NAT : ( b₁ in dom X & c1 in X . b₁ ) } is set
card { b₁ where b₁ is epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() Element of NAT : ( b₁ in dom X & c1 in X . b₁ ) } is epsilon-transitive epsilon-connected ordinal cardinal set
c2 is epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() set
A is epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() set
c1 is epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() set
X is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
(X) is epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() set
len X is epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() Element of NAT
A is set
(X,A) is epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() set
dom X is finite Element of bool NAT
{ b₁ where b₁ is epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() Element of NAT : ( b₁ in dom X & A in X . b₁ ) } is set
card { b₁ where b₁ is epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() Element of NAT : ( b₁ in dom X & A in X . b₁ ) } is epsilon-transitive epsilon-connected ordinal cardinal set
X is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
len X is epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() Element of NAT
(X) is epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() set
A is set
(X,A) is epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() set
dom X is finite Element of bool NAT
{ b₁ where b₁ is epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() Element of NAT : ( b₁ in dom X & A in X . b₁ ) } is set
card { b₁ where b₁ is epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() Element of NAT : ( b₁ in dom X & A in X . b₁ ) } is epsilon-transitive epsilon-connected ordinal cardinal 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
c1 is epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() set
A is Relation-like NAT -defined bool X -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of bool X
{ b₁ where b₁ is Element of X : c1 <= (A,b₁) } is set
c2 is set
z is Element of X
(A,z) is epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() set
dom A is finite Element of bool NAT
{ b₁ where b₁ is epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() Element of NAT : ( b₁ in dom A & z in A . b₁ ) } is set
card { b₁ where b₁ is epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() Element of NAT : ( b₁ in dom A & z in A . b₁ ) } is epsilon-transitive epsilon-connected ordinal cardinal set
c2 is epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() set
{ b₁ where b₁ is Element of X : ( c1 <= (A,b₁) & (A,b₁) <= c2 ) } is set
z is set
x is Element of X
(A,x) is epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() set
dom A is finite Element of bool NAT
{ b₁ where b₁ is epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() Element of NAT : ( b₁ in dom A & x in A . b₁ ) } is set
card { b₁ where b₁ is epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() Element of NAT : ( b₁ in dom A & x in A . b₁ ) } is epsilon-transitive epsilon-connected ordinal cardinal 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
A is Relation-like NAT -defined bool X -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of bool X
(A) is epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() set
(X,A,(A)) 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
A is epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() set
c1 is Relation-like NAT -defined bool X -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of bool X
len c1 is epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() Element of NAT
(X,c1,A,(len c1)) is Element of bool X
(X,c1,A) is Element of bool X
c2 is set
{ b₁ where b₁ is Element of X : ( A <= (c1,b₁) & (c1,b₁) <= len c1 ) } is set
{ b₁ where b₁ is Element of X : A <= (c1,b₁) } is set
z is Element of X
(c1,z) is epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() set
dom c1 is finite Element of bool NAT
{ b₁ where b₁ is epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() Element of NAT : ( b₁ in dom c1 & z in c1 . b₁ ) } is set
card { b₁ where b₁ is epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() Element of NAT : ( b₁ in dom c1 & z in c1 . b₁ ) } is epsilon-transitive epsilon-connected ordinal cardinal set
c2 is set
{ b₁ where b₁ is Element of X : A <= (c1,b₁) } is set
z is Element of X
(c1,z) is epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() set
dom c1 is finite Element of bool NAT
{ b₁ where b₁ is epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() Element of NAT : ( b₁ in dom c1 & z in c1 . b₁ ) } is set
card { b₁ where b₁ is epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() Element of NAT : ( b₁ in dom c1 & z in c1 . b₁ ) } is epsilon-transitive epsilon-connected ordinal cardinal set
{ b₁ where b₁ is Element of X : ( A <= (c1,b₁) & (c1,b₁) <= len c1 ) } 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
A is epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() set
c1 is epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() set
c2 is Relation-like NAT -defined bool X -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of bool X
(X,c2,c1) is Element of bool X
(X,c2,A) is Element of bool X
z is set
{ b₁ where b₁ is Element of X : c1 <= (c2,b₁) } is set
x is Element of X
(c2,x) is epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() set
dom c2 is finite Element of bool NAT
{ b₁ where b₁ is epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() Element of NAT : ( b₁ in dom c2 & x in c2 . b₁ ) } is set
card { b₁ where b₁ is epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() Element of NAT : ( b₁ in dom c2 & x in c2 . b₁ ) } is epsilon-transitive epsilon-connected ordinal cardinal set
{ b₁ where b₁ is Element of X : A <= (c2,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
A is Relation-like NAT -defined bool X -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of bool X
c1 is epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() set
z is epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() set
c2 is epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() set
x is epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() set
(X,A,z,c2) is Element of bool X
(X,A,c1,x) is Element of bool X
s is set
{ b₁ where b₁ is Element of X : ( z <= (A,b₁) & (A,b₁) <= c2 ) } is set
s is Element of X
(A,s) is epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() set
dom A is finite Element of bool NAT
{ b₁ where b₁ is epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() Element of NAT : ( b₁ in dom A & s in A . b₁ ) } is set
card { b₁ where b₁ is epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() Element of NAT : ( b₁ in dom A & s in A . b₁ ) } is epsilon-transitive epsilon-connected ordinal cardinal set
{ b₁ where b₁ is Element of X : ( c1 <= (A,b₁) & (A,b₁) <= x ) } 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
A is epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() set
c1 is epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() set
c2 is Relation-like NAT -defined bool X -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of bool X
(X,c2,A,c1) is Element of bool X
(X,c2,A) is Element of bool X
z is set
{ b₁ where b₁ is Element of X : ( A <= (c2,b₁) & (c2,b₁) <= c1 ) } is set
{ b₁ where b₁ is Element of X : A <= (c2,b₁) } is set
x is Element of X
(c2,x) is epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() set
dom c2 is finite Element of bool NAT
{ b₁ where b₁ is epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() Element of NAT : ( b₁ in dom c2 & x in c2 . b₁ ) } is set
card { b₁ where b₁ is epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() Element of NAT : ( b₁ in dom c2 & x in c2 . b₁ ) } is epsilon-transitive epsilon-connected ordinal cardinal 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
A is Relation-like NAT -defined bool X -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of bool X
len A is epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() Element of NAT
(X,A,(len A)) is Element of bool X
rng A is finite Element of bool (bool X)
bool (bool X) is non empty set
meet (rng A) is Element of bool X
c1 is set
{ b₁ where b₁ is Element of X : len A <= (A,b₁) } is set
c2 is Element of X
(A,c2) is epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() set
dom A is finite Element of bool NAT
{ b₁ where b₁ is epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() Element of NAT : ( b₁ in dom A & c2 in A . b₁ ) } is set
card { b₁ where b₁ is epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() Element of NAT : ( b₁ in dom A & c2 in A . b₁ ) } is epsilon-transitive epsilon-connected ordinal cardinal set
c1 is set
(A,c1) is epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() set
dom A is finite Element of bool NAT
{ b₁ where b₁ is epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() Element of NAT : ( b₁ in dom A & c1 in A . b₁ ) } is set
card { b₁ where b₁ is epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() Element of NAT : ( b₁ in dom A & c1 in A . b₁ ) } is epsilon-transitive epsilon-connected ordinal cardinal set
{ b₁ where b₁ is Element of X : len A <= (A,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
A is Relation-like NAT -defined bool X -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of bool X
(X,A,1) is Element of bool X
Union A is Element of bool X
c1 is set
{ b₁ where b₁ is Element of X : 1 <= (A,b₁) } is set
c2 is Element of X
(A,c2) is epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() set
dom A is finite Element of bool NAT
{ b₁ where b₁ is epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() Element of NAT : ( b₁ in dom A & c2 in A . b₁ ) } is set
card { b₁ where b₁ is epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() Element of NAT : ( b₁ in dom A & c2 in A . b₁ ) } is epsilon-transitive epsilon-connected ordinal cardinal set
0 + 1 is epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() Element of NAT
{ b₁ where b₁ is epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() Element of NAT : ( b₁ in dom A & c2 in A . b₁ ) } is set
z is set
x is epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() Element of NAT
A . x is Element of bool X
c1 is set
dom A is finite Element of bool NAT
c2 is set
A . c2 is set
{ b₁ where b₁ is epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() Element of NAT : ( b₁ in dom A & c1 in A . b₁ ) } is set
{c2} is non empty trivial finite 1 -element set
card {c2} is non empty epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() Element of omega
(A,c1) is epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() set
{ b₁ where b₁ is epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() Element of NAT : ( b₁ in dom A & c1 in A . b₁ ) } is set
card { b₁ where b₁ is epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() Element of NAT : ( b₁ in dom A & c1 in A . b₁ ) } is epsilon-transitive epsilon-connected ordinal cardinal set
{ b₁ where b₁ is Element of X : 1 <= (A,b₁) } is set
X is set
bool X is non empty set
A is Element of bool X
c1 is Element of bool X
<*A,c1*> is non empty Relation-like NAT -defined bool X -valued Function-like finite 2 -element FinSequence-like FinSubsequence-like FinSequence of bool X
(X,<*A,c1*>,2) is Element of bool X
(X,A,c1) is Element of bool X
len <*A,c1*> is non empty epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() Element of NAT
rng <*A,c1*> is finite Element of bool (bool X)
bool (bool X) is non empty set
{A,c1} is finite set
meet {A,c1} is set
X is set
bool X is non empty set
A is Element of bool X
c1 is Element of bool X
<*A,c1*> is non empty Relation-like NAT -defined bool X -valued Function-like finite 2 -element FinSequence-like FinSubsequence-like FinSequence of bool X
(X,<*A,c1*>,1) is Element of bool X
(X,A,c1) is Element of bool X
len <*A,c1*> is non empty epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() Element of NAT
rng <*A,c1*> is finite Element of bool (bool X)
bool (bool X) is non empty set
{A,c1} is finite set
union {A,c1} is set
Union <*A,c1*> is Element of bool X
union (rng <*A,c1*>) is Element of bool X
X is set
bool X is non empty set
A is Element of bool X
[:X,A:] is set
bool [:X,A:] is non empty set
c1 is Relation-like X -defined A -valued Element of bool [:X,A:]
[:X,X:] is set
bool [:X,X:] is non empty set
X is ()
the carrier of X is set
the of X is Element of bool the carrier of X
bool the carrier of X is non empty set
the of X is Relation-like the carrier of X -defined the of X -valued Element of bool [: the carrier of X, the of X:]
[: the carrier of X, the of X:] is set
bool [: the carrier of X, the of X:] is non empty set
( the carrier of X, the of X, the of X) is Relation-like the carrier of X -defined the carrier of X -valued Element of bool [: the carrier of X, the carrier of X:]
[: the carrier of X, the carrier of X:] is set
bool [: the carrier of X, the carrier of X:] is non empty set
A is Element of the carrier of X
( the carrier of X,( the carrier of X, the of X, the of X),A) is Element of bool the carrier of X
{A} is non empty trivial finite 1 -element set
( the carrier of X, the of X, the of X) .: {A} is set
( the carrier of X, the of X, the of X) ~ is Relation-like the carrier of X -defined the carrier of X -valued Element of bool [: the carrier of X, the carrier of X:]
( the carrier of X,(( the carrier of X, the of X, the of X) ~),A) is Element of bool the carrier of X
(( the carrier of X, the of X, the of X) ~) .: {A} is set
X is ()
the carrier of X is set
A is Element of the carrier of X
c1 is Element of the carrier of X
(X,c1) is Element of bool the carrier of X
bool the carrier of X is non empty set
the of X is Element of bool the carrier of X
the of X is Relation-like the carrier of X -defined the of X -valued Element of bool [: the carrier of X, the of X:]
[: the carrier of X, the of X:] is set
bool [: the carrier of X, the of X:] is non empty set
( the carrier of X, the of X, the of X) is Relation-like the carrier of X -defined the carrier of X -valued Element of bool [: the carrier of X, the carrier of X:]
[: the carrier of X, the carrier of X:] is set
bool [: the carrier of X, the carrier of X:] is non empty set
( the carrier of X,( the carrier of X, the of X, the of X),c1) is Element of bool the carrier of X
{c1} is non empty trivial finite 1 -element set
( the carrier of X, the of X, the of X) .: {c1} is set
(X,A) is Element of bool the carrier of X
( the carrier of X, the of X, the of X) ~ is Relation-like the carrier of X -defined the carrier of X -valued Element of bool [: the carrier of X, the carrier of X:]
( the carrier of X,(( the carrier of X, the of X, the of X) ~),A) is Element of bool the carrier of X
{A} is non empty trivial finite 1 -element set
(( the carrier of X, the of X, the of X) ~) .: {A} is set
[c1,A] is set
{c1,A} is finite set
{{c1,A},{c1}} is finite V37() set
[A,c1] is set
{A,c1} is finite set
{{A,c1},{A}} is finite V37() set
X is ()
the carrier of X is set
A is Element of the carrier of X
(X,A) is Element of bool the carrier of X
bool the carrier of X is non empty set
the of X is Element of bool the carrier of X
the of X is Relation-like the carrier of X -defined the of X -valued Element of bool [: the carrier of X, the of X:]
[: the carrier of X, the of X:] is set
bool [: the carrier of X, the of X:] is non empty set
( the carrier of X, the of X, the of X) is Relation-like the carrier of X -defined the carrier of X -valued Element of bool [: the carrier of X, the carrier of X:]
[: the carrier of X, the carrier of X:] is set
bool [: the carrier of X, the carrier of X:] is non empty set
( the carrier of X,( the carrier of X, the of X, the of X),A) is Element of bool the carrier of X
{A} is non empty trivial finite 1 -element set
( the carrier of X, the of X, the of X) .: {A} is set
the non empty finite set is non empty finite set
bool the non empty finite set is non empty finite V37() set
the finite Element of bool the non empty finite set is finite Element of bool the non empty finite set
[: the non empty finite set , the finite Element of bool the non empty finite set :] is finite set
bool [: the non empty finite set , the finite Element of bool the non empty finite set :] is non empty finite V37() set
the Relation-like the non empty finite set -defined the finite Element of bool the non empty finite set -valued finite Element of bool [: the non empty finite set , the finite Element of bool the non empty finite set :] is Relation-like the non empty finite set -defined the finite Element of bool the non empty finite set -valued finite Element of bool [: the non empty finite set , the finite Element of bool the non empty finite set :]
( the non empty finite set , the finite Element of bool the non empty finite set , the Relation-like the non empty finite set -defined the finite Element of bool the non empty finite set -valued finite Element of bool [: the non empty finite set , the finite Element of bool the non empty finite set :]) is () ()
c2 is () ()
the carrier of c2 is set
X is () ()
the carrier of X is set
A is Element of the carrier of X
(X,A) is Element of bool the carrier of X
bool the carrier of X is non empty set
the of X is Element of bool the carrier of X
the of X is Relation-like the carrier of X -defined the of X -valued Element of bool [: the carrier of X, the of X:]
[: the carrier of X, the of X:] is set
bool [: the carrier of X, the of X:] is non empty set
( the carrier of X, the of X, the of X) is Relation-like the carrier of X -defined the carrier of X -valued Element of bool [: the carrier of X, the carrier of X:]
[: the carrier of X, the carrier of X:] is set
bool [: the carrier of X, the carrier of X:] is non empty set
( the carrier of X,( the carrier of X, the of X, the of X),A) is Element of bool the carrier of X
{A} is non empty trivial finite 1 -element set
( the carrier of X, the of X, the of X) .: {A} is set
X is ()
the of X is Element of bool the carrier of X
the carrier of X is set
bool the carrier of X is non empty set
A is Relation-like NAT -defined the of X -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the of X
rng A is finite Element of bool the of X
bool the of X is non empty set
{ b₁ where b₁ is Element of the carrier of X : rng A c= (X,b₁) } is set
c1 is set
c2 is Element of the carrier of X
(X,c2) is Element of bool the carrier of X
the of X is Relation-like the carrier of X -defined the of X -valued Element of bool [: the carrier of X, the of X:]
[: the carrier of X, the of X:] is set
bool [: the carrier of X, the of X:] is non empty set
( the carrier of X, the of X, the of X) is Relation-like the carrier of X -defined the carrier of X -valued Element of bool [: the carrier of X, the carrier of X:]
[: the carrier of X, the carrier of X:] is set
bool [: the carrier of X, the carrier of X:] is non empty set
( the carrier of X,( the carrier of X, the of X, the of X),c2) is Element of bool the carrier of X
{c2} is non empty trivial finite 1 -element set
( the carrier of X, the of X, the of X) .: {c2} is set
{ b₁ where b₁ is Element of the carrier of X : (X,b₁) c= rng A } is set
c1 is set
c2 is Element of the carrier of X
(X,c2) is Element of bool the carrier of X
the of X is Relation-like the carrier of X -defined the of X -valued Element of bool [: the carrier of X, the of X:]
[: the carrier of X, the of X:] is set
bool [: the carrier of X, the of X:] is non empty set
( the carrier of X, the of X, the of X) is Relation-like the carrier of X -defined the carrier of X -valued Element of bool [: the carrier of X, the carrier of X:]
[: the carrier of X, the carrier of X:] is set
bool [: the carrier of X, the carrier of X:] is non empty set
( the carrier of X,( the carrier of X, the of X, the of X),c2) is Element of bool the carrier of X
{c2} is non empty trivial finite 1 -element set
( the carrier of X, the of X, the of X) .: {c2} is set
{ b₁ where b₁ is Element of the carrier of X : (X,b₁) = rng A } is set
c1 is set
c2 is Element of the carrier of X
(X,c2) is Element of bool the carrier of X
the of X is Relation-like the carrier of X -defined the of X -valued Element of bool [: the carrier of X, the of X:]
[: the carrier of X, the of X:] is set
bool [: the carrier of X, the of X:] is non empty set
( the carrier of X, the of X, the of X) is Relation-like the carrier of X -defined the carrier of X -valued Element of bool [: the carrier of X, the carrier of X:]
[: the carrier of X, the carrier of X:] is set
bool [: the carrier of X, the carrier of X:] is non empty set
( the carrier of X,( the carrier of X, the of X, the of X),c2) is Element of bool the carrier of X
{c2} is non empty trivial finite 1 -element set
( the carrier of X, the of X, the of X) .: {c2} is set
c1 is epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() set
{ b₁ where b₁ is Element of the carrier of X : card ((rng A) \ (X,b₁)) <= c1 } is set
c2 is set
z is Element of the carrier of X
(X,z) is Element of bool the carrier of X
the of X is Relation-like the carrier of X -defined the of X -valued Element of bool [: the carrier of X, the of X:]
[: the carrier of X, the of X:] is set
bool [: the carrier of X, the of X:] is non empty set
( the carrier of X, the of X, the of X) is Relation-like the carrier of X -defined the carrier of X -valued Element of bool [: the carrier of X, the carrier of X:]
[: the carrier of X, the carrier of X:] is set
bool [: the carrier of X, the carrier of X:] is non empty set
( the carrier of X,( the carrier of X, the of X, the of X),z) is Element of bool the carrier of X
{z} is non empty trivial finite 1 -element set
( the carrier of X, the of X, the of X) .: {z} is set
(rng A) \ (X,z) is finite Element of bool the of X
card ((rng A) \ (X,z)) is epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() Element of omega
X is () ()
the of X is Element of bool the carrier of X
the carrier of X is set
bool the carrier of X is non empty set
A is Relation-like NAT -defined the of X -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the of X
rng A is finite Element of bool the of X
bool the of X is non empty set
c1 is epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() set
{ b₁ where b₁ is Element of the carrier of X : card ((X,b₁) \ (rng A)) <= c1 } is set
c2 is set
z is Element of the carrier of X
(X,z) is finite Element of bool the carrier of X
the of X is Relation-like the carrier of X -defined the of X -valued Element of bool [: the carrier of X, the of X:]
[: the carrier of X, the of X:] is set
bool [: the carrier of X, the of X:] is non empty set
( the carrier of X, the of X, the of X) is Relation-like the carrier of X -defined the carrier of X -valued Element of bool [: the carrier of X, the carrier of X:]
[: the carrier of X, the carrier of X:] is set
bool [: the carrier of X, the carrier of X:] is non empty set
( the carrier of X,( the carrier of X, the of X, the of X),z) is Element of bool the carrier of X
{z} is non empty trivial finite 1 -element set
( the carrier of X, the of X, the of X) .: {z} is set
(X,z) \ (rng A) is finite Element of bool the carrier of X
card ((X,z) \ (rng A)) is epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() Element of omega
c2 is epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() set
{ b₁ where b₁ is Element of the carrier of X : ( card ((X,b₁) \ (rng A)) <= c1 & card ((rng A) \ (X,b₁)) <= c2 ) } is set
z is set
x is Element of the carrier of X
(X,x) is finite Element of bool the carrier of X
the of X is Relation-like the carrier of X -defined the of X -valued Element of bool [: the carrier of X, the of X:]
[: the carrier of X, the of X:] is set
bool [: the carrier of X, the of X:] is non empty set
( the carrier of X, the of X, the of X) is Relation-like the carrier of X -defined the carrier of X -valued Element of bool [: the carrier of X, the carrier of X:]
[: the carrier of X, the carrier of X:] is set
bool [: the carrier of X, the carrier of X:] is non empty set
( the carrier of X,( the carrier of X, the of X, the of X),x) is Element of bool the carrier of X
{x} is non empty trivial finite 1 -element set
( the carrier of X, the of X, the of X) .: {x} is set
(X,x) \ (rng A) is finite Element of bool the carrier of X
card ((X,x) \ (rng A)) is epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() Element of omega
(rng A) \ (X,x) is finite Element of bool the of X
card ((rng A) \ (X,x)) is epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() Element of omega
X is ()
the of X is Element of bool the carrier of X
the carrier of X is set
bool the carrier of X is non empty set
A is Relation-like NAT -defined the of X -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the of X
(X,A,0) is Element of bool the carrier of X
(X,A) is Element of bool the carrier of X
rng A is finite Element of bool the of X
bool the of X is non empty set
{ b₁ where b₁ is Element of the carrier of X : card ((rng A) \ (X,b₁)) <= 0 } is set
{ b₁ where b₁ is Element of the carrier of X : rng A c= (X,b₁) } is set
c1 is set
c2 is Element of the carrier of X
(X,c2) is Element of bool the carrier of X
the of X is Relation-like the carrier of X -defined the of X -valued Element of bool [: the carrier of X, the of X:]
[: the carrier of X, the of X:] is set
bool [: the carrier of X, the of X:] is non empty set
( the carrier of X, the of X, the of X) is Relation-like the carrier of X -defined the carrier of X -valued Element of bool [: the carrier of X, the carrier of X:]
[: the carrier of X, the carrier of X:] is set
bool [: the carrier of X, the carrier of X:] is non empty set
( the carrier of X,( the carrier of X, the of X, the of X),c2) is Element of bool the carrier of X
{c2} is non empty trivial finite 1 -element set
( the carrier of X, the of X, the of X) .: {c2} is set
(rng A) \ (X,c2) is finite Element of bool the of X
card ((rng A) \ (X,c2)) is epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() Element of omega
c1 is set
c2 is Element of the carrier of X
(X,c2) is Element of bool the carrier of X
the of X is Relation-like the carrier of X -defined the of X -valued Element of bool [: the carrier of X, the of X:]
[: the carrier of X, the of X:] is set
bool [: the carrier of X, the of X:] is non empty set
( the carrier of X, the of X, the of X) is Relation-like the carrier of X -defined the carrier of X -valued Element of bool [: the carrier of X, the carrier of X:]
[: the carrier of X, the carrier of X:] is set
bool [: the carrier of X, the carrier of X:] is non empty set
( the carrier of X,( the carrier of X, the of X, the of X),c2) is Element of bool the carrier of X
{c2} is non empty trivial finite 1 -element set
( the carrier of X, the of X, the of X) .: {c2} is set
(rng A) \ (X,c2) is finite Element of bool the of X
card ((rng A) \ (X,c2)) is epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() Element of omega
X is () ()
the of X is Element of bool the carrier of X
the carrier of X is set
bool the carrier of X is non empty set
A is Relation-like NAT -defined the of X -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the of X
(X,A,0) is Element of bool the carrier of X
(X,A) is Element of bool the carrier of X
rng A is finite Element of bool the of X
bool the of X is non empty set
{ b₁ where b₁ is Element of the carrier of X : card ((X,b₁) \ (rng A)) <= 0 } is set
{ b₁ where b₁ is Element of the carrier of X : (X,b₁) c= rng A } is set
c1 is set
c2 is Element of the carrier of X
(X,c2) is finite Element of bool the carrier of X
the of X is Relation-like the carrier of X -defined the of X -valued Element of bool [: the carrier of X, the of X:]
[: the carrier of X, the of X:] is set
bool [: the carrier of X, the of X:] is non empty set
( the carrier of X, the of X, the of X) is Relation-like the carrier of X -defined the carrier of X -valued Element of bool [: the carrier of X, the carrier of X:]
[: the carrier of X, the carrier of X:] is set
bool [: the carrier of X, the carrier of X:] is non empty set
( the carrier of X,( the carrier of X, the of X, the of X),c2) is Element of bool the carrier of X
{c2} is non empty trivial finite 1 -element set
( the carrier of X, the of X, the of X) .: {c2} is set
(X,c2) \ (rng A) is finite Element of bool the carrier of X
card ((X,c2) \ (rng A)) is epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() Element of omega
c1 is set
c2 is Element of the carrier of X
(X,c2) is finite Element of bool the carrier of X
the of X is Relation-like the carrier of X -defined the of X -valued Element of bool [: the carrier of X, the of X:]
[: the carrier of X, the of X:] is set
bool [: the carrier of X, the of X:] is non empty set
( the carrier of X, the of X, the of X) is Relation-like the carrier of X -defined the carrier of X -valued Element of bool [: the carrier of X, the carrier of X:]
[: the carrier of X, the carrier of X:] is set
bool [: the carrier of X, the carrier of X:] is non empty set
( the carrier of X,( the carrier of X, the of X, the of X),c2) is Element of bool the carrier of X
{c2} is non empty trivial finite 1 -element set
( the carrier of X, the of X, the of X) .: {c2} is set
(X,c2) \ (rng A) is finite Element of bool the carrier of X
card ((X,c2) \ (rng A)) is epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() Element of omega
X is () ()
the of X is Element of bool the carrier of X
the carrier of X is set
bool the carrier of X is non empty set
A is Relation-like NAT -defined the of X -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the of X
(X,A,0,0) is Element of bool the carrier of X
(X,A) is Element of bool the carrier of X
rng A is finite Element of bool the of X
bool the of X is non empty set
{ b₁ where b₁ is Element of the carrier of X : ( card ((X,b₁) \ (rng A)) <= 0 & card ((rng A) \ (X,b₁)) <= 0 ) } is set
{ b₁ where b₁ is Element of the carrier of X : (X,b₁) = rng A } is set
c1 is set
c2 is Element of the carrier of X
(X,c2) is finite Element of bool the carrier of X
the of X is Relation-like the carrier of X -defined the of X -valued Element of bool [: the carrier of X, the of X:]
[: the carrier of X, the of X:] is set
bool [: the carrier of X, the of X:] is non empty set
( the carrier of X, the of X, the of X) is Relation-like the carrier of X -defined the carrier of X -valued Element of bool [: the carrier of X, the carrier of X:]
[: the carrier of X, the carrier of X:] is set
bool [: the carrier of X, the carrier of X:] is non empty set
( the carrier of X,( the carrier of X, the of X, the of X),c2) is Element of bool the carrier of X
{c2} is non empty trivial finite 1 -element set
( the carrier of X, the of X, the of X) .: {c2} is set
(X,c2) \ (rng A) is finite Element of bool the carrier of X
card ((X,c2) \ (rng A)) is epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() Element of omega
(rng A) \ (X,c2) is finite Element of bool the of X
card ((rng A) \ (X,c2)) is epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() Element of omega
c1 is set
c2 is Element of the carrier of X
(X,c2) is finite Element of bool the carrier of X
the of X is Relation-like the carrier of X -defined the of X -valued Element of bool [: the carrier of X, the of X:]
[: the carrier of X, the of X:] is set
bool [: the carrier of X, the of X:] is non empty set
( the carrier of X, the of X, the of X) is Relation-like the carrier of X -defined the carrier of X -valued Element of bool [: the carrier of X, the carrier of X:]
[: the carrier of X, the carrier of X:] is set
bool [: the carrier of X, the carrier of X:] is non empty set
( the carrier of X,( the carrier of X, the of X, the of X),c2) is Element of bool the carrier of X
{c2} is non empty trivial finite 1 -element set
( the carrier of X, the of X, the of X) .: {c2} is set
(X,c2) \ (rng A) is finite Element of bool the carrier of X
(rng A) \ (X,c2) is finite Element of bool the of X
card ((X,c2) \ (rng A)) is epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() Element of omega
card ((rng A) \ (X,c2)) is epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() Element of omega
X is epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() set
A is epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() set
c1 is ()
the of c1 is Element of bool the carrier of c1
the carrier of c1 is set
bool the carrier of c1 is non empty set
c2 is Relation-like NAT -defined the of c1 -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the of c1
(c1,c2,X) is Element of bool the carrier of c1
(c1,c2,A) is Element of bool the carrier of c1
z is set
rng c2 is finite Element of bool the of c1
bool the of c1 is non empty set
{ b₁ where b₁ is Element of the carrier of c1 : card ((rng c2) \ (c1,b₁)) <= X } is set
x is Element of the carrier of c1
(c1,x) is Element of bool the carrier of c1
the of c1 is Relation-like the carrier of c1 -defined the of c1 -valued Element of bool [: the carrier of c1, the of c1:]
[: the carrier of c1, the of c1:] is set
bool [: the carrier of c1, the of c1:] is non empty set
( the carrier of c1, the of c1, the of c1) is Relation-like the carrier of c1 -defined the carrier of c1 -valued Element of bool [: the carrier of c1, the carrier of c1:]
[: the carrier of c1, the carrier of c1:] is set
bool [: the carrier of c1, the carrier of c1:] is non empty set
( the carrier of c1,( the carrier of c1, the of c1, the of c1),x) is Element of bool the carrier of c1
{x} is non empty trivial finite 1 -element set
( the carrier of c1, the of c1, the of c1) .: {x} is set
(rng c2) \ (c1,x) is finite Element of bool the of c1
card ((rng c2) \ (c1,x)) is epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() Element of omega
{ b₁ where b₁ is Element of the carrier of c1 : card ((rng c2) \ (c1,b₁)) <= A } is set
X is epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() set
A is epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() set
c1 is () ()
the of c1 is Element of bool the carrier of c1
the carrier of c1 is set
bool the carrier of c1 is non empty set
c2 is Relation-like NAT -defined the of c1 -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the of c1
(c1,c2,X) is Element of bool the carrier of c1
(c1,c2,A) is Element of bool the carrier of c1
z is set
rng c2 is finite Element of bool the of c1
bool the of c1 is non empty set
{ b₁ where b₁ is Element of the carrier of c1 : card ((c1,b₁) \ (rng c2)) <= X } is set
x is Element of the carrier of c1
(c1,x) is finite Element of bool the carrier of c1
the of c1 is Relation-like the carrier of c1 -defined the of c1 -valued Element of bool [: the carrier of c1, the of c1:]
[: the carrier of c1, the of c1:] is set
bool [: the carrier of c1, the of c1:] is non empty set
( the carrier of c1, the of c1, the of c1) is Relation-like the carrier of c1 -defined the carrier of c1 -valued Element of bool [: the carrier of c1, the carrier of c1:]
[: the carrier of c1, the carrier of c1:] is set
bool [: the carrier of c1, the carrier of c1:] is non empty set
( the carrier of c1,( the carrier of c1, the of c1, the of c1),x) is Element of bool the carrier of c1
{x} is non empty trivial finite 1 -element set
( the carrier of c1, the of c1, the of c1) .: {x} is set
(c1,x) \ (rng c2) is finite Element of bool the carrier of c1
card ((c1,x) \ (rng c2)) is epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() Element of omega
{ b₁ where b₁ is Element of the carrier of c1 : card ((c1,b₁) \ (rng c2)) <= A } is set
X is () ()
the of X is Element of bool the carrier of X
the carrier of X is set
bool the carrier of X is non empty set
A is Relation-like NAT -defined the of X -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the of X
c1 is epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() set
z is epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() set
c2 is epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() set
x is epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() set
(X,A,c1,c2) is Element of bool the carrier of X
(X,A,z,x) is Element of bool the carrier of X
s is set
rng A is finite Element of bool the of X
bool the of X is non empty set
{ b₁ where b₁ is Element of the carrier of X : ( card ((X,b₁) \ (rng A)) <= c1 & card ((rng A) \ (X,b₁)) <= c2 ) } is set
s is Element of the carrier of X
(X,s) is finite Element of bool the carrier of X
the of X is Relation-like the carrier of X -defined the of X -valued Element of bool [: the carrier of X, the of X:]
[: the carrier of X, the of X:] is set
bool [: the carrier of X, the of X:] is non empty set
( the carrier of X, the of X, the of X) is Relation-like the carrier of X -defined the carrier of X -valued Element of bool [: the carrier of X, the carrier of X:]
[: the carrier of X, the carrier of X:] is set
bool [: the carrier of X, the carrier of X:] is non empty set
( the carrier of X,( the carrier of X, the of X, the of X),s) is Element of bool the carrier of X
{s} is non empty trivial finite 1 -element set
( the carrier of X, the of X, the of X) .: {s} is set
(X,s) \ (rng A) is finite Element of bool the carrier of X
card ((X,s) \ (rng A)) is epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() Element of omega
(rng A) \ (X,s) is finite Element of bool the of X
card ((rng A) \ (X,s)) is epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() Element of omega
{ b₁ where b₁ is Element of the carrier of X : ( card ((X,b₁) \ (rng A)) <= z & card ((rng A) \ (X,b₁)) <= x ) } is set
X is epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() set
A is ()
the of A is Element of bool the carrier of A
the carrier of A is set
bool the carrier of A is non empty set
c1 is Relation-like NAT -defined the of A -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the of A
(A,c1) is Element of bool the carrier of A
(A,c1,X) is Element of bool the carrier of A
(A,c1,0) is Element of bool the carrier of A
X is epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() set
A is () ()
the of A is Element of bool the carrier of A
the carrier of A is set
bool the carrier of A is non empty set
c1 is Relation-like NAT -defined the of A -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the of A
(A,c1) is Element of bool the carrier of A
(A,c1,X) is Element of bool the carrier of A
(A,c1,0) is Element of bool the carrier of A
X is epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() set
A is epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() set
c1 is () ()
the of c1 is Element of bool the carrier of c1
the carrier of c1 is set
bool the carrier of c1 is non empty set
c2 is Relation-like NAT -defined the of c1 -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the of c1
(c1,c2) is Element of bool the carrier of c1
(c1,c2,X,A) is Element of bool the carrier of c1
(c1,c2,0,0) is Element of bool the carrier of c1
X is ()
the of X is Element of bool the carrier of X
the carrier of X is set
bool the carrier of X is non empty set
A is Relation-like NAT -defined the of X -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the of X
(X,A) is Element of bool the carrier of X
(X,A) is Element of bool the carrier of X
(X,A) is Element of bool the carrier of X
( the carrier of X,(X,A),(X,A)) is Element of bool the carrier of X
c1 is set
rng A is finite Element of bool the of X
bool the of X is non empty set
{ b₁ where b₁ is Element of the carrier of X : (X,b₁) = rng A } is set
c2 is Element of the carrier of X
(X,c2) is Element of bool the carrier of X
the of X is Relation-like the carrier of X -defined the of X -valued Element of bool [: the carrier of X, the of X:]
[: the carrier of X, the of X:] is set
bool [: the carrier of X, the of X:] is non empty set
( the carrier of X, the of X, the of X) is Relation-like the carrier of X -defined the carrier of X -valued Element of bool [: the carrier of X, the carrier of X:]
[: the carrier of X, the carrier of X:] is set
bool [: the carrier of X, the carrier of X:] is non empty set
( the carrier of X,( the carrier of X, the of X, the of X),c2) is Element of bool the carrier of X
{c2} is non empty trivial finite 1 -element set
( the carrier of X, the of X, the of X) .: {c2} is set
{ b₁ where b₁ is Element of the carrier of X : rng A c= (X,b₁) } is set
{ b₁ where b₁ is Element of the carrier of X : (X,b₁) c= rng A } is set
c1 is set
rng A is finite Element of bool the of X
bool the of X is non empty set
{ b₁ where b₁ is Element of the carrier of X : (X,b₁) c= rng A } is set
c2 is Element of the carrier of X
(X,c2) is Element of bool the carrier of X
the of X is Relation-like the carrier of X -defined the of X -valued Element of bool [: the carrier of X, the of X:]
[: the carrier of X, the of X:] is set
bool [: the carrier of X, the of X:] is non empty set
( the carrier of X, the of X, the of X) is Relation-like the carrier of X -defined the carrier of X -valued Element of bool [: the carrier of X, the carrier of X:]
[: the carrier of X, the carrier of X:] is set
bool [: the carrier of X, the carrier of X:] is non empty set
( the carrier of X,( the carrier of X, the of X, the of X),c2) is Element of bool the carrier of X
{c2} is non empty trivial finite 1 -element set
( the carrier of X, the of X, the of X) .: {c2} is set
{ b₁ where b₁ is Element of the carrier of X : rng A c= (X,b₁) } is set
z is Element of the carrier of X
(X,z) is Element of bool the carrier of X
( the carrier of X,( the carrier of X, the of X, the of X),z) is Element of bool the carrier of X
{z} is non empty trivial finite 1 -element set
( the carrier of X, the of X, the of X) .: {z} is set
{ b₁ where b₁ is Element of the carrier of X : (X,b₁) = rng A } is set
X is epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() set
A is epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() set
c1 is () ()
the of c1 is Element of bool the carrier of c1
the carrier of c1 is set
bool the carrier of c1 is non empty set
c2 is Relation-like NAT -defined the of c1 -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the of c1
(c1,c2,X,A) is Element of bool the carrier of c1
(c1,c2,A) is Element of bool the carrier of c1
(c1,c2,X) is Element of bool the carrier of c1
( the carrier of c1,(c1,c2,A),(c1,c2,X)) is Element of bool the carrier of c1
z is set
rng c2 is finite Element of bool the of c1
bool the of c1 is non empty set
{ b₁ where b₁ is Element of the carrier of c1 : ( card ((c1,b₁) \ (rng c2)) <= X & card ((rng c2) \ (c1,b₁)) <= A ) } is set
x is Element of the carrier of c1
(c1,x) is finite Element of bool the carrier of c1
the of c1 is Relation-like the carrier of c1 -defined the of c1 -valued Element of bool [: the carrier of c1, the of c1:]
[: the carrier of c1, the of c1:] is set
bool [: the carrier of c1, the of c1:] is non empty set
( the carrier of c1, the of c1, the of c1) is Relation-like the carrier of c1 -defined the carrier of c1 -valued Element of bool [: the carrier of c1, the carrier of c1:]
[: the carrier of c1, the carrier of c1:] is set
bool [: the carrier of c1, the carrier of c1:] is non empty set
( the carrier of c1,( the carrier of c1, the of c1, the of c1),x) is Element of bool the carrier of c1
{x} is non empty trivial finite 1 -element set
( the carrier of c1, the of c1, the of c1) .: {x} is set
(c1,x) \ (rng c2) is finite Element of bool the carrier of c1
card ((c1,x) \ (rng c2)) is epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() Element of omega
(rng c2) \ (c1,x) is finite Element of bool the of c1
card ((rng c2) \ (c1,x)) is epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() Element of omega
{ b₁ where b₁ is Element of the carrier of c1 : card ((rng c2) \ (c1,b₁)) <= A } is set
{ b₁ where b₁ is Element of the carrier of c1 : card ((c1,b₁) \ (rng c2)) <= X } is set
z is set
rng c2 is finite Element of bool the of c1
bool the of c1 is non empty set
{ b₁ where b₁ is Element of the carrier of c1 : card ((c1,b₁) \ (rng c2)) <= X } is set
{ b₁ where b₁ is Element of the carrier of c1 : card ((rng c2) \ (c1,b₁)) <= A } is set
{ b₁ where b₁ is Element of the carrier of c1 : ( card ((c1,b₁) \ (rng c2)) <= X & card ((rng c2) \ (c1,b₁)) <= A ) } is set
x is Element of the carrier of c1
(c1,x) is finite Element of bool the carrier of c1
the of c1 is Relation-like the carrier of c1 -defined the of c1 -valued Element of bool [: the carrier of c1, the of c1:]
[: the carrier of c1, the of c1:] is set
bool [: the carrier of c1, the of c1:] is non empty set
( the carrier of c1, the of c1, the of c1) is Relation-like the carrier of c1 -defined the carrier of c1 -valued Element of bool [: the carrier of c1, the carrier of c1:]
[: the carrier of c1, the carrier of c1:] is set
bool [: the carrier of c1, the carrier of c1:] is non empty set
( the carrier of c1,( the carrier of c1, the of c1, the of c1),x) is Element of bool the carrier of c1
{x} is non empty trivial finite 1 -element set
( the carrier of c1, the of c1, the of c1) .: {x} is set
(rng c2) \ (c1,x) is finite Element of bool the of c1
card ((rng c2) \ (c1,x)) is epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() Element of omega
s is Element of the carrier of c1
(c1,s) is finite Element of bool the carrier of c1
( the carrier of c1,( the carrier of c1, the of c1, the of c1),s) is Element of bool the carrier of c1
{s} is non empty trivial finite 1 -element set
( the carrier of c1, the of c1, the of c1) .: {s} is set
(c1,s) \ (rng c2) is finite Element of bool the carrier of c1
card ((c1,s) \ (rng c2)) is epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() Element of omega
X is ()
the of X is Element of bool the carrier of X
the carrier of X is set
bool the carrier of X is non empty set
A is Relation-like NAT -defined the of X -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the of X
(X,A) is Element of bool the carrier of X
rng A is finite Element of bool the of X
bool the of X is non empty set
{ (X,b₁) where b₁ is Element of the carrier of X : b₁ in rng A } is set
meet { (X,b₁) where b₁ is Element of the carrier of X : b₁ in rng A } is set
c1 is set
c2 is Element of the carrier of X
(X,c2) is Element of bool the carrier of X
the of X is Relation-like the carrier of X -defined the of X -valued Element of bool [: the carrier of X, the of X:]
[: the carrier of X, the of X:] is set
bool [: the carrier of X, the of X:] is non empty set
( the carrier of X, the of X, the of X) is Relation-like the carrier of X -defined the carrier of X -valued Element of bool [: the carrier of X, the carrier of X:]
[: the carrier of X, the carrier of X:] is set
bool [: the carrier of X, the carrier of X:] is non empty set
( the carrier of X, the of X, the of X) ~ is Relation-like the carrier of X -defined the carrier of X -valued Element of bool [: the carrier of X, the carrier of X:]
( the carrier of X,(( the carrier of X, the of X, the of X) ~),c2) is Element of bool the carrier of X
{c2} is non empty trivial finite 1 -element set
(( the carrier of X, the of X, the of X) ~) .: {c2} is set
z is set
{ b₁ where b₁ is Element of the carrier of X : rng A c= (X,b₁) } is set
x is Element of the carrier of X
(X,x) is Element of bool the carrier of X
( the carrier of X,( the carrier of X, the of X, the of X),x) is Element of bool the carrier of X
{x} is non empty trivial finite 1 -element set
( the carrier of X, the of X, the of X) .: {x} is set
s is set
s is Element of the carrier of X
(X,s) is Element of bool the carrier of X
( the carrier of X,(( the carrier of X, the of X, the of X) ~),s) is Element of bool the carrier of X
{s} is non empty trivial finite 1 -element set
(( the carrier of X, the of X, the of X) ~) .: {s} is set
z is set
x is Element of the carrier of X
(X,x) is Element of bool the carrier of X
( the carrier of X,( the carrier of X, the of X, the of X),x) is Element of bool the carrier of X
{x} is non empty trivial finite 1 -element set
( the carrier of X, the of X, the of X) .: {x} is set
s is set
s is Element of the carrier of X
(X,s) is Element of bool the carrier of X
( the carrier of X,(( the carrier of X, the of X, the of X) ~),s) is Element of bool the carrier of X
{s} is non empty trivial finite 1 -element set
(( the carrier of X, the of X, the of X) ~) .: {s} is set
{ b₁ where b₁ is Element of the carrier of X : rng A c= (X,b₁) } is set
X is ()
the of X is Element of bool the carrier of X
the carrier of X is set
bool the carrier of X is non empty set
A is Relation-like NAT -defined the of X -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the of X
(X,A) is Element of bool the carrier of X
c1 is Element of the carrier of X
c2 is Element of the carrier of X
<*c1,c2*> is non empty Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like set
(X,c1) is Element of bool the carrier of X
the of X is Relation-like the carrier of X -defined the of X -valued Element of bool [: the carrier of X, the of X:]
[: the carrier of X, the of X:] is set
bool [: the carrier of X, the of X:] is non empty set
( the carrier of X, the of X, the of X) is Relation-like the carrier of X -defined the carrier of X -valued Element of bool [: the carrier of X, the carrier of X:]
[: the carrier of X, the carrier of X:] is set
bool [: the carrier of X, the carrier of X:] is non empty set
( the carrier of X, the of X, the of X) ~ is Relation-like the carrier of X -defined the carrier of X -valued Element of bool [: the carrier of X, the carrier of X:]
( the carrier of X,(( the carrier of X, the of X, the of X) ~),c1) is Element of bool the carrier of X
{c1} is non empty trivial finite 1 -element set
(( the carrier of X, the of X, the of X) ~) .: {c1} is set
(X,c2) is Element of bool the carrier of X
( the carrier of X,(( the carrier of X, the of X, the of X) ~),c2) is Element of bool the carrier of X
{c2} is non empty trivial finite 1 -element set
(( the carrier of X, the of X, the of X) ~) .: {c2} is set
( the carrier of X,(X,c1),(X,c2)) is Element of bool the carrier of X
rng A is finite Element of bool the of X
bool the of X is non empty set
{c1,c2} is finite set
{ (X,b₁) where b₁ is Element of the carrier of X : b₁ in rng A } is set
{(X,c1),(X,c2)} is finite set
z is set
x is Element of the carrier of X
(X,x) is Element of bool the carrier of X
( the carrier of X,(( the carrier of X, the of X, the of X) ~),x) is Element of bool the carrier of X
{x} is non empty trivial finite 1 -element set
(( the carrier of X, the of X, the of X) ~) .: {x} is set
z is set
meet { (X,b₁) where b₁ is Element of the carrier of X : b₁ in rng A } is set