:: NORMFORM semantic presentation

K133() is set
bool K133() is non empty cup-closed diff-closed preBoolean set
1 is non empty set
{} is set
the Relation-like non-empty empty-yielding empty set is Relation-like non-empty empty-yielding empty set
A is non empty cup-closed diff-closed preBoolean set
Z is non empty cup-closed diff-closed preBoolean set
[:A,Z:] is Relation-like non empty set
u9 is Element of [:A,Z:]
u9 `1 is Element of A
K is Element of [:A,Z:]
K `2 is Element of Z
u is Element of [:A,Z:]
u `1 is Element of A
z is Element of [:A,Z:]
z `1 is Element of A
(u `1) \/ (z `1) is Element of A
u `2 is Element of Z
z `2 is Element of Z
(u `2) \/ (z `2) is Element of Z
[((u `1) \/ (z `1)),((u `2) \/ (z `2))] is V15() Element of [:A,Z:]
{((u `1) \/ (z `1)),((u `2) \/ (z `2))} is set
{((u `1) \/ (z `1))} is set
{{((u `1) \/ (z `1)),((u `2) \/ (z `2))},{((u `1) \/ (z `1))}} is set
u9 is Element of [:A,Z:]
K is Element of [:A,Z:]
K `1 is Element of A
L is Element of [:A,Z:]
L `1 is Element of A
(K `1) \/ (L `1) is Element of A
K `2 is Element of Z
L `2 is Element of Z
(K `2) \/ (L `2) is Element of Z
[((K `1) \/ (L `1)),((K `2) \/ (L `2))] is V15() Element of [:A,Z:]
{((K `1) \/ (L `1)),((K `2) \/ (L `2))} is set
{((K `1) \/ (L `1))} is set
{{((K `1) \/ (L `1)),((K `2) \/ (L `2))},{((K `1) \/ (L `1))}} is set
(L `1) \/ (K `1) is Element of A
(L `2) \/ (K `2) is Element of Z
[((L `1) \/ (K `1)),((L `2) \/ (K `2))] is V15() Element of [:A,Z:]
{((L `1) \/ (K `1)),((L `2) \/ (K `2))} is set
{((L `1) \/ (K `1))} is set
{{((L `1) \/ (K `1)),((L `2) \/ (K `2))},{((L `1) \/ (K `1))}} is set
u9 is Element of [:A,Z:]
u9 `1 is Element of A
(u9 `1) \/ (u9 `1) is Element of A
u9 `2 is Element of Z
(u9 `2) \/ (u9 `2) is Element of Z
[((u9 `1) \/ (u9 `1)),((u9 `2) \/ (u9 `2))] is V15() Element of [:A,Z:]
{((u9 `1) \/ (u9 `1)),((u9 `2) \/ (u9 `2))} is set
{((u9 `1) \/ (u9 `1))} is set
{{((u9 `1) \/ (u9 `1)),((u9 `2) \/ (u9 `2))},{((u9 `1) \/ (u9 `1))}} is set
(u `1) /\ (z `1) is Element of A
(u `2) /\ (z `2) is Element of Z
[((u `1) /\ (z `1)),((u `2) /\ (z `2))] is V15() Element of [:A,Z:]
{((u `1) /\ (z `1)),((u `2) /\ (z `2))} is set
{((u `1) /\ (z `1))} is set
{{((u `1) /\ (z `1)),((u `2) /\ (z `2))},{((u `1) /\ (z `1))}} is set
u9 is Element of [:A,Z:]
K is Element of [:A,Z:]
K `1 is Element of A
L is Element of [:A,Z:]
L `1 is Element of A
(K `1) /\ (L `1) is Element of A
K `2 is Element of Z
L `2 is Element of Z
(K `2) /\ (L `2) is Element of Z
[((K `1) /\ (L `1)),((K `2) /\ (L `2))] is V15() Element of [:A,Z:]
{((K `1) /\ (L `1)),((K `2) /\ (L `2))} is set
{((K `1) /\ (L `1))} is set
{{((K `1) /\ (L `1)),((K `2) /\ (L `2))},{((K `1) /\ (L `1))}} is set
(L `1) /\ (K `1) is Element of A
(L `2) /\ (K `2) is Element of Z
[((L `1) /\ (K `1)),((L `2) /\ (K `2))] is V15() Element of [:A,Z:]
{((L `1) /\ (K `1)),((L `2) /\ (K `2))} is set
{((L `1) /\ (K `1))} is set
{{((L `1) /\ (K `1)),((L `2) /\ (K `2))},{((L `1) /\ (K `1))}} is set
u9 is Element of [:A,Z:]
u9 `1 is Element of A
(u9 `1) /\ (u9 `1) is Element of A
u9 `2 is Element of Z
(u9 `2) /\ (u9 `2) is Element of Z
[((u9 `1) /\ (u9 `1)),((u9 `2) /\ (u9 `2))] is V15() Element of [:A,Z:]
{((u9 `1) /\ (u9 `1)),((u9 `2) /\ (u9 `2))} is set
{((u9 `1) /\ (u9 `1))} is set
{{((u9 `1) /\ (u9 `1)),((u9 `2) /\ (u9 `2))},{((u9 `1) /\ (u9 `1))}} is set
(u `1) \ (z `1) is Element of A
(u `2) \ (z `2) is Element of Z
[((u `1) \ (z `1)),((u `2) \ (z `2))] is V15() Element of [:A,Z:]
{((u `1) \ (z `1)),((u `2) \ (z `2))} is set
{((u `1) \ (z `1))} is set
{{((u `1) \ (z `1)),((u `2) \ (z `2))},{((u `1) \ (z `1))}} is set
(u `1) \+\ (z `1) is Element of A
(u `1) \ (z `1) is set
(z `1) \ (u `1) is set
((u `1) \ (z `1)) \/ ((z `1) \ (u `1)) is set
(u `2) \+\ (z `2) is Element of Z
(u `2) \ (z `2) is set
(z `2) \ (u `2) is set
((u `2) \ (z `2)) \/ ((z `2) \ (u `2)) is set
[((u `1) \+\ (z `1)),((u `2) \+\ (z `2))] is V15() Element of [:A,Z:]
{((u `1) \+\ (z `1)),((u `2) \+\ (z `2))} is set
{((u `1) \+\ (z `1))} is set
{{((u `1) \+\ (z `1)),((u `2) \+\ (z `2))},{((u `1) \+\ (z `1))}} is set
u9 is Element of [:A,Z:]
K is Element of [:A,Z:]
K `1 is Element of A
L is Element of [:A,Z:]
L `1 is Element of A
(K `1) \+\ (L `1) is Element of A
(K `1) \ (L `1) is set
(L `1) \ (K `1) is set
((K `1) \ (L `1)) \/ ((L `1) \ (K `1)) is set
K `2 is Element of Z
L `2 is Element of Z
(K `2) \+\ (L `2) is Element of Z
(K `2) \ (L `2) is set
(L `2) \ (K `2) is set
((K `2) \ (L `2)) \/ ((L `2) \ (K `2)) is set
[((K `1) \+\ (L `1)),((K `2) \+\ (L `2))] is V15() Element of [:A,Z:]
{((K `1) \+\ (L `1)),((K `2) \+\ (L `2))} is set
{((K `1) \+\ (L `1))} is set
{{((K `1) \+\ (L `1)),((K `2) \+\ (L `2))},{((K `1) \+\ (L `1))}} is set
(L `1) \+\ (K `1) is Element of A
((L `1) \ (K `1)) \/ ((K `1) \ (L `1)) is set
(L `2) \+\ (K `2) is Element of Z
((L `2) \ (K `2)) \/ ((K `2) \ (L `2)) is set
[((L `1) \+\ (K `1)),((L `2) \+\ (K `2))] is V15() Element of [:A,Z:]
{((L `1) \+\ (K `1)),((L `2) \+\ (K `2))} is set
{((L `1) \+\ (K `1))} is set
{{((L `1) \+\ (K `1)),((L `2) \+\ (K `2))},{((L `1) \+\ (K `1))}} is set
A is non empty cup-closed diff-closed preBoolean set
Z is non empty cup-closed diff-closed preBoolean set
[:A,Z:] is Relation-like non empty set
u is Element of [:A,Z:]
z is Element of [:A,Z:]
u `1 is Element of A
z `1 is Element of A
u `2 is Element of Z
z `2 is Element of Z
A is non empty cup-closed diff-closed preBoolean set
Z is non empty cup-closed diff-closed preBoolean set
[:A,Z:] is Relation-like non empty set
u is Element of [:A,Z:]
z is Element of [:A,Z:]
u9 is Element of [:A,Z:]
u `1 is Element of A
z `1 is Element of A
u `2 is Element of Z
z `2 is Element of Z
u9 `1 is Element of A
u9 `2 is Element of Z
A is non empty cup-closed diff-closed preBoolean set
Z is non empty cup-closed diff-closed preBoolean set
[:A,Z:] is Relation-like non empty set
u is Element of [:A,Z:]
z is Element of [:A,Z:]
(A,Z,u,z) is Element of [:A,Z:]
u `1 is Element of A
z `1 is Element of A
(u `1) \/ (z `1) is Element of A
u `2 is Element of Z
z `2 is Element of Z
(u `2) \/ (z `2) is Element of Z
[((u `1) \/ (z `1)),((u `2) \/ (z `2))] is V15() Element of [:A,Z:]
{((u `1) \/ (z `1)),((u `2) \/ (z `2))} is set
{((u `1) \/ (z `1))} is set
{{((u `1) \/ (z `1)),((u `2) \/ (z `2))},{((u `1) \/ (z `1))}} is set
u9 is Element of [:A,Z:]
(A,Z,(A,Z,u,z),u9) is Element of [:A,Z:]
(A,Z,u,z) `1 is Element of A
u9 `1 is Element of A
((A,Z,u,z) `1) \/ (u9 `1) is Element of A
(A,Z,u,z) `2 is Element of Z
u9 `2 is Element of Z
((A,Z,u,z) `2) \/ (u9 `2) is Element of Z
[(((A,Z,u,z) `1) \/ (u9 `1)),(((A,Z,u,z) `2) \/ (u9 `2))] is V15() Element of [:A,Z:]
{(((A,Z,u,z) `1) \/ (u9 `1)),(((A,Z,u,z) `2) \/ (u9 `2))} is set
{(((A,Z,u,z) `1) \/ (u9 `1))} is set
{{(((A,Z,u,z) `1) \/ (u9 `1)),(((A,Z,u,z) `2) \/ (u9 `2))},{(((A,Z,u,z) `1) \/ (u9 `1))}} is set
(A,Z,z,u9) is Element of [:A,Z:]
(z `1) \/ (u9 `1) is Element of A
(z `2) \/ (u9 `2) is Element of Z
[((z `1) \/ (u9 `1)),((z `2) \/ (u9 `2))] is V15() Element of [:A,Z:]
{((z `1) \/ (u9 `1)),((z `2) \/ (u9 `2))} is set
{((z `1) \/ (u9 `1))} is set
{{((z `1) \/ (u9 `1)),((z `2) \/ (u9 `2))},{((z `1) \/ (u9 `1))}} is set
(A,Z,u,(A,Z,z,u9)) is Element of [:A,Z:]
(A,Z,z,u9) `1 is Element of A
(u `1) \/ ((A,Z,z,u9) `1) is Element of A
(A,Z,z,u9) `2 is Element of Z
(u `2) \/ ((A,Z,z,u9) `2) is Element of Z
[((u `1) \/ ((A,Z,z,u9) `1)),((u `2) \/ ((A,Z,z,u9) `2))] is V15() Element of [:A,Z:]
{((u `1) \/ ((A,Z,z,u9) `1)),((u `2) \/ ((A,Z,z,u9) `2))} is set
{((u `1) \/ ((A,Z,z,u9) `1))} is set
{{((u `1) \/ ((A,Z,z,u9) `1)),((u `2) \/ ((A,Z,z,u9) `2))},{((u `1) \/ ((A,Z,z,u9) `1))}} is set
(A,Z,(A,Z,u,z),u9) `2 is Element of Z
((u `2) \/ (z `2)) \/ (u9 `2) is Element of Z
(u `2) \/ ((z `2) \/ (u9 `2)) is Element of Z
(A,Z,u,(A,Z,z,u9)) `2 is Element of Z
(A,Z,(A,Z,u,z),u9) `1 is Element of A
((u `1) \/ (z `1)) \/ (u9 `1) is Element of A
(u `1) \/ ((z `1) \/ (u9 `1)) is Element of A
(A,Z,u,(A,Z,z,u9)) `1 is Element of A
A is non empty cup-closed diff-closed preBoolean set
Z is non empty cup-closed diff-closed preBoolean set
[:A,Z:] is Relation-like non empty set
u is Element of [:A,Z:]
z is Element of [:A,Z:]
(A,Z,u,z) is Element of [:A,Z:]
u `1 is Element of A
z `1 is Element of A
(u `1) /\ (z `1) is Element of A
u `2 is Element of Z
z `2 is Element of Z
(u `2) /\ (z `2) is Element of Z
[((u `1) /\ (z `1)),((u `2) /\ (z `2))] is V15() Element of [:A,Z:]
{((u `1) /\ (z `1)),((u `2) /\ (z `2))} is set
{((u `1) /\ (z `1))} is set
{{((u `1) /\ (z `1)),((u `2) /\ (z `2))},{((u `1) /\ (z `1))}} is set
u9 is Element of [:A,Z:]
(A,Z,(A,Z,u,z),u9) is Element of [:A,Z:]
(A,Z,u,z) `1 is Element of A
u9 `1 is Element of A
((A,Z,u,z) `1) /\ (u9 `1) is Element of A
(A,Z,u,z) `2 is Element of Z
u9 `2 is Element of Z
((A,Z,u,z) `2) /\ (u9 `2) is Element of Z
[(((A,Z,u,z) `1) /\ (u9 `1)),(((A,Z,u,z) `2) /\ (u9 `2))] is V15() Element of [:A,Z:]
{(((A,Z,u,z) `1) /\ (u9 `1)),(((A,Z,u,z) `2) /\ (u9 `2))} is set
{(((A,Z,u,z) `1) /\ (u9 `1))} is set
{{(((A,Z,u,z) `1) /\ (u9 `1)),(((A,Z,u,z) `2) /\ (u9 `2))},{(((A,Z,u,z) `1) /\ (u9 `1))}} is set
(A,Z,z,u9) is Element of [:A,Z:]
(z `1) /\ (u9 `1) is Element of A
(z `2) /\ (u9 `2) is Element of Z
[((z `1) /\ (u9 `1)),((z `2) /\ (u9 `2))] is V15() Element of [:A,Z:]
{((z `1) /\ (u9 `1)),((z `2) /\ (u9 `2))} is set
{((z `1) /\ (u9 `1))} is set
{{((z `1) /\ (u9 `1)),((z `2) /\ (u9 `2))},{((z `1) /\ (u9 `1))}} is set
(A,Z,u,(A,Z,z,u9)) is Element of [:A,Z:]
(A,Z,z,u9) `1 is Element of A
(u `1) /\ ((A,Z,z,u9) `1) is Element of A
(A,Z,z,u9) `2 is Element of Z
(u `2) /\ ((A,Z,z,u9) `2) is Element of Z
[((u `1) /\ ((A,Z,z,u9) `1)),((u `2) /\ ((A,Z,z,u9) `2))] is V15() Element of [:A,Z:]
{((u `1) /\ ((A,Z,z,u9) `1)),((u `2) /\ ((A,Z,z,u9) `2))} is set
{((u `1) /\ ((A,Z,z,u9) `1))} is set
{{((u `1) /\ ((A,Z,z,u9) `1)),((u `2) /\ ((A,Z,z,u9) `2))},{((u `1) /\ ((A,Z,z,u9) `1))}} is set
(A,Z,(A,Z,u,z),u9) `2 is Element of Z
((u `2) /\ (z `2)) /\ (u9 `2) is Element of Z
(u `2) /\ ((z `2) /\ (u9 `2)) is Element of Z
(A,Z,u,(A,Z,z,u9)) `2 is Element of Z
(A,Z,(A,Z,u,z),u9) `1 is Element of A
((u `1) /\ (z `1)) /\ (u9 `1) is Element of A
(u `1) /\ ((z `1) /\ (u9 `1)) is Element of A
(A,Z,u,(A,Z,z,u9)) `1 is Element of A
A is non empty cup-closed diff-closed preBoolean set
Z is non empty cup-closed diff-closed preBoolean set
[:A,Z:] is Relation-like non empty set
u is Element of [:A,Z:]
z is Element of [:A,Z:]
(A,Z,u,z) is Element of [:A,Z:]
u `1 is Element of A
z `1 is Element of A
(u `1) /\ (z `1) is Element of A
u `2 is Element of Z
z `2 is Element of Z
(u `2) /\ (z `2) is Element of Z
[((u `1) /\ (z `1)),((u `2) /\ (z `2))] is V15() Element of [:A,Z:]
{((u `1) /\ (z `1)),((u `2) /\ (z `2))} is set
{((u `1) /\ (z `1))} is set
{{((u `1) /\ (z `1)),((u `2) /\ (z `2))},{((u `1) /\ (z `1))}} is set
u9 is Element of [:A,Z:]
(A,Z,z,u9) is Element of [:A,Z:]
u9 `1 is Element of A
(z `1) \/ (u9 `1) is Element of A
u9 `2 is Element of Z
(z `2) \/ (u9 `2) is Element of Z
[((z `1) \/ (u9 `1)),((z `2) \/ (u9 `2))] is V15() Element of [:A,Z:]
{((z `1) \/ (u9 `1)),((z `2) \/ (u9 `2))} is set
{((z `1) \/ (u9 `1))} is set
{{((z `1) \/ (u9 `1)),((z `2) \/ (u9 `2))},{((z `1) \/ (u9 `1))}} is set
(A,Z,u,(A,Z,z,u9)) is Element of [:A,Z:]
(A,Z,z,u9) `1 is Element of A
(u `1) /\ ((A,Z,z,u9) `1) is Element of A
(A,Z,z,u9) `2 is Element of Z
(u `2) /\ ((A,Z,z,u9) `2) is Element of Z
[((u `1) /\ ((A,Z,z,u9) `1)),((u `2) /\ ((A,Z,z,u9) `2))] is V15() Element of [:A,Z:]
{((u `1) /\ ((A,Z,z,u9) `1)),((u `2) /\ ((A,Z,z,u9) `2))} is set
{((u `1) /\ ((A,Z,z,u9) `1))} is set
{{((u `1) /\ ((A,Z,z,u9) `1)),((u `2) /\ ((A,Z,z,u9) `2))},{((u `1) /\ ((A,Z,z,u9) `1))}} is set
(A,Z,u,u9) is Element of [:A,Z:]
(u `1) /\ (u9 `1) is Element of A
(u `2) /\ (u9 `2) is Element of Z
[((u `1) /\ (u9 `1)),((u `2) /\ (u9 `2))] is V15() Element of [:A,Z:]
{((u `1) /\ (u9 `1)),((u `2) /\ (u9 `2))} is set
{((u `1) /\ (u9 `1))} is set
{{((u `1) /\ (u9 `1)),((u `2) /\ (u9 `2))},{((u `1) /\ (u9 `1))}} is set
(A,Z,(A,Z,u,z),(A,Z,u,u9)) is Element of [:A,Z:]
(A,Z,u,z) `1 is Element of A
(A,Z,u,u9) `1 is Element of A
((A,Z,u,z) `1) \/ ((A,Z,u,u9) `1) is Element of A
(A,Z,u,z) `2 is Element of Z
(A,Z,u,u9) `2 is Element of Z
((A,Z,u,z) `2) \/ ((A,Z,u,u9) `2) is Element of Z
[(((A,Z,u,z) `1) \/ ((A,Z,u,u9) `1)),(((A,Z,u,z) `2) \/ ((A,Z,u,u9) `2))] is V15() Element of [:A,Z:]
{(((A,Z,u,z) `1) \/ ((A,Z,u,u9) `1)),(((A,Z,u,z) `2) \/ ((A,Z,u,u9) `2))} is set
{(((A,Z,u,z) `1) \/ ((A,Z,u,u9) `1))} is set
{{(((A,Z,u,z) `1) \/ ((A,Z,u,u9) `1)),(((A,Z,u,z) `2) \/ ((A,Z,u,u9) `2))},{(((A,Z,u,z) `1) \/ ((A,Z,u,u9) `1))}} is set
(A,Z,u,(A,Z,z,u9)) `2 is Element of Z
(u `2) /\ ((z `2) \/ (u9 `2)) is Element of Z
((u `2) /\ (z `2)) \/ ((u `2) /\ (u9 `2)) is Element of Z
((u `2) /\ (z `2)) \/ ((A,Z,u,u9) `2) is Element of Z
(A,Z,(A,Z,u,z),(A,Z,u,u9)) `2 is Element of Z
(A,Z,u,(A,Z,z,u9)) `1 is Element of A
(u `1) /\ ((z `1) \/ (u9 `1)) is Element of A
((u `1) /\ (z `1)) \/ ((u `1) /\ (u9 `1)) is Element of A
((u `1) /\ (z `1)) \/ ((A,Z,u,u9) `1) is Element of A
(A,Z,(A,Z,u,z),(A,Z,u,u9)) `1 is Element of A
A is non empty cup-closed diff-closed preBoolean set
Z is non empty cup-closed diff-closed preBoolean set
[:A,Z:] is Relation-like non empty set
u is Element of [:A,Z:]
z is Element of [:A,Z:]
(A,Z,z,u) is Element of [:A,Z:]
z `1 is Element of A
u `1 is Element of A
(z `1) /\ (u `1) is Element of A
z `2 is Element of Z
u `2 is Element of Z
(z `2) /\ (u `2) is Element of Z
[((z `1) /\ (u `1)),((z `2) /\ (u `2))] is V15() Element of [:A,Z:]
{((z `1) /\ (u `1)),((z `2) /\ (u `2))} is set
{((z `1) /\ (u `1))} is set
{{((z `1) /\ (u `1)),((z `2) /\ (u `2))},{((z `1) /\ (u `1))}} is set
(A,Z,u,(A,Z,z,u)) is Element of [:A,Z:]
(A,Z,z,u) `1 is Element of A
(u `1) \/ ((A,Z,z,u) `1) is Element of A
(A,Z,z,u) `2 is Element of Z
(u `2) \/ ((A,Z,z,u) `2) is Element of Z
[((u `1) \/ ((A,Z,z,u) `1)),((u `2) \/ ((A,Z,z,u) `2))] is V15() Element of [:A,Z:]
{((u `1) \/ ((A,Z,z,u) `1)),((u `2) \/ ((A,Z,z,u) `2))} is set
{((u `1) \/ ((A,Z,z,u) `1))} is set
{{((u `1) \/ ((A,Z,z,u) `1)),((u `2) \/ ((A,Z,z,u) `2))},{((u `1) \/ ((A,Z,z,u) `1))}} is set
(A,Z,u,(A,Z,z,u)) `2 is Element of Z
(u `2) \/ ((z `2) /\ (u `2)) is Element of Z
(A,Z,u,(A,Z,z,u)) `1 is Element of A
(u `1) \/ ((z `1) /\ (u `1)) is Element of A
A is non empty cup-closed diff-closed preBoolean set
Z is non empty cup-closed diff-closed preBoolean set
[:A,Z:] is Relation-like non empty set
u is Element of [:A,Z:]
z is Element of [:A,Z:]
(A,Z,z,u) is Element of [:A,Z:]
z `1 is Element of A
u `1 is Element of A
(z `1) \/ (u `1) is Element of A
z `2 is Element of Z
u `2 is Element of Z
(z `2) \/ (u `2) is Element of Z
[((z `1) \/ (u `1)),((z `2) \/ (u `2))] is V15() Element of [:A,Z:]
{((z `1) \/ (u `1)),((z `2) \/ (u `2))} is set
{((z `1) \/ (u `1))} is set
{{((z `1) \/ (u `1)),((z `2) \/ (u `2))},{((z `1) \/ (u `1))}} is set
(A,Z,u,(A,Z,z,u)) is Element of [:A,Z:]
(A,Z,z,u) `1 is Element of A
(u `1) /\ ((A,Z,z,u) `1) is Element of A
(A,Z,z,u) `2 is Element of Z
(u `2) /\ ((A,Z,z,u) `2) is Element of Z
[((u `1) /\ ((A,Z,z,u) `1)),((u `2) /\ ((A,Z,z,u) `2))] is V15() Element of [:A,Z:]
{((u `1) /\ ((A,Z,z,u) `1)),((u `2) /\ ((A,Z,z,u) `2))} is set
{((u `1) /\ ((A,Z,z,u) `1))} is set
{{((u `1) /\ ((A,Z,z,u) `1)),((u `2) /\ ((A,Z,z,u) `2))},{((u `1) /\ ((A,Z,z,u) `1))}} is set
(A,Z,u,z) is Element of [:A,Z:]
(u `1) /\ (z `1) is Element of A
(u `2) /\ (z `2) is Element of Z
[((u `1) /\ (z `1)),((u `2) /\ (z `2))] is V15() Element of [:A,Z:]
{((u `1) /\ (z `1)),((u `2) /\ (z `2))} is set
{((u `1) /\ (z `1))} is set
{{((u `1) /\ (z `1)),((u `2) /\ (z `2))},{((u `1) /\ (z `1))}} is set
(A,Z,u,u) is Element of [:A,Z:]
(u `1) /\ (u `1) is Element of A
(u `2) /\ (u `2) is Element of Z
[((u `1) /\ (u `1)),((u `2) /\ (u `2))] is V15() Element of [:A,Z:]
{((u `1) /\ (u `1)),((u `2) /\ (u `2))} is set
{((u `1) /\ (u `1))} is set
{{((u `1) /\ (u `1)),((u `2) /\ (u `2))},{((u `1) /\ (u `1))}} is set
(A,Z,(A,Z,u,z),(A,Z,u,u)) is Element of [:A,Z:]
(A,Z,u,z) `1 is Element of A
(A,Z,u,u) `1 is Element of A
((A,Z,u,z) `1) \/ ((A,Z,u,u) `1) is Element of A
(A,Z,u,z) `2 is Element of Z
(A,Z,u,u) `2 is Element of Z
((A,Z,u,z) `2) \/ ((A,Z,u,u) `2) is Element of Z
[(((A,Z,u,z) `1) \/ ((A,Z,u,u) `1)),(((A,Z,u,z) `2) \/ ((A,Z,u,u) `2))] is V15() Element of [:A,Z:]
{(((A,Z,u,z) `1) \/ ((A,Z,u,u) `1)),(((A,Z,u,z) `2) \/ ((A,Z,u,u) `2))} is set
{(((A,Z,u,z) `1) \/ ((A,Z,u,u) `1))} is set
{{(((A,Z,u,z) `1) \/ ((A,Z,u,u) `1)),(((A,Z,u,z) `2) \/ ((A,Z,u,u) `2))},{(((A,Z,u,z) `1) \/ ((A,Z,u,u) `1))}} is set
A is non empty cup-closed diff-closed preBoolean set
Z is non empty cup-closed diff-closed preBoolean set
[:A,Z:] is Relation-like non empty set
u is Element of [:A,Z:]
z is Element of [:A,Z:]
(A,Z,u,z) is Element of [:A,Z:]
u `1 is Element of A
z `1 is Element of A
(u `1) \/ (z `1) is Element of A
u `2 is Element of Z
z `2 is Element of Z
(u `2) \/ (z `2) is Element of Z
[((u `1) \/ (z `1)),((u `2) \/ (z `2))] is V15() Element of [:A,Z:]
{((u `1) \/ (z `1)),((u `2) \/ (z `2))} is set
{((u `1) \/ (z `1))} is set
{{((u `1) \/ (z `1)),((u `2) \/ (z `2))},{((u `1) \/ (z `1))}} is set
u9 is Element of [:A,Z:]
(A,Z,z,u9) is Element of [:A,Z:]
u9 `1 is Element of A
(z `1) /\ (u9 `1) is Element of A
u9 `2 is Element of Z
(z `2) /\ (u9 `2) is Element of Z
[((z `1) /\ (u9 `1)),((z `2) /\ (u9 `2))] is V15() Element of [:A,Z:]
{((z `1) /\ (u9 `1)),((z `2) /\ (u9 `2))} is set
{((z `1) /\ (u9 `1))} is set
{{((z `1) /\ (u9 `1)),((z `2) /\ (u9 `2))},{((z `1) /\ (u9 `1))}} is set
(A,Z,u,(A,Z,z,u9)) is Element of [:A,Z:]
(A,Z,z,u9) `1 is Element of A
(u `1) \/ ((A,Z,z,u9) `1) is Element of A
(A,Z,z,u9) `2 is Element of Z
(u `2) \/ ((A,Z,z,u9) `2) is Element of Z
[((u `1) \/ ((A,Z,z,u9) `1)),((u `2) \/ ((A,Z,z,u9) `2))] is V15() Element of [:A,Z:]
{((u `1) \/ ((A,Z,z,u9) `1)),((u `2) \/ ((A,Z,z,u9) `2))} is set
{((u `1) \/ ((A,Z,z,u9) `1))} is set
{{((u `1) \/ ((A,Z,z,u9) `1)),((u `2) \/ ((A,Z,z,u9) `2))},{((u `1) \/ ((A,Z,z,u9) `1))}} is set
(A,Z,u,u9) is Element of [:A,Z:]
(u `1) \/ (u9 `1) is Element of A
(u `2) \/ (u9 `2) is Element of Z
[((u `1) \/ (u9 `1)),((u `2) \/ (u9 `2))] is V15() Element of [:A,Z:]
{((u `1) \/ (u9 `1)),((u `2) \/ (u9 `2))} is set
{((u `1) \/ (u9 `1))} is set
{{((u `1) \/ (u9 `1)),((u `2) \/ (u9 `2))},{((u `1) \/ (u9 `1))}} is set
(A,Z,(A,Z,u,z),(A,Z,u,u9)) is Element of [:A,Z:]
(A,Z,u,z) `1 is Element of A
(A,Z,u,u9) `1 is Element of A
((A,Z,u,z) `1) /\ ((A,Z,u,u9) `1) is Element of A
(A,Z,u,z) `2 is Element of Z
(A,Z,u,u9) `2 is Element of Z
((A,Z,u,z) `2) /\ ((A,Z,u,u9) `2) is Element of Z
[(((A,Z,u,z) `1) /\ ((A,Z,u,u9) `1)),(((A,Z,u,z) `2) /\ ((A,Z,u,u9) `2))] is V15() Element of [:A,Z:]
{(((A,Z,u,z) `1) /\ ((A,Z,u,u9) `1)),(((A,Z,u,z) `2) /\ ((A,Z,u,u9) `2))} is set
{(((A,Z,u,z) `1) /\ ((A,Z,u,u9) `1))} is set
{{(((A,Z,u,z) `1) /\ ((A,Z,u,u9) `1)),(((A,Z,u,z) `2) /\ ((A,Z,u,u9) `2))},{(((A,Z,u,z) `1) /\ ((A,Z,u,u9) `1))}} is set
(A,Z,u9,u) is Element of [:A,Z:]
(u9 `1) /\ (u `1) is Element of A
(u9 `2) /\ (u `2) is Element of Z
[((u9 `1) /\ (u `1)),((u9 `2) /\ (u `2))] is V15() Element of [:A,Z:]
{((u9 `1) /\ (u `1)),((u9 `2) /\ (u `2))} is set
{((u9 `1) /\ (u `1))} is set
{{((u9 `1) /\ (u `1)),((u9 `2) /\ (u `2))},{((u9 `1) /\ (u `1))}} is set
(A,Z,u,(A,Z,u9,u)) is Element of [:A,Z:]
(A,Z,u9,u) `1 is Element of A
(u `1) \/ ((A,Z,u9,u) `1) is Element of A
(A,Z,u9,u) `2 is Element of Z
(u `2) \/ ((A,Z,u9,u) `2) is Element of Z
[((u `1) \/ ((A,Z,u9,u) `1)),((u `2) \/ ((A,Z,u9,u) `2))] is V15() Element of [:A,Z:]
{((u `1) \/ ((A,Z,u9,u) `1)),((u `2) \/ ((A,Z,u9,u) `2))} is set
{((u `1) \/ ((A,Z,u9,u) `1))} is set
{{((u `1) \/ ((A,Z,u9,u) `1)),((u `2) \/ ((A,Z,u9,u) `2))},{((u `1) \/ ((A,Z,u9,u) `1))}} is set
(A,Z,u9,z) is Element of [:A,Z:]
(u9 `1) /\ (z `1) is Element of A
(u9 `2) /\ (z `2) is Element of Z
[((u9 `1) /\ (z `1)),((u9 `2) /\ (z `2))] is V15() Element of [:A,Z:]
{((u9 `1) /\ (z `1)),((u9 `2) /\ (z `2))} is set
{((u9 `1) /\ (z `1))} is set
{{((u9 `1) /\ (z `1)),((u9 `2) /\ (z `2))},{((u9 `1) /\ (z `1))}} is set
(A,Z,(A,Z,u,(A,Z,u9,u)),(A,Z,u9,z)) is Element of [:A,Z:]
(A,Z,u,(A,Z,u9,u)) `1 is Element of A
(A,Z,u9,z) `1 is Element of A
((A,Z,u,(A,Z,u9,u)) `1) \/ ((A,Z,u9,z) `1) is Element of A
(A,Z,u,(A,Z,u9,u)) `2 is Element of Z
(A,Z,u9,z) `2 is Element of Z
((A,Z,u,(A,Z,u9,u)) `2) \/ ((A,Z,u9,z) `2) is Element of Z
[(((A,Z,u,(A,Z,u9,u)) `1) \/ ((A,Z,u9,z) `1)),(((A,Z,u,(A,Z,u9,u)) `2) \/ ((A,Z,u9,z) `2))] is V15() Element of [:A,Z:]
{(((A,Z,u,(A,Z,u9,u)) `1) \/ ((A,Z,u9,z) `1)),(((A,Z,u,(A,Z,u9,u)) `2) \/ ((A,Z,u9,z) `2))} is set
{(((A,Z,u,(A,Z,u9,u)) `1) \/ ((A,Z,u9,z) `1))} is set
{{(((A,Z,u,(A,Z,u9,u)) `1) \/ ((A,Z,u9,z) `1)),(((A,Z,u,(A,Z,u9,u)) `2) \/ ((A,Z,u9,z) `2))},{(((A,Z,u,(A,Z,u9,u)) `1) \/ ((A,Z,u9,z) `1))}} is set
(A,Z,(A,Z,u9,u),(A,Z,u9,z)) is Element of [:A,Z:]
((A,Z,u9,u) `1) \/ ((A,Z,u9,z) `1) is Element of A
((A,Z,u9,u) `2) \/ ((A,Z,u9,z) `2) is Element of Z
[(((A,Z,u9,u) `1) \/ ((A,Z,u9,z) `1)),(((A,Z,u9,u) `2) \/ ((A,Z,u9,z) `2))] is V15() Element of [:A,Z:]
{(((A,Z,u9,u) `1) \/ ((A,Z,u9,z) `1)),(((A,Z,u9,u) `2) \/ ((A,Z,u9,z) `2))} is set
{(((A,Z,u9,u) `1) \/ ((A,Z,u9,z) `1))} is set
{{(((A,Z,u9,u) `1) \/ ((A,Z,u9,z) `1)),(((A,Z,u9,u) `2) \/ ((A,Z,u9,z) `2))},{(((A,Z,u9,u) `1) \/ ((A,Z,u9,z) `1))}} is set
(A,Z,u,(A,Z,(A,Z,u9,u),(A,Z,u9,z))) is Element of [:A,Z:]
(A,Z,(A,Z,u9,u),(A,Z,u9,z)) `1 is Element of A
(u `1) \/ ((A,Z,(A,Z,u9,u),(A,Z,u9,z)) `1) is Element of A
(A,Z,(A,Z,u9,u),(A,Z,u9,z)) `2 is Element of Z
(u `2) \/ ((A,Z,(A,Z,u9,u),(A,Z,u9,z)) `2) is Element of Z
[((u `1) \/ ((A,Z,(A,Z,u9,u),(A,Z,u9,z)) `1)),((u `2) \/ ((A,Z,(A,Z,u9,u),(A,Z,u9,z)) `2))] is V15() Element of [:A,Z:]
{((u `1) \/ ((A,Z,(A,Z,u9,u),(A,Z,u9,z)) `1)),((u `2) \/ ((A,Z,(A,Z,u9,u),(A,Z,u9,z)) `2))} is set
{((u `1) \/ ((A,Z,(A,Z,u9,u),(A,Z,u9,z)) `1))} is set
{{((u `1) \/ ((A,Z,(A,Z,u9,u),(A,Z,u9,z)) `1)),((u `2) \/ ((A,Z,(A,Z,u9,u),(A,Z,u9,z)) `2))},{((u `1) \/ ((A,Z,(A,Z,u9,u),(A,Z,u9,z)) `1))}} is set
(A,Z,u9,(A,Z,u,z)) is Element of [:A,Z:]
(u9 `1) /\ ((A,Z,u,z) `1) is Element of A
(u9 `2) /\ ((A,Z,u,z) `2) is Element of Z
[((u9 `1) /\ ((A,Z,u,z) `1)),((u9 `2) /\ ((A,Z,u,z) `2))] is V15() Element of [:A,Z:]
{((u9 `1) /\ ((A,Z,u,z) `1)),((u9 `2) /\ ((A,Z,u,z) `2))} is set
{((u9 `1) /\ ((A,Z,u,z) `1))} is set
{{((u9 `1) /\ ((A,Z,u,z) `1)),((u9 `2) /\ ((A,Z,u,z) `2))},{((u9 `1) /\ ((A,Z,u,z) `1))}} is set
(A,Z,u,(A,Z,u9,(A,Z,u,z))) is Element of [:A,Z:]
(A,Z,u9,(A,Z,u,z)) `1 is Element of A
(u `1) \/ ((A,Z,u9,(A,Z,u,z)) `1) is Element of A
(A,Z,u9,(A,Z,u,z)) `2 is Element of Z
(u `2) \/ ((A,Z,u9,(A,Z,u,z)) `2) is Element of Z
[((u `1) \/ ((A,Z,u9,(A,Z,u,z)) `1)),((u `2) \/ ((A,Z,u9,(A,Z,u,z)) `2))] is V15() Element of [:A,Z:]
{((u `1) \/ ((A,Z,u9,(A,Z,u,z)) `1)),((u `2) \/ ((A,Z,u9,(A,Z,u,z)) `2))} is set
{((u `1) \/ ((A,Z,u9,(A,Z,u,z)) `1))} is set
{{((u `1) \/ ((A,Z,u9,(A,Z,u,z)) `1)),((u `2) \/ ((A,Z,u9,(A,Z,u,z)) `2))},{((u `1) \/ ((A,Z,u9,(A,Z,u,z)) `1))}} is set
(A,Z,(A,Z,u,z),u) is Element of [:A,Z:]
((A,Z,u,z) `1) /\ (u `1) is Element of A
((A,Z,u,z) `2) /\ (u `2) is Element of Z
[(((A,Z,u,z) `1) /\ (u `1)),(((A,Z,u,z) `2) /\ (u `2))] is V15() Element of [:A,Z:]
{(((A,Z,u,z) `1) /\ (u `1)),(((A,Z,u,z) `2) /\ (u `2))} is set
{(((A,Z,u,z) `1) /\ (u `1))} is set
{{(((A,Z,u,z) `1) /\ (u `1)),(((A,Z,u,z) `2) /\ (u `2))},{(((A,Z,u,z) `1) /\ (u `1))}} is set
(A,Z,(A,Z,u,z),u9) is Element of [:A,Z:]
((A,Z,u,z) `1) /\ (u9 `1) is Element of A
((A,Z,u,z) `2) /\ (u9 `2) is Element of Z
[(((A,Z,u,z) `1) /\ (u9 `1)),(((A,Z,u,z) `2) /\ (u9 `2))] is V15() Element of [:A,Z:]
{(((A,Z,u,z) `1) /\ (u9 `1)),(((A,Z,u,z) `2) /\ (u9 `2))} is set
{(((A,Z,u,z) `1) /\ (u9 `1))} is set
{{(((A,Z,u,z) `1) /\ (u9 `1)),(((A,Z,u,z) `2) /\ (u9 `2))},{(((A,Z,u,z) `1) /\ (u9 `1))}} is set
(A,Z,(A,Z,(A,Z,u,z),u),(A,Z,(A,Z,u,z),u9)) is Element of [:A,Z:]
(A,Z,(A,Z,u,z),u) `1 is Element of A
(A,Z,(A,Z,u,z),u9) `1 is Element of A
((A,Z,(A,Z,u,z),u) `1) \/ ((A,Z,(A,Z,u,z),u9) `1) is Element of A
(A,Z,(A,Z,u,z),u) `2 is Element of Z
(A,Z,(A,Z,u,z),u9) `2 is Element of Z
((A,Z,(A,Z,u,z),u) `2) \/ ((A,Z,(A,Z,u,z),u9) `2) is Element of Z
[(((A,Z,(A,Z,u,z),u) `1) \/ ((A,Z,(A,Z,u,z),u9) `1)),(((A,Z,(A,Z,u,z),u) `2) \/ ((A,Z,(A,Z,u,z),u9) `2))] is V15() Element of [:A,Z:]
{(((A,Z,(A,Z,u,z),u) `1) \/ ((A,Z,(A,Z,u,z),u9) `1)),(((A,Z,(A,Z,u,z),u) `2) \/ ((A,Z,(A,Z,u,z),u9) `2))} is set
{(((A,Z,(A,Z,u,z),u) `1) \/ ((A,Z,(A,Z,u,z),u9) `1))} is set
{{(((A,Z,(A,Z,u,z),u) `1) \/ ((A,Z,(A,Z,u,z),u9) `1)),(((A,Z,(A,Z,u,z),u) `2) \/ ((A,Z,(A,Z,u,z),u9) `2))},{(((A,Z,(A,Z,u,z),u) `1) \/ ((A,Z,(A,Z,u,z),u9) `1))}} is set
A is non empty cup-closed diff-closed preBoolean set
Z is non empty cup-closed diff-closed preBoolean set
[:A,Z:] is Relation-like non empty set
u is Element of [:A,Z:]
z is Element of [:A,Z:]
u9 is Element of [:A,Z:]
(A,Z,u,u9) is Element of [:A,Z:]
u `1 is Element of A
u9 `1 is Element of A
(u `1) \/ (u9 `1) is Element of A
u `2 is Element of Z
u9 `2 is Element of Z
(u `2) \/ (u9 `2) is Element of Z
[((u `1) \/ (u9 `1)),((u `2) \/ (u9 `2))] is V15() Element of [:A,Z:]
{((u `1) \/ (u9 `1)),((u `2) \/ (u9 `2))} is set
{((u `1) \/ (u9 `1))} is set
{{((u `1) \/ (u9 `1)),((u `2) \/ (u9 `2))},{((u `1) \/ (u9 `1))}} is set
z `1 is Element of A
z `2 is Element of Z
(A,Z,u,u9) `1 is Element of A
(A,Z,u,u9) `2 is Element of Z
A is non empty cup-closed diff-closed preBoolean set
Z is non empty cup-closed diff-closed preBoolean set
[:A,Z:] is Relation-like non empty set
u is Element of [:A,Z:]
z is Element of [:A,Z:]
(A,Z,u,z) is Element of [:A,Z:]
u `1 is Element of A
z `1 is Element of A
(u `1) \/ (z `1) is Element of A
u `2 is Element of Z
z `2 is Element of Z
(u `2) \/ (z `2) is Element of Z
[((u `1) \/ (z `1)),((u `2) \/ (z `2))] is V15() Element of [:A,Z:]
{((u `1) \/ (z `1)),((u `2) \/ (z `2))} is set
{((u `1) \/ (z `1))} is set
{{((u `1) \/ (z `1)),((u `2) \/ (z `2))},{((u `1) \/ (z `1))}} is set
(A,Z,u,z) `1 is Element of A
(A,Z,u,z) `2 is Element of Z
A is non empty cup-closed diff-closed preBoolean set
Z is non empty cup-closed diff-closed preBoolean set
[:A,Z:] is Relation-like non empty set
u is Element of [:A,Z:]
z is Element of [:A,Z:]
(A,Z,u,z) is Element of [:A,Z:]
u `1 is Element of A
z `1 is Element of A
(u `1) \/ (z `1) is Element of A
u `2 is Element of Z
z `2 is Element of Z
(u `2) \/ (z `2) is Element of Z
[((u `1) \/ (z `1)),((u `2) \/ (z `2))] is V15() Element of [:A,Z:]
{((u `1) \/ (z `1)),((u `2) \/ (z `2))} is set
{((u `1) \/ (z `1))} is set
{{((u `1) \/ (z `1)),((u `2) \/ (z `2))},{((u `1) \/ (z `1))}} is set
A is non empty cup-closed diff-closed preBoolean set
Z is non empty cup-closed diff-closed preBoolean set
[:A,Z:] is Relation-like non empty set
u is Element of [:A,Z:]
z is Element of [:A,Z:]
u9 is Element of [:A,Z:]
(A,Z,u9,u) is Element of [:A,Z:]
u9 `1 is Element of A
u `1 is Element of A
(u9 `1) \/ (u `1) is Element of A
u9 `2 is Element of Z
u `2 is Element of Z
(u9 `2) \/ (u `2) is Element of Z
[((u9 `1) \/ (u `1)),((u9 `2) \/ (u `2))] is V15() Element of [:A,Z:]
{((u9 `1) \/ (u `1)),((u9 `2) \/ (u `2))} is set
{((u9 `1) \/ (u `1))} is set
{{((u9 `1) \/ (u `1)),((u9 `2) \/ (u `2))},{((u9 `1) \/ (u `1))}} is set
(A,Z,u9,z) is Element of [:A,Z:]
z `1 is Element of A
(u9 `1) \/ (z `1) is Element of A
z `2 is Element of Z
(u9 `2) \/ (z `2) is Element of Z
[((u9 `1) \/ (z `1)),((u9 `2) \/ (z `2))] is V15() Element of [:A,Z:]
{((u9 `1) \/ (z `1)),((u9 `2) \/ (z `2))} is set
{((u9 `1) \/ (z `1))} is set
{{((u9 `1) \/ (z `1)),((u9 `2) \/ (z `2))},{((u9 `1) \/ (z `1))}} is set
(A,Z,u,u9) is Element of [:A,Z:]
(u `1) \/ (u9 `1) is Element of A
(u `2) \/ (u9 `2) is Element of Z
[((u `1) \/ (u9 `1)),((u `2) \/ (u9 `2))] is V15() Element of [:A,Z:]
{((u `1) \/ (u9 `1)),((u `2) \/ (u9 `2))} is set
{((u `1) \/ (u9 `1))} is set
{{((u `1) \/ (u9 `1)),((u `2) \/ (u9 `2))},{((u `1) \/ (u9 `1))}} is set
(A,Z,z,u9) is Element of [:A,Z:]
(z `1) \/ (u9 `1) is Element of A
(z `2) \/ (u9 `2) is Element of Z
[((z `1) \/ (u9 `1)),((z `2) \/ (u9 `2))] is V15() Element of [:A,Z:]
{((z `1) \/ (u9 `1)),((z `2) \/ (u9 `2))} is set
{((z `1) \/ (u9 `1))} is set
{{((z `1) \/ (u9 `1)),((z `2) \/ (u9 `2))},{((z `1) \/ (u9 `1))}} is set
(A,Z,u9,z) `1 is Element of A
(A,Z,u9,z) `2 is Element of Z
(A,Z,u9,u) `1 is Element of A
(A,Z,u9,u) `2 is Element of Z
(A,Z,z,u9) `1 is Element of A
(A,Z,z,u9) `2 is Element of Z
(A,Z,u,u9) `1 is Element of A
(A,Z,u,u9) `2 is Element of Z
A is non empty cup-closed diff-closed preBoolean set
Z is non empty cup-closed diff-closed preBoolean set
[:A,Z:] is Relation-like non empty set
u is Element of [:A,Z:]
z is Element of [:A,Z:]
(A,Z,u,z) is Element of [:A,Z:]
u `1 is Element of A
z `1 is Element of A
(u `1) \ (z `1) is Element of A
u `2 is Element of Z
z `2 is Element of Z
(u `2) \ (z `2) is Element of Z
[((u `1) \ (z `1)),((u `2) \ (z `2))] is V15() Element of [:A,Z:]
{((u `1) \ (z `1)),((u `2) \ (z `2))} is set
{((u `1) \ (z `1))} is set
{{((u `1) \ (z `1)),((u `2) \ (z `2))},{((u `1) \ (z `1))}} is set
(A,Z,(A,Z,u,z),z) is Element of [:A,Z:]
(A,Z,u,z) `1 is Element of A
((A,Z,u,z) `1) \/ (z `1) is Element of A
(A,Z,u,z) `2 is Element of Z
((A,Z,u,z) `2) \/ (z `2) is Element of Z
[(((A,Z,u,z) `1) \/ (z `1)),(((A,Z,u,z) `2) \/ (z `2))] is V15() Element of [:A,Z:]
{(((A,Z,u,z) `1) \/ (z `1)),(((A,Z,u,z) `2) \/ (z `2))} is set
{(((A,Z,u,z) `1) \/ (z `1))} is set
{{(((A,Z,u,z) `1) \/ (z `1)),(((A,Z,u,z) `2) \/ (z `2))},{(((A,Z,u,z) `1) \/ (z `1))}} is set
(A,Z,u,z) is Element of [:A,Z:]
(u `1) \/ (z `1) is Element of A
(u `2) \/ (z `2) is Element of Z
[((u `1) \/ (z `1)),((u `2) \/ (z `2))] is V15() Element of [:A,Z:]
{((u `1) \/ (z `1)),((u `2) \/ (z `2))} is set
{((u `1) \/ (z `1))} is set
{{((u `1) \/ (z `1)),((u `2) \/ (z `2))},{((u `1) \/ (z `1))}} is set
((u `1) \ (z `1)) \/ (z `1) is Element of A
((u `2) \ (z `2)) \/ (z `2) is Element of Z
A is non empty cup-closed diff-closed preBoolean set
Z is non empty cup-closed diff-closed preBoolean set
[:A,Z:] is Relation-like non empty set
u is Element of [:A,Z:]
z is Element of [:A,Z:]
(A,Z,u,z) is Element of [:A,Z:]
u `1 is Element of A
z `1 is Element of A
(u `1) \ (z `1) is Element of A
u `2 is Element of Z
z `2 is Element of Z
(u `2) \ (z `2) is Element of Z
[((u `1) \ (z `1)),((u `2) \ (z `2))] is V15() Element of [:A,Z:]
{((u `1) \ (z `1)),((u `2) \ (z `2))} is set
{((u `1) \ (z `1))} is set
{{((u `1) \ (z `1)),((u `2) \ (z `2))},{((u `1) \ (z `1))}} is set
u9 is Element of [:A,Z:]
(A,Z,z,u9) is Element of [:A,Z:]
u9 `1 is Element of A
(z `1) \/ (u9 `1) is Element of A
u9 `2 is Element of Z
(z `2) \/ (u9 `2) is Element of Z
[((z `1) \/ (u9 `1)),((z `2) \/ (u9 `2))] is V15() Element of [:A,Z:]
{((z `1) \/ (u9 `1)),((z `2) \/ (u9 `2))} is set
{((z `1) \/ (u9 `1))} is set
{{((z `1) \/ (u9 `1)),((z `2) \/ (u9 `2))},{((z `1) \/ (u9 `1))}} is set
(A,Z,u,z) `1 is Element of A
(A,Z,u,z) `2 is Element of Z
(A,Z,z,u9) `1 is Element of A
(A,Z,z,u9) `2 is Element of Z
A is non empty cup-closed diff-closed preBoolean set
Z is non empty cup-closed diff-closed preBoolean set
[:A,Z:] is Relation-like non empty set
u is Element of [:A,Z:]
z is Element of [:A,Z:]
u9 is Element of [:A,Z:]
(A,Z,z,u9) is Element of [:A,Z:]
z `1 is Element of A
u9 `1 is Element of A
(z `1) \/ (u9 `1) is Element of A
z `2 is Element of Z
u9 `2 is Element of Z
(z `2) \/ (u9 `2) is Element of Z
[((z `1) \/ (u9 `1)),((z `2) \/ (u9 `2))] is V15() Element of [:A,Z:]
{((z `1) \/ (u9 `1)),((z `2) \/ (u9 `2))} is set
{((z `1) \/ (u9 `1))} is set
{{((z `1) \/ (u9 `1)),((z `2) \/ (u9 `2))},{((z `1) \/ (u9 `1))}} is set
(A,Z,u,u9) is Element of [:A,Z:]
u `1 is Element of A
(u `1) \ (u9 `1) is Element of A
u `2 is Element of Z
(u `2) \ (u9 `2) is Element of Z
[((u `1) \ (u9 `1)),((u `2) \ (u9 `2))] is V15() Element of [:A,Z:]
{((u `1) \ (u9 `1)),((u `2) \ (u9 `2))} is set
{((u `1) \ (u9 `1))} is set
{{((u `1) \ (u9 `1)),((u `2) \ (u9 `2))},{((u `1) \ (u9 `1))}} is set
(A,Z,z,u9) `1 is Element of A
(A,Z,z,u9) `2 is Element of Z
(A,Z,u,u9) `1 is Element of A
(A,Z,u,u9) `2 is Element of Z
A is set
Fin A is non empty cup-closed diff-closed preBoolean set
[:(Fin A),(Fin A):] is Relation-like non empty set
[:[:(Fin A),(Fin A):],[:(Fin A),(Fin A):]:] is Relation-like non empty set
[:[:[:(Fin A),(Fin A):],[:(Fin A),(Fin A):]:],[:(Fin A),(Fin A):]:] is Relation-like non empty set
bool [:[:[:(Fin A),(Fin A):],[:(Fin A),(Fin A):]:],[:(Fin A),(Fin A):]:] is non empty cup-closed diff-closed preBoolean set
Z is Relation-like [:[:(Fin A),(Fin A):],[:(Fin A),(Fin A):]:] -defined [:(Fin A),(Fin A):] -valued V6() non empty V14([:[:(Fin A),(Fin A):],[:(Fin A),(Fin A):]:]) V18([:[:(Fin A),(Fin A):],[:(Fin A),(Fin A):]:],[:(Fin A),(Fin A):]) Element of bool [:[:[:(Fin A),(Fin A):],[:(Fin A),(Fin A):]:],[:(Fin A),(Fin A):]:]
Z is Relation-like [:[:(Fin A),(Fin A):],[:(Fin A),(Fin A):]:] -defined [:(Fin A),(Fin A):] -valued V6() non empty V14([:[:(Fin A),(Fin A):],[:(Fin A),(Fin A):]:]) V18([:[:(Fin A),(Fin A):],[:(Fin A),(Fin A):]:],[:(Fin A),(Fin A):]) Element of bool [:[:[:(Fin A),(Fin A):],[:(Fin A),(Fin A):]:],[:(Fin A),(Fin A):]:]
u is Relation-like [:[:(Fin A),(Fin A):],[:(Fin A),(Fin A):]:] -defined [:(Fin A),(Fin A):] -valued V6() non empty V14([:[:(Fin A),(Fin A):],[:(Fin A),(Fin A):]:]) V18([:[:(Fin A),(Fin A):],[:(Fin A),(Fin A):]:],[:(Fin A),(Fin A):]) Element of bool [:[:[:(Fin A),(Fin A):],[:(Fin A),(Fin A):]:],[:(Fin A),(Fin A):]:]
z is Element of [:(Fin A),(Fin A):]
u9 is Element of [:(Fin A),(Fin A):]
Z . (z,u9) is Element of [:(Fin A),(Fin A):]
[z,u9] is V15() set
{z,u9} is set
{z} is set
{{z,u9},{z}} is set
K11(Z,[z,u9]) is set
((Fin A),(Fin A),z,u9) is Element of [:(Fin A),(Fin A):]
z `1 is finite Element of Fin A
u9 `1 is finite Element of Fin A
(z `1) \/ (u9 `1) is finite Element of Fin A
z `2 is finite Element of Fin A
u9 `2 is finite Element of Fin A
(z `2) \/ (u9 `2) is finite Element of Fin A
[((z `1) \/ (u9 `1)),((z `2) \/ (u9 `2))] is V15() Element of [:(Fin A),(Fin A):]
{((z `1) \/ (u9 `1)),((z `2) \/ (u9 `2))} is set
{((z `1) \/ (u9 `1))} is set
{{((z `1) \/ (u9 `1)),((z `2) \/ (u9 `2))},{((z `1) \/ (u9 `1))}} is set
u . (z,u9) is Element of [:(Fin A),(Fin A):]
K11(u,[z,u9]) is set
A is non empty set
Fin A is non empty cup-closed diff-closed preBoolean set
Z is set
Fin Z is non empty cup-closed diff-closed preBoolean set
[:(Fin Z),(Fin Z):] is Relation-like non empty set
[:A,[:(Fin Z),(Fin Z):]:] is Relation-like non empty set
bool [:A,[:(Fin Z),(Fin Z):]:] is non empty cup-closed diff-closed preBoolean set
(Z) is Relation-like [:[:(Fin Z),(Fin Z):],[:(Fin Z),(Fin Z):]:] -defined [:(Fin Z),(Fin Z):] -valued V6() non empty V14([:[:(Fin Z),(Fin Z):],[:(Fin Z),(Fin Z):]:]) V18([:[:(Fin Z),(Fin Z):],[:(Fin Z),(Fin Z):]:],[:(Fin Z),(Fin Z):]) Element of bool [:[:[:(Fin Z),(Fin Z):],[:(Fin Z),(Fin Z):]:],[:(Fin Z),(Fin Z):]:]
[:[:(Fin Z),(Fin Z):],[:(Fin Z),(Fin Z):]:] is Relation-like non empty set
[:[:[:(Fin Z),(Fin Z):],[:(Fin Z),(Fin Z):]:],[:(Fin Z),(Fin Z):]:] is Relation-like non empty set
bool [:[:[:(Fin Z),(Fin Z):],[:(Fin Z),(Fin Z):]:],[:(Fin Z),(Fin Z):]:] is non empty cup-closed diff-closed preBoolean set
u is finite Element of Fin A
z is Relation-like A -defined [:(Fin Z),(Fin Z):] -valued V6() non empty V14(A) V18(A,[:(Fin Z),(Fin Z):]) Element of bool [:A,[:(Fin Z),(Fin Z):]:]
(Z) $$ (u,z) is Element of [:(Fin Z),(Fin Z):]
A is set
Fin A is non empty cup-closed diff-closed preBoolean set
[:(Fin A),(Fin A):] is Relation-like non empty set
(A) is Relation-like [:[:(Fin A),(Fin A):],[:(Fin A),(Fin A):]:] -defined [:(Fin A),(Fin A):] -valued V6() non empty V14([:[:(Fin A),(Fin A):],[:(Fin A),(Fin A):]:]) V18([:[:(Fin A),(Fin A):],[:(Fin A),(Fin A):]:],[:(Fin A),(Fin A):]) Element of bool [:[:[:(Fin A),(Fin A):],[:(Fin A),(Fin A):]:],[:(Fin A),(Fin A):]:]
[:[:(Fin A),(Fin A):],[:(Fin A),(Fin A):]:] is Relation-like non empty set
[:[:[:(Fin A),(Fin A):],[:(Fin A),(Fin A):]:],[:(Fin A),(Fin A):]:] is Relation-like non empty set
bool [:[:[:(Fin A),(Fin A):],[:(Fin A),(Fin A):]:],[:(Fin A),(Fin A):]:] is non empty cup-closed diff-closed preBoolean set
Z is Element of [:(Fin A),(Fin A):]
(A) . (Z,Z) is Element of [:(Fin A),(Fin A):]
[Z,Z] is V15() set
{Z,Z} is set
{Z} is set
{{Z,Z},{Z}} is set
K11((A),[Z,Z]) is set
(A) . (Z,Z) is Element of [:(Fin A),(Fin A):]
((Fin A),(Fin A),Z,Z) is Element of [:(Fin A),(Fin A):]
Z `1 is finite Element of Fin A
(Z `1) \/ (Z `1) is finite Element of Fin A
Z `2 is finite Element of Fin A
(Z `2) \/ (Z `2) is finite Element of Fin A
[((Z `1) \/ (Z `1)),((Z `2) \/ (Z `2))] is V15() Element of [:(Fin A),(Fin A):]
{((Z `1) \/ (Z `1)),((Z `2) \/ (Z `2))} is set
{((Z `1) \/ (Z `1))} is set
{{((Z `1) \/ (Z `1)),((Z `2) \/ (Z `2))},{((Z `1) \/ (Z `1))}} is set
A is set
Fin A is non empty cup-closed diff-closed preBoolean set
[:(Fin A),(Fin A):] is Relation-like non empty set
(A) is Relation-like [:[:(Fin A),(Fin A):],[:(Fin A),(Fin A):]:] -defined [:(Fin A),(Fin A):] -valued V6() non empty V14([:[:(Fin A),(Fin A):],[:(Fin A),(Fin A):]:]) V18([:[:(Fin A),(Fin A):],[:(Fin A),(Fin A):]:],[:(Fin A),(Fin A):]) Element of bool [:[:[:(Fin A),(Fin A):],[:(Fin A),(Fin A):]:],[:(Fin A),(Fin A):]:]
[:[:(Fin A),(Fin A):],[:(Fin A),(Fin A):]:] is Relation-like non empty set
[:[:[:(Fin A),(Fin A):],[:(Fin A),(Fin A):]:],[:(Fin A),(Fin A):]:] is Relation-like non empty set
bool [:[:[:(Fin A),(Fin A):],[:(Fin A),(Fin A):]:],[:(Fin A),(Fin A):]:] is non empty cup-closed diff-closed preBoolean set
Z is Element of [:(Fin A),(Fin A):]
u is Element of [:(Fin A),(Fin A):]
(A) . (Z,u) is Element of [:(Fin A),(Fin A):]
[Z,u] is V15() set
{Z,u} is set
{Z} is set
{{Z,u},{Z}} is set
K11((A),[Z,u]) is set
(A) . (u,Z) is Element of [:(Fin A),(Fin A):]
[u,Z] is V15() set
{u,Z} is set
{u} is set
{{u,Z},{u}} is set
K11((A),[u,Z]) is set
(A) . (Z,u) is Element of [:(Fin A),(Fin A):]
((Fin A),(Fin A),u,Z) is Element of [:(Fin A),(Fin A):]
u `1 is finite Element of Fin A
Z `1 is finite Element of Fin A
(u `1) \/ (Z `1) is finite Element of Fin A
u `2 is finite Element of Fin A
Z `2 is finite Element of Fin A
(u `2) \/ (Z `2) is finite Element of Fin A
[((u `1) \/ (Z `1)),((u `2) \/ (Z `2))] is V15() Element of [:(Fin A),(Fin A):]
{((u `1) \/ (Z `1)),((u `2) \/ (Z `2))} is set
{((u `1) \/ (Z `1))} is set
{{((u `1) \/ (Z `1)),((u `2) \/ (Z `2))},{((u `1) \/ (Z `1))}} is set
(A) . (u,Z) is Element of [:(Fin A),(Fin A):]
A is set
Fin A is non empty cup-closed diff-closed preBoolean set
[:(Fin A),(Fin A):] is Relation-like non empty set
(A) is Relation-like [:[:(Fin A),(Fin A):],[:(Fin A),(Fin A):]:] -defined [:(Fin A),(Fin A):] -valued V6() non empty V14([:[:(Fin A),(Fin A):],[:(Fin A),(Fin A):]:]) V18([:[:(Fin A),(Fin A):],[:(Fin A),(Fin A):]:],[:(Fin A),(Fin A):]) Element of bool [:[:[:(Fin A),(Fin A):],[:(Fin A),(Fin A):]:],[:(Fin A),(Fin A):]:]
[:[:(Fin A),(Fin A):],[:(Fin A),(Fin A):]:] is Relation-like non empty set
[:[:[:(Fin A),(Fin A):],[:(Fin A),(Fin A):]:],[:(Fin A),(Fin A):]:] is Relation-like non empty set
bool [:[:[:(Fin A),(Fin A):],[:(Fin A),(Fin A):]:],[:(Fin A),(Fin A):]:] is non empty cup-closed diff-closed preBoolean set
Z is Element of [:(Fin A),(Fin A):]
u is Element of [:(Fin A),(Fin A):]
z is Element of [:(Fin A),(Fin A)