:: PARTIT1 semantic presentation

REAL is V36() V37() V38() V42() set

NAT is V36() V37() V38() V39() V40() V41() V42() Element of bool REAL

bool REAL is non empty set

NAT is V36() V37() V38() V39() V40() V41() V42() set

bool NAT is non empty set

bool NAT is non empty set

{} is empty V36() V37() V38() V39() V40() V41() V42() set

1 is non empty ext-real positive V27() V34() V35() V36() V37() V38() V39() V40() V41() Element of NAT

union {} is set

2 is non empty ext-real positive V27() V34() V35() V36() V37() V38() V39() V40() V41() Element of NAT

0 is empty ext-real V27() V34() V35() V36() V37() V38() V39() V40() V41() V42() Element of NAT

Seg 1 is V36() V37() V38() V39() V40() V41() Element of bool NAT

3 is non empty ext-real positive V27() V34() V35() V36() V37() V38() V39() V40() V41() Element of NAT

Y is non empty set

PA is non empty with_non-empty_elements a_partition of Y

z is set

a is set

the Element of z is Element of z

{{}} is non empty set

Y is set

Y \ {{}} is Element of bool Y

bool Y is non empty set

union (Y \ {{}}) is set

union Y is set

PA is set

z is set

PA is set

z is set

Y is non empty set

z is non empty with_non-empty_elements a_partition of Y

PA is non empty with_non-empty_elements a_partition of Y

a is set

x is set

b is set

Y is non empty set

z is non empty with_non-empty_elements a_partition of Y

PA is non empty with_non-empty_elements a_partition of Y

Y is non empty set

z is non empty with_non-empty_elements a_partition of Y

PA is non empty with_non-empty_elements a_partition of Y

a is set

the Element of a is Element of a

union z is Element of bool Y

bool Y is non empty set

b is set

x1 is set

Y is non empty set

Y is non empty set

Y is non empty set

z is non empty with_non-empty_elements a_partition of Y

PA is non empty with_non-empty_elements a_partition of Y

union z is Element of bool Y

bool Y is non empty set

a is set

