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

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 () 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
{ b1 where b1 is Element of bool Y : ( b1 in z & b1 c= a ) } is set
b is set
x1 is set
C is Element of bool Y
union { b1 where b1 is Element of bool Y : ( b1 in z & b1 c= a ) } is set
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

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)):]
{ H1(b1) where b1 is Element of a : S2[b1] } is set
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) \ () 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
{ b1 where b1 is Element of bool Y : S1[b1] } is set
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 /\ () 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) /\ () 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

dom PA is 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
{ b1 where b1 is Element of Y : [ the Element of b,b1] in (Y,z) } is set
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 . 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 . 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

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
{ b1 where b1 is Element of PA : ex b2 being Relation-like NAT -defined Y -valued Function-like FinSequence-like FinSequence of Y st
( 1 <= len b2 & b2 . 1 = a & b2 . (len b2) in b1 & ( for b3 being ext-real V27() V34() V35() V36() V37() V38() V39() V40() V41() Element of NAT holds
( not 1 <= b3 or len b2 <= b3 or ex b4, b5, b6 being set st
( b4 in PA & b5 in z & b2 . b3 in b4 & b6 in b4 /\ b5 & b2 . (b3 + 1) in b5 ) ) ) )
}
is set

Ca is set
union Ca is set
{ b1 where b1 is Element of z : ex b2 being set st
( b2 in Ca & not b1 /\ b2 = {} )
}
is set

x9 is Element 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

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

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

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

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

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

len c28 is ext-real V27() V34() V35() V36() V37() V38() V39() V40() V41() Element of NAT
c28 . 1 is set
c28 . (len c28) is set
u is set
x2 is set
y2 is set
u /\ x2 is set
c28 is set
c29 is set
c30 is set
c28 /\ c29 is set
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

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

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

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) + () 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

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
c28 is set
c29 is set
y2 /\ c28 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 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

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

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

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

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
c28 is set
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

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
{ b1 where b1 is Element of bool Y : ex b2 being set st
( b1 = {b2} & b2 in Y )
}
is set

z is set
{ {b1} where b1 is Element of Y : verum } is set
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
{ {b1} where b1 is Element of Y : verum } is set
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

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
{ {b1} where b1 is Element of Y : verum } is set
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

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 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 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
{ {b1} where b1 is Element of Y : verum } is set
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

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,) 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

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,,PA) is non empty with_non-empty_elements a_partition of Y
(Y,,PA) is non empty with_non-empty_elements a_partition of Y
INTERSECTION (,PA) is set
(INTERSECTION (,PA)) \ is Element of bool (INTERSECTION (,PA))
bool (INTERSECTION (,PA)) is non empty set
(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,,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,) "\/" (Y,PA) is Relation-like Y -defined Y -valued V17(Y) V43() V45() V50() Element of bool [:Y,Y:]
(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,,PA)) is Relation-like Y -defined Y -valued V17(Y) V43() V45() V50() Element of bool [:Y,Y:]
(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:]