:: EQREL_1 semantic presentation

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

F

[:F

bool [:F

X is Relation-like F

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 F

bool F

P is Relation-like F

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)

{ {b

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