{ b

b is set

x1 is set

C is Element of bool Y

union { b

x1 is set

C is set

Ca is set

x1 is set

C is set

Ca is Element of bool Y

a is set

Y is non empty set

PA is non empty with_non-empty_elements a_partition of Y

{Y} is non empty set

bool Y is non empty set

bool (bool Y) is non empty set

union {Y} is set

z is Element of bool Y

a is Element of bool Y

z is set

the Element of z is Element of z

x is set

Y is non empty set

bool Y is non empty set

bool (bool Y) is non empty set

PA is non empty with_non-empty_elements a_partition of Y

z is Element of bool (bool Y)

Intersect z is Element of bool Y

x is set

x is Relation-like Function-like set

dom x is set

rng x is set

bool Y is non empty Element of bool (bool Y)

bool (bool Y) is non empty Element of bool (bool (bool Y))

bool (bool Y) is non empty set

bool (bool (bool Y)) is non empty set

b is set

x1 is set

x . x1 is set

a is non empty Element of bool (bool Y)

[:a,(bool (bool Y)):] is non empty set

bool [:a,(bool (bool Y)):] is non empty set

b is Relation-like a -defined bool (bool Y) -valued Function-like V21(a, bool (bool Y)) Element of bool [:a,(bool (bool Y)):]

{ H

x1 is Element of bool (bool (bool Y))

C is Element of bool (bool (bool Y))

Intersect C is Element of bool (bool Y)

Ca is Element of bool (bool Y)

union Ca is set

pb is set

Cb is set

b . Cb is set

pb is set

b . pb is set

Cb is set

x9 is Element of Y

EqClass (x9,PA) is Element of bool Y

meet z is Element of bool Y

y5 is set

z5 is Element of a

b . z5 is Element of bool (bool Y)

union (b . z5) is Element of bool Y

y1 is set

meet C is Element of bool (bool Y)

union Ca is Element of bool Y

pb is set

meet z is Element of bool Y

Cb is Element of Y

x9 is non empty with_non-empty_elements a_partition of Y

EqClass (Cb,x9) is Element of bool Y

y5 is set

b . y5 is set

z5 is set

y1 is Element of a

b . y1 is Element of bool (bool Y)

union (b . y1) is Element of bool Y

q is set

meet C is Element of bool (bool Y)

pb is set

Cb is set

b . Cb is set

x9 is set

meet C is Element of bool (bool Y)

fx is set

b . fx is set

union (b . fx) is set

meet z is Element of bool Y

Y is non empty set

bool Y is non empty set

PA is non empty with_non-empty_elements a_partition of Y

z is Element of bool Y

a is Element of bool Y

z /\ a is Element of bool Y

x is set

union x is set

b is set

union b is set

x /\ b is set

union (x /\ b) is set

x1 is set

C is set

Ca is set

x1 is set

C is set

x \/ b is set

x1 is set

Y is non empty set

bool Y is non empty set

PA is non empty with_non-empty_elements a_partition of Y

z is Element of bool Y

z ` is Element of bool Y

a is set

union a is set

PA \ a is Element of bool (bool Y)

bool (bool Y) is non empty set

union (PA \ a) is set

union PA is Element of bool Y

(union PA) \ (union a) is Element of bool Y

bool PA is non empty set

x is Element of bool PA

PA \ x is Element of bool (bool Y)

Y is non empty set

bool Y is non empty set

PA is non empty with_non-empty_elements a_partition of Y

z is non empty with_non-empty_elements a_partition of Y

a is Element of Y

union PA is Element of bool Y

x is set

b is set

bool (bool Y) is non empty set

{ b

x is Element of bool (bool Y)

b is Element of bool (bool Y)

x1 is set

C is Element of bool Y

meet b is Element of bool Y

Intersect b is Element of bool Y

x1 is set

C is Element of bool Y

x1 is set

C is Element of bool Y

x1 is set

C is set

union C is set

Ca is set

Ca is Element of bool Y

Ca ` is Element of bool Y

Y \ Ca is Element of bool Y

Ca /\ (Ca `) is Element of bool Y

pb is set

Ca /\ (Intersect b) is Element of bool Y

Ca /\ Ca is Element of bool Y

pb is set

Y is non empty set

bool Y is non empty set

PA is non empty with_non-empty_elements a_partition of Y

z is Element of Y

[:Y,Y:] is non empty set

bool [:Y,Y:] is non empty set

a is Relation-like Y -defined Y -valued V17(Y) V43() V45() V50() Element of bool [:Y,Y:]

Class a is non empty with_non-empty_elements a_partition of Y

Class (a,z) is Element of bool Y

{z} is non empty set

a .: {z} is set

Y is set

bool Y is non empty Element of bool (bool Y)

bool Y is non empty set

bool (bool Y) is non empty set

bool (bool Y) is non empty Element of bool (bool (bool Y))

bool (bool Y) is non empty set

bool (bool (bool Y)) is non empty set

PA is set

z is set

PA is set

z is set

a is set

Y is set

(Y) is set

PA is non empty set

{PA} is non empty set

bool PA is non empty set

bool (bool PA) is non empty set

union {PA} is set

z is Element of bool PA

a is Element of bool PA

Y is non empty set

PA is non empty with_non-empty_elements a_partition of Y

z is non empty with_non-empty_elements a_partition of Y

INTERSECTION (PA,z) is set

(INTERSECTION (PA,z)) \ {{}} is Element of bool (INTERSECTION (PA,z))

bool (INTERSECTION (PA,z)) is non empty set

bool Y is non empty set

bool (bool Y) is non empty set

bool Y is non empty Element of bool (bool Y)

b is set

x1 is set

C is set

x1 /\ C is set

b is Element of bool (bool Y)

a is Element of bool (bool Y)

b \ a is Element of bool (bool Y)

union PA is Element of bool Y

union z is Element of bool Y

x1 is Element of bool (bool Y)

union x1 is Element of bool Y

union (INTERSECTION (PA,z)) is set

(union PA) /\ (union z) is Element of bool Y

C is Element of bool Y

Ca is set

pb is set

Ca /\ pb is set

Cb is set

x9 is set

Cb /\ x9 is set

(Ca /\ pb) /\ (Cb /\ x9) is set

pb /\ Cb is set

(pb /\ Cb) /\ x9 is set

Ca /\ ((pb /\ Cb) /\ x9) is set

pb /\ (Cb /\ x9) is set

Ca /\ (pb /\ (Cb /\ x9)) is set

Ca is Element of bool Y

pb is set

Cb is set

pb /\ Cb is set

x9 is set

fx is set

x9 /\ fx is set

pb /\ x9 is set

Cb /\ fx is set

(pb /\ x9) /\ (Cb /\ fx) is set

x9 /\ Cb is set

(x9 /\ Cb) /\ fx is set

pb /\ ((x9 /\ Cb) /\ fx) is set

(pb /\ Cb) /\ (x9 /\ fx) is set

Ca is Element of bool Y

a is non empty with_non-empty_elements a_partition of Y

x is non empty with_non-empty_elements a_partition of Y

b is non empty with_non-empty_elements a_partition of Y

INTERSECTION (x,b) is set

(INTERSECTION (x,b)) \ {{}} is Element of bool (INTERSECTION (x,b))

bool (INTERSECTION (x,b)) is non empty set

INTERSECTION (b,x) is set

(INTERSECTION (b,x)) \ {{}} is Element of bool (INTERSECTION (b,x))

bool (INTERSECTION (b,x)) is non empty set

Y is non empty set

PA is non empty with_non-empty_elements a_partition of Y

(Y,PA,PA) is non empty with_non-empty_elements a_partition of Y

INTERSECTION (PA,PA) is set

(INTERSECTION (PA,PA)) \ {{}} is Element of bool (INTERSECTION (PA,PA))

bool (INTERSECTION (PA,PA)) is non empty set

z is set

a is set

x is set

a /\ x is set

z is set

z /\ z is set

Y is non empty set

PA is non empty with_non-empty_elements a_partition of Y

z is non empty with_non-empty_elements a_partition of Y

(Y,PA,z) is non empty with_non-empty_elements a_partition of Y

INTERSECTION (PA,z) is set

(INTERSECTION (PA,z)) \ {{}} is Element of bool (INTERSECTION (PA,z))

bool (INTERSECTION (PA,z)) is non empty set

a is non empty with_non-empty_elements a_partition of Y

(Y,(Y,PA,z),a) is non empty with_non-empty_elements a_partition of Y

INTERSECTION ((Y,PA,z),a) is set

(INTERSECTION ((Y,PA,z),a)) \ {{}} is Element of bool (INTERSECTION ((Y,PA,z),a))

bool (INTERSECTION ((Y,PA,z),a)) is non empty set

(Y,z,a) is non empty with_non-empty_elements a_partition of Y

INTERSECTION (z,a) is set

(INTERSECTION (z,a)) \ {{}} is Element of bool (INTERSECTION (z,a))

bool (INTERSECTION (z,a)) is non empty set

(Y,PA,(Y,z,a)) is non empty with_non-empty_elements a_partition of Y

INTERSECTION (PA,(Y,z,a)) is set

(INTERSECTION (PA,(Y,z,a))) \ {{}} is Element of bool (INTERSECTION (PA,(Y,z,a)))

bool (INTERSECTION (PA,(Y,z,a))) is non empty set

x is non empty with_non-empty_elements a_partition of Y

b is non empty with_non-empty_elements a_partition of Y

(Y,x,a) is non empty with_non-empty_elements a_partition of Y

INTERSECTION (x,a) is set

(INTERSECTION (x,a)) \ {{}} is Element of bool (INTERSECTION (x,a))

bool (INTERSECTION (x,a)) is non empty set

(Y,PA,b) is non empty with_non-empty_elements a_partition of Y

INTERSECTION (PA,b) is set

(INTERSECTION (PA,b)) \ {{}} is Element of bool (INTERSECTION (PA,b))

bool (INTERSECTION (PA,b)) is non empty set

x1 is set

C is set

Ca is set

C /\ Ca is set

pb is set

Cb is set

pb /\ Cb is set

Cb /\ Ca is set

(pb /\ Cb) /\ Ca is set

fx is set

y5 is set

x9 is set

y5 /\ fx is set

pb /\ fx is set

x1 is set

C is set

Ca is set

C /\ Ca is set

pb is set

Cb is set

pb /\ Cb is set

C /\ pb is set

(C /\ pb) /\ Cb is set

fx is set

y5 is set

x9 is set

Y is non empty set

PA is non empty with_non-empty_elements a_partition of Y

z is non empty with_non-empty_elements a_partition of Y

(Y,PA,z) is non empty with_non-empty_elements a_partition of Y

INTERSECTION (PA,z) is set

(INTERSECTION (PA,z)) \ {{}} is Element of bool (INTERSECTION (PA,z))

bool (INTERSECTION (PA,z)) is non empty set

a is set

x is set

b is set

x /\ b is set

Y is non empty set

PA is non empty with_non-empty_elements a_partition of Y

z is non empty with_non-empty_elements a_partition of Y

union PA is Element of bool Y

bool Y is non empty set

a is set

x is set

bool Y is non empty Element of bool (bool Y)

bool (bool Y) is non empty set

a is set

x is set

b is set

x1 is set

union x1 is set

union a is set

x is set

b is Element of bool Y

x is set

b is set

x1 is set

union x1 is set

x is Element of bool Y

b is set

union b is set

x1 is set

C is Element of bool Y

x /\ C is Element of bool Y

Ca is set

Ca is set

x is set

b is set

union b is set

x is Element of bool (bool Y)

b is set

x1 is set

a is non empty with_non-empty_elements a_partition of Y

x is non empty with_non-empty_elements a_partition of Y

b is set

a is non empty with_non-empty_elements a_partition of Y

x is non empty with_non-empty_elements a_partition of Y

b is non empty with_non-empty_elements a_partition of Y

x1 is set

C is set

x1 is set

C is set

x1 is set

C is set

x1 is set

C is set

Y is non empty set

PA is non empty with_non-empty_elements a_partition of Y

z is non empty with_non-empty_elements a_partition of Y

(Y,PA,z) is non empty with_non-empty_elements a_partition of Y

a is set

the Element of a is Element of a

union (Y,PA,z) is Element of bool Y

bool Y is non empty set

b is set

x1 is set

union x1 is set

C is set

a /\ C is set

Y is non empty set

PA is non empty with_non-empty_elements a_partition of Y

(Y,PA,PA) is non empty with_non-empty_elements a_partition of Y

z is set

a is set

union a is set

the Element of z is Element of z

union PA is Element of bool Y

bool Y is non empty set

b is set

x1 is set

b /\ x1 is set

Y is non empty set

PA is set

z is set

a is set

x is non empty with_non-empty_elements a_partition of Y

b is non empty with_non-empty_elements a_partition of Y

x1 is set

Y is non empty set

PA is set

x is non empty with_non-empty_elements a_partition of Y

b is non empty with_non-empty_elements a_partition of Y

(Y,x,b) is non empty with_non-empty_elements a_partition of Y

z is set

a is set

Y is non empty set

[:Y,Y:] is non empty set

bool [:Y,Y:] is non empty set

bool Y is non empty set

PA is non empty with_non-empty_elements a_partition of Y

union PA is Element of bool Y

z is set

a is set

a is non empty set

x is Element of bool Y

x is Element of bool Y

z is set

a is set

z is set

a is set

x is set

b is Element of bool Y

x1 is Element of bool Y

z is Relation-like Y -defined Y -valued V17(Y) V43() V45() V50() Element of bool [:Y,Y:]

a is set

x is set

[a,x] is set

{a,x} is non empty set

{a} is non empty set

{{a,x},{a}} is non empty set

C is Element of bool Y

b is set

x1 is set

[b,x1] is set

{b,x1} is non empty set

{b} is non empty set

{{b,x1},{b}} is non empty set

z is Relation-like Y -defined Y -valued V17(Y) V43() V45() V50() Element of bool [:Y,Y:]

z is Relation-like Y -defined Y -valued V17(Y) V43() V45() V50() Element of bool [:Y,Y:]

a is Relation-like Y -defined Y -valued V17(Y) V43() V45() V50() Element of bool [:Y,Y:]

x is set

b is set

[x,b] is set

{x,b} is non empty set

{x} is non empty set

{{x,b},{x}} is non empty set

x1 is Element of bool Y

x1 is Element of bool Y

Y is non empty set

(Y) is non empty set

PA is set

z is non empty with_non-empty_elements a_partition of Y

(Y,z) is Relation-like Y -defined Y -valued V17(Y) V43() V45() V50() Element of bool [:Y,Y:]

[:Y,Y:] is non empty set

bool [:Y,Y:] is non empty set

PA is Relation-like Function-like set

dom PA is set

z is Relation-like Function-like set

dom z is set

a is set

PA . a is set

z . a is set

x is non empty with_non-empty_elements a_partition of Y

(Y,x) is Relation-like Y -defined Y -valued V17(Y) V43() V45() V50() Element of bool [:Y,Y:]

[:Y,Y:] is non empty set

bool [:Y,Y:] is non empty set

b is non empty with_non-empty_elements a_partition of Y

(Y,b) is Relation-like Y -defined Y -valued V17(Y) V43() V45() V50() Element of bool [:Y,Y:]

Y is non empty set

PA is non empty with_non-empty_elements a_partition of Y

z is non empty with_non-empty_elements a_partition of Y

(Y,PA) is Relation-like Y -defined Y -valued V17(Y) V43() V45() V50() Element of bool [:Y,Y:]

[:Y,Y:] is non empty set

bool [:Y,Y:] is non empty set

(Y,z) is Relation-like Y -defined Y -valued V17(Y) V43() V45() V50() Element of bool [:Y,Y:]

b is set

x1 is set

[b,x1] is set

{b,x1} is non empty set

{b} is non empty set

{{b,x1},{b}} is non empty set

bool Y is non empty set

C is Element of bool Y

Ca is set

b is set

the Element of b is Element of b

{ b

Ca is set

[ the Element of b,Ca] is set

{ the Element of b,Ca} is non empty set

{ the Element of b} is non empty set

{{ the Element of b,Ca},{ the Element of b}} is non empty set

[ the Element of b, the Element of b] is set

{ the Element of b, the Element of b} is non empty set

{ the Element of b} is non empty set

{{ the Element of b, the Element of b},{ the Element of b}} is non empty set

bool Y is non empty set

pb is Element of bool Y

Cb is set

x9 is Element of Y

[ the Element of b,x9] is set

{ the Element of b,x9} is non empty set

{{ the Element of b,x9},{ the Element of b}} is non empty set

x9 is Element of bool Y

Cb is set

[ the Element of b,Cb] is set

{ the Element of b,Cb} is non empty set

{{ the Element of b,Cb},{ the Element of b}} is non empty set

Y is non empty set

PA is non empty with_non-empty_elements a_partition of Y

z is non empty with_non-empty_elements a_partition of Y

a is set

x is set

b is set

x1 is Relation-like NAT -defined Y -valued Function-like FinSequence-like FinSequence of Y

x1 . 1 is set

len x1 is ext-real V27() V34() V35() V36() V37() V38() V39() V40() V41() Element of NAT

x1 . (len x1) is set

C is set

union C is set

Ca is set

union Ca is set

union PA is Element of bool Y

bool Y is non empty set

pb is set

Cb is set

pb is set

Cb is set

x1 . 0 is set

pb is ext-real V27() V34() V35() V36() V37() V38() V39() V40() V41() Element of NAT

x1 . pb is set

pb + 1 is ext-real V27() V34() V35() V36() V37() V38() V39() V40() V41() Element of NAT

x1 . (pb + 1) is set

Cb is set

x9 is set

fx is set

y5 is set

z5 is set

y1 is set

q is set

Y is non empty set

[:Y,Y:] is non empty set

bool [:Y,Y:] is non empty set

PA is Relation-like Y -defined Y -valued V17(Y) V43() V45() V50() Element of bool [:Y,Y:]

z is Relation-like Y -defined Y -valued V17(Y) V43() V45() V50() Element of bool [:Y,Y:]

PA \/ z is Relation-like Y -defined Y -valued Element of bool [:Y,Y:]

PA "\/" z is Relation-like Y -defined Y -valued V17(Y) V43() V45() V50() Element of bool [:Y,Y:]

a is Relation-like NAT -defined Y -valued Function-like FinSequence-like FinSequence of Y

a . 1 is set

len a is ext-real V27() V34() V35() V36() V37() V38() V39() V40() V41() Element of NAT

a . (len a) is set

x is set

b is set

[x,b] is set

{x,b} is non empty set

{x} is non empty set

{{x,b},{x}} is non empty set

a . 0 is set

[(a . 1),(a . 0)] is set

{(a . 1),(a . 0)} is non empty set

{(a . 1)} is non empty set

{{(a . 1),(a . 0)},{(a . 1)}} is non empty set

x1 is ext-real V27() V34() V35() V36() V37() V38() V39() V40() V41() Element of NAT

a . x1 is set

[(a . 1),(a . x1)] is set

{(a . 1),(a . x1)} is non empty set

{{(a . 1),(a . x1)},{(a . 1)}} is non empty set

x1 + 1 is ext-real V27() V34() V35() V36() V37() V38() V39() V40() V41() Element of NAT

a . (x1 + 1) is set

[(a . 1),(a . (x1 + 1))] is set

{(a . 1),(a . (x1 + 1))} is non empty set

{{(a . 1),(a . (x1 + 1))},{(a . 1)}} is non empty set

C is set

[(a . x1),C] is set

{(a . x1),C} is non empty set

{(a . x1)} is non empty set

{{(a . x1),C},{(a . x1)}} is non empty set

[C,(a . (x1 + 1))] is set

{C,(a . (x1 + 1))} is non empty set

{C} is non empty set

{{C,(a . (x1 + 1))},{C}} is non empty set

dom a is V36() V37() V38() V39() V40() V41() Element of bool NAT

Seg (len a) is V36() V37() V38() V39() V40() V41() Element of bool NAT

pb is Element of Y

Ca is Element of Y

Cb is Element of Y

<*pb,Ca,Cb*> is Relation-like NAT -defined Y -valued Function-like FinSequence-like FinSequence of Y

x9 is Relation-like NAT -defined Y -valued Function-like FinSequence-like FinSequence of Y

len x9 is ext-real V27() V34() V35() V36() V37() V38() V39() V40() V41() Element of NAT

x9 . 1 is set

x9 . 3 is set

fx is ext-real V27() V34() V35() V36() V37() V38() V39() V40() V41() Element of NAT

x9 . fx is set

fx + 1 is ext-real V27() V34() V35() V36() V37() V38() V39() V40() V41() Element of NAT

x9 . (fx + 1) is set

[(x9 . fx),(x9 . (fx + 1))] is set

{(x9 . fx),(x9 . (fx + 1))} is non empty set

{(x9 . fx)} is non empty set

{{(x9 . fx),(x9 . (fx + 1))},{(x9 . fx)}} is non empty set

2 + 1 is ext-real V27() V34() V35() V36() V37() V38() V39() V40() V41() Element of NAT

[(a . x1),(a . (x1 + 1))] is set

{(a . x1),(a . (x1 + 1))} is non empty set

{{(a . x1),(a . (x1 + 1))},{(a . x1)}} is non empty set

[(a . 1),(a . 1)] is set

{(a . 1),(a . 1)} is non empty set

{{(a . 1),(a . 1)},{(a . 1)}} is non empty set

Y is non empty set

PA is non empty with_non-empty_elements a_partition of Y

z is non empty with_non-empty_elements a_partition of Y

(Y,PA,z) is non empty with_non-empty_elements a_partition of Y

(Y,(Y,PA,z)) is Relation-like Y -defined Y -valued V17(Y) V43() V45() V50() Element of bool [:Y,Y:]

[:Y,Y:] is non empty set

bool [:Y,Y:] is non empty set

(Y,PA) is Relation-like Y -defined Y -valued V17(Y) V43() V45() V50() Element of bool [:Y,Y:]

(Y,z) is Relation-like Y -defined Y -valued V17(Y) V43() V45() V50() Element of bool [:Y,Y:]

(Y,PA) "\/" (Y,z) is Relation-like Y -defined Y -valued V17(Y) V43() V45() V50() Element of bool [:Y,Y:]

union PA is Element of bool Y

bool Y is non empty set

union z is Element of bool Y

a is set

x is set

[a,x] is set

{a,x} is non empty set

{a} is non empty set

{{a,x},{a}} is non empty set

b is Element of bool Y

x1 is set

union x1 is set

C is set

{ b

( 1 <= len b

( not 1 <= b

( b

Ca is set

union Ca is set

{ b

( b

x9 is Element of Y

<*x9*> is Relation-like NAT -defined Y -valued Function-like FinSequence-like FinSequence of Y

fx is Relation-like NAT -defined Y -valued Function-like FinSequence-like FinSequence of Y

fx . 1 is set

len fx is ext-real V27() V34() V35() V36() V37() V38() V39() V40() V41() Element of NAT

fx . (len fx) is set

y5 is ext-real V27() V34() V35() V36() V37() V38() V39() V40() V41() Element of NAT

fx . y5 is set

y5 + 1 is ext-real V27() V34() V35() V36() V37() V38() V39() V40() V41() Element of NAT

fx . (y5 + 1) is set

y5 is set

z5 is set

y5 /\ z5 is set

Cb is set

y1 is set

q is Element of PA

fd is Relation-like NAT -defined Y -valued Function-like FinSequence-like FinSequence of Y

len fd is ext-real V27() V34() V35() V36() V37() V38() V39() V40() V41() Element of NAT

fd . 1 is set

fd . (len fd) is set

pb is set

union Cb is set

y1 is set

q is set

fd is Element of PA

y9 is Relation-like NAT -defined Y -valued Function-like FinSequence-like FinSequence of Y

len y9 is ext-real V27() V34() V35() V36() V37() V38() V39() V40() V41() Element of NAT

y9 . 1 is set

y9 . (len y9) is set

fd is set

q /\ fd is set

y1 is set

q is set

fd is Element of z

y9 is set

fd /\ y9 is Element of bool Y

fd is set

q /\ fd is set

y9 is Element of z

f is set

y9 /\ f is Element of bool Y

y9 is set

f is Element of PA

z0 is Relation-like NAT -defined Y -valued Function-like FinSequence-like FinSequence of Y

len z0 is ext-real V27() V34() V35() V36() V37() V38() V39() V40() V41() Element of NAT

z0 . 1 is set

z0 . (len z0) is set

f is Relation-like NAT -defined Y -valued Function-like FinSequence-like FinSequence of Y

len f is ext-real V27() V34() V35() V36() V37() V38() V39() V40() V41() Element of NAT

f . 1 is set

f . (len f) is set

i is Element of z

p1 is set

i /\ p1 is Element of bool Y

z0 is Element of Y

<*z0*> is Relation-like NAT -defined Y -valued Function-like FinSequence-like FinSequence of Y

f ^ <*z0*> is Relation-like NAT -defined Y -valued Function-like FinSequence-like FinSequence of Y

i is Relation-like NAT -defined Y -valued Function-like FinSequence-like FinSequence of Y

len i is ext-real V27() V34() V35() V36() V37() V38() V39() V40() V41() Element of NAT

len <*z0*> is ext-real V27() V34() V35() V36() V37() V38() V39() V40() V41() Element of NAT

(len f) + (len <*z0*>) is ext-real V27() V34() V35() V36() V37() V38() V39() V40() V41() Element of NAT

(len f) + 1 is ext-real V27() V34() V35() V36() V37() V38() V39() V40() V41() Element of NAT

1 + 1 is ext-real V27() V34() V35() V36() V37() V38() V39() V40() V41() Element of NAT

i . ((len f) + 1) is set

p1 is set

dom f is V36() V37() V38() V39() V40() V41() Element of bool NAT

Seg (len f) is V36() V37() V38() V39() V40() V41() Element of bool NAT

p2 is ext-real V27() V34() V35() V36() V37() V38() V39() V40() V41() Element of NAT

i . p2 is set

f . p2 is set

(f ^ <*z0*>) . ((len f) + 1) is set

i . 1 is set

i . (len f) is set

p2 is ext-real V27() V34() V35() V36() V37() V38() V39() V40() V41() Element of NAT

i . p2 is set

p2 + 1 is ext-real V27() V34() V35() V36() V37() V38() V39() V40() V41() Element of NAT

i . (p2 + 1) is set

f . p2 is set

f . (p2 + 1) is set

p2 is ext-real V27() V34() V35() V36() V37() V38() V39() V40() V41() Element of NAT

i . p2 is set

p2 + 1 is ext-real V27() V34() V35() V36() V37() V38() V39() V40() V41() Element of NAT

i . (p2 + 1) is set

u is Element of z

x2 is set

u /\ x2 is Element of bool Y

y2 is Element of PA

c

len c

c

c

u is set

x2 is set

y2 is set

u /\ x2 is set

c

c

c

c

y1 is set

q is Element of z

fd is set

q /\ fd is Element of bool Y

pb \ b is Element of bool pb

bool pb is non empty set

y1 is set

q is set

fd is Element of z

y9 is set

fd /\ y9 is Element of bool Y

fd is set

q /\ fd is set

y9 is Element of PA

f is Relation-like NAT -defined Y -valued Function-like FinSequence-like FinSequence of Y

len f is ext-real V27() V34() V35() V36() V37() V38() V39() V40() V41() Element of NAT

f . 1 is set

f . (len f) is set

y9 is Relation-like NAT -defined Y -valued Function-like FinSequence-like FinSequence of Y

len y9 is ext-real V27() V34() V35() V36() V37() V38() V39() V40() V41() Element of NAT

y9 . 1 is set

y9 . (len y9) is set

z0 is Element of z

i is set

z0 /\ i is Element of bool Y

f is Element of Y

<*f*> is Relation-like NAT -defined Y -valued Function-like FinSequence-like FinSequence of Y

y9 ^ <*f*> is Relation-like NAT -defined Y -valued Function-like FinSequence-like FinSequence of Y

z0 is Relation-like NAT -defined Y -valued Function-like FinSequence-like FinSequence of Y

len z0 is ext-real V27() V34() V35() V36() V37() V38() V39() V40() V41() Element of NAT

len <*f*> is ext-real V27() V34() V35() V36() V37() V38() V39() V40() V41() Element of NAT

(len y9) + (len <*f*>) is ext-real V27() V34() V35() V36() V37() V38() V39() V40() V41() Element of NAT

(len y9) + 1 is ext-real V27() V34() V35() V36() V37() V38() V39() V40() V41() Element of NAT

1 + 1 is ext-real V27() V34() V35() V36() V37() V38() V39() V40() V41() Element of NAT

z0 . ((len y9) + 1) is set

i is set

dom y9 is V36() V37() V38() V39() V40() V41() Element of bool NAT

Seg (len y9) is V36() V37() V38() V39() V40() V41() Element of bool NAT

p1 is ext-real V27() V34() V35() V36() V37() V38() V39() V40() V41() Element of NAT

z0 . p1 is set

y9 . p1 is set

(y9 ^ <*f*>) . ((len y9) + 1) is set

z0 . 1 is set

z0 . (len y9) is set

p1 is ext-real V27() V34() V35() V36() V37() V38() V39() V40() V41() Element of NAT

z0 . p1 is set

p1 + 1 is ext-real V27() V34() V35() V36() V37() V38() V39() V40() V41() Element of NAT

z0 . (p1 + 1) is set

y9 . p1 is set

y9 . (p1 + 1) is set

p1 is ext-real V27() V34() V35() V36() V37() V38() V39() V40() V41() Element of NAT

z0 . p1 is set

p1 + 1 is ext-real V27() V34() V35() V36() V37() V38() V39() V40() V41() Element of NAT

z0 . (p1 + 1) is set

p2 is Element of z

u is set

p2 /\ u is Element of bool Y

x2 is Element of PA

y2 is Relation-like NAT -defined Y -valued Function-like FinSequence-like FinSequence of Y

len y2 is ext-real V27() V34() V35() V36() V37() V38() V39() V40() V41() Element of NAT

y2 . 1 is set

y2 . (len y2) is set

p2 is set

u is set

x2 is set

p2 /\ u is set

y2 is set

c

c

y2 /\ c

p1 is ext-real V27() V34() V35() V36() V37() V38() V39() V40() V41() Element of NAT

z0 . p1 is set

p1 + 1 is ext-real V27() V34() V35() V36() V37() V38() V39() V40() V41() Element of NAT

z0 . (p1 + 1) is set

p2 is set

u is set

x2 is set

p2 /\ u is set

y1 is set

q is Element of z

fd is set

q /\ fd is Element of bool Y

q is set

y1 /\ q is set

fd is Element of PA

y9 is Relation-like NAT -defined Y -valued Function-like FinSequence-like FinSequence of Y

len y9 is ext-real V27() V34() V35() V36() V37() V38() V39() V40() V41() Element of NAT

y9 . 1 is set

y9 . (len y9) is set

fd is Relation-like NAT -defined Y -valued Function-like FinSequence-like FinSequence of Y

len fd is ext-real V27() V34() V35() V36() V37() V38() V39() V40() V41() Element of NAT

fd . 1 is set

fd . (len fd) is set

y9 is Element of Y

<*y9*> is Relation-like NAT -defined Y -valued Function-like FinSequence-like FinSequence of Y

fd ^ <*y9*> is Relation-like NAT -defined Y -valued Function-like FinSequence-like FinSequence of Y

f is Relation-like NAT -defined Y -valued Function-like FinSequence-like FinSequence of Y

len f is ext-real V27() V34() V35() V36() V37() V38() V39() V40() V41() Element of NAT

len <*y9*> is ext-real V27() V34() V35() V36() V37() V38() V39() V40() V41() Element of NAT

(len fd) + (len <*y9*>) is ext-real V27() V34() V35() V36() V37() V38() V39() V40() V41() Element of NAT

(len fd) + 1 is ext-real V27() V34() V35() V36() V37() V38() V39() V40() V41() Element of NAT

f . ((len fd) + 1) is set

z0 is set

dom fd is V36() V37() V38() V39() V40() V41() Element of bool NAT

Seg (len fd) is V36() V37() V38() V39() V40() V41() Element of bool NAT

i is ext-real V27() V34() V35() V36() V37() V38() V39() V40() V41() Element of NAT

f . i is set

fd . i is set

f . (len fd) is set

i is ext-real V27() V34() V35() V36() V37() V38() V39() V40() V41() Element of NAT

f . i is set

i + 1 is ext-real V27() V34() V35() V36() V37() V38() V39() V40() V41() Element of NAT

f . (i + 1) is set

fd . i is set

fd . (i + 1) is set

i is ext-real V27() V34() V35() V36() V37() V38() V39() V40() V41() Element of NAT

f . i is set

i + 1 is ext-real V27() V34() V35() V36() V37() V38() V39() V40() V41() Element of NAT

f . (i + 1) is set

p1 is Element of z

p2 is set

p1 /\ p2 is Element of bool Y

u is Element of PA

x2 is Relation-like NAT -defined Y -valued Function-like FinSequence-like FinSequence of Y

len x2 is ext-real V27() V34() V35() V36() V37() V38() V39() V40() V41() Element of NAT

x2 . 1 is set

x2 . (len x2) is set

p1 is set

p2 is set

u is set

p1 /\ p2 is set

x2 is set

y2 is set

c

x2 /\ y2 is set

(fd ^ <*y9*>) . ((len fd) + 1) is set

f . 1 is set

(Y,PA) \/ (Y,z) is Relation-like Y -defined Y -valued Element of bool [:Y,Y:]

i is ext-real V27() V34() V35() V36() V37() V38() V39() V40() V41() Element of NAT

f . i is set

i + 1 is ext-real V27() V34() V35() V36() V37() V38() V39() V40() V41() Element of NAT

f . (i + 1) is set

p1 is set

p2 is set

u is set

p1 /\ p2 is set

x2 is set

[x2,u] is set

{x2,u} is non empty set

{x2} is non empty set

{{x2,u},{x2}} is non empty set

y2 is set

[u,y2] is set

{u,y2} is non empty set

{u} is non empty set

{{u,y2},{u}} is non empty set

[x9,y9] is set

{x9,y9} is non empty set

{x9} is non empty set

{{x9,y9},{x9}} is non empty set

(Y,PA) \/ (Y,z) is Relation-like Y -defined Y -valued Element of bool [:Y,Y:]

a is set

x is set

[a,x] is set

{a,x} is non empty set

{a} is non empty set

{{a,x},{a}} is non empty set

b is Element of bool Y

b is Element of bool Y

x1 is set

b is Element of bool Y

b is Element of bool Y

x1 is set

b is Element of bool Y

x1 is Element of bool Y

b is Element of bool Y

x1 is Element of bool Y

Y is non empty set

PA is non empty with_non-empty_elements a_partition of Y

z is non empty with_non-empty_elements a_partition of Y

(Y,PA,z) is non empty with_non-empty_elements a_partition of Y

INTERSECTION (PA,z) is set

(INTERSECTION (PA,z)) \ {{}} is Element of bool (INTERSECTION (PA,z))

bool (INTERSECTION (PA,z)) is non empty set

(Y,(Y,PA,z)) is Relation-like Y -defined Y -valued V17(Y) V43() V45() V50() Element of bool [:Y,Y:]

[:Y,Y:] is non empty set

bool [:Y,Y:] is non empty set

(Y,PA) is Relation-like Y -defined Y -valued V17(Y) V43() V45() V50() Element of bool [:Y,Y:]

(Y,z) is Relation-like Y -defined Y -valued V17(Y) V43() V45() V50() Element of bool [:Y,Y:]

(Y,PA) /\ (Y,z) is Relation-like Y -defined Y -valued V17(Y) V43() V45() V50() Element of bool [:Y,Y:]

a is set

x is set

[a,x] is set

{a,x} is non empty set

{a} is non empty set

{{a,x},{a}} is non empty set

bool Y is non empty set

b is Element of bool Y

x1 is set

x1 is set

b is Element of bool Y

x1 is Element of bool Y

b /\ x1 is Element of bool Y

C is Element of bool Y

Y is non empty set

PA is non empty with_non-empty_elements a_partition of Y

(Y,PA) is Relation-like Y -defined Y -valued V17(Y) V43() V45() V50() Element of bool [:Y,Y:]

[:Y,Y:] is non empty set

bool [:Y,Y:] is non empty set

z is non empty with_non-empty_elements a_partition of Y

(Y,z) is Relation-like Y -defined Y -valued V17(Y) V43() V45() V50() Element of bool [:Y,Y:]

Y is non empty set

PA is non empty with_non-empty_elements a_partition of Y

z is non empty with_non-empty_elements a_partition of Y

(Y,PA,z) is non empty with_non-empty_elements a_partition of Y

a is non empty with_non-empty_elements a_partition of Y

(Y,(Y,PA,z),a) is non empty with_non-empty_elements a_partition of Y

(Y,z,a) is non empty with_non-empty_elements a_partition of Y

(Y,PA,(Y,z,a)) is non empty with_non-empty_elements a_partition of Y

(Y,(Y,(Y,PA,z),a)) is Relation-like Y -defined Y -valued V17(Y) V43() V45() V50() Element of bool [:Y,Y:]

[:Y,Y:] is non empty set

bool [:Y,Y:] is non empty set

(Y,(Y,PA,z)) is Relation-like Y -defined Y -valued V17(Y) V43() V45() V50() Element of bool [:Y,Y:]

(Y,a) is Relation-like Y -defined Y -valued V17(Y) V43() V45() V50() Element of bool [:Y,Y:]

(Y,(Y,PA,z)) "\/" (Y,a) is Relation-like Y -defined Y -valued V17(Y) V43() V45() V50() Element of bool [:Y,Y:]

(Y,PA) is Relation-like Y -defined Y -valued V17(Y) V43() V45() V50() Element of bool [:Y,Y:]

(Y,z) is Relation-like Y -defined Y -valued V17(Y) V43() V45() V50() Element of bool [:Y,Y:]

(Y,PA) "\/" (Y,z) is Relation-like Y -defined Y -valued V17(Y) V43() V45() V50() Element of bool [:Y,Y:]

((Y,PA) "\/" (Y,z)) "\/" (Y,a) is Relation-like Y -defined Y -valued V17(Y) V43() V45() V50() Element of bool [:Y,Y:]

(Y,z) "\/" (Y,a) is Relation-like Y -defined Y -valued V17(Y) V43() V45() V50() Element of bool [:Y,Y:]

(Y,PA) "\/" ((Y,z) "\/" (Y,a)) is Relation-like Y -defined Y -valued V17(Y) V43() V45() V50() Element of bool [:Y,Y:]

(Y,(Y,z,a)) is Relation-like Y -defined Y -valued V17(Y) V43() V45() V50() Element of bool [:Y,Y:]

(Y,PA) "\/" (Y,(Y,z,a)) is Relation-like Y -defined Y -valued V17(Y) V43() V45() V50() Element of bool [:Y,Y:]

(Y,(Y,PA,(Y,z,a))) is Relation-like Y -defined Y -valued V17(Y) V43() V45() V50() Element of bool [:Y,Y:]

Y is non empty set

PA is non empty with_non-empty_elements a_partition of Y

z is non empty with_non-empty_elements a_partition of Y

(Y,PA,z) is non empty with_non-empty_elements a_partition of Y

(Y,PA,(Y,PA,z)) is non empty with_non-empty_elements a_partition of Y

INTERSECTION (PA,(Y,PA,z)) is set

(INTERSECTION (PA,(Y,PA,z))) \ {{}} is Element of bool (INTERSECTION (PA,(Y,PA,z)))

bool (INTERSECTION (PA,(Y,PA,z))) is non empty set

(Y,(Y,PA,(Y,PA,z))) is Relation-like Y -defined Y -valued V17(Y) V43() V45() V50() Element of bool [:Y,Y:]

[:Y,Y:] is non empty set

bool [:Y,Y:] is non empty set

(Y,PA) is Relation-like Y -defined Y -valued V17(Y) V43() V45() V50() Element of bool [:Y,Y:]

(Y,(Y,PA,z)) is Relation-like Y -defined Y -valued V17(Y) V43() V45() V50() Element of bool [:Y,Y:]

(Y,PA) /\ (Y,(Y,PA,z)) is Relation-like Y -defined Y -valued V17(Y) V43() V45() V50() Element of bool [:Y,Y:]

(Y,z) is Relation-like Y -defined Y -valued V17(Y) V43() V45() V50() Element of bool [:Y,Y:]

(Y,PA) "\/" (Y,z) is Relation-like Y -defined Y -valued V17(Y) V43() V45() V50() Element of bool [:Y,Y:]

(Y,PA) /\ ((Y,PA) "\/" (Y,z)) is Relation-like Y -defined Y -valued V17(Y) V43() V45() V50() Element of bool [:Y,Y:]

Y is non empty set

PA is non empty with_non-empty_elements a_partition of Y

z is non empty with_non-empty_elements a_partition of Y

(Y,PA,z) is non empty with_non-empty_elements a_partition of Y

INTERSECTION (PA,z) is set

(INTERSECTION (PA,z)) \ {{}} is Element of bool (INTERSECTION (PA,z))

bool (INTERSECTION (PA,z)) is non empty set

(Y,PA,(Y,PA,z)) is non empty with_non-empty_elements a_partition of Y

(Y,(Y,PA,(Y,PA,z))) is Relation-like Y -defined Y -valued V17(Y) V43() V45() V50() Element of bool [:Y,Y:]

[:Y,Y:] is non empty set

bool [:Y,Y:] is non empty set

(Y,PA) is Relation-like Y -defined Y -valued V17(Y) V43() V45() V50() Element of bool [:Y,Y:]

(Y,(Y,PA,z)) is Relation-like Y -defined Y -valued V17(Y) V43() V45() V50() Element of bool [:Y,Y:]

(Y,PA) "\/" (Y,(Y,PA,z)) is Relation-like Y -defined Y -valued V17(Y) V43() V45() V50() Element of bool [:Y,Y:]

(Y,z) is Relation-like Y -defined Y -valued V17(Y) V43() V45() V50() Element of bool [:Y,Y:]

(Y,PA) /\ (Y,z) is Relation-like Y -defined Y -valued V17(Y) V43() V45() V50() Element of bool [:Y,Y:]

(Y,PA) "\/" ((Y,PA) /\ (Y,z)) is Relation-like Y -defined Y -valued V17(Y) V43() V45() V50() Element of bool [:Y,Y:]

Y is non empty set

PA is non empty with_non-empty_elements a_partition of Y

a is non empty with_non-empty_elements a_partition of Y

z is non empty with_non-empty_elements a_partition of Y

(Y,PA,z) is non empty with_non-empty_elements a_partition of Y

(Y,PA) is Relation-like Y -defined Y -valued V17(Y) V43() V45() V50() Element of bool [:Y,Y:]

[:Y,Y:] is non empty set

bool [:Y,Y:] is non empty set

(Y,a) is Relation-like Y -defined Y -valued V17(Y) V43() V45() V50() Element of bool [:Y,Y:]

(Y,z) is Relation-like Y -defined Y -valued V17(Y) V43() V45() V50() Element of bool [:Y,Y:]

(Y,(Y,PA,z)) is Relation-like Y -defined Y -valued V17(Y) V43() V45() V50() Element of bool [:Y,Y:]

(Y,PA) "\/" (Y,z) is Relation-like Y -defined Y -valued V17(Y) V43() V45() V50() Element of bool [:Y,Y:]

(Y,PA) \/ (Y,z) is Relation-like Y -defined Y -valued Element of bool [:Y,Y:]

Y is non empty set

a is non empty with_non-empty_elements a_partition of Y

PA is non empty with_non-empty_elements a_partition of Y

z is non empty with_non-empty_elements a_partition of Y

(Y,PA,z) is non empty with_non-empty_elements a_partition of Y

INTERSECTION (PA,z) is set

(INTERSECTION (PA,z)) \ {{}} is Element of bool (INTERSECTION (PA,z))

bool (INTERSECTION (PA,z)) is non empty set

(Y,a) is Relation-like Y -defined Y -valued V17(Y) V43() V45() V50() Element of bool [:Y,Y:]

[:Y,Y:] is non empty set

bool [:Y,Y:] is non empty set

(Y,PA) is Relation-like Y -defined Y -valued V17(Y) V43() V45() V50() Element of bool [:Y,Y:]

(Y,z) is Relation-like Y -defined Y -valued V17(Y) V43() V45() V50() Element of bool [:Y,Y:]

(Y,(Y,PA,z)) is Relation-like Y -defined Y -valued V17(Y) V43() V45() V50() Element of bool [:Y,Y:]

(Y,PA) /\ (Y,z) is Relation-like Y -defined Y -valued V17(Y) V43() V45() V50() Element of bool [:Y,Y:]

Y is non empty set

{Y} is non empty set

bool Y is non empty set

bool (bool Y) is non empty set

union {Y} is set

PA is Element of bool Y

z is Element of bool Y

Y is non empty set

SmallestPartition Y is non empty with_non-empty_elements a_partition of Y

K51(Y) is non empty Relation-like Y -defined Y -valued V17(Y) V43() V45() V46() V50() Element of bool [:Y,Y:]

[:Y,Y:] is non empty set

bool [:Y,Y:] is non empty set

Class K51(Y) is non empty with_non-empty_elements a_partition of Y

bool Y is non empty set

{ b

( b

z is set

{ {b

a is Element of Y

{a} is non empty set

x is Element of Y

{x} is non empty set

b is Element of bool Y

z is set

{ {b

a is Element of bool Y

x is set

{x} is non empty set

Y is non empty set

(Y) is non empty with_non-empty_elements a_partition of Y

{Y} is non empty set

SmallestPartition Y is non empty with_non-empty_elements a_partition of Y

K51(Y) is non empty Relation-like Y -defined Y -valued V17(Y) V43() V45() V46() V50() Element of bool [:Y,Y:]

[:Y,Y:] is non empty set

bool [:Y,Y:] is non empty set

Class K51(Y) is non empty with_non-empty_elements a_partition of Y

PA is non empty with_non-empty_elements a_partition of Y

z is set

the Element of z is Element of z

union (Y) is Element of bool Y

bool Y is non empty set

x is set

z is set

{ {b

a is Element of Y

{a} is non empty set

the Element of z is Element of z

union PA is Element of bool Y

bool Y is non empty set

b is set

x1 is set

Y is non empty set

(Y) is non empty with_non-empty_elements a_partition of Y

{Y} is non empty set

(Y,(Y)) is Relation-like Y -defined Y -valued V17(Y) V43() V45() V50() Element of bool [:Y,Y:]

[:Y,Y:] is non empty set

bool [:Y,Y:] is non empty set

nabla Y is Relation-like Y -defined Y -valued V17(Y) V43() V45() V50() Element of bool [:Y,Y:]

PA is set

z is set

[PA,z] is set

{PA,z} is non empty set

{PA} is non empty set

{{PA,z},{PA}} is non empty set

Y is non empty set

SmallestPartition Y is non empty with_non-empty_elements a_partition of Y

K51(Y) is non empty Relation-like Y -defined Y -valued V17(Y) V43() V45() V46() V50() Element of bool [:Y,Y:]

[:Y,Y:] is non empty set

bool [:Y,Y:] is non empty set

Class K51(Y) is non empty with_non-empty_elements a_partition of Y

(Y,(SmallestPartition Y)) is Relation-like Y -defined Y -valued V17(Y) V43() V45() V50() Element of bool [:Y,Y:]

id Y is non empty Relation-like V43() V45() V46() V50() set

union (SmallestPartition Y) is Element of bool Y

bool Y is non empty set

PA is set

z is set

[PA,z] is set

{PA,z} is non empty set

{PA} is non empty set

{{PA,z},{PA}} is non empty set

a is Element of bool Y

{ {b

x is Element of Y

{x} is non empty set

PA is set

z is set

[PA,z] is set

{PA,z} is non empty set

{PA} is non empty set

{{PA,z},{PA}} is non empty set

a is set

Y is non empty set

SmallestPartition Y is non empty with_non-empty_elements a_partition of Y

K51(Y) is non empty Relation-like Y -defined Y -valued V17(Y) V43() V45() V46() V50() Element of bool [:Y,Y:]

[:Y,Y:] is non empty set

bool [:Y,Y:] is non empty set

Class K51(Y) is non empty with_non-empty_elements a_partition of Y

(Y) is non empty with_non-empty_elements a_partition of Y

{Y} is non empty set

(Y,(Y)) is Relation-like Y -defined Y -valued V17(Y) V43() V45() V50() Element of bool [:Y,Y:]

nabla Y is Relation-like Y -defined Y -valued V17(Y) V43() V45() V50() Element of bool [:Y,Y:]

(Y,(SmallestPartition Y)) is Relation-like Y -defined Y -valued V17(Y) V43() V45() V50() Element of bool [:Y,Y:]

Y is non empty set

(Y) is non empty with_non-empty_elements a_partition of Y

{Y} is non empty set

PA is non empty with_non-empty_elements a_partition of Y

(Y,(Y),PA) is non empty with_non-empty_elements a_partition of Y

(Y,(Y),PA) is non empty with_non-empty_elements a_partition of Y

INTERSECTION ((Y),PA) is set

(INTERSECTION ((Y),PA)) \ {{}} is Element of bool (INTERSECTION ((Y),PA))

bool (INTERSECTION ((Y),PA)) is non empty set

(Y,(Y,(Y),PA)) is Relation-like Y -defined Y -valued V17(Y) V43() V45() V50() Element of bool [:Y,Y:]

[:Y,Y:] is non empty set

bool [:Y,Y:] is non empty set

(Y,(Y)) is Relation-like Y -defined Y -valued V17(Y) V43() V45() V50() Element of bool [:Y,Y:]

(Y,PA) is Relation-like Y -defined Y -valued V17(Y) V43() V45() V50() Element of bool [:Y,Y:]

(Y,(Y)) "\/" (Y,PA) is Relation-like Y -defined Y -valued V17(Y) V43() V45() V50() Element of bool [:Y,Y:]

nabla Y is Relation-like Y -defined Y -valued V17(Y) V43() V45() V50() Element of bool [:Y,Y:]

(Y,(Y)) \/ (Y,PA) is Relation-like Y -defined Y -valued Element of bool [:Y,Y:]

(Y,PA,(Y)) is non empty with_non-empty_elements a_partition of Y

(Y,(Y,(Y),PA)) is Relation-like Y -defined Y -valued V17(Y) V43() V45() V50() Element of bool [:Y,Y:]

(Y,(Y)) /\ (Y,PA) is Relation-like Y -defined Y -valued V17(Y) V43() V45() V50() Element of bool [:Y,Y:]

Y is non empty set

SmallestPartition Y is non empty with_non-empty_elements a_partition of Y

K51(Y) is non empty Relation-like Y -defined Y -valued V17(Y) V43() V45() V46() V50() Element of bool [:Y,Y:]

[:Y,Y:] is non empty set

bool [:Y,Y:] is non empty set

Class K51(Y) is non empty with_non-empty_elements a_partition of Y

PA is non empty with_non-empty_elements a_partition of Y

(Y,(SmallestPartition Y),PA) is non empty with_non-empty_elements a_partition of Y

(Y,(SmallestPartition Y),PA) is non empty with_non-empty_elements a_partition of Y

INTERSECTION ((SmallestPartition Y),PA) is set

(INTERSECTION ((SmallestPartition Y),PA)) \ {{}} is Element of bool (INTERSECTION ((SmallestPartition Y),PA))

bool (INTERSECTION ((SmallestPartition Y),PA)) is non empty set

(Y,(SmallestPartition Y)) is Relation-like Y -defined Y -valued V17(Y) V43() V45() V50() Element of bool [:Y,Y:]

id Y is non empty Relation-like V43() V45() V46() V50() set

(Y,(Y,(SmallestPartition Y),PA)) is Relation-like Y -defined Y -valued V17(Y) V43() V45() V50() Element of bool [:Y,Y:]

(Y,PA) is Relation-like Y -defined Y -valued V17(Y) V43() V45() V50() Element of bool [:Y,Y:]

(Y,(SmallestPartition Y)) "\/" (Y,PA) is Relation-like Y -defined Y -valued V17(Y) V43() V45() V50() Element of bool [:Y,Y:]

(Y,(SmallestPartition Y)) \/ (Y,PA) is Relation-like Y -defined Y -valued Element of bool [:Y,Y:]

(id Y) \/ (Y,PA) is non empty set

z is set

(Y,(Y,(SmallestPartition Y),PA)) is Relation-like Y -defined Y -valued V17(Y) V43() V45() V50() Element of bool [:Y,Y:]

(Y,(SmallestPartition Y)) /\ (Y,PA) is Relation-like Y -defined Y -valued V17(Y) V43() V45() V50() Element of bool [:Y,Y:]

(id Y) /\ (Y,PA) is Relation-like Y -defined Y -valued Element of bool [:Y,Y:]