:: MMLQUERY semantic presentation

REAL is set

bool REAL is non empty set

bool omega is non empty non trivial non finite set
bool NAT is non empty non trivial non finite set

bool is non empty set
bool () is non empty set
{} is set

dom {} is set
rng {} is 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

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

c1 is Element of bool X
A .: c1 is set
A .: c1 is Element of bool X
{ (X,A,b1) where b1 is Element of X : b1 in c1 } is set
union { (X,A,b1) where b1 is Element of X : b1 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,b1) where b1 is Element of X : b1 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
{ b1 where b1 is Element of X : ex b2 being Element of X st
( (b1,b2,A) & b1 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:]
{ b1 where b1 is Element of X : ( card (X,A,b1) = card (X,c2,b1) & b1 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

(X,c2,x) is Element of bool X
c2 .: {x} is set

{ b1 where b1 is Element of X : ( card (X,A,b1) c= card (X,c2,b1) & b1 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

(X,c2,x) is Element of bool X
c2 .: {x} is set

{ b1 where b1 is Element of X : ( card (X,c2,b1) c= card (X,A,b1) & b1 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

(X,A,x) is Element of bool X
A .: {x} is set

{ b1 where b1 is Element of X : ( card (X,A,b1) in card (X,c2,b1) & b1 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

(X,c2,x) is Element of bool X
c2 .: {x} is set

{ b1 where b1 is Element of X : ( card (X,c2,b1) in card (X,A,b1) & b1 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

(X,A,x) is Element of bool X
A .: {x} is 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:]

A is Element of bool X
{ b1 where b1 is Element of X : ( card (X,c1,b1) = c2 & b1 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

{ b1 where b1 is Element of X : ( card (X,c1,b1) c= c2 & b1 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

{ b1 where b1 is Element of X : ( c2 c= card (X,c1,b1) & b1 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

{ b1 where b1 is Element of X : ( card (X,c1,b1) in c2 & b1 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

{ b1 where b1 is Element of X : ( c2 in card (X,c1,b1) & b1 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

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
{ b1 where b1 is Element of X : ex b2 being Element of X st
( (b1,b2,c2) & b1 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
{ b1 where b1 is Element of X : ex b2 being Element of X st
( (b1,b2,c1) & b1 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
{ b1 where b1 is Element of X : ex b2 being Element of X st
( (b1,b2,c1) & b1 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
{ b1 where b1 is Element of X : ex b2 being Element of X st
( (b1,b2,c2) & b1 in c1 )
}
is set

(X,A,c2,z) is Element of bool X
{ b1 where b1 is Element of X : ( z c= card (X,c2,b1) & b1 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

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
{ b1 where b1 is Element of X : ( 1 c= card (X,c1,b1) & b1 in A ) } is set
(X,c1,A) is Element of bool X
{ b1 where b1 is Element of X : ex b2 being Element of X st
( (b1,b2,c1) & b1 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
{ b1 where b1 is Element of X : ex b2 being Element of X st
( (b1,b2,c2) & b1 in c1 )
}
is set

(X,A,c2,z) is Element of bool X
{ b1 where b1 is Element of X : ( z in card (X,c2,b1) & b1 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

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
{ b1 where b1 is Element of X : ( 0 in card (X,c1,b1) & b1 in A ) } is set
(X,c1,A) is Element of bool X
{ b1 where b1 is Element of X : ex b2 being Element of X st
( (b1,b2,c1) & b1 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
{ b1 where b1 is Element of X : ex b2 being Element of X st
( (b1,b2,c2) & b1 in c1 )
}
is set

(X,A,c2,z) is Element of bool X
{ b1 where b1 is Element of X : ( card (X,c2,b1) = z & b1 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

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,(c2 + 1)) is Element of bool X
{ b1 where b1 is Element of X : ( c2 + 1 c= card (X,c1,b1) & b1 in A ) } is set
(X,A,c1,c2) is Element of bool X
{ b1 where b1 is Element of X : ( c2 in card (X,c1,b1) & b1 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

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

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,c2) is Element of bool X
{ b1 where b1 is Element of X : ( card (X,c1,b1) c= c2 & b1 in A ) } is set

(X,A,c1,(c2 + 1)) is Element of bool X
{ b1 where b1 is Element of X : ( card (X,c1,b1) in c2 + 1 & b1 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

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

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,c1,z,x) is Element of bool X
{ b1 where b1 is Element of X : ( x c= card (X,z,b1) & b1 in c1 ) } is set

(X,A,c2,s) is Element of bool X
{ b1 where b1 is Element of X : ( s c= card (X,c2,b1) & b1 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

(X,z,x) is Element of bool X
z .: {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,c1,z,x) is Element of bool X
{ b1 where b1 is Element of X : ( x in card (X,z,b1) & b1 in c1 ) } is set

(X,A,c2,s) is Element of bool X
{ b1 where b1 is Element of X : ( s in card (X,c2,b1) & b1 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

(X,z,x) is Element of bool X
z .: {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,A,z,x) is Element of bool X
{ b1 where b1 is Element of X : ( card (X,z,b1) c= x & b1 in A ) } is set

(X,c1,c2,s) is Element of bool X
{ b1 where b1 is Element of X : ( card (X,c2,b1) c= s & b1 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

(X,c2,x) is Element of bool X
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,A,z,x) is Element of bool X
{ b1 where b1 is Element of X : ( card (X,z,b1) in x & b1 in A ) } is set

(X,c1,c2,s) is Element of bool X
{ b1 where b1 is Element of X : ( card (X,c2,b1) in s & b1 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

(X,c2,x) is Element of bool X
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,x,A,z) is Element of bool X
{ b1 where b1 is Element of X : ( card (X,z,b1) c= card (X,x,b1) & b1 in A ) } is set

(X,s,c1,c2) is Element of bool X
{ b1 where b1 is Element of X : ( card (X,c2,b1) c= card (X,s,b1) & b1 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

(X,x,x) is Element of bool X
x .: {x} is 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

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,x,A,z) is Element of bool X
{ b1 where b1 is Element of X : ( card (X,z,b1) in card (X,x,b1) & b1 in A ) } is set

(X,s,c1,c2) is Element of bool X
{ b1 where b1 is Element of X : ( card (X,c2,b1) in card (X,s,b1) & b1 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

(X,x,x) is Element of bool X
x .: {x} is 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

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,x,c1,z) is Element of bool X
{ b1 where b1 is Element of X : ( card (X,x,b1) c= card (X,z,b1) & b1 in c1 ) } is set

(X,s,A,c2) is Element of bool X
{ b1 where b1 is Element of X : ( card (X,s,b1) c= card (X,c2,b1) & b1 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

(X,c2,x) is Element of bool X
c2 .: {x} is set

(X,z,x) is Element of bool X
z .: {x} is set

(X,x,x) is Element of bool X
x .: {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,x,c1,z) is Element of bool X
{ b1 where b1 is Element of X : ( card (X,x,b1) in card (X,z,b1) & b1 in c1 ) } is set

(X,s,A,c2) is Element of bool X
{ b1 where b1 is Element of X : ( card (X,s,b1) in card (X,c2,b1) & b1 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

(X,c2,x) is Element of bool X
c2 .: {x} is set

(X,z,x) is Element of bool X
z .: {x} is set

(X,x,x) is Element of bool X
x .: {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
{ b1 where b1 is Element of X : ex b2 being Element of X st
( (b1,b2,c1) & b1 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
{ b1 where b1 is Element of X : ( card (X,c2,b1) in card (X,c1,b1) & b1 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

(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 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
{ b1 where b1 is Element of X : ex b2 being Element of X st
( (b1,b2,c2) & b1 in A )
}
is set

(X,z,c1) is Element of bool X
{ b1 where b1 is Element of X : ex b2 being Element of X st
( (b1,b2,z) & b1 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,b1) where b1 is Element of X : b1 in A } is set
union { (X,c1,b1) where b1 is Element of X : b1 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,b1) where b1 is Element of X : b1 in (X,A,c1) } is set
meet { (X,c2,b1) where b1 is Element of X : b1 in (X,A,c1) } is set
(X,c2,A) is Element of bool X
{ (X,c2,b1) where b1 is Element of X : b1 in A } is set
meet { (X,c2,b1) where b1 is Element of X : b1 in A } is set
(X,c2,c1) is Element of bool X
{ (X,c2,b1) where b1 is Element of X : b1 in c1 } is set
meet { (X,c2,b1) where b1 is Element of X : b1 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,b1) where b1 is Element of X : b1 in A } is set
union { (X,c2,b1) where b1 is Element of X : b1 in A } is set

(X,z,c1) is Element of bool X
{ (X,z,b1) where b1 is Element of X : b1 in c1 } is set
union { (X,z,b1) where b1 is Element of X : b1 in c1 } is set
(X,c2,c1) is Element of bool X
{ (X,c2,b1) where b1 is Element of X : b1 in c1 } is set
union { (X,c2,b1) where b1 is Element of X : b1 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,b1) where b1 is Element of X : b1 in A } is set
meet { (X,c1,b1) where b1 is Element of X : b1 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,b1) where b1 is Element of X : b1 in A } is set
meet { (X,c2,b1) where b1 is Element of X : b1 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,b1) where b1 is Element of X : b1 in A } is set
meet { (X,c1,b1) where b1 is Element of X : b1 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),b1) where b1 is Element of X : b1 in A } is set
meet { (X,([:X,X:],c1,c2),b1) where b1 is Element of X : b1 in A } is set
(X,c2,A) is Element of bool X
{ (X,c2,b1) where b1 is Element of X : b1 in A } is set
meet { (X,c2,b1) where b1 is Element of X : b1 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,b1) where b1 is Element of X : b1 in c1 } is set
meet { (X,c2,b1) where b1 is Element of X : b1 in c1 } is set
(X,c2,A) is Element of bool X
{ (X,c2,b1) where b1 is Element of X : b1 in A } is set
meet { (X,c2,b1) where b1 is Element of X : b1 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

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

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,b1) where b1 is Element of X : b1 in z } is set
union { (X,A,b1) where b1 is Element of X : b1 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

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,b1) where b1 is Element of X : b1 in z } is set
union { (X,c2,b1) where b1 is Element of X : b1 in z } is set
{ (IFEQ ((X,A,b1),{},{b1},{})) where b1 is Element of X : b1 in z } is set
union { (IFEQ ((X,A,b1),{},{b1},{})) where b1 is Element of X : b1 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,b1) where b1 is Element of X : b1 in z } is set
union { (X,c1,b1) where b1 is Element of X : b1 in z } is set
{ (IFEQ ((X,A,b1),{},{b1},{})) where b1 is Element of X : b1 in z } is set
union { (IFEQ ((X,A,b1),{},{b1},{})) where b1 is Element of X : b1 in z } is set
(X,c2,z) is Element of bool X
{ (X,c2,b1) where b1 is Element of X : b1 in z } is set
union { (X,c2,b1) where b1 is Element of X : b1 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

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,b1) where b1 is Element of X : b1 in z } is set
union { (X,c2,b1) where b1 is Element of X : b1 in z } is set
{ (X,(X,A,b1),(X,c1,b1)) where b1 is Element of X : b1 in z } is set
union { (X,(X,A,b1),(X,c1,b1)) where b1 is Element of X : b1 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,b1) where b1 is Element of X : b1 in z } is set
union { (X,c2,b1) where b1 is Element of X : b1 in z } is set
{ (X,(X,A,b1),(X,c1,b1)) where b1 is Element of X : b1 in z } is set
union { (X,(X,A,b1),(X,c1,b1)) where b1 is Element of X : b1 in z } is set
z is Element of bool X
(X,c2,z) is Element of bool X
{ (X,c2,b1) where b1 is Element of X : b1 in z } is set
union { (X,c2,b1) where b1 is Element of X : b1 in z } is set
{ (X,(X,A,b1),(X,c1,b1)) where b1 is Element of X : b1 in z } is set
union { (X,(X,A,b1),(X,c1,b1)) where b1 is Element of X : b1 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),b1) where b1 is Element of X : b1 in z } is set
union { (X,(A /\ c1),b1) where b1 is Element of X : b1 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,b1) where b1 is Element of X : b1 in z } is set
union { (X,c2,b1) where b1 is Element of X : b1 in z } is set
{ (X,(X,A,b1),(X,c1,b1)) where b1 is Element of X : b1 in z } is set
union { (X,(X,A,b1),(X,c1,b1)) where b1 is Element of X : b1 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,b1) where b1 is Element of X : b1 in z } is set
union { (X,c2,b1) where b1 is Element of X : b1 in z } is set
{ (X,(X,A,b1),(X,c1,b1)) where b1 is Element of X : b1 in z } is set
union { (X,(X,A,b1),(X,c1,b1)) where b1 is Element of X : b1 in z } is set
z is Element of bool X
(X,c2,z) is Element of bool X
{ (X,c2,b1) where b1 is Element of X : b1 in z } is set
union { (X,c2,b1) where b1 is Element of X : b1 in z } is set
{ (X,(X,A,b1),(X,c1,b1)) where b1 is Element of X : b1 in z } is set
union { (X,(X,A,b1),(X,c1,b1)) where b1 is Element of X : b1 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),b1) where b1 is Element of X : b1 in z } is set
union { (X,(A \/ c1),b1) where b1 is Element of X : b1 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,b1) where b1 is Element of X : b1 in z } is set
union { (X,c2,b1) where b1 is Element of X : b1 in z } is set
{ (X,(X,A,b1),(X,c1,b1)) where b1 is Element of X : b1 in z } is set
union { (X,(X,A,b1),(X,c1,b1)) where b1 is Element of X : b1 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,b1) where b1 is Element of X : b1 in z } is set
union { (X,c2,b1) where b1 is Element of X : b1 in z } is set
{ (X,(X,A,b1),(X,c1,b1)) where b1 is Element of X : b1 in z } is set
union { (X,(X,A,b1),(X,c1,b1)) where b1 is Element of X : b1 in z } is set
z is Element of bool X
(X,c2,z) is Element of bool X
{ (X,c2,b1) where b1 is Element of X : b1 in z } is set
union { (X,c2,b1) where b1 is Element of X : b1 in z } is set
{ (X,(X,A,b1),(X,c1,b1)) where b1 is Element of X : b1 in z } is set
union { (X,(X,A,b1),(X,c1,b1)) where b1 is Element of X : b1 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),b1) where b1 is Element of X : b1 in z } is set
union { (X,(A \ c1),b1) where b1 is Element of X : b1 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,b1) where b1 is Element of X : b1 in z } is set
union { (X,c2,b1) where b1 is Element of X : b1 in z } is set
(X,A,z) is Element of bool X
{ (X,A,b1) where b1 is Element of X : b1 in z } is set
union { (X,A,b1) where b1 is Element of X : b1 in z } is set
(X,c1,(X,A,z)) is Element of bool X
{ (X,c1,b1) where b1 is Element of X : b1 in (X,A,z) } is set
union { (X,c1,b1) where b1 is Element of X : b1 in (X,A,z) } is set
z is Element of bool X
(X,c2,z) is Element of bool X
{ (X,c2,b1) where b1 is Element of X : b1 in z } is set
union { (X,c2,b1) where b1 is Element of X : b1 in z } is set
(X,A,z) is Element of bool X
{ (X,A,b1) where b1 is Element of X : b1 in z } is set
union { (X,A,b1) where b1 is Element of X : b1 in z } is set
(X,c1,(X,A,z)) is Element of bool X
{ (X,c1,b1) where b1 is Element of X : b1 in (X,A,z) } is set
union { (X,c1,b1) where b1 is Element of X : b1 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),b1) where b1 is Element of X : b1 in z } is set
union { (X,(A * c1),b1) where b1 is Element of X : b1 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

x is Element of bool X
(X,z,x) is Element of bool X
{ (X,z,b1) where b1 is Element of X : b1 in x } is set
union { (X,z,b1) where b1 is Element of X : b1 in x } is set
{ (X,c1,(X,A,b1)) where b1 is Element of X : b1 in x } is set
union { (X,c1,(X,A,b1)) where b1 is Element of X : b1 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,b1) where b1 is Element of X : b1 in (X,A,s) } is set
meet { (X,c1,b1) where b1 is Element of X : b1 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,b1) where b1 is Element of X : b1 in (X,A,x) } is set
meet { (X,c1,b1) where b1 is Element of X : b1 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,b1) where b1 is Element of X : b1 in (X,A,x) } is set
meet { (X,c1,b1) where b1 is Element of X : b1 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:]

x is Element of bool X
(X,c2,x) is Element of bool X
{ (X,c2,b1) where b1 is Element of X : b1 in x } is set
union { (X,c2,b1) where b1 is Element of X : b1 in x } is set
{ (X,c1,(X,A,b1)) where b1 is Element of X : b1 in x } is set
union { (X,c1,(X,A,b1)) where b1 is Element of X : b1 in x } is set
(X,z,x) is Element of bool X
{ (X,z,b1) where b1 is Element of X : b1 in x } is set
union { (X,z,b1) where b1 is Element of X : b1 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,b1) where b1 is Element of X : b1 in (X,c1,A) } is set
union { (X,c2,b1) where b1 is Element of X : b1 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,b1) where b1 is Element of X : b1 in (X,c1,A) } is set
meet { (X,c2,b1) where b1 is Element of X : b1 in (X,c1,A) } is set
z is Element of bool X
{ (X,c2,(X,c1,b1)) where b1 is Element of X : b1 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,b1) where b1 is Element of X : b1 in (X,c1,s) } is set
meet { (X,c2,b1) where b1 is Element of X : b1 in (X,c1,s) } is set
x is set
union { (X,c2,(X,c1,b1)) where b1 is Element of X : b1 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,b1),{},{b1},{})) where b1 is Element of c1 : b1 in {X} } is set
union { (IFEQ ((c1,c2,b1),{},{b1},{})) where b1 is Element of c1 : b1 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,b1),{},{b1},{})) where b1 is Element of c1 : b1 in {z} } is set
union { (IFEQ ((c1,c2,b1),{},{b1},{})) where b1 is Element of c1 : b1 in {z} } is set
x is Element of bool c1
(c1,(c1,c2),x) is Element of bool c1
{ (c1,(c1,c2),b1) where b1 is Element of c1 : b1 in x } is set
union { (c1,(c1,c2),b1) where b1 is Element of c1 : b1 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

(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

(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
{ b1 where b1 is Element of X : ex b2 being Element of X st
( (b1,b2,(X,(X,c1))) & b1 in A )
}
is set

(X,c1,A) is Element of bool X
{ b1 where b1 is Element of X : ex b2 being Element of X st
( (b1,b2,c1) & b1 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
{ b1 where b1 is Element of X : ( card (X,c1,b1) = 0 & b1 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
{ b1 where b1 is Element of X : ex b2 being Element of X st
( (b1,b2,(X,c1)) & b1 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

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

s is Element of X
X is set
[:X,X:] is set
bool [:X,X:] is non empty set

(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

(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

(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

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,b1) where b1 is Element of X : b1 in (X,(X,A,c1),s) } is set
meet { (X,c2,b1) where b1 is Element of X : b1 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