REAL is set
NAT is non empty V30() V31() V32() Element of bool REAL
bool REAL is non empty set
NAT is non empty V30() V31() V32() set
bool NAT is non empty set
bool NAT is non empty set
{} is empty trivial Relation-like non-empty empty-yielding NAT -defined reflexive irreflexive symmetric antisymmetric asymmetric connected strongly_connected transitive Function-like one-to-one constant functional ext-real non positive non negative V29() V30() V31() V32() V34() V35() V36() V37() V44() FinSequence-like FinSubsequence-like FinSequence-membered set
the empty trivial Relation-like non-empty empty-yielding NAT -defined reflexive irreflexive symmetric antisymmetric asymmetric connected strongly_connected transitive Function-like one-to-one constant functional ext-real non positive non negative V29() V30() V31() V32() V34() V35() V36() V37() V44() FinSequence-like FinSubsequence-like FinSequence-membered set is empty trivial Relation-like non-empty empty-yielding NAT -defined reflexive irreflexive symmetric antisymmetric asymmetric connected strongly_connected transitive Function-like one-to-one constant functional ext-real non positive non negative V29() V30() V31() V32() V34() V35() V36() V37() V44() FinSequence-like FinSubsequence-like FinSequence-membered set
1 is non empty ext-real positive non negative V29() V30() V31() V32() V36() V37() Element of NAT
{{},1} is non empty set
2 is non empty ext-real positive non negative V29() V30() V31() V32() V36() V37() Element of NAT
3 is non empty ext-real positive non negative V29() V30() V31() V32() V36() V37() Element of NAT
X is set
[:X,X:] is Relation-like set
bool [:X,X:] is non empty set
X is set
(X) is Relation-like X -defined X -valued Element of bool [:X,X:]
[:X,X:] is Relation-like set
bool [:X,X:] is non empty set
dom (X) is Element of bool X
bool X is non empty set
P is set
[P,P] is non empty V38() set
{P,P} is non empty set
{P} is non empty trivial set
{{P,P},{P}} is non empty set
P is set
field (X) is set
proj1 (X) is set
proj2 (X) is set
(proj1 (X)) \/ (proj2 (X)) is set
[P,P] is non empty V38() set
{P,P} is non empty set
{P} is non empty trivial set
{{P,P},{P}} is non empty set
rng (X) is Element of bool X
(dom (X)) \/ (rng (X)) is Element of bool X
X is set
[:X,X:] is Relation-like set
bool [:X,X:] is non empty set
P 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:]
P /\ x is Relation-like X -defined X -valued set
P /\ x is Relation-like X -defined X -valued Element of bool [:X,X:]
P \/ x is Relation-like X -defined X -valued set
P \/ x is Relation-like X -defined X -valued Element of bool [:X,X:]
X is set
[:X,X:] is Relation-like set
bool [:X,X:] is non empty set
(X) is Relation-like X -defined X -valued reflexive total V41(X,X) Element of bool [:X,X:]
P is Relation-like X -defined X -valued Element of bool [:X,X:]
(X,(X),P) is Relation-like X -defined X -valued Element of bool [:X,X:]
X is set
id X is Relation-like X -defined X -valued reflexive symmetric antisymmetric transitive Function-like one-to-one total V41(X,X) V42(X) V43(X,X) Element of bool [:X,X:]
[:X,X:] is Relation-like set
bool [:X,X:] is non empty set
P is set
[P,P] is non empty V38() set
{P,P} is non empty set
{P} is non empty trivial set
{{P,P},{P}} is non empty set
P is set
x is set
[P,x] is non empty V38() set
{P,x} is non empty set
{P} is non empty trivial set
{{P,x},{P}} is non empty set
[x,P] is non empty V38() set
{x,P} is non empty set
{x} is non empty trivial set
{{x,P},{x}} is non empty set
P is set
x is set
a is set
[P,x] is non empty V38() set
{P,x} is non empty set
{P} is non empty trivial set
{{P,x},{P}} is non empty set
[x,a] is non empty V38() set
{x,a} is non empty set
{x} is non empty trivial set
{{x,a},{x}} is non empty set
[P,a] is non empty V38() set
{P,a} is non empty set
{{P,a},{P}} is non empty set
X is set
id X is Relation-like X -defined X -valued reflexive symmetric antisymmetric transitive Function-like one-to-one total V41(X,X) V42(X) V43(X,X) Element of bool [:X,X:]
[:X,X:] is Relation-like set
bool [:X,X:] is non empty set
X is set
(X) is Relation-like X -defined X -valued reflexive total V41(X,X) Element of bool [:X,X:]
[:X,X:] is Relation-like set
bool [:X,X:] is non empty set
P is set
x is set
[P,x] is non empty V38() set
{P,x} is non empty set
{P} is non empty trivial set
{{P,x},{P}} is non empty set
[x,P] is non empty V38() set
{x,P} is non empty set
{x} is non empty trivial set
{{x,P},{x}} is non empty set
P is set
x is set
a is set
[P,x] is non empty V38() set
{P,x} is non empty set
{P} is non empty trivial set
{{P,x},{P}} is non empty set
[x,a] is non empty V38() set
{x,a} is non empty set
{x} is non empty trivial set
{{x,a},{x}} is non empty set
[P,a] is non empty V38() set
{P,a} is non empty set
{{P,a},{P}} is non empty set
field (X) is set
proj1 (X) is set
proj2 (X) is set
(proj1 (X)) \/ (proj2 (X)) is set
X is set
(X) is Relation-like X -defined X -valued reflexive total V41(X,X) Element of bool [:X,X:]
[:X,X:] is Relation-like set
bool [:X,X:] is non empty set
X is set
P is set
[X,P] is non empty V38() set
{X,P} is non empty set
{X} is non empty trivial set
{{X,P},{X}} is non empty set
x is set
[:x,x:] is Relation-like 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
rng a is Element of bool x
X is set
[:X,X:] is Relation-like set
bool [:X,X:] is non empty set
P is set
[P,P] is non empty V38() set
{P,P} is non empty set
{P} is non empty trivial set
{{P,P},{P}} is non empty set
x is Relation-like X -defined X -valued reflexive total V41(X,X) Element of bool [:X,X:]
field x is set
proj1 x is set
proj2 x is set
(proj1 x) \/ (proj2 x) is set
X is set
[:X,X:] is Relation-like set
bool [:X,X:] is non empty set
P is set
x is set
[P,x] is non empty V38() set
{P,x} is non empty set
{P} is non empty trivial set
{{P,x},{P}} is non empty set
[x,P] is non empty V38() set
{x,P} is non empty set
{x} is non empty trivial set
{{x,P},{x}} is non empty set
a is Relation-like X -defined X -valued symmetric total V41(X,X) Element of bool [:X,X:]
field a is set
proj1 a is set
proj2 a is set
(proj1 a) \/ (proj2 a) is set
X is set
[:X,X:] is Relation-like set
bool [:X,X:] is non empty set
P is set
x is set
[P,x] is non empty V38() set
{P,x} is non empty set
{P} is non empty trivial set
{{P,x},{P}} is non empty set
a is set
[x,a] is non empty V38() set
{x,a} is non empty set
{x} is non empty trivial set
{{x,a},{x}} is non empty set
[P,a] is non empty V38() set
{P,a} is non empty set
{{P,a},{P}} is non empty set
b is Relation-like X -defined X -valued transitive total V41(X,X) Element of bool [:X,X:]
field b is set
proj1 b is set
proj2 b is set
(proj1 b) \/ (proj2 b) is set
X is set
[:X,X:] is Relation-like set
bool [:X,X:] is non empty set
x is set
P is Relation-like X -defined X -valued reflexive total V41(X,X) Element of bool [:X,X:]
X is set
[:X,X:] is Relation-like set
bool [:X,X:] is non empty set
P is Relation-like X -defined X -valued Element of bool [:X,X:]
field P is set
proj1 P is set
proj2 P is set
(proj1 P) \/ (proj2 P) is set
dom P is Element of bool X
bool X is non empty set
X is set
[:X,X:] is Relation-like set
bool [:X,X:] is non empty set
P is Relation-like X -defined X -valued reflexive symmetric transitive total V41(X,X) Element of bool [:X,X:]
x is Relation-like X -defined X -valued reflexive symmetric transitive total V41(X,X) Element of bool [:X,X:]
P /\ x is Relation-like X -defined X -valued reflexive symmetric transitive set
a is set
[a,a] is non empty V38() set
{a,a} is non empty set
{a} is non empty trivial set
{{a,a},{a}} is non empty set
id X is Relation-like X -defined X -valued reflexive symmetric antisymmetric transitive Function-like one-to-one total V41(X,X) V42(X) V43(X,X) Element of bool [:X,X:]
a is set
[a,a] is non empty V38() set
{a,a} is non empty set
{a} is non empty trivial set
{{a,a},{a}} is non empty set
(X,P,x) is Relation-like X -defined X -valued reflexive symmetric transitive Element of bool [:X,X:]
dom (X,P,x) is Element of bool X
bool X is non empty set
rng (X,P,x) is Element of bool X
field (X,P,x) is set
proj1 (X,P,x) is set
proj2 (X,P,x) is set
(proj1 (X,P,x)) \/ (proj2 (X,P,x)) is set
X is set
[:X,X:] is Relation-like set
bool [:X,X:] is non empty set
id X is Relation-like X -defined X -valued reflexive symmetric antisymmetric transitive Function-like one-to-one total V41(X,X) V42(X) V43(X,X) Element of bool [:X,X:]
P is Relation-like X -defined X -valued reflexive symmetric transitive total V41(X,X) Element of bool [:X,X:]
(X,(id X),P) is Relation-like X -defined X -valued reflexive symmetric antisymmetric transitive total V41(X,X) Element of bool [:X,X:]
x is set
a is set
[x,a] is non empty V38() set
{x,a} is non empty set
{x} is non empty trivial set
{{x,a},{x}} is non empty set
X is set
[:X,X:] is Relation-like set
bool [:X,X:] is non empty set
bool (bool [:X,X:]) is non empty set
P is Element of bool (bool [:X,X:])
meet P 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:]
a is set
b is set
[a,b] is non empty V38() set
{a,b} is non empty set
{a} is non empty trivial set
{{a,b},{a}} is non empty set
[b,a] is non empty V38() set
{b,a} is non empty set
{b} is non empty trivial set
{{b,a},{b}} is non empty set
c is set
a is set
b is set
[a,b] is non empty V38() set
{a,b} is non empty set
{a} is non empty trivial set
{{a,b},{a}} is non empty set
c is set
[b,c] is non empty V38() set
{b,c} is non empty set
{b} is non empty trivial set
{{b,c},{b}} is non empty set
[a,c] is non empty V38() set
{a,c} is non empty set
{{a,c},{a}} is non empty set
B is set
a is set
[a,a] is non empty V38() set
{a,a} is non empty set
{a} is non empty trivial set
{{a,a},{a}} is non empty set
b is set
field x is set
proj1 x is set
proj2 x is set
(proj1 x) \/ (proj2 x) is set
dom x is Element of bool X
bool X is non empty set
X is set
[:X,X:] is Relation-like set
bool [:X,X:] is non empty set
P is Relation-like X -defined X -valued Element of bool [:X,X:]
bool (bool [:X,X:]) is non empty set
x is Element of bool (bool [:X,X:])
(X) is Relation-like X -defined X -valued reflexive symmetric transitive total V41(X,X) Element of bool [:X,X:]
a is set
meet x is Relation-like X -defined X -valued Element of bool [:X,X:]
b is Relation-like X -defined X -valued reflexive symmetric transitive total V41(X,X) Element of bool [:X,X:]
a is Relation-like X -defined X -valued reflexive symmetric transitive total V41(X,X) Element of bool [:X,X:]
b is set
b is Relation-like X -defined X -valued reflexive symmetric transitive total V41(X,X) Element of bool [:X,X:]
X is set
[:X,X:] is Relation-like set
bool [:X,X:] is non empty set
P is Relation-like X -defined X -valued reflexive symmetric transitive total V41(X,X) Element of bool [:X,X:]
x is Relation-like X -defined X -valued reflexive symmetric transitive total V41(X,X) Element of bool [:X,X:]
(X,P,x) is Relation-like X -defined X -valued reflexive symmetric Element of bool [:X,X:]
a is Relation-like X -defined X -valued reflexive symmetric transitive total V41(X,X) Element of bool [:X,X:]
b is Relation-like X -defined X -valued reflexive symmetric transitive total V41(X,X) Element of bool [:X,X:]
b is Relation-like X -defined X -valued reflexive symmetric transitive total V41(X,X) Element of bool [:X,X:]
c is Relation-like X -defined X -valued reflexive symmetric transitive total V41(X,X) Element of bool [:X,X:]
(X,b,c) is Relation-like X -defined X -valued reflexive symmetric Element of bool [:X,X:]
a is Relation-like X -defined X -valued reflexive symmetric transitive total V41(X,X) Element of bool [:X,X:]
(X,c,b) is Relation-like X -defined X -valued reflexive symmetric Element of bool [:X,X:]
B is Relation-like X -defined X -valued reflexive symmetric transitive total V41(X,X) Element of bool [:X,X:]
a is Relation-like X -defined X -valued reflexive symmetric transitive total V41(X,X) Element of bool [:X,X:]
(X,a,a) is Relation-like X -defined X -valued reflexive symmetric Element of bool [:X,X:]
b is Relation-like X -defined X -valued reflexive symmetric transitive total V41(X,X) Element of bool [:X,X:]
(X,b,b) is Relation-like X -defined X -valued reflexive symmetric Element of bool [:X,X:]
c is Relation-like X -defined X -valued reflexive symmetric transitive total V41(X,X) Element of bool [:X,X:]
X is set
[:X,X:] is Relation-like set
bool [:X,X:] is non empty set
P is Relation-like X -defined X -valued reflexive symmetric transitive total V41(X,X) Element of bool [:X,X:]
x is Relation-like X -defined X -valued reflexive symmetric transitive total V41(X,X) Element of bool [:X,X:]
(X,P,x) is Relation-like X -defined X -valued reflexive symmetric transitive total V41(X,X) Element of bool [:X,X:]
a is Relation-like X -defined X -valued reflexive symmetric transitive total V41(X,X) Element of bool [:X,X:]
(X,(X,P,x),a) is Relation-like X -defined X -valued reflexive symmetric transitive total V41(X,X) Element of bool [:X,X:]
(X,x,a) is Relation-like X -defined X -valued reflexive symmetric transitive total V41(X,X) Element of bool [:X,X:]
(X,P,(X,x,a)) is Relation-like X -defined X -valued reflexive symmetric transitive total V41(X,X) Element of bool [:X,X:]
b is Relation-like X -defined X -valued reflexive symmetric transitive total V41(X,X) Element of bool [:X,X:]
(X,x,a) is Relation-like X -defined X -valued reflexive symmetric Element of bool [:X,X:]
(X,P,(X,x,a)) is Relation-like X -defined X -valued reflexive symmetric Element of bool [:X,X:]
(X,P,x) is Relation-like X -defined X -valued reflexive symmetric Element of bool [:X,X:]
(X,(X,P,x),a) is Relation-like X -defined X -valued reflexive symmetric Element of bool [:X,X:]
b is Relation-like X -defined X -valued reflexive symmetric transitive total V41(X,X) Element of bool [:X,X:]
(X,P,x) is Relation-like X -defined X -valued reflexive symmetric Element of bool [:X,X:]
(X,(X,P,x),a) is Relation-like X -defined X -valued reflexive symmetric Element of bool [:X,X:]
(X,x,a) is Relation-like X -defined X -valued reflexive symmetric Element of bool [:X,X:]
(X,P,(X,x,a)) is Relation-like X -defined X -valued reflexive symmetric Element of bool [:X,X:]
X is set
[:X,X:] is Relation-like set
bool [:X,X:] is non empty set
P is Relation-like X -defined X -valued reflexive symmetric transitive total V41(X,X) Element of bool [:X,X:]
(X,P,P) is Relation-like X -defined X -valued reflexive symmetric transitive total V41(X,X) Element of bool [:X,X:]
X is set
[:X,X:] is Relation-like set
bool [:X,X:] is non empty set
P is Relation-like X -defined X -valued reflexive symmetric transitive total V41(X,X) Element of bool [:X,X:]
x is Relation-like X -defined X -valued reflexive symmetric transitive total V41(X,X) Element of bool [:X,X:]
(X,P,x) is Relation-like X -defined X -valued reflexive symmetric transitive total V41(X,X) Element of bool [:X,X:]
(X,x,P) is Relation-like X -defined X -valued reflexive symmetric transitive total V41(X,X) Element of bool [:X,X:]
X is set
[:X,X:] is Relation-like set
bool [:X,X:] is non empty set
P is Relation-like X -defined X -valued reflexive symmetric transitive total V41(X,X) Element of bool [:X,X:]
x is Relation-like X -defined X -valued reflexive symmetric transitive total V41(X,X) Element of bool [:X,X:]
(X,P,x) is Relation-like X -defined X -valued reflexive symmetric transitive total V41(X,X) Element of bool [:X,X:]
(X,P,(X,P,x)) is Relation-like X -defined X -valued reflexive symmetric transitive total V41(X,X) Element of bool [:X,X:]
(X,P,x) is Relation-like X -defined X -valued reflexive symmetric Element of bool [:X,X:]
X is set
[:X,X:] is Relation-like set
bool [:X,X:] is non empty set
P is Relation-like X -defined X -valued reflexive symmetric transitive total V41(X,X) Element of bool [:X,X:]
x is Relation-like X -defined X -valued reflexive symmetric transitive total V41(X,X) Element of bool [:X,X:]
(X,P,x) is Relation-like X -defined X -valued reflexive symmetric transitive total V41(X,X) Element of bool [:X,X:]
(X,P,(X,P,x)) is Relation-like X -defined X -valued reflexive symmetric transitive total V41(X,X) Element of bool [:X,X:]
(X,P,(X,P,x)) is Relation-like X -defined X -valued reflexive symmetric Element of bool [:X,X:]
a is Relation-like X -defined X -valued reflexive symmetric transitive total V41(X,X) Element of bool [:X,X:]
F1() is set
[:F1(),F1():] is Relation-like set
bool [:F1(),F1():] is non empty set
X is Relation-like F1() -defined F1() -valued Element of bool [:F1(),F1():]
P is set
x is set
[P,x] is non empty V38() set
{P,x} is non empty set
{P} is non empty trivial set
{{P,x},{P}} is non empty set
a is set
[x,a] is non empty V38() set
{x,a} is non empty set
{x} is non empty trivial set
{{x,a},{x}} is non empty set
[P,a] is non empty V38() set
{P,a} is non empty set
{{P,a},{P}} is non empty set
P is set
x is set
[P,x] is non empty V38() set
{P,x} is non empty set
{P} is non empty trivial set
{{P,x},{P}} is non empty set
[x,P] is non empty V38() set
{x,P} is non empty set
{x} is non empty trivial set
{{x,P},{x}} is non empty set
P is set
[P,P] is non empty V38() set
{P,P} is non empty set
{P} is non empty trivial set
{{P,P},{P}} is non empty set
field X is set
proj1 X is set
proj2 X is set
(proj1 X) \/ (proj2 X) is set
dom X is Element of bool F1()
bool F1() is non empty set
P is Relation-like F1() -defined F1() -valued reflexive symmetric transitive total V41(F1(),F1()) Element of bool [:F1(),F1():]
x is set
a is set
[x,a] is non empty V38() set
{x,a} is non empty set
{x} is non empty trivial set
{{x,a},{x}} is non empty set
b is set
c is set
[b,c] is non empty V38() set
{b,c} is non empty set
{b} is non empty trivial set
{{b,c},{b}} is non empty set
X is set
P is set
[:X,P:] is Relation-like set
bool [:X,P:] is non empty set
x is Relation-like X -defined P -valued Element of bool [:X,P:]
a is set
Im (x,a) is set
{a} is non empty trivial set
x .: {a} is set
bool P is non empty set
x .: {a} is Element of bool P
X is set
P is set
[P,X] is non empty V38() set
{P,X} is non empty set
{P} is non empty trivial set
{{P,X},{P}} is non empty set
x is Relation-like set
Im (x,P) is set
x .: {P} is set
a is set
[a,X] is non empty V38() set
{a,X} is non empty set
{a} is non empty trivial set
{{a,X},{a}} is non empty set
X is set
[:X,X:] is Relation-like set
bool [:X,X:] is non empty set
P is set
x is set
[P,x] is non empty V38() set
{P,x} is non empty set
{P} is non empty trivial set
{{P,x},{P}} is non empty set
a is Relation-like X -defined X -valued symmetric total V41(X,X) Element of bool [:X,X:]
(X,X,a,x) is Element of bool X
bool X is non empty set
{x} is non empty trivial set
a .: {x} is set
[x,P] is non empty V38() set
{x,P} is non empty set
{{x,P},{x}} is non empty set
b is set
[b,P] is non empty V38() set
{b,P} is non empty set
{b} is non empty trivial set
{{b,P},{b}} is non empty set
[x,P] is non empty V38() set
{x,P} is non empty set
{{x,P},{x}} is non empty set
X is set
[:X,X:] is Relation-like set
bool [:X,X:] is non empty set
P is Relation-like X -defined X -valued reflexive symmetric total V41(X,X) Element of bool [:X,X:]
x is set
(X,X,P,x) is Element of bool X
bool X is non empty set
{x} is non empty trivial set
P .: {x} is set
[x,x] is non empty V38() set
{x,x} is non empty set
{{x,x},{x}} is non empty set
X is set
[:X,X:] is Relation-like set
bool [:X,X:] is non empty set
P is Relation-like X -defined X -valued reflexive symmetric total V41(X,X) Element of bool [:X,X:]
x is set
(X,X,P,x) is Element of bool X
bool X is non empty set
{x} is non empty trivial set
P .: {x} is set
X is set
[:X,X:] is Relation-like set
bool [:X,X:] is non empty set
P is set
x is set
a is set
[P,a] is non empty V38() set
{P,a} is non empty set
{P} is non empty trivial set
{{P,a},{P}} is non empty set
b is Relation-like X -defined X -valued reflexive symmetric transitive total V41(X,X) Element of bool [:X,X:]
(X,X,b,x) is Element of bool X
bool X is non empty set
{x} is non empty trivial set
b .: {x} is set
[a,x] is non empty V38() set
{a,x} is non empty set
{a} is non empty trivial set
{{a,x},{a}} is non empty set
[x,a] is non empty V38() set
{x,a} is non empty set
{{x,a},{x}} is non empty set
[P,x] is non empty V38() set
{P,x} is non empty set
{{P,x},{P}} is non empty set
X is set
[:X,X:] is Relation-like set
bool [:X,X:] is non empty set
P is set
x is Relation-like X -defined X -valued reflexive symmetric transitive total V41(X,X) Element of bool [:X,X:]
(X,X,x,P) is Element of bool X
bool X is non empty set
{P} is non empty trivial set
x .: {P} is set
a is set
[a,P] is non empty V38() set
{a,P} is non empty set
{a} is non empty trivial set
{{a,P},{a}} is non empty set
(X,X,x,a) is Element of bool X
x .: {a} is set
b is set
[b,P] is non empty V38() set
{b,P} is non empty set
{b} is non empty trivial set
{{b,P},{b}} is non empty set
[P,a] is non empty V38() set
{P,a} is non empty set
{{P,a},{P}} is non empty set
[b,a] is non empty V38() set
{b,a} is non empty set
{{b,a},{b}} is non empty set
b is set
[b,a] is non empty V38() set
{b,a} is non empty set
{b} is non empty trivial set
{{b,a},{b}} is non empty set
[b,P] is non empty V38() set
{b,P} is non empty set
{{b,P},{b}} is non empty set
X is set
[:X,X:] is Relation-like set
bool [:X,X:] is non empty set
P is set
x is Relation-like X -defined X -valued reflexive symmetric transitive total V41(X,X) Element of bool [:X,X:]
(X,X,x,P) is Element of bool X
bool X is non empty set
{P} is non empty trivial set
x .: {P} is set
a is set
(X,X,x,a) is Element of bool X
{a} is non empty trivial set
x .: {a} is set
[P,a] is non empty V38() set
{P,a} is non empty set
{{P,a},{P}} is non empty set
[a,P] is non empty V38() set
{a,P} is non empty set
{{a,P},{a}} is non empty set
[a,P] is non empty V38() set
{a,P} is non empty set
{{a,P},{a}} is non empty set
[P,a] is non empty V38() set
{P,a} is non empty set
{{P,a},{P}} is non empty set
X is set
[:X,X:] is Relation-like set
bool [:X,X:] is non empty set
P is Relation-like X -defined X -valued reflexive symmetric transitive total V41(X,X) Element of bool [:X,X:]
x is set
(X,X,P,x) is Element of bool X
bool X is non empty set
{x} is non empty trivial set
P .: {x} is set
a is set
(X,X,P,a) is Element of bool X
{a} is non empty trivial set
P .: {a} is set
[x,a] is non empty V38() set
{x,a} is non empty set
{{x,a},{x}} is non empty set
b is set
[b,x] is non empty V38() set
{b,x} is non empty set
{b} is non empty trivial set
{{b,x},{b}} is non empty set
[x,b] is non empty V38() set
{x,b} is non empty set
{{x,b},{x}} is non empty set
[b,a] is non empty V38() set
{b,a} is non empty set
{{b,a},{b}} is non empty set
X is set
id X is Relation-like X -defined X -valued reflexive symmetric antisymmetric transitive Function-like one-to-one total V41(X,X) V42(X) V43(X,X) Element of bool [:X,X:]
[:X,X:] is Relation-like set
bool [:X,X:] is non empty set
P is set
(X,X,(id X),P) is Element of bool X
bool X is non empty set
{P} is non empty trivial set
(id X) .: {P} is set
x is set
[x,P] is non empty V38() set
{x,P} is non empty set
{x} is non empty trivial set
{{x,P},{x}} is non empty set
x is set
a is set
X is set
(X) is Relation-like X -defined X -valued reflexive symmetric transitive total V41(X,X) Element of bool [:X,X:]
[:X,X:] is Relation-like set
bool [:X,X:] is non empty set
P is set
(X,X,(X),P) is Element of bool X
bool X is non empty set
{P} is non empty trivial set
(X) .: {P} is set
x is set
[x,P] is non empty V38() set
{x,P} is non empty set
{x} is non empty trivial set
{{x,P},{x}} is non empty set
x is set
a is set
X is set
[:X,X:] is Relation-like set
bool [:X,X:] is non empty set
(X) is Relation-like X -defined X -valued reflexive symmetric transitive total V41(X,X) Element of bool [:X,X:]
P is Relation-like X -defined X -valued reflexive symmetric transitive total V41(X,X) Element of bool [:X,X:]
x is set
(X,X,P,x) is Element of bool X
bool X is non empty set
{x} is non empty trivial set
P .: {x} is set
a is set
b is set
[a,b] is non empty V38() set
{a,b} is non empty set
{a} is non empty trivial set
{{a,b},{a}} is non empty set
[b,x] is non empty V38() set
{b,x} is non empty set
{b} is non empty trivial set
{{b,x},{b}} is non empty set
[x,b] is non empty V38() set
{x,b} is non empty set
{{x,b},{x}} is non empty set
[a,x] is non empty V38() set
{a,x} is non empty set
{{a,x},{a}} is non empty set
X is set
P is set
[:P,P:] is Relation-like set
bool [:P,P:] is non empty set
x is set
[X,x] is non empty V38() set
{X,x} is non empty set
{X} is non empty trivial set
{{X,x},{X}} is non empty set
a is Relation-like P -defined P -valued reflexive symmetric transitive total V41(P,P) Element of bool [:P,P:]
b is Relation-like P -defined P -valued reflexive symmetric transitive total V41(P,P) Element of bool [:P,P:]
(P,a,b) is Relation-like P -defined P -valued reflexive symmetric transitive total V41(P,P) Element of bool [:P,P:]
(P,a,b) is Relation-like P -defined P -valued reflexive symmetric Element of bool [:P,P:]
c is Relation-like P -defined P -valued Element of bool [:P,P:]
B is set
u is set
[B,u] is non empty V38() set
{B,u} is non empty set
{B} is non empty trivial set
{{B,u},{B}} is non empty set
X1 is set
[u,X1] is non empty V38() set
{u,X1} is non empty set
{u} is non empty trivial set
{{u,X1},{u}} is non empty set
[B,X1] is non empty V38() set
{B,X1} is non empty set
{{B,X1},{B}} is non empty set
Y1 is Relation-like NAT -defined Function-like V44() FinSequence-like FinSubsequence-like set
len Y1 is ext-real V29() V30() V31() V32() V36() V37() Element of NAT
Y1 . 1 is set
Y1 . (len Y1) is set
y is Relation-like NAT -defined Function-like V44() FinSequence-like FinSubsequence-like set
len y is ext-real V29() V30() V31() V32() V36() V37() Element of NAT
y . 1 is set
y . (len y) is set
y ^ Y1 is Relation-like NAT -defined Function-like V44() FinSequence-like FinSubsequence-like set
len (y ^ Y1) is ext-real V29() V30() V31() V32() V36() V37() Element of NAT
(len y) + (len Y1) is ext-real V29() V30() V31() V32() V36() V37() Element of NAT
(len y) + 1 is ext-real V29() V30() V31() V32() V36() V37() Element of NAT
(y ^ Y1) . (len (y ^ Y1)) is set
(len Y1) + (len y) is ext-real V29() V30() V31() V32() V36() V37() Element of NAT
((len Y1) + (len y)) - (len y) is ext-real V29() V37() set
Y1 . (((len Y1) + (len y)) - (len y)) is set
A is ext-real V29() V30() V31() V32() V36() V37() Element of NAT
(y ^ Y1) . A is set
A + 1 is ext-real V29() V30() V31() V32() V36() V37() Element of NAT
(y ^ Y1) . (A + 1) is set
[((y ^ Y1) . A),((y ^ Y1) . (A + 1))] is non empty V38() set
{((y ^ Y1) . A),((y ^ Y1) . (A + 1))} is non empty set
{((y ^ Y1) . A)} is non empty trivial set
{{((y ^ Y1) . A),((y ^ Y1) . (A + 1))},{((y ^ Y1) . A)}} is non empty set
Seg (len y) is V44() V51( len y) Element of bool NAT
dom y is Element of bool NAT
y . (A + 1) is set
y . A is set
Seg (len y) is V44() V51( len y) Element of bool NAT
dom y is Element of bool NAT
[u,u] is non empty V38() set
{u,u} is non empty set
{{u,u},{u}} is non empty set
1 + (len y) is ext-real V29() V30() V31() V32() V36() V37() Element of NAT
(1 + (len y)) - (len y) is ext-real V29() V37() set
Y1 . ((1 + (len y)) - (len y)) is set
A - (len y) is ext-real V29() V37() set
1 + A is ext-real V29() V30() V31() V32() V36() V37() Element of NAT
(1 + A) - (len y) is ext-real V29() V37() set
Y1 . ((1 + A) - (len y)) is set
(A - (len y)) + 1 is ext-real V29() V37() set
Y1 . ((A - (len y)) + 1) is set
1 + (len y) is ext-real V29() V30() V31() V32() V36() V37() Element of NAT
(1 + (len y)) - (len y) is ext-real V29() V37() set
T is ext-real V29() V30() V31() V32() V36() V37() Element of NAT
Y1 . T is set
T + 1 is ext-real V29() V30() V31() V32() V36() V37() Element of NAT
Y1 . (T + 1) is set
[(Y1 . T),(Y1 . (T + 1))] is non empty V38() set
{(Y1 . T),(Y1 . (T + 1))} is non empty set
{(Y1 . T)} is non empty trivial set
{{(Y1 . T),(Y1 . (T + 1))},{(Y1 . T)}} is non empty set
Seg (len y) is V44() V51( len y) Element of bool NAT
dom y is Element of bool NAT
(y ^ Y1) . 1 is set
B is set
u is set
[B,u] is non empty V38() set
{B,u} is non empty set
{B} is non empty trivial set
{{B,u},{B}} is non empty set
[u,B] is non empty V38() set
{u,B} is non empty set
{u} is non empty trivial set
{{u,B},{u}} is non empty set
X1 is Relation-like NAT -defined Function-like V44() FinSequence-like FinSubsequence-like set
len X1 is ext-real V29() V30() V31() V32() V36() V37() Element of NAT
X1 . 1 is set
X1 . (len X1) is set
1 + (len X1) is ext-real V29() V30() V31() V32() V36() V37() Element of NAT
Seg (len X1) is V44() V51( len X1) Element of bool NAT
Y1 is ext-real V29() V30() V31() V32() V36() V37() set
(1 + (len X1)) - Y1 is ext-real V29() V37() set
X1 . ((1 + (len X1)) - Y1) is set
Y1 is Relation-like NAT -defined Function-like V44() FinSequence-like FinSubsequence-like set
dom Y1 is Element of bool NAT
len Y1 is ext-real V29() V30() V31() V32() V36() V37() Element of NAT
y is ext-real V29() V30() V31() V32() V36() V37() Element of NAT
Y1 . y is set
y + 1 is ext-real V29() V30() V31() V32() V36() V37() Element of NAT
Y1 . (y + 1) is set
[(Y1 . y),(Y1 . (y + 1))] is non empty V38() set
{(Y1 . y),(Y1 . (y + 1))} is non empty set
{(Y1 . y)} is non empty trivial set
{{(Y1 . y),(Y1 . (y + 1))},{(Y1 . y)}} is non empty set
(len X1) - y is ext-real V29() V37() set
(len X1) - (len X1) is ext-real V29() V37() set
y - (len X1) is ext-real V29() V37() set
0 is empty trivial Relation-like non-empty empty-yielding NAT -defined reflexive irreflexive symmetric antisymmetric asymmetric connected strongly_connected transitive Function-like one-to-one constant functional ext-real non positive non negative V29() V30() V31() V32() V34() V35() V36() V37() V44() FinSequence-like FinSubsequence-like FinSequence-membered Element of NAT
- 0 is empty trivial Relation-like non-empty empty-yielding NAT -defined reflexive irreflexive symmetric antisymmetric asymmetric connected strongly_connected transitive Function-like one-to-one constant functional ext-real non positive non negative V29() V30() V31() V32() V34() V35() V36() V37() V44() FinSequence-like FinSubsequence-like FinSequence-membered set
- ((len X1) - y) is ext-real V29() V37() set
c is ext-real V29() V30() V31() V32() V36() V37() Element of NAT
0 + 1 is non empty ext-real positive non negative V29() V30() V31() V32() V36() V37() Element of NAT
- y is ext-real V29() V37() set
0 + (len X1) is ext-real V29() V30() V31() V32() V36() V37() Element of NAT
(len X1) + (- y) is ext-real V29() V37() set
X1 . c is set
c + 1 is ext-real V29() V30() V31() V32() V36() V37() Element of NAT
X1 . (c + 1) is set
[(X1 . c),(X1 . (c + 1))] is non empty V38() set
{(X1 . c),(X1 . (c + 1))} is non empty set
{(X1 . c)} is non empty trivial set
{{(X1 . c),(X1 . (c + 1))},{(X1 . c)}} is non empty set
[(X1 . (c + 1)),(X1 . c)] is non empty V38() set
{(X1 . (c + 1)),(X1 . c)} is non empty set
{(X1 . (c + 1))} is non empty trivial set
{{(X1 . (c + 1)),(X1 . c)},{(X1 . (c + 1))}} is non empty set
[(X1 . (c + 1)),(X1 . c)] is non empty V38() set
{(X1 . (c + 1)),(X1 . c)} is non empty set
{(X1 . (c + 1))} is non empty trivial set
{{(X1 . (c + 1)),(X1 . c)},{(X1 . (c + 1))}} is non empty set
[(X1 . (c + 1)),(X1 . c)] is non empty V38() set
{(X1 . (c + 1)),(X1 . c)} is non empty set
{(X1 . (c + 1))} is non empty trivial set
{{(X1 . (c + 1)),(X1 . c)},{(X1 . (c + 1))}} is non empty set
[(X1 . (c + 1)),(X1 . c)] is non empty V38() set
{(X1 . (c + 1)),(X1 . c)} is non empty set
{(X1 . (c + 1))} is non empty trivial set
{{(X1 . (c + 1)),(X1 . c)},{(X1 . (c + 1))}} is non empty set
(len X1) + 1 is ext-real V29() V30() V31() V32() V36() V37() Element of NAT
1 + y is ext-real V29() V30() V31() V32() V36() V37() Element of NAT
((len X1) + 1) - (1 + y) is ext-real V29() V37() set
X1 . (((len X1) + 1) - (1 + y)) is set
X1 . ((len X1) - y) is set
(1 + (len X1)) - y is ext-real V29() V37() set
X1 . ((1 + (len X1)) - y) is set
((len X1) - y) + 1 is ext-real V29() V37() set
X1 . (((len X1) - y) + 1) is set
Y1 . (len X1) is set
(1 + (len X1)) - (len X1) is ext-real V29() V37() set
X1 . ((1 + (len X1)) - (len X1)) is set
0 is empty trivial Relation-like non-empty empty-yielding NAT -defined reflexive irreflexive symmetric antisymmetric asymmetric connected strongly_connected transitive Function-like one-to-one constant functional ext-real non positive non negative V29() V30() V31() V32() V34() V35() V36() V37() V44() FinSequence-like FinSubsequence-like FinSequence-membered Element of NAT
1 + 0 is non empty ext-real positive non negative V29() V30() V31() V32() V36() V37() Element of NAT
X1 . (1 + 0) is set
Y1 . (len Y1) is set
Y1 . 1 is set
(len X1) + 1 is ext-real V29() V30() V31() V32() V36() V37() Element of NAT
((len X1) + 1) - 1 is ext-real V29() V37() set
X1 . (((len X1) + 1) - 1) is set
B is set
[B,B] is non empty V38() set
{B,B} is non empty set
{B} is non empty trivial set
{{B,B},{B}} is non empty set
<*B*> is non empty Relation-like NAT -defined Function-like V44() V51(1) FinSequence-like FinSubsequence-like set
len <*B*> is ext-real V29() V30() V31() V32() V36() V37() Element of NAT
X1 is ext-real V29() V30() V31() V32() V36() V37() Element of NAT
<*B*> . X1 is set
X1 + 1 is ext-real V29() V30() V31() V32() V36() V37() Element of NAT
<*B*> . (X1 + 1) is set
[(<*B*> . X1),(<*B*> . (X1 + 1))] is non empty V38() set
{(<*B*> . X1),(<*B*> . (X1 + 1))} is non empty set
{(<*B*> . X1)} is non empty trivial set
{{(<*B*> . X1),(<*B*> . (X1 + 1))},{(<*B*> . X1)}} is non empty set
<*B*> . 1 is set
field c is set
proj1 c is set
proj2 c is set
(proj1 c) \/ (proj2 c) is set
dom c is Element of bool P
bool P is non empty set
B is Relation-like P -defined P -valued reflexive symmetric transitive total V41(P,P) Element of bool [:P,P:]
u is set
X1 is set
[u,X1] is non empty V38() set
{u,X1} is non empty set
{u} is non empty trivial set
{{u,X1},{u}} is non empty set
<*u,X1*> is non empty Relation-like NAT -defined Function-like V44() V51(2) FinSequence-like FinSubsequence-like set
len <*u,X1*> is ext-real V29() V30() V31() V32() V36() V37() Element of NAT
1 + 1 is non empty ext-real positive non negative V29() V30() V31() V32() V36() V37() Element of NAT
<*u,X1*> . 1 is set
y is ext-real V29() V30() V31() V32() V36() V37() Element of NAT
<*u,X1*> . y is set
y + 1 is ext-real V29() V30() V31() V32() V36() V37() Element of NAT
<*u,X1*> . (y + 1) is set
[(<*u,X1*> . y),(<*u,X1*> . (y + 1))] is non empty V38() set
{(<*u,X1*> . y),(<*u,X1*> . (y + 1))} is non empty set
{(<*u,X1*> . y)} is non empty trivial set
{{(<*u,X1*> . y),(<*u,X1*> . (y + 1))},{(<*u,X1*> . y)}} is non empty set
<*u,X1*> . (len <*u,X1*>) is set
u is Relation-like NAT -defined Function-like V44() FinSequence-like FinSubsequence-like set
len u is ext-real V29() V30() V31() V32() V36() V37() Element of NAT
u . 1 is set
u . (len u) is set
X1 is ext-real V29() V30() V31() V32() V36() V37() Element of NAT
u . X1 is set
X1 + 1 is ext-real V29() V30() V31() V32() V36() V37() Element of NAT
u . (X1 + 1) is set
[(u . X1),(u . (X1 + 1))] is non empty V38() set
{(u . X1),(u . (X1 + 1))} is non empty set
{(u . X1)} is non empty trivial set
{{(u . X1),(u . (X1 + 1))},{(u . X1)}} is non empty set
c is Relation-like NAT -defined Function-like V44() FinSequence-like FinSubsequence-like set
len c is ext-real V29() V30() V31() V32() V36() V37() Element of NAT
c . 1 is set
c . (len c) is set
B is ext-real V29() V30() V31() V32() V36() V37() Element of NAT
c . B is set
[(c . 1),(c . B)] is non empty V38() set
{(c . 1),(c . B)} is non empty set
{(c . 1)} is non empty trivial set
{{(c . 1),(c . B)},{(c . 1)}} is non empty set
B + 1 is ext-real V29() V30() V31() V32() V36() V37() Element of NAT
c . (B + 1) is set
[(c . 1),(c . (B + 1))] is non empty V38() set
{(c . 1),(c . (B + 1))} is non empty set
{{(c . 1),(c . (B + 1))},{(c . 1)}} is non empty set
[(c . B),(c . (B + 1))] is non empty V38() set
{(c . B),(c . (B + 1))} is non empty set
{(c . B)} is non empty trivial set
{{(c . B),(c . (B + 1))},{(c . B)}} is non empty set
0 is empty trivial Relation-like non-empty empty-yielding NAT -defined reflexive irreflexive symmetric antisymmetric asymmetric connected strongly_connected transitive Function-like one-to-one constant functional ext-real non positive non negative V29() V30() V31() V32() V34() V35() V36() V37() V44() FinSequence-like FinSubsequence-like FinSequence-membered Element of NAT
[(c . 1),(c . 1)] is non empty V38() set
{(c . 1),(c . 1)} is non empty set
{{(c . 1),(c . 1)},{(c . 1)}} is non empty set
0 is empty trivial Relation-like non-empty empty-yielding NAT -defined reflexive irreflexive symmetric antisymmetric asymmetric connected strongly_connected transitive Function-like one-to-one constant functional ext-real non positive non negative V29() V30() V31() V32() V34() V35() V36() V37() V44() FinSequence-like FinSubsequence-like FinSequence-membered Element of NAT
0 is empty trivial Relation-like non-empty empty-yielding NAT -defined reflexive irreflexive symmetric antisymmetric asymmetric connected strongly_connected transitive Function-like one-to-one constant functional ext-real non positive non negative V29() V30() V31() V32() V34() V35() V36() V37() V44() FinSequence-like FinSubsequence-like FinSequence-membered Element of NAT
c . 0 is set
[(c . 1),(c . 0)] is non empty V38() set
{(c . 1),(c . 0)} is non empty set
{{(c . 1),(c . 0)},{(c . 1)}} is non empty set
X is set
[:X,X:] is Relation-like set
bool [:X,X:] is non empty set
P is Relation-like X -defined X -valued reflexive symmetric transitive total V41(X,X) Element of bool [:X,X:]
x is Relation-like X -defined X -valued reflexive symmetric transitive total V41(X,X) Element of bool [:X,X:]
(X,P,x) is Relation-like X -defined X -valued reflexive symmetric Element of bool [:X,X:]
a is Relation-like X -defined X -valued reflexive symmetric transitive total V41(X,X) Element of bool [:X,X:]
b is set
(X,X,a,b) is Element of bool X
bool X is non empty set
{b} is non empty trivial set
a .: {b} is set
(X,X,P,b) is Element of bool X
P .: {b} is set
(X,X,x,b) is Element of bool X
x .: {b} is set
c is set
[c,b] is non empty V38() set
{c,b} is non empty set
{c} is non empty trivial set
{{c,b},{c}} is non empty set
B is set
[B,b] is non empty V38() set
{B,b} is non empty set
{B} is non empty trivial set
{{B,b},{B}} is non empty set
[c,B] is non empty V38() set
{c,B} is non empty set
{{c,B},{c}} is non empty set
[B,c] is non empty V38() set
{B,c} is non empty set
{{B,c},{B}} is non empty set
[b,B] is non empty V38() set
{b,B} is non empty set
{{b,B},{b}} is non empty set
[b,c] is non empty V38() set
{b,c} is non empty set
{{b,c},{b}} is non empty set
b is set
(X,X,a,b) is Element of bool X
bool X is non empty set
{b} is non empty trivial set
a .: {b} is set
(X,X,P,b) is Element of bool X
P .: {b} is set
(X,X,x,b) is Element of bool X
x .: {b} is set
X is set
[:X,X:] is Relation-like set
bool [:X,X:] is non empty set
(X) is Relation-like X -defined X -valued reflexive symmetric transitive total V41(X,X) Element of bool [:X,X:]
P is Relation-like X -defined X -valued reflexive symmetric transitive total V41(X,X) Element of bool [:X,X:]
x is Relation-like X -defined X -valued reflexive symmetric transitive total V41(X,X) Element of bool [:X,X:]
(X,P,x) is Relation-like X -defined X -valued reflexive symmetric Element of bool [:X,X:]
the Element of X is Element of X
b is set
(X,X,(X),b) is Element of bool X
bool X is non empty set
{b} is non empty trivial set
(X) .: {b} is set
(X,X,P,b) is Element of bool X
P .: {b} is set
(X,X,x,b) is Element of bool X
x .: {b} is set
(X,X,P, the Element of X) is Element of bool X
{ the Element of X} is non empty trivial set
P .: { the Element of X} is set
(X,X,x, the Element of X) is Element of bool X
x .: { the Element of X} is set
X is set
[:X,X:] is Relation-like set
bool [:X,X:] is non empty set
bool X is non empty set
bool (bool X) is non empty set
P is Relation-like X -defined X -valued reflexive symmetric transitive total V41(X,X) Element of bool [:X,X:]
x is Element of bool (bool X)
a is Element of bool X
c is set
b is Element of bool X
(X,X,P,c) is Element of bool X
{c} is non empty trivial set
P .: {c} is set
x is Element of bool (bool X)
a is Element of bool (bool X)
b is Element of bool X
c is set
(X,X,P,c) is Element of bool X
{c} is non empty trivial set
P .: {c} is set
c is set
(X,X,P,c) is Element of bool X
{c} is non empty trivial set
P .: {c} is set
X is set
[:X,X:] is Relation-like set
bool [:X,X:] is non empty set
P is Relation-like X -defined X -valued reflexive symmetric transitive total V41(X,X) Element of bool [:X,X:]
(X,P) is Element of bool (bool X)
bool X is non empty set
bool (bool X) is non empty set
the Element of (X,P) is Element of (X,P)
a is set
(X,X,P,a) is Element of bool X
{a} is non empty trivial set
P .: {a} is set
X is set
bool X is non empty set
bool (bool X) is non empty set
P is Element of bool (bool X)
x is Element of bool X
a is set
{a} is non empty trivial set
b is Element of bool X
c is set
{c} is non empty trivial set
B is set
union P is Element of bool X
x is set
{x} is non empty trivial set
a is set
b is set
x is Element of bool X
a is Element of bool X
X is ( {} )
P is set
X is set
[:X,X:] is Relation-like set
bool [:X,X:] is non empty set
P is Relation-like X -defined X -valued reflexive symmetric transitive total V41(X,X) Element of bool [:X,X:]
(X,P) is Element of bool (bool X)
bool X is non empty set
bool (bool X) is non empty set
x is set
(X,X,P,x) is Element of bool X
{x} is non empty trivial set
P .: {x} is set
a is set
a is set
b is set
union (X,P) is Element of bool X
x is Element of bool X
a is set
(X,X,P,a) is Element of bool X
{a} is non empty trivial set
P .: {a} is set
a is Element of bool X
b is set
(X,X,P,b) is Element of bool X
{b} is non empty trivial set
P .: {b} is set
c is set
(X,X,P,c) is Element of bool X
{c} is non empty trivial set
P .: {c} is set
X is set
[:X,X:] is Relation-like set
bool [:X,X:] is non empty set
P is (X)
bool X is non empty set
x is set
a is set
b is set
c is Element of bool X
B is Element of bool X
union P is Element of bool X
x is set
a is set
b is Element of bool X
b is Element of bool X
x is set
a is set
x is Relation-like X -defined X -valued reflexive symmetric transitive total V41(X,X) Element of bool [:X,X:]
(X,x) is Element of bool (bool X)
bool (bool X) is non empty set
a is Element of bool X
the Element of a is Element of a
c is set
(X,X,x, the Element of a) is Element of bool X
{ the Element of a} is non empty trivial set
x .: { the Element of a} is set
[c, the Element of a] is non empty V38() set
{c, the Element of a} is non empty set
{c} is non empty trivial set
{{c, the Element of a},{c}} is non empty set
B is Element of bool X
b is set
(X,X,x,b) is Element of bool X
{b} is non empty trivial set
x .: {b} is set
[b,b] is non empty V38() set
{b,b} is non empty set
{{b,b},{b}} is non empty set
c is Element of bool X
B is set
[B,b] is non empty V38() set
{B,b} is non empty set
{B} is non empty trivial set
{{B,b},{B}} is non empty set
u is Element of bool X
the Relation-like X -defined X -valued reflexive symmetric transitive total V41(X,X) Element of bool [:X,X:] is Relation-like X -defined X -valued reflexive symmetric transitive total V41(X,X) Element of bool [:X,X:]
(X, the Relation-like X -defined X -valued reflexive symmetric transitive total V41(X,X) Element of bool [:X,X:]) is Element of bool (bool X)
bool X is non empty set
bool (bool X) is non empty set
x is Relation-like X -defined X -valued reflexive symmetric transitive total V41(X,X) Element of bool [:X,X:]
(X,x) is Element of bool (bool X)
bool X is non empty set
bool (bool X) is non empty set
a is Relation-like X -defined X -valued reflexive symmetric transitive total V41(X,X) Element of bool [:X,X:]
(X,a) is Element of bool (bool X)
X is set
[:X,X:] is Relation-like set
bool [:X,X:] is non empty set
a is set
P is set
[a,P] is non empty V38() set
{a,P} is non empty set
{a} is non empty trivial set
{{a,P},{a}} is non empty set
x is Relation-like X -defined X -valued reflexive symmetric transitive total V41(X,X) Element of bool [:X,X:]
(X,X,x,a) is Element of bool X
bool X is non empty set
x .: {a} is set
(X,X,x,P) is Element of bool X
{P} is non empty trivial set
x .: {P} is set
X is set
P is set
[:P,P:] is Relation-like set
bool [:P,P:] is non empty set
x is Relation-like P -defined P -valued reflexive symmetric transitive total V41(P,P) Element of bool [:P,P:]
(P,x) is Element of bool (bool P)
bool P is non empty set
bool (bool P) is non empty set
a is Element of bool P
b is set
(P,P,x,b) is Element of bool P
{b} is non empty trivial set
x .: {b} is set
c is Element of P
(P,P,x,c) is Element of bool P
{c} is non empty trivial set
x .: {c} is set
X is non empty set
the Element of X is Element of X
x is (X)
union x is Element of bool X
bool X is non empty set
a is set
X is set
P is (X)
X is set
[:X,X:] is Relation-like set
bool [:X,X:] is non empty set
P is Relation-like X -defined X -valued reflexive symmetric transitive total V41(X,X) Element of bool [:X,X:]
(X,P) is Element of bool (bool X)
bool X is non empty set
bool (bool X) is non empty set
X is non empty set
[:X,X:] is non empty Relation-like set
bool [:X,X:] is non empty set
P is Relation-like X -defined X -valued reflexive symmetric transitive total V41(X,X) Element of bool [:X,X:]
(X,P) is non empty with_non-empty_elements (X)
X is non empty set
[:X,X:] is non empty Relation-like set
bool [:X,X:] is non empty set
P is Relation-like X -defined X -valued reflexive symmetric transitive total V41(X,X) Element of bool [:X,X:]
(X,P) is non empty with_non-empty_elements (X)
X is non empty set
[:X,X:] is non empty Relation-like set
bool [:X,X:] is non empty set
X is non empty set
[:X,X:] is non empty Relation-like set
bool [:X,X:] is non empty set
P is Relation-like X -defined X -valued reflexive symmetric transitive total V41(X,X) Element of bool [:X,X:]
x is Element of X
Im (P,x) is set
{x} is non empty trivial set
P .: {x} is set
bool X is non empty set
(X,P) is non empty with_non-empty_elements (X)
(X,X,P,x) is Element of bool X
X is set
id X is Relation-like X -defined X -valued reflexive symmetric antisymmetric transitive Function-like one-to-one total V41(X,X) V42(X) V43(X,X) Element of bool [:X,X:]
[:X,X:] is Relation-like set
bool [:X,X:] is non empty set
(X,(id X)) is with_non-empty_elements (X)
X is non empty set
(X) is non empty with_non-empty_elements (X)
id X is non empty Relation-like X -defined X -valued reflexive symmetric antisymmetric transitive Function-like one-to-one total V41(X,X) V42(X) V43(X,X) Element of bool [:X,X:]
[:X,X:] is non empty Relation-like set
bool [:X,X:] is non empty set
(X,(id X)) is non empty with_non-empty_elements (X)
{ {b1} where b1 is Element of X : verum } is set
x is set
a is set
(X,X,(id X),a) is Element of bool X
bool X is non empty set
{a} is non empty trivial set
(id X) .: {a} is set
x is set
a is Element of X
{a} is non empty trivial Element of bool X
(X,X,(id X),a) is Element of bool X
{a} is non empty trivial set
(id X) .: {a} is set
X is non empty set
bool X is non empty set
P is Element of X
x is non empty with_non-empty_elements (X)
[:X,X:] is non empty Relation-like set
bool [:X,X:] is non empty set
a is Relation-like X -defined X -valued reflexive symmetric transitive total V41(X,X) Element of bool [:X,X:]
(X,a) is non empty with_non-empty_elements (X)
(X,X,a,P) is Element of bool X
{P} is non empty trivial set
a .: {P} is set
a is Element of bool X
b is Element of bool X
X is non empty set
P is non empty with_non-empty_elements (X)
x is non empty with_non-empty_elements (X)
bool X is non empty set
a is Element of bool X
the Element of a is Element of a
c is Element of X
(X,c,P) is Element of bool X
(X,c,x) is Element of bool X
the Element of a is Element of a
c is Element of X
(X,c,x) is Element of bool X
(X,c,P) is Element of bool X
X is non empty set
{X} is non empty trivial set
bool X is non empty set
bool (bool X) is non empty set
P is Element of bool (bool X)
x is Element of bool X
a is Element of bool X
union P is Element of bool X
X is set
bool X is non empty Element of bool (bool X)
bool X is non empty set
bool (bool X) is non empty set
bool (bool X) is non empty set
bool (bool (bool X)) is non empty set
X is set
bool X is non empty Element of bool (bool X)
bool X is non empty set
bool (bool X) is non empty set
bool (bool X) is non empty set
bool (bool (bool X)) is non empty set
P is Element of bool (bool (bool X))
x is set
X is non empty set
{X} is non empty trivial set
bool X is non empty set
bool (bool X) is non empty set
X is set
bool X is non empty set
bool (bool X) is non empty set
bool X is non empty Element of bool (bool X)
bool (bool X) is non empty set
bool (bool (bool X)) is non empty set
P is with_non-empty_elements (X)
{P} is non empty trivial Element of bool (bool (bool X))
bool (bool (bool X)) is non empty set
x is set
X is set
bool X is non empty Element of bool (bool X)
bool X is non empty set
bool (bool X) is non empty set
bool (bool X) is non empty set
bool (bool (bool X)) is non empty set
the with_non-empty_elements (X) is with_non-empty_elements (X)
{ the with_non-empty_elements (X)} is non empty trivial Element of bool (bool (bool X))
bool (bool (bool X)) is non empty set
x is (X) Element of bool (bool (bool X))
X is non empty set
P is non empty with_non-empty_elements (X)
x is Element of X
(X,x,P) is Element of bool X
bool X is non empty set
a is Element of X
(X,a,P) is Element of bool X
[:X,X:] is non empty Relation-like set
bool [:X,X:] is non empty set
b is Relation-like X -defined X -valued reflexive symmetric transitive total V41(X,X) Element of bool [:X,X:]
(X,b) is non empty with_non-empty_elements (X)
(X,X,b,a) is Element of bool X
{a} is non empty trivial set
b .: {a} is set
(X,X,b,x) is Element of bool X
{x} is non empty trivial set
b .: {x} is set
X is non empty set
bool X is non empty Element of bool (bool X)
bool X is non empty set
bool (bool X) is non empty set
bool (bool X) is non empty set
bool (bool (bool X)) is non empty set
P is Element of X
x is (X) Element of bool (bool (bool X))
{ (X,P,b1) where b1 is non empty with_non-empty_elements (X) : b1 in x } is set
a is set
b is non empty with_non-empty_elements (X)
(X,P,b) is Element of bool X
X is set
P is non empty set
x is non empty with_non-empty_elements (P)
a is set
(P,a,x) is Element of bool P
bool P is non empty set
X is non empty set
bool X is non empty Element of bool (bool X)
bool X is non empty set
bool (bool X) is non empty set
bool (bool X) is non empty set
bool (bool (bool X)) is non empty set
P is non empty (X) Element of bool (bool (bool X))
x is non empty with_non-empty_elements (X)
a is non empty with_non-empty_elements (X)
b is Element of X
(X,b,x) is Element of bool X
{ (X,b,b1) where b1 is non empty with_non-empty_elements (X) : b1 in P } is set
meet { (X,b,b1) where b1 is non empty with_non-empty_elements (X) : b1 in P } is set
(X,b,a) is Element of bool X
{ (meet { (X,b1,b2) where b2 is non empty with_non-empty_elements (X) : b2 in P } ) where b1 is Element of X : verum } is set
a is set
b is Element of X
{ (X,b,b1) where b1 is non empty with_non-empty_elements (X) : b1 in P } is set
meet { (X,b,b1) where b1 is non empty with_non-empty_elements (X) : b1 in P } is set
c is set
B is set
u is non empty with_non-empty_elements (X)
(X,b,u) is Element of bool X
X1 is set
Y1 is non empty with_non-empty_elements (X)
(X,b,Y1) is Element of bool X
a is Element of bool (bool X)
union a is Element of bool X
b is set
c is set
B is Element of X
{ (X,B,b1) where b1 is non empty with_non-empty_elements (X) : b1 in P } is set
meet { (X,B,b1) where b1 is non empty with_non-empty_elements (X) : b1 in P } is set
X1 is set
Y1 is non empty with_non-empty_elements (X)
(X,B,Y1) is Element of bool X
u is non empty with_non-empty_elements (X)
(X,B,u) is Element of bool X
b is Element of bool X
c is set
u is Element of X
{ (X,u,b1) where b1 is non empty with_non-empty_elements (X) : b1 in P } is set
meet { (X,u,b1) where b1 is non empty with_non-empty_elements (X) : b1 in P } is set
X1 is set
Y1 is non empty with_non-empty_elements (X)
(X,u,Y1) is Element of bool X
B is non empty with_non-empty_elements (X)
(X,u,B) is Element of bool X
X1 is Element of X
{ (X,X1,b1) where b1 is non empty with_non-empty_elements (X) : b1 in P } is set
meet { (X,X1,b1) where b1 is non empty with_non-empty_elements (X) : b1 in P } is set
Y1 is Element of bool X
y is Element of X
{ (X,y,b1) where b1 is non empty with_non-empty_elements (X) : b1 in P } is set
meet { (X,y,b1) where b1 is non empty with_non-empty_elements (X) : b1 in P } is set
c is set
A is non empty with_non-empty_elements (X)
(X,y,A) is Element of bool X
c is set
A is non empty with_non-empty_elements (X)
(X,X1,A) is Element of bool X
c is set
(meet { (X,X1,b1) where b1 is non empty with_non-empty_elements (X) : b1 in P } ) /\ (meet { (X,y,b1) where b1 is non empty with_non-empty_elements (X) : b1 in P } ) is set
{ (X,X1,b1) where b1 is non empty with_non-empty_elements (X) : b1 in P } \/ { (X,y,b1) where b1 is non empty with_non-empty_elements (X) : b1 in P } is set
meet ( { (X,X1,b1) where b1 is non empty with_non-empty_elements (X) : b1 in P } \/ { (X,y,b1) where b1 is non empty with_non-empty_elements (X) : b1 in P } ) is set
A is non empty with_non-empty_elements (X)
(X,y,A) is Element of bool X
A is non empty with_non-empty_elements (X)
(X,X1,A) is Element of bool X
A is non empty with_non-empty_elements (X)
(X,X1,A) is Element of bool X
(X,y,A) is Element of bool X
A is non empty with_non-empty_elements (X)
(X,X1,A) is Element of bool X
(X,y,A) is Element of bool X
T is set
A is set
T is non empty with_non-empty_elements (X)
(X,y,T) is Element of bool X
(X,X1,T) is Element of bool X
A is set
T is non empty with_non-empty_elements (X)
(X,X1,T) is Element of bool X
(X,y,T) is Element of bool X
b is non empty with_non-empty_elements (X)
c is Element of X
(X,c,b) is Element of bool X
{ (X,c,b1) where b1 is non empty with_non-empty_elements (X) : b1 in P } is set
meet { (X,c,b1) where b1 is non empty with_non-empty_elements (X) : b1 in P } is set
B is set
u is non empty with_non-empty_elements (X)
(X,c,u) is Element of bool X
B is set
u is non empty with_non-empty_elements (X)
(X,c,u) is Element of bool X
c is Element of X
(X,c,b) is Element of bool X
{ (X,c,b1) where b1 is non empty with_non-empty_elements (X) : b1 in P } is set
meet { (X,c,b1) where b1 is non empty with_non-empty_elements (X) : b1 in P } is set
X is non empty set
bool X is non empty set
P is non empty with_non-empty_elements (X)
bool P is non empty set
union P is Element of bool X
x is Element of bool P
union x is set
(union P) \ (union x) is Element of bool X
P \ x is Element of bool (bool X)
bool (bool X) is non empty set
union (P \ x) is Element of bool X
a is set
b is set
a is set
b is set
c is set
c is set
X is non empty set
bool X is non empty set
P is Element of bool X
{P} is non empty trivial Element of bool (bool X)
bool (bool X) is non empty set
X \ P is Element of bool X
x is non empty with_non-empty_elements (X)
x \ {P} is Element of bool (bool X)
union (x \ {P}) is Element of bool X
a is set
bool x is non empty set
union x is Element of bool X
a is Element of bool x
union a is set
(union x) \ (union a) is Element of bool X
union {P} is Element of bool X
X \ (union {P}) is Element of bool X
bool {} is non empty set
bool (bool {}) is non empty set
X is Element of bool (bool {})
union X is empty trivial non proper Relation-like non-empty empty-yielding NAT -defined reflexive irreflexive symmetric antisymmetric asymmetric connected strongly_connected transitive Function-like one-to-one constant functional ext-real non positive non negative V29() V30() V31() V32() V34() V35() V36() V37() V44() FinSequence-like FinSubsequence-like FinSequence-membered Element of bool {}
P is empty trivial non proper Relation-like non-empty empty-yielding NAT -defined reflexive irreflexive symmetric antisymmetric asymmetric connected strongly_connected transitive Function-like one-to-one constant functional ext-real non positive non negative V29() V30() V31() V32() V34() V35() V36() V37() V44() FinSequence-like FinSubsequence-like FinSequence-membered Element of bool {}
x is empty trivial non proper Relation-like non-empty empty-yielding NAT -defined reflexive irreflexive symmetric antisymmetric asymmetric connected strongly_connected transitive Function-like one-to-one constant functional ext-real non positive non negative V29() V30() V31() V32() V34() V35() V36() V37() V44() FinSequence-like FinSubsequence-like FinSequence-membered Element of bool {}
X is set
P is set
x is Relation-like Function-like set
x " P is set
x .: X is set
x .: (x " P) is set
X is set
P is set
x is set
[:P,x:] is Relation-like set
pr1 (P,x) is Relation-like [:P,x:] -defined P -valued Function-like V41([:P,x:],P) Element of bool [:[:P,x:],P:]
[:[:P,x:],P:] is Relation-like set
bool [:[:P,x:],P:] is non empty set
.: (pr1 (P,x)) is Relation-like Function-like set
(.: (pr1 (P,x))) . X is set
(pr1 (P,x)) .: X is Element of bool P
bool P is non empty set
dom (pr1 (P,x)) is Relation-like P -defined x -valued Element of bool [:P,x:]
bool [:P,x:] is non empty set
X is set
P is set
x is set
[:P,x:] is Relation-like set
pr2 (P,x) is Relation-like [:P,x:] -defined x -valued Function-like V41([:P,x:],x) Element of bool [:[:P,x:],x:]
[:[:P,x:],x:] is Relation-like set
bool [:[:P,x:],x:] is non empty set
.: (pr2 (P,x)) is Relation-like Function-like set
(.: (pr2 (P,x))) . X is set
(pr2 (P,x)) .: X is Element of bool x
bool x is non empty set
dom (pr2 (P,x)) is Relation-like P -defined x -valued Element of bool [:P,x:]
bool [:P,x:] is non empty set
X is set
bool X is non empty set
P is set
bool P is non empty set
[:X,P:] is Relation-like set
pr1 (X,P) is Relation-like [:X,P:] -defined X -valued Function-like V41([:X,P:],X) Element of bool [:[:X,P:],X:]
[:[:X,P:],X:] is Relation-like set
bool [:[:X,P:],X:] is non empty set
pr2 (X,P) is Relation-like [:X,P:] -defined P -valued Function-like V41([:X,P:],P) Element of bool [:[:X,P:],P:]
[:[:X,P:],P:] is Relation-like set
bool [:[:X,P:],P:] is non empty set
x is Element of bool X
a is Element of bool P
[:x,a:] is Relation-like X -defined P -valued Element of bool [:X,P:]
bool [:X,P:] is non empty set
(pr1 (X,P)) .: [:x,a:] is Element of bool X
(pr2 (X,P)) .: [:x,a:] is Element of bool P
the Element of a is Element of a
c is set
B is set
(pr1 (X,P)) . B is set
B `2 is set
B `1 is set
(pr1 (X,P)) . ((B `1),(B `2)) is set
[(B `1),(B `2)] is non empty V38() set
{(B `1),(B `2)} is non empty set
{(B `1)} is non empty trivial set
{{(B `1),(B `2)},{(B `1)}} is non empty set
(pr1 (X,P)) . [(B `1),(B `2)] is set
(pr1 (X,P)) . (c, the Element of a) is set
[c, the Element of a] is non empty V38() set
{c, the Element of a} is non empty set
{c} is non empty trivial set
{{c, the Element of a},{c}} is non empty set
(pr1 (X,P)) . [c, the Element of a] is set
the Element of x is Element of x
c is set
B is set
(pr2 (X,P)) . B is set
B `1 is set
B `2 is set
(pr2 (X,P)) . ((B `1),(B `2)) is set
[(B `1),(B `2)] is non empty V38() set
{(B `1),(B `2)} is non empty set
{(B `1)} is non empty trivial set
{{(B `1),(B `2)},{(B `1)}} is non empty set
(pr2 (X,P)) . [(B `1),(B `2)] is set
(pr2 (X,P)) . ( the Element of x,c) is set
[ the Element of x,c] is non empty V38() set
{ the Element of x,c} is non empty set
{ the Element of x} is non empty trivial set
{{ the Element of x,c},{ the Element of x}} is non empty set
(pr2 (X,P)) . [ the Element of x,c] is set
X is set
bool X is non empty set
P is set
bool P is non empty set
pr1 (X,P) is Relation-like [:X,P:] -defined X -valued Function-like V41([:X,P:],X) Element of bool [:[:X,P:],X:]
[:X,P:] is Relation-like set
[:[:X,P:],X:] is Relation-like set
bool [:[:X,P:],X:] is non empty set
.: (pr1 (X,P)) is Relation-like Function-like set
pr2 (X,P) is Relation-like [:X,P:] -defined P -valued Function-like V41([:X,P:],P) Element of bool [:[:X,P:],P:]
[:[:X,P:],P:] is Relation-like set
bool [:[:X,P:],P:] is non empty set
.: (pr2 (X,P)) is Relation-like Function-like set
x is Element of bool X
a is Element of bool P
[:x,a:] is Relation-like X -defined P -valued Element of bool [:X,P:]
bool [:X,P:] is non empty set
(.: (pr1 (X,P))) . [:x,a:] is set
(.: (pr2 (X,P))) . [:x,a:] is set
(pr1 (X,P)) .: [:x,a:] is Element of bool X
(pr2 (X,P)) .: [:x,a:] is Element of bool P
X is set
bool X is non empty set
P is set
[:X,P:] is Relation-like set
bool [:X,P:] is non empty set
bool (bool [:X,P:]) is non empty set
bool P is non empty set
pr1 (X,P) is Relation-like [:X,P:] -defined X -valued Function-like V41([:X,P:],X) Element of bool [:[:X,P:],X:]
[:[:X,P:],X:] is Relation-like set
bool [:[:X,P:],X:] is non empty set
.: (pr1 (X,P)) is Relation-like Function-like set
pr2 (X,P) is Relation-like [:X,P:] -defined P -valued Function-like V41([:X,P:],P) Element of bool [:[:X,P:],P:]
[:[:X,P:],P:] is Relation-like set
bool [:[:X,P:],P:] is non empty set
.: (pr2 (X,P)) is Relation-like Function-like set
x is Relation-like X -defined P -valued Element of bool [:X,P:]
a is Element of bool (bool [:X,P:])
(.: (pr1 (X,P))) .: a is set
union ((.: (pr1 (X,P))) .: a) is set
(.: (pr2 (X,P))) .: a is set
meet ((.: (pr2 (X,P))) .: a) is set
[:(union ((.: (pr1 (X,P))) .: a)),(meet ((.: (pr2 (X,P))) .: a)):] is Relation-like set
b is set
c is set
[b,c] is non empty V38() set
{b,c} is non empty set
{b} is non empty trivial set
{{b,c},{b}} is non empty set
B is set
proj1 (.: (pr1 (X,P))) is set
u is set
(.: (pr1 (X,P))) . u is set
X1 is Element of bool X
Y1 is Element of bool P
[:X1,Y1:] is Relation-like X -defined P -valued Element of bool [:X,P:]
bool [:X,P:] is non empty Element of bool (bool [:X,P:])
dom (pr2 (X,P)) is Relation-like X -defined P -valued Element of bool [:X,P:]
bool (dom (pr2 (X,P))) is non empty Element of bool (bool (dom (pr2 (X,P))))
bool (dom (pr2 (X,P))) is non empty set
bool (bool (dom (pr2 (X,P)))) is non empty set
proj1 (.: (pr2 (X,P))) is set
(.: (pr2 (X,P))) . u is set
X is set
bool X is non empty set
P is set
[:X,P:] is Relation-like set
bool [:X,P:] is non empty set
bool (bool [:X,P:]) is non empty set
bool P is non empty set
pr1 (X,P) is Relation-like [:X,P:] -defined X -valued Function-like V41([:X,P:],X) Element of bool [:[:X,P:],X:]
[:[:X,P:],X:] is Relation-like set
bool [:[:X,P:],X:] is non empty set
.: (pr1 (X,P)) is Relation-like Function-like set
pr2 (X,P) is Relation-like [:X,P:] -defined P -valued Function-like V41([:X,P:],P) Element of bool [:[:X,P:],P:]
[:[:X,P:],P:] is Relation-like set
bool [:[:X,P:],P:] is non empty set
.: (pr2 (X,P)) is Relation-like Function-like set
x is Relation-like X -defined P -valued Element of bool [:X,P:]
a is Element of bool (bool [:X,P:])
(.: (pr1 (X,P))) .: a is set
meet ((.: (pr1 (X,P))) .: a) is set
(.: (pr2 (X,P))) .: a is set
union ((.: (pr2 (X,P))) .: a) is set
[:(meet ((.: (pr1 (X,P))) .: a)),(union ((.: (pr2 (X,P))) .: a)):] is Relation-like set
b is set
c is set
[b,c] is non empty V38() set
{b,c} is non empty set
{b} is non empty trivial set
{{b,c},{b}} is non empty set
B is set
proj1 (.: (pr2 (X,P))) is set
u is set
(.: (pr2 (X,P))) . u is set
X1 is Element of bool X
Y1 is Element of bool P
[:X1,Y1:] is Relation-like X -defined P -valued Element of bool [:X,P:]
bool [:X,P:] is non empty Element of bool (bool [:X,P:])
dom (pr1 (X,P)) is Relation-like X -defined P -valued Element of bool [:X,P:]
bool (dom (pr1 (X,P))) is non empty Element of bool (bool (dom (pr1 (X,P))))
bool (dom (pr1 (X,P))) is non empty set
bool (bool (dom (pr1 (X,P)))) is non empty set
proj1 (.: (pr1 (X,P))) is set
(.: (pr1 (X,P))) . u is set
X is set
bool X is non empty set
bool (bool X) is non empty set
P is non empty set
[:X,P:] is Relation-like set
bool [:X,P:] is non empty set
bool P is non empty set
x is Relation-like X -defined P -valued Function-like total V41(X,P) Element of bool [:X,P:]
.: x is non empty Relation-like bool X -defined bool P -valued Function-like total V41( bool X, bool P) Element of bool [:(bool X),(bool P):]
[:(bool X),(bool P):] is non empty Relation-like set
bool [:(bool X),(bool P):] is non empty set
a is Element of bool (bool X)
(.: x) .: a is Element of bool (bool P)
bool (bool P) is non empty set
union ((.: x) .: a) is Element of bool P
union a is Element of bool X
x .: (union a) is Element of bool P
dom x is Element of bool X
X is set
bool X is non empty set
bool (bool X) is non empty set
P is Element of bool (bool X)
union P is Element of bool X
union (union P) is set
{ (union b1) where b1 is Element of bool X : b1 in P } is set
union { (union b1) where b1 is Element of bool X : b1 in P } is set
x is set
a is set
b is set
union b is set
x is set
a is set
b is Element of bool X
union b is set
c is set
X is set
bool X is non empty set
bool (bool X) is non empty set
P is Element of bool (bool X)
union P is Element of bool X
bool P is non empty set
x is Element of bool P
union x is set
x ` is Element of bool P
P \ x is set
union (x `) is set
a is Element of bool X
a ` is Element of bool X
X \ a is set
b is set
c is set
X is non empty set
P is non empty set
[:X,P:] is non empty Relation-like set
bool [:X,P:] is non empty set
x is non empty set
[:X,x:] is non empty Relation-like set
bool [:X,x:] is non empty set
[:P,x:] is non empty Relation-like set
bool [:P,x:] is non empty set
a is non empty Relation-like X -defined P -valued Function-like total V41(X,P) Element of bool [:X,P:]
b is non empty Relation-like X -defined x -valued Function-like total V41(X,x) Element of bool [:X,x:]
c is set
B is Element of X
a . B is Element of P
B is Element of X
a . B is Element of P
b . B is Element of x
u is Element of x
X1 is Element of X
a . X1 is Element of P
the Element of x is Element of x
B is Element of X
a . B is Element of P
B is Element of X
a . B is Element of P
u is Element of x
X1 is Element of X
a . X1 is Element of P
b . X1 is Element of x
Y1 is set
y is Element of X
a . y is Element of P
b . y is Element of x
B is set
u is set
X1 is Element of X
a . X1 is Element of P
Y1 is Element of X
a . Y1 is Element of P
b . Y1 is Element of x
y is Element of X
a . y is Element of P
b . y is Element of x
c is non empty Relation-like P -defined x -valued Function-like total V41(P,x) Element of bool [:P,x:]
c * a is non empty Relation-like X -defined x -valued Function-like total V41(X,x) Element of bool [:X,x:]
B is Element of X
(c * a) . B is Element of x
a . B is Element of P
c . (a . B) is Element of x
b . B is Element of x
X is non empty set
P is non empty set
[:X,P:] is non empty Relation-like set
bool [:X,P:] is non empty set
x is non empty set
[:P,x:] is non empty Relation-like set
bool [:P,x:] is non empty set
a is Element of P
{a} is non empty trivial Element of bool P
bool P is non empty set
b is non empty Relation-like X -defined P -valued Function-like total V41(X,P) Element of bool [:X,P:]
b " {a} is Element of bool X
bool X is non empty set
c is non empty Relation-like P -defined x -valued Function-like total V41(P,x) Element of bool [:P,x:]
c * b is non empty Relation-like X -defined x -valued Function-like total V41(X,x) Element of bool [:X,x:]
[:X,x:] is non empty Relation-like set
bool [:X,x:] is non empty set
c . a is Element of x
{(c . a)} is non empty trivial Element of bool x
bool x is non empty set
(c * b) " {(c . a)} is Element of bool X
Im (c,a) is set
{a} is non empty trivial set
c .: {a} is set
(c * b) " (Im (c,a)) is Element of bool X
X is non empty set
P is non empty set
[:X,P:] is non empty Relation-like set
bool [:X,P:] is non empty set
x is non empty set
[:P,x:] is non empty Relation-like set
id x is non empty Relation-like x -defined x -valued reflexive symmetric antisymmetric transitive Function-like one-to-one total V41(x,x) V42(x) V43(x,x) Element of bool [:x,x:]
[:x,x:] is non empty Relation-like set
bool [:x,x:] is non empty set
a is non empty Relation-like X -defined P -valued Function-like total V41(X,P) Element of bool [:X,P:]
[:a,(id x):] is non empty Relation-like [:X,x:] -defined [:P,x:] -valued Function-like total V41([:X,x:],[:P,x:]) Element of bool [:[:X,x:],[:P,x:]:]
[:X,x:] is non empty Relation-like set
[:[:X,x:],[:P,x:]:] is non empty Relation-like set
bool [:[:X,x:],[:P,x:]:] is non empty set
b is Element of X
a . b is Element of P
c is Element of x
[:a,(id x):] . (b,c) is Element of [:P,x:]
[b,c] is non empty V38() set
{b,c} is non empty set
{b} is non empty trivial set
{{b,c},{b}} is non empty set
[:a,(id x):] . [b,c] is set
[(a . b),c] is non empty V38() Element of [:P,x:]
{(a . b),c} is non empty set
{(a . b)} is non empty trivial set
{{(a . b),c},{(a . b)}} is non empty set
(id x) . c is Element of x
[(a . b),((id x) . c)] is non empty V38() Element of [:P,x:]
{(a . b),((id x) . c)} is non empty set
{{(a . b),((id x) . c)},{(a . b)}} is non empty set
X is non empty set
bool X is non empty set
P is non empty set
[:X,P:] is non empty Relation-like set
bool [:X,P:] is non empty set
x is non empty set
bool x is non empty set
[:X,x:] is non empty Relation-like set
[:P,x:] is non empty Relation-like set
id x is non empty Relation-like x -defined x -valued reflexive symmetric antisymmetric transitive Function-like one-to-one total V41(x,x) V42(x) V43(x,x) Element of bool [:x,x:]
[:x,x:] is non empty Relation-like set
bool [:x,x:] is non empty set
a is non empty Relation-like X -defined P -valued Function-like total V41(X,P) Element of bool [:X,P:]
[:a,(id x):] is non empty Relation-like [:X,x:] -defined [:P,x:] -valued Function-like total V41([:X,x:],[:P,x:]) Element of bool [:[:X,x:],[:P,x:]:]
[:[:X,x:],[:P,x:]:] is non empty Relation-like set
bool [:[:X,x:],[:P,x:]:] is non empty set
b is Element of bool X
a .: b is Element of bool P
bool P is non empty set
c is Element of bool x
[:b,c:] is Relation-like X -defined x -valued Element of bool [:X,x:]
bool [:X,x:] is non empty set
[:a,(id x):] .: [:b,c:] is Relation-like P -defined x -valued Element of bool [:P,x:]
bool [:P,x:] is non empty set
[:(a .: b),c:] is Relation-like P -defined x -valued Element of bool [:P,x:]
(id x) .: c is Element of bool x
[:(a .: b),((id x) .: c):] is Relation-like P -defined x -valued Element of bool [:P,x:]
X is non empty set
P is non empty set
[:X,P:] is non empty Relation-like set
bool [:X,P:] is non empty set
x is non empty set
[:X,x:] is non empty Relation-like set
[:P,x:] is non empty Relation-like set
id x is non empty Relation-like x -defined x -valued reflexive symmetric antisymmetric transitive Function-like one-to-one total V41(x,x) V42(x) V43(x,x) Element of bool [:x,x:]
[:x,x:] is non empty Relation-like set
bool [:x,x:] is non empty set
a is non empty Relation-like X -defined P -valued Function-like total V41(X,P) Element of bool [:X,P:]
[:a,(id x):] is non empty Relation-like [:X,x:] -defined [:P,x:] -valued Function-like total V41([:X,x:],[:P,x:]) Element of bool [:[:X,x:],[:P,x:]:]
[:[:X,x:],[:P,x:]:] is non empty Relation-like set
bool [:[:X,x:],[:P,x:]:] is non empty set
b is Element of P
{b} is non empty trivial Element of bool P
bool P is non empty set
a " {b} is Element of bool X
bool X is non empty set
c is Element of x
[b,c] is non empty V38() Element of [:P,x:]
{b,c} is non empty set
{b} is non empty trivial set
{{b,c},{b}} is non empty set
{[b,c]} is non empty trivial Relation-like P -defined x -valued Function-like constant Element of bool [:P,x:]
bool [:P,x:] is non empty set
[:a,(id x):] " {[b,c]} is Relation-like X -defined x -valued Element of bool [:X,x:]
bool [:X,x:] is non empty set
{c} is non empty trivial Element of bool x
bool x is non empty set
[:(a " {b}),{c}:] is Relation-like X -defined x -valued Element of bool [:X,x:]
[:{b},{c}:] is non empty Relation-like P -defined x -valued Element of bool [:P,x:]
[:a,(id x):] " [:{b},{c}:] is Relation-like X -defined x -valued Element of bool [:X,x:]
(id x) " {c} is Element of bool x
[:(a " {b}),((id x) " {c}):] is Relation-like X -defined x -valued Element of bool [:X,x:]
X is non empty set
bool X is non empty set
bool (bool X) is non empty set
P is Element of bool (bool X)
bool P is non empty set
x is Element of bool P
union x is set
a is set
union P is Element of bool X
b is set
X is set
P is with_non-empty_elements (X)
bool P is non empty set
x is Element of bool P
a is Element of bool P
x /\ a is Element of bool P
union (x /\ a) is set
union x is set
union a is set
(union x) /\ (union a) is set
b is set
c is set
B is set
X is non empty set
bool X is non empty set
P is non empty with_non-empty_elements (X)
bool P is non empty set
x is Element of bool P
union x is set
x ` is Element of bool P
P \ x is set
union (x `) is set
a is Element of bool X
a ` is Element of bool X
X \ a is set
union P is Element of bool X
b is set
c is set
B is set
X is non empty set
[:X,X:] is non empty Relation-like set
bool [:X,X:] is non empty set
P is Relation-like X -defined X -valued reflexive symmetric transitive total V41(X,X) Element of bool [:X,X:]
(X,P) is non empty with_non-empty_elements (X)
X is non empty set
(X) is Relation-like X -defined X -valued reflexive symmetric transitive total V41(X,X) Element of bool [:X,X:]
[:X,X:] is non empty Relation-like set
bool [:X,X:] is non empty set
(X,(X)) is non empty with_non-empty_elements (X)
P is non empty with_non-empty_elements (X)
X is non empty set
P is non empty with_non-empty_elements (X)
[:X,P:] is non empty Relation-like set
bool [:X,P:] is non empty set
union P is Element of bool X
bool X is non empty set
x is set
a is set
x is non empty Relation-like X -defined P -valued Function-like total V41(X,P) Element of bool [:X,P:]
a is Element of X
x . a is Element of P
x is non empty Relation-like X -defined P -valued Function-like total V41(X,P) Element of bool [:X,P:]
a is non empty Relation-like X -defined P -valued Function-like total V41(X,P) Element of bool [:X,P:]
b is Element of X
x . b is Element of P
a . b is Element of P
bool X is non empty set
X is non empty set
bool X is non empty set
P is non empty with_non-empty_elements (X)
(X,P) is non empty Relation-like X -defined P -valued Function-like total V41(X,P) Element of bool [:X,P:]
[:X,P:] is non empty Relation-like set
bool [:X,P:] is non empty set
x is Element of X
(X,P) . x is Element of P
a is Element of P
X is non empty set
bool X is non empty set
P is non empty with_non-empty_elements (X)
(X,P) is non empty Relation-like X -defined P -valued Function-like total V41(X,P) Element of bool [:X,P:]
[:X,P:] is non empty Relation-like set
bool [:X,P:] is non empty set
x is Element of P
{x} is non empty trivial Element of bool P
bool P is non empty set
(X,P) " {x} is Element of bool X
a is set
(X,P) . a is set
a is set
(X,P) . a is set
X is non empty set
P is non empty with_non-empty_elements (X)
bool P is non empty set
(X,P) is non empty Relation-like X -defined P -valued Function-like total V41(X,P) Element of bool [:X,P:]
[:X,P:] is non empty Relation-like set
bool [:X,P:] is non empty set
x is Element of bool P
(X,P) " x is Element of bool X
bool X is non empty set
union x is set
a is set
(X,P) . a is set
a is set
b is set
(X,P) . a is set
X is non empty set
bool X is non empty set
P is non empty with_non-empty_elements (X)
(X,P) is non empty Relation-like X -defined P -valued Function-like total V41(X,P) Element of bool [:X,P:]
[:X,P:] is non empty Relation-like set
bool [:X,P:] is non empty set
x is Element of P
a is Element of bool X
b is Element of X
(X,P) . b is Element of P
X is non empty set
bool X is non empty set
P is non empty with_non-empty_elements (X)
(X,P) is non empty Relation-like X -defined P -valued Function-like total V41(X,P) Element of bool [:X,P:]
[:X,P:] is non empty Relation-like set
bool [:X,P:] is non empty set
x is Element of bool X
(X,P) .: x is Element of bool P
bool P is non empty set
(X,P) " ((X,P) .: x) is Element of bool X
dom (X,P) is non empty Element of bool X
a is set
(X,P) . a is set
b is Element of X
(X,P) . b is Element of P
c is Element of X
(X,P) . c is Element of P
B is Element of bool X
X is set
P is with_non-empty_elements (X)
x is set
a is set
b is set