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