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

union { (X,A,b

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

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

( (b

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

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

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

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

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

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

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

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

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

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

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

( (b

(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

( (b

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

( (b

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

( (b

z is epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() set

(X,A,c2,z) is Element of bool X

{ b

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

(X,c1,A) is Element of bool X

{ b

( (b

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

( (b

z is epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() set

(X,A,c2,z) is Element of bool X

{ b

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

(X,c1,A) is Element of bool X

{ b

( (b

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

( (b

z is epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() set

(X,A,c2,z) is Element of bool X

{ b

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

(X,A,c1,c2) is Element of bool X

{ b

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

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

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

s is epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() set

(X,A,c2,s) is Element of bool X

{ b

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

s is epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() set

(X,A,c2,s) is Element of bool X

{ b

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

s is epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() set

(X,c1,c2,s) is Element of bool X

{ b

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

s is epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() set

(X,c1,c2,s) is Element of bool X

{ b

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

s is Relation-like X -defined X -valued Element of bool [:X,X:]

(X,s,c1,c2) is Element of bool X

{ b

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

s is Relation-like X -defined X -valued Element of bool [:X,X:]

(X,s,c1,c2) is Element of bool X

{ b

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

s is Relation-like X -defined X -valued Element of bool [:X,X:]

(X,s,A,c2) is Element of bool X

{ b

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

s is Relation-like X -defined X -valued Element of bool [:X,X:]

(X,s,A,c2) is Element of bool X

{ b

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

( (b

c2 is Relation-like X -defined X -valued Element of bool [:X,X:]

(X,c1,A,c2) is Element of bool X

{ b

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

( (b

z is Relation-like X -defined X -valued Element of bool [:X,X:]

(X,z,c1) is Element of bool X

{ b

( (b

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

union { (X,c1,b

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

meet { (X,c2,b

(X,c2,A) is Element of bool X

{ (X,c2,b

meet { (X,c2,b

(X,c2,c1) is Element of bool X

{ (X,c2,b

meet { (X,c2,b

(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

union { (X,c2,b

z is Relation-like X -defined X -valued Element of bool [:X,X:]

(X,z,c1) is Element of bool X

{ (X,z,b

union { (X,z,b

(X,c2,c1) is Element of bool X

{ (X,c2,b

union { (X,c2,b

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

meet { (X,c1,b

c2 is Relation-like X -defined X -valued Element of bool [:X,X:]

(X,c2,A) is Element of bool X

{ (X,c2,b

meet { (X,c2,b

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

meet { (X,c1,b

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

meet { (X,([:X,X:],c1,c2),b

(X,c2,A) is Element of bool X

{ (X,c2,b

meet { (X,c2,b

(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

meet { (X,c2,b

(X,c2,A) is Element of bool X

{ (X,c2,b

meet { (X,c2,b

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

union { (X,A,b

(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

union { (X,c2,b

{ (IFEQ ((X,A,b

union { (IFEQ ((X,A,b

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

union { (X,c1,b

{ (IFEQ ((X,A,b

union { (IFEQ ((X,A,b

(X,c2,z) is Element of bool X

{ (X,c2,b

union { (X,c2,b

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

union { (X,c2,b

{ (X,(X,A,b

union { (X,(X,A,b

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

union { (X,c2,b

{ (X,(X,A,b

union { (X,(X,A,b

z is Element of bool X

(X,c2,z) is Element of bool X

{ (X,c2,b

union { (X,c2,b

{ (X,(X,A,b

union { (X,(X,A,b

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

union { (X,(A /\ c1),b

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

union { (X,c2,b

{ (X,(X,A,b

union { (X,(X,A,b

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

union { (X,c2,b

{ (X,(X,A,b

union { (X,(X,A,b

z is Element of bool X

(X,c2,z) is Element of bool X

{ (X,c2,b

union { (X,c2,b

{ (X,(X,A,b

union { (X,(X,A,b

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

union { (X,(A \/ c1),b

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

union { (X,c2,b

{ (X,(X,A,b

union { (X,(X,A,b

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

union { (X,c2,b

{ (X,(X,A,b

union { (X,(X,A,b

z is Element of bool X

(X,c2,z) is Element of bool X

{ (X,c2,b

union { (X,c2,b

{ (X,(X,A,b

union { (X,(X,A,b

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

union { (X,(A \ c1),b

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

union { (X,c2,b

(X,A,z) is Element of bool X

{ (X,A,b

union { (X,A,b

(X,c1,(X,A,z)) is Element of bool X

{ (X,c1,b

union { (X,c1,b

z is Element of bool X

(X,c2,z) is Element of bool X

{ (X,c2,b

union { (X,c2,b

(X,A,z) is Element of bool X

{ (X,A,b

union { (X,A,b

(X,c1,(X,A,z)) is Element of bool X

{ (X,c1,b

union { (X,c1,b

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

union { (X,(A * c1),b

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

union { (X,z,b

{ (X,c1,(X,A,b

union { (X,c1,(X,A,b

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

meet { (X,c1,b

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

meet { (X,c1,b

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

meet { (X,c1,b

[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

union { (X,c2,b

{ (X,c1,(X,A,b

union { (X,c1,(X,A,b

(X,z,x) is Element of bool X

{ (X,z,b

union { (X,z,b

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

union { (X,c2,b

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

meet { (X,c2,b

z is Element of bool X

{ (X,c2,(X,c1,b

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

meet { (X,c2,b

x is set

union { (X,c2,(X,c1,b

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

union { (IFEQ ((c1,c2,b

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

union { (IFEQ ((c1,c2,b

x is Element of bool c1

(c1,(c1,c2),x) is Element of bool c1

{ (c1,(c1,c2),b

union { (c1,(c1,c2),b

(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

( (b

(X,c1,A) is Element of bool X

{ b

( (b

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

(X,c1) is Relation-like X -defined X -valued Element of bool [:X,X:]

(X,(X,c1),A) is Element of bool X

{ b

( (b

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

meet { (X,c2,b

(X,A,s) is Element of bool X

A .: {s} is set

(X,c1,s) is Element of