:: 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):]
(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,((A) . (u,z))) is Element of [:(Fin A),(Fin A):]
[Z,((A) . (u,z))] is V15() set
{Z,((A) . (u,z))} is set
{Z} is set
{{Z,((A) . (u,z))},{Z}} is set
K11((A),[Z,((A) . (u,z))]) is set
(A) . (Z,u) is Element of [:(Fin A),(Fin A):]
[Z,u] is V15() set
{Z,u} is set
{{Z,u},{Z}} is set
K11((A),[Z,u]) is set
(A) . (((A) . (Z,u)),z) is Element of [:(Fin A),(Fin A):]
[((A) . (Z,u)),z] is V15() set
{((A) . (Z,u)),z} is set
{((A) . (Z,u))} is set
{{((A) . (Z,u)),z},{((A) . (Z,u))}} is set
K11((A),[((A) . (Z,u)),z]) is set
(A) . (u,z) is Element of [:(Fin A),(Fin A):]
(A) . (Z,((A) . (u,z))) is Element of [:(Fin A),(Fin A):]
[Z,((A) . (u,z))] is V15() set
{Z,((A) . (u,z))} is set
{{Z,((A) . (u,z))},{Z}} is set
K11((A),[Z,((A) . (u,z))]) is set
((Fin A),(Fin A),Z,((A) . (u,z))) is Element of [:(Fin A),(Fin A):]
Z `1 is finite Element of Fin A
((A) . (u,z)) `1 is finite Element of Fin A
(Z `1) \/ (((A) . (u,z)) `1) is finite Element of Fin A
Z `2 is finite Element of Fin A
((A) . (u,z)) `2 is finite Element of Fin A
(Z `2) \/ (((A) . (u,z)) `2) is finite Element of Fin A
[((Z `1) \/ (((A) . (u,z)) `1)),((Z `2) \/ (((A) . (u,z)) `2))] is V15() Element of [:(Fin A),(Fin A):]
{((Z `1) \/ (((A) . (u,z)) `1)),((Z `2) \/ (((A) . (u,z)) `2))} is set
{((Z `1) \/ (((A) . (u,z)) `1))} is set
{{((Z `1) \/ (((A) . (u,z)) `1)),((Z `2) \/ (((A) . (u,z)) `2))},{((Z `1) \/ (((A) . (u,z)) `1))}} is set
((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
((Fin A),(Fin A),Z,((Fin A),(Fin A),u,z)) is Element of [:(Fin A),(Fin A):]
((Fin A),(Fin A),u,z) `1 is finite Element of Fin A
(Z `1) \/ (((Fin A),(Fin A),u,z) `1) is finite Element of Fin A
((Fin A),(Fin A),u,z) `2 is finite Element of Fin A
(Z `2) \/ (((Fin A),(Fin A),u,z) `2) is finite Element of Fin A
[((Z `1) \/ (((Fin A),(Fin A),u,z) `1)),((Z `2) \/ (((Fin A),(Fin A),u,z) `2))] is V15() Element of [:(Fin A),(Fin A):]
{((Z `1) \/ (((Fin A),(Fin A),u,z) `1)),((Z `2) \/ (((Fin A),(Fin A),u,z) `2))} is set
{((Z `1) \/ (((Fin A),(Fin A),u,z) `1))} is set
{{((Z `1) \/ (((Fin A),(Fin A),u,z) `1)),((Z `2) \/ (((Fin A),(Fin A),u,z) `2))},{((Z `1) \/ (((Fin A),(Fin A),u,z) `1))}} is set
((Fin A),(Fin A),Z,u) is Element of [:(Fin A),(Fin A):]
(Z `1) \/ (u `1) is finite Element of Fin A
(Z `2) \/ (u `2) is finite Element of Fin A
[((Z `1) \/ (u `1)),((Z `2) \/ (u `2))] is V15() Element of [:(Fin A),(Fin A):]
{((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
((Fin A),(Fin A),((Fin A),(Fin A),Z,u),z) is Element of [:(Fin A),(Fin A):]
((Fin A),(Fin A),Z,u) `1 is finite Element of Fin A
(((Fin A),(Fin A),Z,u) `1) \/ (z `1) is finite Element of Fin A
((Fin A),(Fin A),Z,u) `2 is finite Element of Fin A
(((Fin A),(Fin A),Z,u) `2) \/ (z `2) is finite Element of Fin A
[((((Fin A),(Fin A),Z,u) `1) \/ (z `1)),((((Fin A),(Fin A),Z,u) `2) \/ (z `2))] is V15() Element of [:(Fin A),(Fin A):]
{((((Fin A),(Fin A),Z,u) `1) \/ (z `1)),((((Fin A),(Fin A),Z,u) `2) \/ (z `2))} is set
{((((Fin A),(Fin A),Z,u) `1) \/ (z `1))} is set
{{((((Fin A),(Fin A),Z,u) `1) \/ (z `1)),((((Fin A),(Fin A),Z,u) `2) \/ (z `2))},{((((Fin A),(Fin A),Z,u) `1) \/ (z `1))}} is set
(A) . (Z,u) is Element of [:(Fin A),(Fin A):]
((Fin A),(Fin A),((A) . (Z,u)),z) is Element of [:(Fin A),(Fin A):]
((A) . (Z,u)) `1 is finite Element of Fin A
(((A) . (Z,u)) `1) \/ (z `1) is finite Element of Fin A
((A) . (Z,u)) `2 is finite Element of Fin A
(((A) . (Z,u)) `2) \/ (z `2) is finite Element of Fin A
[((((A) . (Z,u)) `1) \/ (z `1)),((((A) . (Z,u)) `2) \/ (z `2))] is V15() Element of [:(Fin A),(Fin A):]
{((((A) . (Z,u)) `1) \/ (z `1)),((((A) . (Z,u)) `2) \/ (z `2))} is set
{((((A) . (Z,u)) `1) \/ (z `1))} is set
{{((((A) . (Z,u)) `1) \/ (z `1)),((((A) . (Z,u)) `2) \/ (z `2))},{((((A) . (Z,u)) `1) \/ (z `1))}} is set
(A) . (((A) . (Z,u)),z) is Element of [:(Fin A),(Fin A):]
[((A) . (Z,u)),z] is V15() set
{((A) . (Z,u)),z} is set
{((A) . (Z,u))} is set
{{((A) . (Z,u)),z},{((A) . (Z,u))}} is set
K11((A),[((A) . (Z,u)),z]) 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
A is set
Fin A is non empty cup-closed diff-closed preBoolean set
[:(Fin A),(Fin A):] is Relation-like non empty set
Z is non empty set
[:Z,[:(Fin A),(Fin A):]:] is Relation-like non empty set
bool [:Z,[:(Fin A),(Fin A):]:] is non empty cup-closed diff-closed preBoolean set
Fin Z is non empty cup-closed diff-closed preBoolean set
u is Relation-like Z -defined [:(Fin A),(Fin A):] -valued V6() non empty V14(Z) V18(Z,[:(Fin A),(Fin A):]) Element of bool [:Z,[:(Fin A),(Fin A):]:]
z is finite Element of Fin Z
(Z,A,z,u) is Element of [:(Fin A),(Fin A):]
(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):]) commutative associative idempotent 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
(A) $$ (z,u) is Element of [:(Fin A),(Fin A):]
u9 is Element of Z
u . u9 is Element of [:(Fin A),(Fin A):]
{.u9.} is finite Element of Fin Z
z \/ {.u9.} is finite Element of Fin Z
(A) $$ ((z \/ {.u9.}),u) is Element of [:(Fin A),(Fin A):]
(A) . (((A) $$ (z,u)),(u . u9)) is Element of [:(Fin A),(Fin A):]
[((A) $$ (z,u)),(u . u9)] is V15() set
{((A) $$ (z,u)),(u . u9)} is set
{((A) $$ (z,u))} is set
{{((A) $$ (z,u)),(u . u9)},{((A) $$ (z,u))}} is set
K11((A),[((A) $$ (z,u)),(u . u9)]) is set
((Fin A),(Fin A),((A) $$ (z,u)),(u . u9)) is Element of [:(Fin A),(Fin A):]
((A) $$ (z,u)) `1 is finite Element of Fin A
(u . u9) `1 is finite Element of Fin A
(((A) $$ (z,u)) `1) \/ ((u . u9) `1) is finite Element of Fin A
((A) $$ (z,u)) `2 is finite Element of Fin A
(u . u9) `2 is finite Element of Fin A
(((A) $$ (z,u)) `2) \/ ((u . u9) `2) is finite Element of Fin A
[((((A) $$ (z,u)) `1) \/ ((u . u9) `1)),((((A) $$ (z,u)) `2) \/ ((u . u9) `2))] is V15() Element of [:(Fin A),(Fin A):]
{((((A) $$ (z,u)) `1) \/ ((u . u9) `1)),((((A) $$ (z,u)) `2) \/ ((u . u9) `2))} is set
{((((A) $$ (z,u)) `1) \/ ((u . u9) `1))} is set
{{((((A) $$ (z,u)) `1) \/ ((u . u9) `1)),((((A) $$ (z,u)) `2) \/ ((u . u9) `2))},{((((A) $$ (z,u)) `1) \/ ((u . u9) `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 non-empty empty-yielding empty finite Element of Fin A
[({}. A),({}. A)] is V15() Element of [:(Fin A),(Fin A):]
{({}. A),({}. A)} is set
{({}. A)} is set
{{({}. A),({}. A)},{({}. A)}} is 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):]) commutative associative idempotent 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) . ([({}. A),({}. A)],Z) is Element of [:(Fin A),(Fin A):]
[[({}. A),({}. A)],Z] is V15() set
{[({}. A),({}. A)],Z} is set
{[({}. A),({}. A)]} is Relation-like set
{{[({}. A),({}. A)],Z},{[({}. A),({}. A)]}} is set
K11((A),[[({}. A),({}. A)],Z]) is set
((Fin A),(Fin A),[({}. A),({}. A)],Z) is Element of [:(Fin A),(Fin A):]
[({}. A),({}. A)] `1 is finite Element of Fin A
Z `1 is finite Element of Fin A
([({}. A),({}. A)] `1) \/ (Z `1) is finite Element of Fin A
[({}. A),({}. A)] `2 is finite Element of Fin A
Z `2 is finite Element of Fin A
([({}. A),({}. A)] `2) \/ (Z `2) is finite Element of Fin A
[(([({}. A),({}. A)] `1) \/ (Z `1)),(([({}. A),({}. A)] `2) \/ (Z `2))] is V15() Element of [:(Fin A),(Fin A):]
{(([({}. A),({}. A)] `1) \/ (Z `1)),(([({}. A),({}. A)] `2) \/ (Z `2))} is set
{(([({}. A),({}. A)] `1) \/ (Z `1))} is set
{{(([({}. A),({}. A)] `1) \/ (Z `1)),(([({}. A),({}. A)] `2) \/ (Z `2))},{(([({}. A),({}. A)] `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):]) commutative associative idempotent 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
{}. A is Relation-like non-empty empty-yielding empty finite Element of Fin A
[({}. A),({}. A)] is V15() Element of [:(Fin A),(Fin A):]
{({}. A),({}. A)} is set
{({}. A)} is set
{{({}. A),({}. A)},{({}. A)}} 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):]) commutative associative idempotent 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
the_unity_wrt (A) is Element of [:(Fin A),(Fin A):]
{}. A is Relation-like non-empty empty-yielding empty finite Element of Fin A
[({}. A),({}. A)] is V15() Element of [:(Fin A),(Fin A):]
{({}. A),({}. A)} is set
{({}. A)} is set
{{({}. A),({}. A)},{({}. A)}} 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):]) commutative associative idempotent 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
the_unity_wrt (A) is Element of [:(Fin A),(Fin A):]
Z is Element of [:(Fin A),(Fin A):]
{}. A is Relation-like non-empty empty-yielding empty finite Element of Fin A
[({}. A),({}. A)] is V15() Element of [:(Fin A),(Fin A):]
{({}. A),({}. A)} is set
{({}. A)} is set
{{({}. A),({}. A)},{({}. A)}} is set
[{},{}] is V15() set
{{},{}} is set
{{}} is set
{{{},{}},{{}}} is set
(the_unity_wrt (A)) `1 is finite Element of Fin A
(the_unity_wrt (A)) `2 is finite Element of Fin A
Z `1 is finite Element of Fin A
Z `2 is finite Element of 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
Z is non empty set
[:Z,[:(Fin A),(Fin A):]:] is Relation-like non empty set
bool [:Z,[:(Fin A),(Fin A):]:] is non empty cup-closed diff-closed preBoolean set
Fin Z is non empty cup-closed diff-closed preBoolean set
u is Relation-like Z -defined [:(Fin A),(Fin A):] -valued V6() non empty V14(Z) V18(Z,[:(Fin A),(Fin A):]) Element of bool [:Z,[:(Fin A),(Fin A):]:]
z is finite Element of Fin Z
(Z,A,z,u) is Element of [:(Fin A),(Fin A):]
(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):]) commutative associative idempotent 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
(A) $$ (z,u) is Element of [:(Fin A),(Fin A):]
u9 is Element of [:(Fin A),(Fin A):]
K is finite Element of Fin Z
(A) $$ (K,u) is Element of [:(Fin A),(Fin A):]
L is Element of Z
{L} is Element of bool Z
bool Z is non empty cup-closed diff-closed preBoolean set
K \/ {L} is set
u . L is Element of [:(Fin A),(Fin A):]
{.L.} is finite Element of Fin Z
K \/ {.L.} is finite Element of Fin Z
(A) $$ ((K \/ {.L.}),u) is Element of [:(Fin A),(Fin A):]
(A) . (((A) $$ (K,u)),(u . L)) is Element of [:(Fin A),(Fin A):]
[((A) $$ (K,u)),(u . L)] is V15() set
{((A) $$ (K,u)),(u . L)} is set
{((A) $$ (K,u))} is set
{{((A) $$ (K,u)),(u . L)},{((A) $$ (K,u))}} is set
K11((A),[((A) $$ (K,u)),(u . L)]) is set
((Fin A),(Fin A),((A) $$ (K,u)),(u . L)) is Element of [:(Fin A),(Fin A):]
((A) $$ (K,u)) `1 is finite Element of Fin A
(u . L) `1 is finite Element of Fin A
(((A) $$ (K,u)) `1) \/ ((u . L) `1) is finite Element of Fin A
((A) $$ (K,u)) `2 is finite Element of Fin A
(u . L) `2 is finite Element of Fin A
(((A) $$ (K,u)) `2) \/ ((u . L) `2) is finite Element of Fin A
[((((A) $$ (K,u)) `1) \/ ((u . L) `1)),((((A) $$ (K,u)) `2) \/ ((u . L) `2))] is V15() Element of [:(Fin A),(Fin A):]
{((((A) $$ (K,u)) `1) \/ ((u . L) `1)),((((A) $$ (K,u)) `2) \/ ((u . L) `2))} is set
{((((A) $$ (K,u)) `1) \/ ((u . L) `1))} is set
{{((((A) $$ (K,u)) `1) \/ ((u . L) `1)),((((A) $$ (K,u)) `2) \/ ((u . L) `2))},{((((A) $$ (K,u)) `1) \/ ((u . L) `1))}} is set
{}. Z is Relation-like non-empty empty-yielding empty finite Element of Fin Z
(A) $$ (({}. Z),u) is Element of [:(Fin A),(Fin A):]
the_unity_wrt (A) 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
Z is non empty set
Fin Z is non empty cup-closed diff-closed preBoolean set
[:Z,[:(Fin A),(Fin A):]:] is Relation-like non empty set
bool [:Z,[:(Fin A),(Fin A):]:] is non empty cup-closed diff-closed preBoolean set
u is finite Element of Fin Z
z is Relation-like Z -defined [:(Fin A),(Fin A):] -valued V6() non empty V14(Z) V18(Z,[:(Fin A),(Fin A):]) Element of bool [:Z,[:(Fin A),(Fin A):]:]
z | u is Relation-like u -defined Z -defined [:(Fin A),(Fin A):] -valued set
u9 is Relation-like Z -defined [:(Fin A),(Fin A):] -valued V6() non empty V14(Z) V18(Z,[:(Fin A),(Fin A):]) Element of bool [:Z,[:(Fin A),(Fin A):]:]
u9 | u is Relation-like u -defined Z -defined [:(Fin A),(Fin A):] -valued set
(Z,A,u,z) is Element of [:(Fin A),(Fin A):]
(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):]) commutative associative idempotent 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
(A) $$ (u,z) is Element of [:(Fin A),(Fin A):]
(Z,A,u,u9) is Element of [:(Fin A),(Fin A):]
(A) $$ (u,u9) is Element of [:(Fin A),(Fin A):]
{}. A is Relation-like non-empty empty-yielding empty finite Element of Fin A
[({}. A),({}. A)] is V15() Element of [:(Fin A),(Fin A):]
{({}. A),({}. A)} is set
{({}. A)} is set
{{({}. A),({}. A)},{({}. A)}} is set
the_unity_wrt (A) is Element of [:(Fin A),(Fin A):]
{}. Z is Relation-like non-empty empty-yielding empty finite Element of Fin Z
(A) $$ (({}. Z),z) is Element of [:(Fin A),(Fin A):]
(A) $$ (({}. Z),u9) is Element of [:(Fin A),(Fin A):]
z .: u is finite Element of Fin [:(Fin A),(Fin A):]
Fin [:(Fin A),(Fin A):] is non empty cup-closed diff-closed preBoolean set
u9 .: u is finite Element of Fin [:(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
{ b₁ where b₁ is Element of [:(Fin A),(Fin A):] : b₁ `1 misses b<sub>1</sub> `2 } is set
bool [:(Fin A),(Fin A):] is non empty cup-closed diff-closed preBoolean set
u is set
z is Element of [:(Fin A),(Fin A):]
z `1 is finite Element of Fin A
z `2 is finite Element of Fin A
A is set
(A) is Relation-like Fin A -defined Fin A -valued Element of bool [:(Fin A),(Fin A):]
Fin A is non empty cup-closed diff-closed preBoolean set
[:(Fin A),(Fin A):] is Relation-like non empty set
bool [:(Fin A),(Fin A):] is non empty cup-closed diff-closed preBoolean set
{ b₁ where b₁ is Element of [:(Fin A),(Fin A):] : b₁ `1 misses b<sub>1</sub> `2 } is set
[{},{}] is V15() set
{{},{}} is set
{{}} is set
{{{},{}},{{}}} is set
Z is Element of [:(Fin A),(Fin A):]
Z `1 is finite Element of Fin A
Z `2 is finite Element of 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 -defined Fin A -valued non empty Element of bool [:(Fin A),(Fin A):]
bool [:(Fin A),(Fin A):] is non empty cup-closed diff-closed preBoolean set
{ b₁ where b₁ is Element of [:(Fin A),(Fin A):] : b₁ `1 misses b<sub>1</sub> `2 } is set
Z is Element of [:(Fin A),(Fin A):]
Z `1 is finite Element of Fin A
Z `2 is finite Element of Fin A
u is Element of [:(Fin A),(Fin A):]
u `1 is finite Element of Fin A
u `2 is finite Element of Fin A
u is Element of [:(Fin A),(Fin A):]
u `1 is finite Element of Fin A
u `2 is finite Element of 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 -defined Fin A -valued non empty Element of bool [:(Fin A),(Fin A):]
bool [:(Fin A),(Fin A):] is non empty cup-closed diff-closed preBoolean set
{ b₁ where b₁ is Element of [:(Fin A),(Fin A):] : b₁ `1 misses b<sub>1</sub> `2 } is set
Z is Element of [:(Fin A),(Fin A):]
Z `1 is finite Element of Fin A
Z `2 is finite Element of Fin A
u is Element of [:(Fin A),(Fin A):]
((Fin A),(Fin A),Z,u) is Element of [:(Fin A),(Fin A):]
u `1 is finite Element of Fin A
(Z `1) \/ (u `1) is finite Element of Fin A
u `2 is finite Element of Fin A
(Z `2) \/ (u `2) is finite Element of Fin A
[((Z `1) \/ (u `1)),((Z `2) \/ (u `2))] is V15() Element of [:(Fin A),(Fin A):]
{((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
(Z `1) /\ (u `2) is finite Element of Fin A
(u `1) /\ (Z `2) is finite Element of Fin A
((Z `1) /\ (u `2)) \/ ((u `1) /\ (Z `2)) is finite Element of Fin A
(Z `1) \/ (u `1) is finite Element of Fin A
(Z `2) \/ (u `2) is finite Element of Fin A
((Z `1) \/ (u `1)) /\ ((Z `2) \/ (u `2)) is finite Element of Fin A
((Z `1) \/ (u `1)) /\ (Z `2) is finite Element of Fin A
((Z `1) \/ (u `1)) /\ (u `2) is finite Element of Fin A
(((Z `1) \/ (u `1)) /\ (Z `2)) \/ (((Z `1) \/ (u `1)) /\ (u `2)) is finite Element of Fin A
(Z `1) /\ (Z `2) is finite Element of Fin A
((Z `1) /\ (Z `2)) \/ ((u `1) /\ (Z `2)) is finite Element of Fin A
(u `1) /\ (u `2) is finite Element of Fin A
((Z `1) /\ (u `2)) \/ ((u `1) /\ (u `2)) is finite Element of Fin A
((Fin A),(Fin A),Z,u) `1 is finite Element of Fin A
((Fin A),(Fin A),Z,u) `2 is finite Element of 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 -defined Fin A -valued non empty Element of bool [:(Fin A),(Fin A):]
bool [:(Fin A),(Fin A):] is non empty cup-closed diff-closed preBoolean set
{ b₁ where b₁ is Element of [:(Fin A),(Fin A):] : b₁ `1 misses b<sub>1</sub> `2 } is set
Z is Element of (A)
Z `1 is finite Element of Fin A
Z `2 is finite Element of 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 -defined Fin A -valued non empty Element of bool [:(Fin A),(Fin A):]
bool [:(Fin A),(Fin A):] is non empty cup-closed diff-closed preBoolean set
{ b₁ where b₁ is Element of [:(Fin A),(Fin A):] : b₁ `1 misses b<sub>1</sub> `2 } is set
Z is Element of [:(Fin A),(Fin A):]
u is Element of (A)
Z `1 is finite Element of Fin A
u `1 is finite Element of Fin A
Z `2 is finite Element of Fin A
u `2 is finite Element of 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 -defined Fin A -valued non empty Element of bool [:(Fin A),(Fin A):]
bool [:(Fin A),(Fin A):] is non empty cup-closed diff-closed preBoolean set
{ b₁ where b₁ is Element of [:(Fin A),(Fin A):] : b₁ `1 misses b<sub>1</sub> `2 } is set
Z is Element of (A)
Z `1 is finite Element of Fin A
Z `2 is finite Element of Fin A
u 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 -defined Fin A -valued non empty Element of bool [:(Fin A),(Fin A):]
bool [:(Fin A),(Fin A):] is non empty cup-closed diff-closed preBoolean set
{ b₁ where b₁ is Element of [:(Fin A),(Fin A):] : b₁ `1 misses b<sub>1</sub> `2 } is set
Z is Element of (A)
Z `1 is finite Element of Fin A
Z `2 is finite Element of Fin A
u is Element of (A)
((Fin A),(Fin A),Z,u) is Element of [:(Fin A),(Fin A):]
u `1 is finite Element of Fin A
(Z `1) \/ (u `1) is finite Element of Fin A
u `2 is finite Element of Fin A
(Z `2) \/ (u `2) is finite Element of Fin A
[((Z `1) \/ (u `1)),((Z `2) \/ (u `2))] is V15() Element of [:(Fin A),(Fin A):]
{((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
((Fin A),(Fin A),Z,u) `1 is finite Element of Fin A
((Fin A),(Fin A),Z,u) `2 is finite Element of Fin A
(((Fin A),(Fin A),Z,u) `1) /\ (((Fin A),(Fin A),Z,u) `2) is finite Element of Fin A
the Element of (((Fin A),(Fin A),Z,u) `1) /\ (((Fin A),(Fin A),Z,u) `2) is Element of (((Fin A),(Fin A),Z,u) `1) /\ (((Fin A),(Fin A),Z,u) `2)
bool A is non empty cup-closed diff-closed preBoolean set
u9 is Element of A
(Z `2) \/ (u `2) is finite Element of Fin A
(Z `1) \/ (u `1) is finite Element of 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
Z is Element of [:(Fin A),(Fin A):]
Z `1 is finite Element of Fin A
Z `2 is finite Element of Fin A
(A) is Relation-like Fin A -defined Fin A -valued non empty Element of bool [:(Fin A),(Fin A):]
bool [:(Fin A),(Fin A):] is non empty cup-closed diff-closed preBoolean set
{ b₁ where b₁ is Element of [:(Fin A),(Fin A):] : b₁ `1 misses b<sub>1</sub> `2 } 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 -defined Fin A -valued non empty Element of bool [:(Fin A),(Fin A):]
bool [:(Fin A),(Fin A):] is non empty cup-closed diff-closed preBoolean set
{ b₁ where b₁ is Element of [:(Fin A),(Fin A):] : b₁ `1 misses b<sub>1</sub> `2 } is set
Z is Element of (A)
Z `1 is finite Element of Fin A
Z `2 is finite Element of Fin A
u is set
z is set
[u,z] is V15() set
{u,z} is set
{u} is set
{{u,z},{u}} is set
[u,z] `2 is set
[u,z] `1 is set
u9 is Element of [:(Fin A),(Fin A):]
u9 `1 is finite Element of Fin A
u9 `2 is finite Element of Fin A
A is set
(A) is Relation-like Fin A -defined Fin A -valued non empty Element of bool [:(Fin A),(Fin A):]
Fin A is non empty cup-closed diff-closed preBoolean set
[:(Fin A),(Fin A):] is Relation-like non empty set
bool [:(Fin A),(Fin A):] is non empty cup-closed diff-closed preBoolean set
{ b₁ where b₁ is Element of [:(Fin A),(Fin A):] : b₁ `1 misses b<sub>1</sub> `2 } is set
Fin (A) is non empty cup-closed diff-closed preBoolean set
{ b₁ where b₁ is finite Element of Fin (A) : for b₂, b₃ being Element of (A) holds
( not b₂ in b₁ or not b₃ in b₁ or not ( Fin A, Fin A,b₂,b₃) or b₂ = b₃ ) } is set
Z is Element of (A)
u is Element of (A)
A is set
(A) is Relation-like Fin A -defined Fin A -valued non empty Element of bool [:(Fin A),(Fin A):]
Fin A is non empty cup-closed diff-closed preBoolean set
[:(Fin A),(Fin A):] is Relation-like non empty set
bool [:(Fin A),(Fin A):] is non empty cup-closed diff-closed preBoolean set
{ b₁ where b₁ is Element of [:(Fin A),(Fin A):] : b₁ `1 misses b<sub>1</sub> `2 } is set
Fin (A) is non empty cup-closed diff-closed preBoolean set
{ b₁ where b₁ is finite Element of Fin (A) : for b₂, b₃ being Element of (A) holds
( not b₂ in b₁ or not b₃ in b₁ or not ( Fin A, Fin A,b₂,b₃) or b₂ = b₃ ) } is set
bool (Fin (A)) is non empty cup-closed diff-closed preBoolean set
u is set
z is finite Element of Fin (A)
A is set
(A) is Element of bool (Fin (A))
(A) is Relation-like Fin A -defined Fin A -valued non empty Element of bool [:(Fin A),(Fin A):]
Fin A is non empty cup-closed diff-closed preBoolean set
[:(Fin A),(Fin A):] is Relation-like non empty set
bool [:(Fin A),(Fin A):] is non empty cup-closed diff-closed preBoolean set
{ b₁ where b₁ is Element of [:(Fin A),(Fin A):] : b₁ `1 misses b<sub>1</sub> `2 } is set
Fin (A) is non empty cup-closed diff-closed preBoolean set
bool (Fin (A)) is non empty cup-closed diff-closed preBoolean set
{ b₁ where b₁ is finite Element of Fin (A) : for b₂, b₃ being Element of (A) holds
( not b₂ in b₁ or not b₃ in b₁ or not ( Fin A, Fin A,b₂,b₃) or b₂ = b₃ ) } is set
A is set
(A) is non empty Element of bool (Fin (A))
(A) is Relation-like Fin A -defined Fin A -valued non empty Element of bool [:(Fin A),(Fin A):]
Fin A is non empty cup-closed diff-closed preBoolean set
[:(Fin A),(Fin A):] is Relation-like non empty set
bool [:(Fin A),(Fin A):] is non empty cup-closed diff-closed preBoolean set
{ b₁ where b₁ is Element of [:(Fin A),(Fin A):] : b₁ `1 misses b<sub>1</sub> `2 } is set
Fin (A) is non empty cup-closed diff-closed preBoolean set
bool (Fin (A)) is non empty cup-closed diff-closed preBoolean set
{ b₁ where b₁ is finite Element of Fin (A) : for b₂, b₃ being Element of (A) holds
( not b₂ in b₁ or not b₃ in b₁ or not ( Fin A, Fin A,b₂,b₃) or b₂ = b₃ ) } 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 -defined Fin A -valued non empty Element of bool [:(Fin A),(Fin A):]
bool [:(Fin A),(Fin A):] is non empty cup-closed diff-closed preBoolean set
{ b₁ where b₁ is Element of [:(Fin A),(Fin A):] : b₁ `1 misses b<sub>1</sub> `2 } is set
Fin (A) is non empty cup-closed diff-closed preBoolean set
(A) is non empty Element of bool (Fin (A))
bool (Fin (A)) is non empty cup-closed diff-closed preBoolean set
{ b₁ where b₁ is finite Element of Fin (A) : for b₂, b₃ being Element of (A) holds
( not b₂ in b₁ or not b₃ in b₁ or not ( Fin A, Fin A,b₂,b₃) or b₂ = b₃ ) } is set
Z is Element of (A)
u is Element of (A)
z is finite Element of Fin (A)
u9 is finite Element of Fin (A)
A is set
(A) is Relation-like Fin A -defined Fin A -valued non empty Element of bool [:(Fin A),(Fin A):]
Fin A is non empty cup-closed diff-closed preBoolean set
[:(Fin A),(Fin A):] is Relation-like non empty set
bool [:(Fin A),(Fin A):] is non empty cup-closed diff-closed preBoolean set
{ b₁ where b₁ is Element of [:(Fin A),(Fin A):] : b₁ `1 misses b<sub>1</sub> `2 } is set
Fin (A) is non empty cup-closed diff-closed preBoolean set
Z is finite Element of Fin (A)
(A) is non empty Element of bool (Fin (A))
bool (Fin (A)) is non empty cup-closed diff-closed preBoolean set
{ b₁ where b₁ is finite Element of Fin (A) : for b₂, b₃ being Element of (A) holds
( not b₂ in b₁ or not b₃ in b₁ or not ( Fin A, Fin A,b₂,b₃) or b₂ = b₃ ) } is set
A is set
(A) is Relation-like Fin A -defined Fin A -valued non empty Element of bool [:(Fin A),(Fin A):]
Fin A is non empty cup-closed diff-closed preBoolean set
[:(Fin A),(Fin A):] is Relation-like non empty set
bool [:(Fin A),(Fin A):] is non empty cup-closed diff-closed preBoolean set
{ b₁ where b₁ is Element of [:(Fin A),(Fin A):] : b₁ `1 misses b<sub>1</sub> `2 } is set
Fin (A) is non empty cup-closed diff-closed preBoolean set
Z is finite Element of Fin (A)
{ b₁ where b₁ is Element of (A) : for b₂ being Element of (A) holds
( ( not b₂ in Z or not ( Fin A, Fin A,b₂,b₁) or b₂ = b₁ ) & ( not b₂ = b₁ or ( b₂ in Z & ( Fin A, Fin A,b₂,b₁) ) ) ) } is set
(A) is non empty Element of bool (Fin (A))
bool (Fin (A)) is non empty cup-closed diff-closed preBoolean set
{ b₁ where b₁ is finite Element of Fin (A) : for b₂, b₃ being Element of (A) holds
( not b₂ in b₁ or not b₃ in b₁ or not ( Fin A, Fin A,b₂,b₃) or b₂ = b₃ ) } is set
z is set
u9 is Element of (A)
u9 is Element of (A)
L is Element of (A)
K is Element of (A)
L is Element of (A)
z is finite Element of Fin (A)
u is finite Element of Fin (A)
{ ((Fin A),(Fin A),b₁,b₂) where b₁, b₂ is Element of (A) : ( b₁ in Z & b₂ in u ) } is set
(A) /\ { ((Fin A),(Fin A),b₁,b₂) where b₁, b₂ is Element of (A) : ( b₁ in Z & b₂ in u ) } is Relation-like Fin A -defined Fin A -valued Element of bool [:(Fin A),(Fin A):]
{ H₁(b₁,b₂) where b₁, b₂ is Element of (A) : ( b₁ in Z & b₂ in u ) } is set
(A) /\ { H₁(b₁,b₂) where b₁, b₂ is Element of (A) : ( b₁ in Z & b₂ in u ) } is Relation-like Fin A -defined Fin A -valued Element of bool [:(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 -defined Fin A -valued non empty Element of bool [:(Fin A),(Fin A):]
bool [:(Fin A),(Fin A):] is non empty cup-closed diff-closed preBoolean set
{ b₁ where b₁ is Element of [:(Fin A),(Fin A):] : b₁ `1 misses b<sub>1</sub> `2 } is set
Fin (A) is non empty cup-closed diff-closed preBoolean set
Z is Element of [:(Fin A),(Fin A):]
u is finite Element of Fin (A)
z is finite Element of Fin (A)
(A,u,z) is finite Element of Fin (A)
{ ((Fin A),(Fin A),b₁,b₂) where b₁, b₂ is Element of (A) : ( b₁ in u & b₂ in z ) } is set
(A) /\ { ((Fin A),(Fin A),b₁,b₂) where b₁, b₂ is Element of (A) : ( b₁ in u & b₂ in z ) } is Relation-like Fin A -defined Fin A -valued Element of bool [:(Fin A),(Fin A):]
u9 is Element of (A)
K is Element of (A)
((Fin A),(Fin A),u9,K) is Element of [:(Fin A),(Fin A):]
u9 `1 is finite Element of Fin A
K `1 is finite Element of Fin A
(u9 `1) \/ (K `1) is finite Element of Fin A
u9 `2 is finite Element of Fin A
K `2 is finite Element of Fin A
(u9 `2) \/ (K `2) is finite Element of Fin A
[((u9 `1) \/ (K `1)),((u9 `2) \/ (K `2))] is V15() Element of [:(Fin A),(Fin A):]
{((u9 `1) \/ (K `1)),((u9 `2) \/ (K `2))} is set
{((u9 `1) \/ (K `1))} is set
{{((u9 `1) \/ (K `1)),((u9 `2) \/ (K `2))},{((u9 `1) \/ (K `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 -defined Fin A -valued non empty Element of bool [:(Fin A),(Fin A):]
bool [:(Fin A),(Fin A):] is non empty cup-closed diff-closed preBoolean set
{ b₁ where b₁ is Element of [:(Fin A),(Fin A):] : b₁ `1 misses b<sub>1</sub> `2 } is set
Fin (A) is non empty cup-closed diff-closed preBoolean set
Z is Element of (A)
u is Element of (A)
((Fin A),(Fin A),Z,u) is Element of [:(Fin A),(Fin A):]
Z `1 is finite Element of Fin A
u `1 is finite Element of Fin A
(Z `1) \/ (u `1) is finite Element of Fin A
Z `2 is finite Element of Fin A
u `2 is finite Element of Fin A
(Z `2) \/ (u `2) is finite Element of Fin A
[((Z `1) \/ (u `1)),((Z `2) \/ (u `2))] is V15() Element of [:(Fin A),(Fin A):]
{((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
z is finite Element of Fin (A)
u9 is finite Element of Fin (A)
(A,z,u9) is finite Element of Fin (A)
{ ((Fin A),(Fin A),b₁,b₂) where b₁, b₂ is Element of (A) : ( b₁ in z & b₂ in u9 ) } is set
(A) /\ { ((Fin A),(Fin A),b₁,b₂) where b₁, b₂ is Element of (A) : ( b₁ in z & b₂ in u9 ) } is Relation-like Fin A -defined Fin A -valued Element of bool [:(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 -defined Fin A -valued non empty Element of bool [:(Fin A),(Fin A):]
bool [:(Fin A),(Fin A):] is non empty cup-closed diff-closed preBoolean set
{ b₁ where b₁ is Element of [:(Fin A),(Fin A):] : b₁ `1 misses b<sub>1</sub> `2 } is set
Fin (A) is non empty cup-closed diff-closed preBoolean set
Z is Element of (A)
u is Element of (A)
z is finite Element of Fin (A)
(A,z) is Element of (A)
(A) is non empty Element of bool (Fin (A))
bool (Fin (A)) is non empty cup-closed diff-closed preBoolean set
{ b₁ where b₁ is finite Element of Fin (A) : for b₂, b₃ being Element of (A) holds
( not b₂ in b₁ or not b₃ in b₁ or not ( Fin A, Fin A,b₂,b₃) or b₂ = b₃ ) } is set
{ b₁ where b₁ is Element of (A) : for b₂ being Element of (A) holds
( ( not b₂ in z or not ( Fin A, Fin A,b₂,b₁) or b₂ = b₁ ) & ( not b₂ = b₁ or ( b₂ in z & ( Fin A, Fin A,b₂,b₁) ) ) ) } is set
u9 is Element of (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 -defined Fin A -valued non empty Element of bool [:(Fin A),(Fin A):]
bool [:(Fin A),(Fin A):] is non empty cup-closed diff-closed preBoolean set
{ b₁ where b₁ is Element of [:(Fin A),(Fin A):] : b₁ `1 misses b<sub>1</sub> `2 } is set
Fin (A) is non empty cup-closed diff-closed preBoolean set
Z is Element of (A)
u is finite Element of Fin (A)
(A,u) is Element of (A)
(A) is non empty Element of bool (Fin (A))
bool (Fin (A)) is non empty cup-closed diff-closed preBoolean set
{ b₁ where b₁ is finite Element of Fin (A) : for b₂, b₃ being Element of (A) holds
( not b₂ in b₁ or not b₃ in b₁ or not ( Fin A, Fin A,b₂,b₃) or b₂ = b₃ ) } is set
{ b₁ where b₁ is Element of (A) : for b₂ being Element of (A) holds
( ( not b₂ in u or not ( Fin A, Fin A,b₂,b₁) or b₂ = b₁ ) & ( not b₂ = b₁ or ( b₂ in u & ( Fin A, Fin A,b₂,b₁) ) ) ) } 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 -defined Fin A -valued non empty Element of bool [:(Fin A),(Fin A):]
bool [:(Fin A),(Fin A):] is non empty cup-closed diff-closed preBoolean set
{ b₁ where b₁ is Element of [:(Fin A),(Fin A):] : b₁ `1 misses b<sub>1</sub> `2 } is set
Fin (A) is non empty cup-closed diff-closed preBoolean set
Z is Element of (A)
z is finite Element of Fin (A)
(A,z) is Element of (A)
(A) is non empty Element of bool (Fin (A))
bool (Fin (A)) is non empty cup-closed diff-closed preBoolean set
{ b₁ where b₁ is finite Element of Fin (A) : for b₂, b₃ being Element of (A) holds
( not b₂ in b₁ or not b₃ in b₁ or not ( Fin A, Fin A,b₂,b₃) or b₂ = b₃ ) } is set
{ b₁ where b₁ is Element of (A) : for b₂ being Element of (A) holds
( ( not b₂ in z or not ( Fin A, Fin A,b₂,b₁) or b₂ = b₁ ) & ( not b₂ = b₁ or ( b₂ in z & ( Fin A, Fin A,b₂,b₁) ) ) ) } is set
u is Element of (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 -defined Fin A -valued non empty Element of bool [:(Fin A),(Fin A):]
bool [:(Fin A),(Fin A):] is non empty cup-closed diff-closed preBoolean set
{ b₁ where b₁ is Element of [:(Fin A),(Fin A):] : b₁ `1 misses b<sub>1</sub> `2 } is set
Fin (A) is non empty cup-closed diff-closed preBoolean set
Z is Element of (A)
u is finite Element of Fin (A)
(A,u) is Element of (A)
(A) is non empty Element of bool (Fin (A))
bool (Fin (A)) is non empty cup-closed diff-closed preBoolean set
{ b₁ where b₁ is finite Element of Fin (A) : for b₂, b₃ being Element of (A) holds
( not b₂ in b₁ or not b₃ in b₁ or not ( Fin A, Fin A,b₂,b₃) or b₂ = b₃ ) } is set
{ b₁ where b₁ is Element of (A) : for b₂ being Element of (A) holds
( ( not b₂ in u or not ( Fin A, Fin A,b₂,b₁) or b₂ = b₁ ) & ( not b₂ = b₁ or ( b₂ in u & ( Fin A, Fin A,b₂,b₁) ) ) ) } is set
z is Element of (A)
u9 is Element of (A)
A is non empty set
bool A is non empty cup-closed diff-closed preBoolean set
Z is non empty Element of bool A
[:Z,Z:] is Relation-like non empty set
[:[:Z,Z:],Z:] is Relation-like non empty set
bool [:[:Z,Z:],Z:] is non empty cup-closed diff-closed preBoolean set
u is Relation-like [:Z,Z:] -defined Z -valued V6() non empty V14([:Z,Z:]) V18([:Z,Z:],Z) Element of bool [:[:Z,Z:],Z:]
z is Element of Z
u9 is Element of Z
u . (z,u9) is set
[z,u9] is V15() set
{z,u9} is set
{z} is set
{{z,u9},{z}} is set
K11(u,[z,u9]) is set
u . (z,u9) is Element of Z
A is set
(A) is Relation-like Fin A -defined Fin A -valued non empty Element of bool [:(Fin A),(Fin A):]
Fin A is non empty cup-closed diff-closed preBoolean set
[:(Fin A),(Fin A):] is Relation-like non empty set
bool [:(Fin A),(Fin A):] is non empty cup-closed diff-closed preBoolean set
{ b₁ where b₁ is Element of [:(Fin A),(Fin A):] : b₁ `1 misses b<sub>1</sub> `2 } is set
Fin (A) is non empty cup-closed diff-closed preBoolean set
Z is finite Element of Fin (A)
u is finite Element of Fin (A)
z is set
A is set
(A) is Relation-like Fin A -defined Fin A -valued non empty Element of bool [:(Fin A),(Fin A):]
Fin A is non empty cup-closed diff-closed preBoolean set
[:(Fin A),(Fin A):] is Relation-like non empty set
bool [:(Fin A),(Fin A):] is non empty cup-closed diff-closed preBoolean set
{ b₁ where b₁ is Element of [:(Fin A),(Fin A):] : b₁ `1 misses b<sub>1</sub> `2 } is set
Fin (A) is non empty cup-closed diff-closed preBoolean set
Z is finite Element of Fin (A)
(A,Z) is Element of (A)
(A) is non empty Element of bool (Fin (A))
bool (Fin (A)) is non empty cup-closed diff-closed preBoolean set
{ b₁ where b₁ is finite Element of Fin (A) : for b₂, b₃ being Element of (A) holds
( not b₂ in b₁ or not b₃ in b₁ or not ( Fin A, Fin A,b₂,b₃) or b₂ = b₃ ) } is set
{ b₁ where b₁ is Element of (A) : for b₂ being Element of (A) holds
( ( not b₂ in Z or not ( Fin A, Fin A,b₂,b₁) or b₂ = b₁ ) & ( not b₂ = b₁ or ( b₂ in Z & ( Fin A, Fin A,b₂,b₁) ) ) ) } is set
u is Element of (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 -defined Fin A -valued non empty Element of bool [:(Fin A),(Fin A):]
bool [:(Fin A),(Fin A):] is non empty cup-closed diff-closed preBoolean set
{ b₁ where b₁ is Element of [:(Fin A),(Fin A):] : b₁ `1 misses b<sub>1</sub> `2 } is set
Fin (A) is non empty cup-closed diff-closed preBoolean set
Z is Element of (A)
u is finite Element of Fin (A)
(A,u) is Element of (A)
(A) is non empty Element of bool (Fin (A))
bool (Fin (A)) is non empty cup-closed diff-closed preBoolean set
{ b₁ where b₁ is finite Element of Fin (A) : for b₂, b₃ being Element of (A) holds
( not b₂ in b₁ or not b₃ in b₁ or not ( Fin A, Fin A,b₂,b₃) or b₂ = b₃ ) } is set
{ b₁ where b₁ is Element of (A) : for b₂ being Element of (A) holds
( ( not b₂ in u or not ( Fin A, Fin A,b₂,b₁) or b₂ = b₁ ) & ( not b₂ = b₁ or ( b₂ in u & ( Fin A, Fin A,b₂,b₁) ) ) ) } is set
z is Element of (A)
z is Element of (A)
u9 is Element of (A)
K is Element of (A)
z is Element of (A)
u9 is Element of (A)
A is set
(A) is Relation-like Fin A -defined Fin A -valued non empty Element of bool [:(Fin A),(Fin A):]
Fin A is non empty cup-closed diff-closed preBoolean set
[:(Fin A),(Fin A):] is Relation-like non empty set
bool [:(Fin A),(Fin A):] is non empty cup-closed diff-closed preBoolean set
{ b₁ where b₁ is Element of [:(Fin A),(Fin A):] : b₁ `1 misses b<sub>1</sub> `2 } is set
Fin (A) is non empty cup-closed diff-closed preBoolean set
(A) is non empty Element of bool (Fin (A))
bool (Fin (A)) is non empty cup-closed diff-closed preBoolean set
{ b₁ where b₁ is finite Element of Fin (A) : for b₂, b₃ being Element of (A) holds
( not b₂ in b₁ or not b₃ in b₁ or not ( Fin A, Fin A,b₂,b₃) or b₂ = b₃ ) } is set
Z is Element of (A)
(A,Z) is Element of (A)
{ b₁ where b₁ is Element of (A) : for b₂ being Element of (A) holds
( ( not b₂ in Z or not ( Fin A, Fin A,b₂,b₁) or b₂ = b₁ ) & ( not b₂ = b₁ or ( b₂ in Z & ( Fin A, Fin A,b₂,b₁) ) ) ) } is set
u is Element of (A)
z is Element of (A)
A is set
(A) is Relation-like Fin A -defined Fin A -valued non empty Element of bool [:(Fin A),(Fin A):]
Fin A is non empty cup-closed diff-closed preBoolean set
[:(Fin A),(Fin A):] is Relation-like non empty set
bool [:(Fin A),(Fin A):] is non empty cup-closed diff-closed preBoolean set
{ b₁ where b₁ is Element of [:(Fin A),(Fin A):] : b₁ `1 misses b<sub>1</sub> `2 } is set
Fin (A) is non empty cup-closed diff-closed preBoolean set
Z is finite Element of Fin (A)
(A,Z) is Element of (A)
(A) is non empty Element of bool (Fin (A))
bool (Fin (A)) is non empty cup-closed diff-closed preBoolean set
{ b₁ where b₁ is finite Element of Fin (A) : for b₂, b₃ being Element of (A) holds
( not b₂ in b₁ or not b₃ in b₁ or not ( Fin A, Fin A,b₂,b₃) or b₂ = b₃ ) } is set
{ b₁ where b₁ is Element of (A) : for b₂ being Element of (A) holds
( ( not b₂ in Z or not ( Fin A, Fin A,b₂,b₁) or b₂ = b₁ ) & ( not b₂ = b₁ or ( b₂ in Z & ( Fin A, Fin A,b₂,b₁) ) ) ) } is set
u is finite Element of Fin (A)
Z \/ u is finite Element of Fin (A)
(A,(Z \/ u)) is Element of (A)
{ b₁ where b₁ is Element of (A) : for b₂ being Element of (A) holds
( ( not b₂ in Z \/ u or not ( Fin A, Fin A,b₂,b₁) or b₂ = b₁ ) & ( not b₂ = b₁ or ( b₂ in Z \/ u & ( Fin A, Fin A,b₂,b₁) ) ) ) } is set
(A,Z) \/ u is finite Element of Fin (A)
z is Element of (A)
u9 is Element of (A)
A is set
(A) is Relation-like Fin A -defined Fin A -valued non empty Element of bool [:(Fin A),(Fin A):]
Fin A is non empty cup-closed diff-closed preBoolean set
[:(Fin A),(Fin A):] is Relation-like non empty set
bool [:(Fin A),(Fin A):] is non empty cup-closed diff-closed preBoolean set
{ b₁ where b₁ is Element of [:(Fin A),(Fin A):] : b₁ `1 misses b<sub>1</sub> `2 } is set
Fin (A) is non empty cup-closed diff-closed preBoolean set
Z is finite Element of Fin (A)
(A,Z) is Element of (A)
(A) is non empty Element of bool (Fin (A))
bool (Fin (A)) is non empty cup-closed diff-closed preBoolean set
{ b₁ where b₁ is finite Element of Fin (A) : for b₂, b₃ being Element of (A) holds
( not b₂ in b₁ or not b₃ in b₁ or not ( Fin A, Fin A,b₂,b₃) or b₂ = b₃ ) } is set
{ b₁ where b₁ is Element of (A) : for b₂ being Element of (A) holds
( ( not b₂ in Z or not ( Fin A, Fin A,b₂,b₁) or b₂ = b₁ ) & ( not b₂ = b₁ or ( b₂ in Z & ( Fin A, Fin A,b₂,b₁) ) ) ) } is set
u is finite Element of Fin (A)
(A,Z) \/ u is finite Element of Fin (A)
(A,((A,Z) \/ u)) is Element of (A)
{ b₁ where b₁ is Element of (A) : for b₂ being Element of (A) holds
( ( not b₂ in (A,Z) \/ u or not ( Fin A, Fin A,b₂,b₁) or b₂ = b₁ ) & ( not b₂ = b₁ or ( b₂ in (A,Z) \/ u & ( Fin A, Fin A,b₂,b₁) ) ) ) } is set
Z \/ u is finite Element of Fin (A)
(A,(Z \/ u)) is Element of (A)
{ b₁ where b₁ is Element of (A) : for b₂ being Element of (A) holds
( ( not b₂ in Z \/ u or not ( Fin A, Fin A,b₂,b₁) or b₂ = b₁ ) & ( not b₂ = b₁ or ( b₂ in Z \/ u & ( Fin A, Fin A,b₂,b₁) ) ) ) } is set
z is Element of (A)
u9 is Element of (A)
K is Element of (A)
z is Element of (A)
u9 is Element of (A)
A is set
(A) is Relation-like Fin A -defined Fin A -valued non empty Element of bool [:(Fin A),(Fin A):]
Fin A is non empty cup-closed diff-closed preBoolean set
[:(Fin A),(Fin A):] is Relation-like non empty set
bool [:(Fin A),(Fin A):] is non empty cup-closed diff-closed preBoolean set
{ b₁ where b₁ is Element of [:(Fin A),(Fin A):] : b₁ `1 misses b<sub>1</sub> `2 } is set
Fin (A) is non empty cup-closed diff-closed preBoolean set
Z is finite Element of Fin (A)
u is finite Element of Fin (A)
(A,u) is Element of (A)
(A) is non empty Element of bool (Fin (A))
bool (Fin (A)) is non empty cup-closed diff-closed preBoolean set
{ b₁ where b₁ is finite Element of Fin (A) : for b₂, b₃ being Element of (A) holds
( not b₂ in b₁ or not b₃ in b₁ or not ( Fin A, Fin A,b₂,b₃) or b₂ = b₃ ) } is set
{ b₁ where b₁ is Element of (A) : for b₂ being Element of (A) holds
( ( not b₂ in u or not ( Fin A, Fin A,b₂,b₁) or b₂ = b₁ ) & ( not b₂ = b₁ or ( b₂ in u & ( Fin A, Fin A,b₂,b₁) ) ) ) } is set
Z \/ (A,u) is finite Element of Fin (A)
(A,(Z \/ (A,u))) is Element of (A)
{ b₁ where b₁ is Element of (A) : for b₂ being Element of (A) holds
( ( not b₂ in Z \/ (A,u) or not ( Fin A, Fin A,b₂,b₁) or b₂ = b₁ ) & ( not b₂ = b₁ or ( b₂ in Z \/ (A,u) & ( Fin A, Fin A,b₂,b₁) ) ) ) } is set
Z \/ u is finite Element of Fin (A)
(A,(Z \/ u)) is Element of (A)
{ b₁ where b₁ is Element of (A) : for b₂ being Element of (A) holds
( ( not b₂ in Z \/ u or not ( Fin A, Fin A,b₂,b₁) or b₂ = b₁ ) & ( not b₂ = b₁ or ( b₂ in Z \/ u & ( Fin A, Fin A,b₂,b₁) ) ) ) } is set
A is set
(A) is Relation-like Fin A -defined Fin A -valued non empty Element of bool [:(Fin A),(Fin A):]
Fin A is non empty cup-closed diff-closed preBoolean set
[:(Fin A),(Fin A):] is Relation-like non empty set
bool [:(Fin A),(Fin A):] is non empty cup-closed diff-closed preBoolean set
{ b₁ where b₁ is Element of [:(Fin A),(Fin A):] : b₁ `1 misses b<sub>1</sub> `2 } is set
Fin (A) is non empty cup-closed diff-closed preBoolean set
Z is finite Element of Fin (A)
u is finite Element of Fin (A)
z is finite Element of Fin (A)
(A,Z,z) is finite Element of Fin (A)
{ ((Fin A),(Fin A),b₁,b₂) where b₁, b₂ is Element of (A) : ( b₁ in Z & b₂ in z ) } is set
(A) /\ { ((Fin A),(Fin A),b₁,b₂) where b₁, b₂ is Element of (A) : ( b₁ in Z & b₂ in z ) } is Relation-like Fin A -defined Fin A -valued Element of bool [:(Fin A),(Fin A):]
(A,u,z) is finite Element of Fin (A)
{ ((Fin A),(Fin A),b₁,b₂) where b₁, b₂ is Element of (A) : ( b₁ in u & b₂ in z ) } is set
(A) /\ { ((Fin A),(Fin A),b₁,b₂) where b₁, b₂ is Element of (A) : ( b₁ in u & b₂ in z ) } is Relation-like Fin A -defined Fin A -valued Element of bool [:(Fin A),(Fin A):]
{ H₁(b₁,b₂) where b₁, b₂ is Element of (A) : S₁[b₁,b₂] } is set
{ H₁(b₁,b₂) where b₁, b₂ is Element of (A) : S₂[b₁,b₂] } is set
L is Element of (A)
M is Element of (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 -defined Fin A -valued non empty Element of bool [:(Fin A),(Fin A):]
bool [:(Fin A),(Fin A):] is non empty cup-closed diff-closed preBoolean set
{ b₁ where b₁ is Element of [:(Fin A),(Fin A):] : b₁ `1 misses b<sub>1</sub> `2 } is set
Fin (A) is non empty cup-closed diff-closed preBoolean set
Z is Element of (A)
u is finite Element of Fin (A)
(A,u) is Element of (A)
(A) is non empty Element of bool (Fin (A))
bool (Fin (A)) is non empty cup-closed diff-closed preBoolean set
{ b₁ where b₁ is finite Element of Fin (A) : for b₂, b₃ being Element of (A) holds
( not b₂ in b₁ or not b₃ in b₁ or not ( Fin A, Fin A,b₂,b₃) or b₂ = b₃ ) } is set
{ b₁ where b₁ is Element of (A) : for b₂ being Element of (A) holds
( ( not b₂ in u or not ( Fin A, Fin A,b₂,b₁) or b₂ = b₁ ) & ( not b₂ = b₁ or ( b₂ in u & ( Fin A, Fin A,b₂,b₁) ) ) ) } is set
z is finite Element of Fin (A)
(A,u,z) is finite Element of Fin (A)
{ ((Fin A),(Fin A),b₁,b₂) where b₁, b₂ is Element of (A) : ( b₁ in u & b₂ in z ) } is set
(A) /\ { ((Fin A),(Fin A),b₁,b₂) where b₁, b₂ is Element of (A) : ( b₁ in u & b₂ in z ) } is Relation-like Fin A -defined Fin A -valued Element of bool [:(Fin A),(Fin A):]
(A,(A,u),z) is finite Element of Fin (A)
{ ((Fin A),(Fin A),b₁,b₂) where b₁, b₂ is Element of (A) : ( b₁ in (A,u) & b₂ in z ) } is set
(A) /\ { ((Fin A),(Fin A),b₁,b₂) where b₁, b₂ is Element of (A) : ( b₁ in (A,u) & b₂ in z ) } is Relation-like Fin A -defined Fin A -valued Element of bool [:(Fin A),(Fin A):]
u9 is Element of (A)
K is Element of (A)
((Fin A),(Fin A),u9,K) is Element of [:(Fin A),(Fin A):]
u9 `1 is finite Element of Fin A
K `1 is finite Element of Fin A
(u9 `1) \/ (K `1) is finite Element of Fin A
u9 `2 is finite Element of Fin A
K `2 is finite Element of Fin A
(u9 `2) \/ (K `2) is finite Element of Fin A
[((u9 `1) \/ (K `1)),((u9 `2) \/ (K `2))] is V15() Element of [:(Fin A),(Fin A):]
{((u9 `1) \/ (K `1)),((u9 `2) \/ (K `2))} is set
{((u9 `1) \/ (K `1))} is set
{{((u9 `1) \/ (K `1)),((u9 `2) \/ (K `2))},{((u9 `1) \/ (K `1))}} is set
L is Element of (A)
((Fin A),(Fin A),L,K) is Element of [:(Fin A),(Fin A):]
L `1 is finite Element of Fin A
(L `1) \/ (K `1) is finite Element of Fin A
L `2 is finite Element of Fin A
(L `2) \/ (K `2) is finite Element of Fin A
[((L `1) \/ (K `1)),((L `2) \/ (K `2))] is V15() Element of [:(Fin A),(Fin A):]
{((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
M is Element of (A)
A is set
(A) is Relation-like Fin A -defined Fin A -valued non empty Element of bool [:(Fin A),(Fin A):]
Fin A is non empty cup-closed diff-closed preBoolean set
[:(Fin A),(Fin A):] is Relation-like non empty set
bool [:(Fin A),(Fin A):] is non empty cup-closed diff-closed preBoolean set
{ b₁ where b₁ is Element of [:(Fin A),(Fin A):] : b₁ `1 misses b<sub>1</sub> `2 } is set
Fin (A) is non empty cup-closed diff-closed preBoolean set
Z is finite Element of Fin (A)
(A,Z) is Element of (A)
(A) is non empty Element of bool (Fin (A))
bool (Fin (A)) is non empty cup-closed diff-closed preBoolean set
{ b₁ where b₁ is finite Element of Fin (A) : for b₂, b₃ being Element of (A) holds
( not b₂ in b₁ or not b₃ in b₁ or not ( Fin A, Fin A,b₂,b₃) or b₂ = b₃ ) } is set
{ b₁ where b₁ is Element of (A) : for b₂ being Element of (A) holds
( ( not b₂ in Z or not ( Fin A, Fin A,b₂,b₁) or b₂ = b₁ ) & ( not b₂ = b₁ or ( b₂ in Z & ( Fin A, Fin A,b₂,b₁) ) ) ) } is set
u is finite Element of Fin (A)
(A,Z,u) is finite Element of Fin (A)
{ ((Fin A),(Fin A),b₁,b₂) where b₁, b₂ is Element of (A) : ( b₁ in Z & b₂ in u ) } is set
(A) /\ { ((Fin A),(Fin A),b₁,b₂) where b₁, b₂ is Element of (A) : ( b₁ in Z & b₂ in u ) } is Relation-like Fin A -defined Fin A -valued Element of bool [:(Fin A),(Fin A):]
(A,(A,Z,u)) is Element of (A)
{ b₁ where b₁ is Element of (A) : for b₂ being Element of (A) holds
( ( not b₂ in (A,Z,u) or not ( Fin A, Fin A,b₂,b₁) or b₂ = b₁ ) & ( not b₂ = b₁ or ( b₂ in (A,Z,u) & ( Fin A, Fin A,b₂,b₁) ) ) ) } is set
(A,(A,Z),u) is finite Element of Fin (A)
{ ((Fin A),(Fin A),b₁,b₂) where b₁, b₂ is Element of (A) : ( b₁ in (A,Z) & b₂ in u ) } is set
(A) /\ { ((Fin A),(Fin A),b₁,b₂) where b₁, b₂ is Element of (A) : ( b₁ in (A,Z) & b₂ in u ) } is Relation-like Fin A -defined Fin A -valued Element of bool [:(Fin A),(Fin A):]
z is Element of (A)
u9 is Element of (A)
A is set
(A) is Relation-like Fin A -defined Fin A -valued non empty Element of bool [:(Fin A),(Fin A):]
Fin A is non empty cup-closed diff-closed preBoolean set
[:(Fin A),(Fin A):] is Relation-like non empty set
bool [:(Fin A),(Fin A):] is non empty cup-closed diff-closed preBoolean set
{ b₁ where b₁ is Element of [:(Fin A),(Fin A):] : b₁ `1 misses b<sub>1</sub> `2 } is set
Fin (A) is non empty cup-closed diff-closed preBoolean set
Z is finite Element of Fin (A)
u is finite Element of Fin (A)
(A,Z,u) is finite Element of Fin (A)
{ ((Fin A),(Fin A),b₁,b₂) where b₁, b₂ is Element of (A) : ( b₁ in Z & b₂ in u ) } is set
(A) /\ { ((Fin A),(Fin A),b₁,b₂) where b₁, b₂ is Element of (A) : ( b₁ in Z & b₂ in u ) } is Relation-like Fin A -defined Fin A -valued Element of bool [:(Fin A),(Fin A):]
(A,u,Z) is finite Element of Fin (A)
{ ((Fin A),(Fin A),b₁,b₂) where b₁, b₂ is Element of (A) : ( b₁ in u & b₂ in Z ) } is set
(A) /\ { ((Fin A),(Fin A),b₁,b₂) where b₁, b₂ is Element of (A) : ( b₁ in u & b₂ in Z ) } is Relation-like Fin A -defined Fin A -valued Element of bool [:(Fin A),(Fin A):]
{ H₁(b₁,b₂) where b₁, b₂ is Element of (A) : S₁[b₁,b₂] } is set
{ H₁(b₂,b₁) where b₁, b₂ is Element of (A) : S₂[b₁,b₂] } is set
K is Element of (A)
L is Element of (A)
((Fin A),(Fin A),K,L) is Element of [:(Fin A),(Fin A):]
K `1 is finite Element of Fin A
L `1 is finite Element of Fin A
(K `1) \/ (L `1) is finite Element of Fin A
K `2 is finite Element of Fin A
L `2 is finite Element of Fin A
(K `2) \/ (L `2) is finite Element of Fin A
[((K `1) \/ (L `1)),((K `2) \/ (L `2))] is V15() Element of [:(Fin A),(Fin A):]
{((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
((Fin A),(Fin A),L,K) is Element of [:(Fin A),(Fin A):]
(L `1) \/ (K `1) is finite Element of Fin A
(L `2) \/ (K `2) is finite Element of Fin A
[((L `1) \/ (K `1)),((L `2) \/ (K `2))] is V15() Element of [:(Fin A),(Fin A):]
{((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
K is set
M is Element of (A)
L is Element of (A)
((Fin A),(Fin A),M,L) is Element of [:(Fin A),(Fin A):]
M `1 is finite Element of Fin A
L `1 is finite Element of Fin A
(M `1) \/ (L `1) is finite Element of Fin A
M `2 is finite Element of Fin A
L `2 is finite Element of Fin A
(M `2) \/ (L `2) is finite Element of Fin A
[((M `1) \/ (L `1)),((M `2) \/ (L `2))] is V15() Element of [:(Fin A),(Fin A):]
{((M `1) \/ (L `1)),((M `2) \/ (L `2))} is set
{((M `1) \/ (L `1))} is set
{{((M `1) \/ (L `1)),((M `2) \/ (L `2))},{((M `1) \/ (L `1))}} is set
L is Element of (A)
M is Element of (A)
((Fin A),(Fin A),L,M) is Element of [:(Fin A),(Fin A):]
L `1 is finite Element of Fin A
M `1 is finite Element of Fin A
(L `1) \/ (M `1) is finite Element of Fin A
L `2 is finite Element of Fin A
M `2 is finite Element of Fin A
(L `2) \/ (M `2) is finite Element of Fin A
[((L `1) \/ (M `1)),((L `2) \/ (M `2))] is V15() Element of [:(Fin A),(Fin A):]
{((L `1) \/ (M `1)),((L `2) \/ (M `2))} is set
{((L `1) \/ (M `1))} is set
{{((L `1) \/ (M `1)),((L `2) \/ (M `2))},{((L `1) \/ (M `1))}} is set
y is Element of (A)
x is Element of (A)
((Fin A),(Fin A),y,x) is Element of [:(Fin A),(Fin A):]
y `1 is finite Element of Fin A
x `1 is finite Element of Fin A
(y `1) \/ (x `1) is finite Element of Fin A
y `2 is finite Element of Fin A
x `2 is finite Element of Fin A
(y `2) \/ (x `2) is finite Element of Fin A
[((y `1) \/ (x `1)),((y `2) \/ (x `2))] is V15() Element of [:(Fin A),(Fin A):]
{((y `1) \/ (x `1)),((y `2) \/ (x `2))} is set
{((y `1) \/ (x `1))} is set
{{((y `1) \/ (x `1)),((y `2) \/ (x `2))},{((y `1) \/ (x `1))}} is set
L is Element of (A)
M is Element of (A)
((Fin A),(Fin A),L,M) is Element of [:(Fin A),(Fin A):]
L `1 is finite Element of Fin A
M `1 is finite Element of Fin A
(L `1) \/ (M `1) is finite Element of Fin A
L `2 is finite Element of Fin A
M `2 is finite Element of Fin A
(L `2) \/ (M `2) is finite Element of Fin A
[((L `1) \/ (M `1)),((L `2) \/ (M `2))] is V15() Element of [:(Fin A),(Fin A):]
{((L `1) \/ (M `1)),((L `2) \/ (M `2))} is set
{((L `1) \/ (M `1))} is set
{{((L `1) \/ (M `1)),((L `2) \/ (M `2))},{((L `1) \/ (M `1))}} is set
K is Element of (A)
L is Element of (A)
x is Element of (A)
M is Element of (A)
A is set
(A) is Relation-like Fin A -defined Fin A -valued non empty Element of bool [:(Fin A),(Fin A):]
Fin A is non empty cup-closed diff-closed preBoolean set
[:(Fin A),(Fin A):] is Relation-like non empty set
bool [:(Fin A),(Fin A):] is non empty cup-closed diff-closed preBoolean set
{ b₁ where b₁ is Element of [:(Fin A),(Fin A):] : b₁ `1 misses b<sub>1</sub> `2 } is set
Fin (A) is non empty cup-closed diff-closed preBoolean set
Z is finite Element of Fin (A)
u is finite Element of Fin (A)
z is finite Element of Fin (A)
(A,z,Z) is finite Element of Fin (A)
{ ((Fin A),(Fin A),b₁,b₂) where b₁, b₂ is Element of (A) : ( b₁ in z & b₂ in Z ) } is set
(A) /\ { ((Fin A),(Fin A),b₁,b₂) where b₁, b₂ is Element of (A) : ( b₁ in z & b₂ in Z ) } is Relation-like Fin A -defined Fin A -valued Element of bool [:(Fin A),(Fin A):]
(A,z,u) is finite Element of Fin (A)
{ ((Fin A),(Fin A),b₁,b₂) where b₁, b₂ is Element of (A) : ( b₁ in z & b₂ in u ) } is set
(A) /\ { ((Fin A),(Fin A),b₁,b₂) where b₁, b₂ is Element of (A) : ( b₁ in z & b₂ in u ) } is Relation-like Fin A -defined Fin A -valued Element of bool [:(Fin A),(Fin A):]
(A,u,z) is finite Element of Fin (A)
{ ((Fin A),(Fin A),b₁,b₂) where b₁, b₂ is Element of (A) : ( b₁ in u & b₂ in z ) } is set
(A) /\ { ((Fin A),(Fin A),b₁,b₂) where b₁, b₂ is Element of (A) : ( b₁ in u & b₂ in z ) } is Relation-like Fin A -defined Fin A -valued Element of bool [:(Fin A),(Fin A):]
(A,Z,z) is finite Element of Fin (A)
{ ((Fin A),(Fin A),b₁,b₂) where b₁, b₂ is Element of (A) : ( b₁ in Z & b₂ in z ) } is set
(A) /\ { ((Fin A),(Fin A),b₁,b₂) where b₁, b₂ is Element of (A) : ( b₁ in Z & b₂ in z ) } is Relation-like Fin A -defined Fin A -valued Element of bool [:(Fin A),(Fin A):]
A is set
(A) is Relation-like Fin A -defined Fin A -valued non empty Element of bool [:(Fin A),(Fin A):]
Fin A is non empty cup-closed diff-closed preBoolean set
[:(Fin A),(Fin A):] is Relation-like non empty set
bool [:(Fin A),(Fin A):] is non empty cup-closed diff-closed preBoolean set
{ b₁ where b₁ is Element of [:(Fin A),(Fin A):] : b₁ `1 misses b<sub>1</sub> `2 } is set
Fin (A) is non empty cup-closed diff-closed preBoolean set
Z is finite Element of Fin (A)
(A,Z) is Element of (A)
(A) is non empty Element of bool (Fin (A))
bool (Fin (A)) is non empty cup-closed diff-closed preBoolean set
{ b₁ where b₁ is finite Element of Fin (A) : for b₂, b₃ being Element of (A) holds
( not b₂ in b₁ or not b₃ in b₁ or not ( Fin A, Fin A,b₂,b₃) or b₂ = b₃ ) } is set
{ b₁ where b₁ is Element of (A) : for b₂ being Element of (A) holds
( ( not b₂ in Z or not ( Fin A, Fin A,b₂,b₁) or b₂ = b₁ ) & ( not b₂ = b₁ or ( b₂ in Z & ( Fin A, Fin A,b₂,b₁) ) ) ) } is set
u is finite Element of Fin (A)
(A,(A,Z),u) is finite Element of Fin (A)
{ ((Fin A),(Fin A),b₁,b₂) where b₁, b₂ is Element of (A) : ( b₁ in (A,Z) & b₂ in u ) } is set
(A) /\ { ((Fin A),(Fin A),b₁,b₂) where b₁, b₂ is Element of (A) : ( b₁ in (A,Z) & b₂ in u ) } is Relation-like Fin A -defined Fin A -valued Element of bool [:(Fin A),(Fin A):]
(A,(A,(A,Z),u)) is Element of (A)
{ b₁ where b₁ is Element of (A) : for b₂ being Element of (A) holds
( ( not b₂ in (A,(A,Z),u) or not ( Fin A, Fin A,b₂,b₁) or b₂ = b₁ ) & ( not b₂ = b₁ or ( b₂ in (A,(A,Z),u) & ( Fin A, Fin A,b₂,b₁) ) ) ) } is set
(A,Z,u) is finite Element of Fin (A)
{ ((Fin A),(Fin A),b₁,b₂) where b₁, b₂ is Element of (A) : ( b₁ in Z & b₂ in u ) } is set
(A) /\ { ((Fin A),(Fin A),b₁,b₂) where b₁, b₂ is Element of (A) : ( b₁ in Z & b₂ in u ) } is Relation-like Fin A -defined Fin A -valued Element of bool [:(Fin A),(Fin A):]
(A,(A,Z,u)) is Element of (A)
{ b₁ where b₁ is Element of (A) : for b₂ being Element of (A) holds
( ( not b₂ in (A,Z,u) or not ( Fin A, Fin A,b₂,b₁) or b₂ = b₁ ) & ( not b₂ = b₁ or ( b₂ in (A,Z,u) & ( Fin A, Fin A,b₂,b₁) ) ) ) } is set
z is Element of (A)
u9 is Element of (A)
K is Element of (A)
z is Element of (A)
u9 is Element of (A)
A is set
(A) is Relation-like Fin A -defined Fin A -valued non empty Element of bool [:(Fin A),(Fin A):]
Fin A is non empty cup-closed diff-closed preBoolean set
[:(Fin A),(Fin A):] is Relation-like non empty set
bool [:(Fin A),(Fin A):] is non empty cup-closed diff-closed preBoolean set
{ b₁ where b₁ is Element of [:(Fin A),(Fin A):] : b₁ `1 misses b<sub>1</sub> `2 } is set
Fin (A) is non empty cup-closed diff-closed preBoolean set
Z is finite Element of Fin (A)
u is finite Element of Fin (A)
(A,u) is Element of (A)
(A) is non empty Element of bool (Fin (A))
bool (Fin (A)) is non empty cup-closed diff-closed preBoolean set
{ b₁ where b₁ is finite Element of Fin (A) : for b₂, b₃ being Element of (A) holds
( not b₂ in b₁ or not b₃ in b₁ or not ( Fin A, Fin A,b₂,b₃) or b₂ = b₃ ) } is set
{ b₁ where b₁ is Element of (A) : for b₂ being Element of (A) holds
( ( not b₂ in u or not ( Fin A, Fin A,b₂,b₁) or b₂ = b₁ ) & ( not b₂ = b₁ or ( b₂ in u & ( Fin A, Fin A,b₂,b₁) ) ) ) } is set
(A,Z,(A,u)) is finite Element of Fin (A)
{ ((Fin A),(Fin A),b₁,b₂) where b₁, b₂ is Element of (A) : ( b₁ in Z & b₂ in (A,u) ) } is set
(A) /\ { ((Fin A),(Fin A),b₁,b₂) where b₁, b₂ is Element of (A) : ( b₁ in Z & b₂ in (A,u) ) } is Relation-like Fin A -defined Fin A -valued Element of bool [:(Fin A),(Fin A):]
(A,(A,Z,(A,u))) is Element of (A)
{ b₁ where b₁ is Element of (A) : for b₂ being Element of (A) holds
( ( not b₂ in (A,Z,(A,u)) or not ( Fin A, Fin A,b₂,b₁) or b₂ = b₁ ) & ( not b₂ = b₁ or ( b₂ in (A,Z,(A,u)) & ( Fin A, Fin A,b₂,b₁) ) ) ) } is set
(A,Z,u) is finite Element of Fin (A)
{ ((Fin A),(Fin A),b₁,b₂) where b₁, b₂ is Element of (A) : ( b₁ in Z & b₂ in u ) } is set
(A) /\ { ((Fin A),(Fin A),b₁,b₂) where b₁, b₂ is Element of (A) : ( b₁ in Z & b₂ in u ) } is Relation-like Fin A -defined Fin A -valued Element of bool [:(Fin A),(Fin A):]
(A,(A,Z,u)) is Element of (A)
{ b₁ where b₁ is Element of (A) : for b₂ being Element of (A) holds
( ( not b₂ in (A,Z,u) or not ( Fin A, Fin A,b₂,b₁) or b₂ = b₁ ) & ( not b₂ = b₁ or ( b₂ in (A,Z,u) & ( Fin A, Fin A,b₂,b₁) ) ) ) } is set
(A,(A,u),Z) is finite Element of Fin (A)
{ ((Fin A),(Fin A),b₁,b₂) where b₁, b₂ is Element of (A) : ( b₁ in (A,u) & b₂ in Z ) } is set
(A) /\ { ((Fin A),(Fin A),b₁,b₂) where b₁, b₂ is Element of (A) : ( b₁ in (A,u) & b₂ in Z ) } is Relation-like Fin A -defined Fin A -valued Element of bool [:(Fin A),(Fin A):]
(A,u,Z) is finite Element of Fin (A)
{ ((Fin A),(Fin A),b₁,b₂) where b₁, b₂ is Element of (A) : ( b₁ in u & b₂ in Z ) } is set
(A) /\ { ((Fin A),(Fin A),b₁,b₂) where b₁, b₂ is Element of (A) : ( b₁ in u & b₂ in Z ) } is Relation-like Fin A -defined Fin A -valued Element of bool [:(Fin A),(Fin A):]
A is set
(A) is Relation-like Fin A -defined Fin A -valued non empty Element of bool [:(Fin A),(Fin A):]
Fin A is non empty cup-closed diff-closed preBoolean set
[:(Fin A),(Fin A):] is Relation-like non empty set
bool [:(Fin A),(Fin A):] is non empty cup-closed diff-closed preBoolean set
{ b₁ where b₁ is Element of [:(Fin A),(Fin A):] : b₁ `1 misses b<sub>1</sub> `2 } is set
Fin (A) is non empty cup-closed diff-closed preBoolean set
(A) is non empty Element of bool (Fin (A))
bool (Fin (A)) is non empty cup-closed diff-closed preBoolean set
{ b₁ where b₁ is finite Element of Fin (A) : for b₂, b₃ being Element of (A) holds
( not b₂ in b₁ or not b₃ in b₁ or not ( Fin A, Fin A,b₂,b₃) or b₂ = b₃ ) } is set
Z is Element of (A)
u is Element of (A)
(A,Z,u) is finite Element of Fin (A)
{ ((Fin A),(Fin A),b₁,b₂) where b₁, b₂ is Element of (A) : ( b₁ in Z & b₂ in u ) } is set
(A) /\ { ((Fin A),(Fin A),b₁,b₂) where b₁, b₂ is Element of (A) : ( b₁ in Z & b₂ in u ) } is Relation-like Fin A -defined Fin A -valued Element of bool [:(Fin A),(Fin A):]
z is Element of (A)
(A,u,z) is finite Element of Fin (A)
{ ((Fin A),(Fin A),b₁,b₂) where b₁, b₂ is Element of (A) : ( b₁ in u & b₂ in z ) } is set
(A) /\ { ((Fin A),(Fin A),b₁,b₂) where b₁, b₂ is Element of (A) : ( b₁ in u & b₂ in z ) } is Relation-like Fin A -defined Fin A -valued Element of bool [:(Fin A),(Fin A):]
(A,Z,(A,u,z)) is finite Element of Fin (A)
{ ((Fin A),(Fin A),b₁,b₂) where b₁, b₂ is Element of (A) : ( b₁ in Z & b₂ in (A,u,z) ) } is set
(A) /\ { ((Fin A),(Fin A),b₁,b₂) where b₁, b₂ is Element of (A) : ( b₁ in Z & b₂ in (A,u,z) ) } is Relation-like Fin A -defined Fin A -valued Element of bool [:(Fin A),(Fin A):]
(A,(A,Z,u),z) is finite Element of Fin (A)
{ ((Fin A),(Fin A),b₁,b₂) where b₁, b₂ is Element of (A) : ( b₁ in (A,Z,u) & b₂ in z ) } is set
(A) /\ { ((Fin A),(Fin A),b₁,b₂) where b₁, b₂ is Element of (A) : ( b₁ in (A,Z,u) & b₂ in z ) } is Relation-like Fin A -defined Fin A -valued Element of bool [:(Fin A),(Fin A):]
(A,z,u) is finite Element of Fin (A)
{ ((Fin A),(Fin A),b₁,b₂) where b₁, b₂ is Element of (A) : ( b₁ in z & b₂ in u ) } is set
(A) /\ { ((Fin A),(Fin A),b₁,b₂) where b₁, b₂ is Element of (A) : ( b₁ in z & b₂ in u ) } is Relation-like Fin A -defined Fin A -valued Element of bool [:(Fin A),(Fin A):]
(A,u,Z) is finite Element of Fin (A)
{ ((Fin A),(Fin A),b₁,b₂) where b₁, b₂ is Element of (A) : ( b₁ in u & b₂ in Z ) } is set
(A) /\ { ((Fin A),(Fin A),b₁,b₂) where b₁, b₂ is Element of (A) : ( b₁ in u & b₂ in Z ) } is Relation-like Fin A -defined Fin A -valued Element of bool [:(Fin A),(Fin A):]
M is Element of (A)
u9 is Element of (A)
K is Element of (A)
L is Element of (A)
(A,K,L) is finite Element of Fin (A)
{ ((Fin A),(Fin A),b₁,b₂) where b₁, b₂ is Element of (A) : ( b₁ in K & b₂ in L ) } is set
(A) /\ { ((Fin A),(Fin A),b₁,b₂) where b₁, b₂ is Element of (A) : ( b₁ in K & b₂ in L ) } is Relation-like Fin A -defined Fin A -valued Element of bool [:(Fin A),(Fin A):]
(A,u9,(A,K,L)) is finite Element of Fin (A)
{ ((Fin A),(Fin A),b₁,b₂) where b₁, b₂ is Element of (A) : ( b₁ in u9 & b₂ in (A,K,L) ) } is set
(A) /\ { ((Fin A),(Fin A),b₁,b₂) where b₁, b₂ is Element of (A) : ( b₁ in u9 & b₂ in (A,K,L) ) } is Relation-like Fin A -defined Fin A -valued Element of bool [:(Fin A),(Fin A):]
x is Element of (A)
y is Element of (A)
((Fin A),(Fin A),x,y) is Element of [:(Fin A),(Fin A):]
x `1 is finite Element of Fin A
y `1 is finite Element of Fin A
(x `1) \/ (y `1) is finite Element of Fin A
x `2 is finite Element of Fin A
y `2 is finite Element of Fin A
(x `2) \/ (y `2) is finite Element of Fin A
[((x `1) \/ (y `1)),((x `2) \/ (y `2))] is V15() Element of [:(Fin A),(Fin A):]
{((x `1) \/ (y `1)),((x `2) \/ (y `2))} is set
{((x `1) \/ (y `1))} is set
{{((x `1) \/ (y `1)),((x `2) \/ (y `2))},{((x `1) \/ (y `1))}} is set
b1 is Element of (A)
c1 is Element of (A)
((Fin A),(Fin A),b1,c1) is Element of [:(Fin A),(Fin A):]
b1 `1 is finite Element of Fin A
c1 `1 is finite Element of Fin A
(b1 `1) \/ (c1 `1) is finite Element of Fin A
b1 `2 is finite Element of Fin A
c1 `2 is finite Element of Fin A
(b1 `2) \/ (c1 `2) is finite Element of Fin A
[((b1 `1) \/ (c1 `1)),((b1 `2) \/ (c1 `2))] is V15() Element of [:(Fin A),(Fin A):]
{((b1 `1) \/ (c1 `1)),((b1 `2) \/ (c1 `2))} is set
{((b1 `1) \/ (c1 `1))} is set
{{((b1 `1) \/ (c1 `1)),((b1 `2) \/ (c1 `2))},{((b1 `1) \/ (c1 `1))}} is set
((Fin A),(Fin A),x,((Fin A),(Fin A),b1,c1)) is Element of [:(Fin A),(Fin A):]
((Fin A),(Fin A),b1,c1) `1 is finite Element of Fin A
(x `1) \/ (((Fin A),(Fin A),b1,c1) `1) is finite Element of Fin A
((Fin A),(Fin A),b1,c1) `2 is finite Element of Fin A
(x `2) \/ (((Fin A),(Fin A),b1,c1) `2) is finite Element of Fin A
[((x `1) \/ (((Fin A),(Fin A),b1,c1) `1)),((x `2) \/ (((Fin A),(Fin A),b1,c1) `2))] is V15() Element of [:(Fin A),(Fin A):]
{((x `1) \/ (((Fin A),(Fin A),b1,c1) `1)),((x `2) \/ (((Fin A),(Fin A),b1,c1) `2))} is set
{((x `1) \/ (((Fin A),(Fin A),b1,c1) `1))} is set
{{((x `1) \/ (((Fin A),(Fin A),b1,c1) `1)),((x `2) \/ (((Fin A),(Fin A),b1,c1) `2))},{((x `1) \/ (((Fin A),(Fin A),b1,c1) `1))}} is set
((Fin A),(Fin A),x,b1) is Element of [:(Fin A),(Fin A):]
(x `1) \/ (b1 `1) is finite Element of Fin A
(x `2) \/ (b1 `2) is finite Element of Fin A
[((x `1) \/ (b1 `1)),((x `2) \/ (b1 `2))] is V15() Element of [:(Fin A),(Fin A):]
{((x `1) \/ (b1 `1)),((x `2) \/ (b1 `2))} is set
{((x `1) \/ (b1 `1))} is set
{{((x `1) \/ (b1 `1)),((x `2) \/ (b1 `2))},{((x `1) \/ (b1 `1))}} is set
((Fin A),(Fin A),((Fin A),(Fin A),x,b1),c1) is Element of [:(Fin A),(Fin A):]
((Fin A),(Fin A),x,b1) `1 is finite Element of Fin A
(((Fin A),(Fin A),x,b1) `1) \/ (c1 `1) is finite Element of Fin A
((Fin A),(Fin A),x,b1) `2 is finite Element of Fin A
(((Fin A),(Fin A),x,b1) `2) \/ (c1 `2) is finite Element of Fin A
[((((Fin A),(Fin A),x,b1) `1) \/ (c1 `1)),((((Fin A),(Fin A),x,b1) `2) \/ (c1 `2))] is V15() Element of [:(Fin A),(Fin A):]
{((((Fin A),(Fin A),x,b1) `1) \/ (c1 `1)),((((Fin A),(Fin A),x,b1) `2) \/ (c1 `2))} is set
{((((Fin A),(Fin A),x,b1) `1) \/ (c1 `1))} is set
{{((((Fin A),(Fin A),x,b1) `1) \/ (c1 `1)),((((Fin A),(Fin A),x,b1) `2) \/ (c1 `2))},{((((Fin A),(Fin A),x,b1) `1) \/ (c1 `1))}} is set
d is Element of (A)
c2 is Element of (A)
(A,u9,K) is finite Element of Fin (A)
{ ((Fin A),(Fin A),b₁,b₂) where b₁, b₂ is Element of (A) : ( b₁ in u9 & b₂ in K ) } is set
(A) /\ { ((Fin A),(Fin A),b₁,b₂) where b₁, b₂ is Element of (A) : ( b₁ in u9 & b₂ in K ) } is Relation-like Fin A -defined Fin A -valued Element of bool [:(Fin A),(Fin A):]
(A,(A,u9,K),L) is finite Element of Fin (A)
{ ((Fin A),(Fin A),b₁,b₂) where b₁, b₂ is Element of (A) : ( b₁ in (A,u9,K) & b₂ in L ) } is set
(A) /\ { ((Fin A),(Fin A),b₁,b₂) where b₁, b₂ is Element of (A) : ( b₁ in (A,u9,K) & b₂ in L ) } is Relation-like Fin A -defined Fin A -valued Element of bool [:(Fin A),(Fin A):]
(A,z,(A,Z,u)) is finite Element of Fin (A)
{ ((Fin A),(Fin A),b₁,b₂) where b₁, b₂ is Element of (A) : ( b₁ in z & b₂ in (A,Z,u) ) } is set
(A) /\ { ((Fin A),(Fin A),b₁,b₂) where b₁, b₂ is Element of (A) : ( b₁ in z & b₂ in (A,Z,u) ) } is Relation-like Fin A -defined Fin A -valued Element of bool [:(Fin A),(Fin A):]
(A,(A,u,z),Z) is finite Element of Fin (A)
{ ((Fin A),(Fin A),b₁,b₂) where b₁, b₂ is Element of (A) : ( b₁ in (A,u,z) & b₂ in Z ) } is set
(A) /\ { ((Fin A),(Fin A),b₁,b₂) where b₁, b₂ is Element of (A) : ( b₁ in (A,u,z) & b₂ in Z ) } is Relation-like Fin A -defined Fin A -valued Element of bool [:(Fin A),(Fin A):]
A is set
(A) is Relation-like Fin A -defined Fin A -valued non empty Element of bool [:(Fin A),(Fin A):]
Fin A is non empty cup-closed diff-closed preBoolean set
[:(Fin A),(Fin A):] is Relation-like non empty set
bool [:(Fin A),(Fin A):] is non empty cup-closed diff-closed preBoolean set
{ b₁ where b₁ is Element of [:(Fin A),(Fin A):] : b₁ `1 misses b<sub>1</sub> `2 } is set
Fin (A) is non empty cup-closed diff-closed preBoolean set
(A) is non empty Element of bool (Fin (A))
bool (Fin (A)) is non empty cup-closed diff-closed preBoolean set
{ b₁ where b₁ is finite Element of Fin (A) : for b₂, b₃ being Element of (A) holds
( not b₂ in b₁ or not b₃ in b₁ or not ( Fin A, Fin A,b₂,b₃) or b₂ = b₃ ) } is set
Z is Element of (A)
u is Element of (A)
(A,Z,u) is finite Element of Fin (A)
{ ((Fin A),(Fin A),b₁,b₂) where b₁, b₂ is Element of (A) : ( b₁ in Z & b₂ in u ) } is set
(A) /\ { ((Fin A),(Fin A),b₁,b₂) where b₁, b₂ is Element of (A) : ( b₁ in Z & b₂ in u ) } is Relation-like Fin A -defined Fin A -valued Element of bool [:(Fin A),(Fin A):]
z is Element of (A)
u \/ z is finite Element of Fin (A)
(A,Z,(u \/ z)) is finite Element of Fin (A)
{ ((Fin A),(Fin A),b₁,b₂) where b₁, b₂ is Element of (A) : ( b₁ in Z & b₂ in u \/ z ) } is set
(A) /\ { ((Fin A),(Fin A),b₁,b₂) where b₁, b₂ is Element of (A) : ( b₁ in Z & b₂ in u \/ z ) } is Relation-like Fin A -defined Fin A -valued Element of bool [:(Fin A),(Fin A):]
(A,Z,z) is finite Element of Fin (A)
{ ((Fin A),(Fin A),b₁,b₂) where b₁, b₂ is Element of (A) : ( b₁ in Z & b₂ in z ) } is set
(A) /\ { ((Fin A),(Fin A),b₁,b₂) where b₁, b₂ is Element of (A) : ( b₁ in Z & b₂ in z ) } is Relation-like Fin A -defined Fin A -valued Element of bool [:(Fin A),(Fin A):]
(A,Z,u) \/ (A,Z,z) is finite Element of Fin (A)
u9 is Element of (A)
K is Element of (A)
L is Element of (A)
((Fin A),(Fin A),K,L) is Element of [:(Fin A),(Fin A):]
K `1 is finite Element of Fin A
L `1 is finite Element of Fin A
(K `1) \/ (L `1) is finite Element of Fin A
K `2 is finite Element of Fin A
L `2 is finite Element of Fin A
(K `2) \/ (L `2) is finite Element of Fin A
[((K `1) \/ (L `1)),((K `2) \/ (L `2))] is V15() Element of [:(Fin A),(Fin A):]
{((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
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 -defined Fin A -valued non empty Element of bool [:(Fin A),(Fin A):]
bool [:(Fin A),(Fin A):] is non empty cup-closed diff-closed preBoolean set
{ b₁ where b₁ is Element of [:(Fin A),(Fin A):] : b₁ `1 misses b<sub>1</sub> `2 } is set
Fin (A) is non empty cup-closed diff-closed preBoolean set
Z is Element of (A)
u is finite Element of Fin (A)
z is finite Element of Fin (A)
(A,u,z) is finite Element of Fin (A)
{ ((Fin A),(Fin A),b₁,b₂) where b₁, b₂ is Element of (A) : ( b₁ in u & b₂ in z ) } is set
(A) /\ { ((Fin A),(Fin A),b₁,b₂) where b₁, b₂ is Element of (A) : ( b₁ in u & b₂ in z ) } is Relation-like Fin A -defined Fin A -valued Element of bool [:(Fin A),(Fin A):]
u9 is Element of (A)
K is Element of (A)
((Fin A),(Fin A),u9,K) is Element of [:(Fin A),(Fin A):]
u9 `1 is finite Element of Fin A
K `1 is finite Element of Fin A
(u9 `1) \/ (K `1) is finite Element of Fin A
u9 `2 is finite Element of Fin A
K `2 is finite Element of Fin A
(u9 `2) \/ (K `2) is finite Element of Fin A
[((u9 `1) \/ (K `1)),((u9 `2) \/ (K `2))] is V15() Element of [:(Fin A),(Fin A):]
{((u9 `1) \/ (K `1)),((u9 `2) \/ (K `2))} is set
{((u9 `1) \/ (K `1))} is set
{{((u9 `1) \/ (K `1)),((u9 `2) \/ (K `2))},{((u9 `1) \/ (K `1))}} is set
A is set
(A) is Relation-like Fin A -defined Fin A -valued non empty Element of bool [:(Fin A),(Fin A):]
Fin A is non empty cup-closed diff-closed preBoolean set
[:(Fin A),(Fin A):] is Relation-like non empty set
bool [:(Fin A),(Fin A):] is non empty cup-closed diff-closed preBoolean set
{ b₁ where b₁ is Element of [:(Fin A),(Fin A):] : b₁ `1 misses b<sub>1</sub> `2 } is set
Fin (A) is non empty cup-closed diff-closed preBoolean set
(A) is non empty Element of bool (Fin (A))
bool (Fin (A)) is non empty cup-closed diff-closed preBoolean set
{ b₁ where b₁ is finite Element of Fin (A) : for b₂, b₃ being Element of (A) holds
( not b₂ in b₁ or not b₃ in b₁ or not ( Fin A, Fin A,b₂,b₃) or b₂ = b₃ ) } is set
Z is Element of (A)
u is Element of (A)
(A,Z,u) is finite Element of Fin (A)
{ ((Fin A),(Fin A),b₁,b₂) where b₁, b₂ is Element of (A) : ( b₁ in Z & b₂ in u ) } is set
(A) /\ { ((Fin A),(Fin A),b₁,b₂) where b₁, b₂ is Element of (A) : ( b₁ in Z & b₂ in u ) } is Relation-like Fin A -defined Fin A -valued Element of bool [:(Fin A),(Fin A):]
(A,Z,u) \/ u is finite Element of Fin (A)
(A,((A,Z,u) \/ u)) is Element of (A)
{ b₁ where b₁ is Element of (A) : for b₂ being Element of (A) holds
( ( not b₂ in (A,Z,u) \/ u or not ( Fin A, Fin A,b₂,b₁) or b₂ = b₁ ) & ( not b₂ = b₁ or ( b₂ in (A,Z,u) \/ u & ( Fin A, Fin A,b₂,b₁) ) ) ) } is set
(A,u) is Element of (A)
{ b₁ where b₁ is Element of (A) : for b₂ being Element of (A) holds
( ( not b₂ in u or not ( Fin A, Fin A,b₂,b₁) or b₂ = b₁ ) & ( not b₂ = b₁ or ( b₂ in u & ( Fin A, Fin A,b₂,b₁) ) ) ) } is set
z is Element of (A)
u9 is Element of (A)
u9 is Element of (A)
z is Element of (A)
u9 is Element of (A)
K is Element of (A)
A is set
(A) is Relation-like Fin A -defined Fin A -valued non empty Element of bool [:(Fin A),(Fin A):]
Fin A is non empty cup-closed diff-closed preBoolean set
[:(Fin A),(Fin A):] is Relation-like non empty set
bool [:(Fin A),(Fin A):] is non empty cup-closed diff-closed preBoolean set
{ b₁ where b₁ is Element of [:(Fin A),(Fin A):] : b₁ `1 misses b<sub>1</sub> `2 } is set
Fin (A) is non empty cup-closed diff-closed preBoolean set
Z is finite Element of Fin (A)
(A,Z,Z) is finite Element of Fin (A)
{ ((Fin A),(Fin A),b₁,b₂) where b₁, b₂ is Element of (A) : ( b₁ in Z & b₂ in Z ) } is set
(A) /\ { ((Fin A),(Fin A),b₁,b₂) where b₁, b₂ is Element of (A) : ( b₁ in Z & b₂ in Z ) } is Relation-like Fin A -defined Fin A -valued Element of bool [:(Fin A),(Fin A):]
u is Element of (A)
((Fin A),(Fin A),u,u) is Element of [:(Fin A),(Fin A):]
u `1 is finite Element of Fin A
(u `1) \/ (u `1) is finite Element of Fin A
u `2 is finite Element of Fin A
(u `2) \/ (u `2) is finite Element of Fin A
[((u `1) \/ (u `1)),((u `2) \/ (u `2))] is V15() Element of [:(Fin A),(Fin A):]
{((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 is set
(A) is Relation-like Fin A -defined Fin A -valued non empty Element of bool [:(Fin A),(Fin A):]
Fin A is non empty cup-closed diff-closed preBoolean set
[:(Fin A),(Fin A):] is Relation-like non empty set
bool [:(Fin A),(Fin A):] is non empty cup-closed diff-closed preBoolean set
{ b₁ where b₁ is Element of [:(Fin A),(Fin A):] : b₁ `1 misses b<sub>1</sub> `2 } is set
Fin (A) is non empty cup-closed diff-closed preBoolean set
(A) is non empty Element of bool (Fin (A))
bool (Fin (A)) is non empty cup-closed diff-closed preBoolean set
{ b₁ where b₁ is finite Element of Fin (A) : for b₂, b₃ being Element of (A) holds
( not b₂ in b₁ or not b₃ in b₁ or not ( Fin A, Fin A,b₂,b₃) or b₂ = b₃ ) } is set
Z is Element of (A)
(A,Z,Z) is finite Element of Fin (A)
{ ((Fin A),(Fin A),b₁,b₂) where b₁, b₂ is Element of (A) : ( b₁ in Z & b₂ in Z ) } is set
(A) /\ { ((Fin A),(Fin A),b₁,b₂) where b₁, b₂ is Element of (A) : ( b₁ in Z & b₂ in Z ) } is Relation-like Fin A -defined Fin A -valued Element of bool [:(Fin A),(Fin A):]
(A,(A,Z,Z)) is Element of (A)
{ b₁ where b₁ is Element of (A) : for b₂ being Element of (A) holds
( ( not b₂ in (A,Z,Z) or not ( Fin A, Fin A,b₂,b₁) or b₂ = b₁ ) & ( not b₂ = b₁ or ( b₂ in (A,Z,Z) & ( Fin A, Fin A,b₂,b₁) ) ) ) } is set
(A,Z) is Element of (A)
{ b₁ where b₁ is Element of (A) : for b₂ being Element of (A) holds
( ( not b₂ in Z or not ( Fin A, Fin A,b₂,b₁) or b₂ = b₁ ) & ( not b₂ = b₁ or ( b₂ in Z & ( Fin A, Fin A,b₂,b₁) ) ) ) } is set
(A,Z,Z) \/ Z is finite Element of Fin (A)
(A,((A,Z,Z) \/ Z)) is Element of (A)
{ b₁ where b₁ is Element of (A) : for b₂ being Element of (A) holds
( ( not b₂ in (A,Z,Z) \/ Z or not ( Fin A, Fin A,b₂,b₁) or b₂ = b₁ ) & ( not b₂ = b₁ or ( b₂ in (A,Z,Z) \/ Z & ( Fin A, Fin A,b₂,b₁) ) ) ) } is set
A is set
(A) is non empty Element of bool (Fin (A))
(A) is Relation-like Fin A -defined Fin A -valued non empty Element of bool [:(Fin A),(Fin A):]
Fin A is non empty cup-closed diff-closed preBoolean set
[:(Fin A),(Fin A):] is Relation-like non empty set
bool [:(Fin A),(Fin A):] is non empty cup-closed diff-closed preBoolean set
{ b₁ where b₁ is Element of [:(Fin A),(Fin A):] : b₁ `1 misses b<sub>1</sub> `2 } is set
Fin (A) is non empty cup-closed diff-closed preBoolean set
bool (Fin (A)) is non empty cup-closed diff-closed preBoolean set
{ b₁ where b₁ is finite Element of Fin (A) : for b₂, b₃ being Element of (A) holds
( not b₂ in b₁ or not b₃ in b₁ or not ( Fin A, Fin A,b₂,b₃) or b₂ = b₃ ) } is set
[:(A),(A):] is Relation-like non empty set
[:[:(A),(A):],(A):] is Relation-like non empty set
bool [:[:(A),(A):],(A):] is non empty cup-closed diff-closed preBoolean set
u is Relation-like [:(A),(A):] -defined (A) -valued V6() non empty V14([:(A),(A):]) V18([:(A),(A):],(A)) Element of bool [:[:(A),(A):],(A):]
z is Relation-like [:(A),(A):] -defined (A) -valued V6() non empty V14([:(A),(A):]) V18([:(A),(A):],(A)) Element of bool [:[:(A),(A):],(A):]
LattStr(# (A),u,z #) is non empty strict LattStr
the carrier of LattStr(# (A),u,z #) is set
the L_join of LattStr(# (A),u,z #) is Relation-like [: the carrier of LattStr(# (A),u,z #), the carrier of LattStr(# (A),u,z #):] -defined the carrier of LattStr(# (A),u,z #) -valued V6() V18([: the carrier of LattStr(# (A),u,z #), the carrier of LattStr(# (A),u,z #):], the carrier of LattStr(# (A),u,z #)) Element of bool [:[: the carrier of LattStr(# (A),u,z #), the carrier of LattStr(# (A),u,z #):], the carrier of LattStr(# (A),u,z #):]
[: the carrier of LattStr(# (A),u,z #), the carrier of LattStr(# (A),u,z #):] is Relation-like set
[:[: the carrier of LattStr(# (A),u,z #), the carrier of LattStr(# (A),u,z #):], the carrier of LattStr(# (A),u,z #):] is Relation-like set
bool [:[: the carrier of LattStr(# (A),u,z #), the carrier of LattStr(# (A),u,z #):], the carrier of LattStr(# (A),u,z #):] is non empty cup-closed diff-closed preBoolean set
the L_meet of LattStr(# (A),u,z #) is Relation-like [: the carrier of LattStr(# (A),u,z #), the carrier of LattStr(# (A),u,z #):] -defined the carrier of LattStr(# (A),u,z #) -valued V6() V18([: the carrier of LattStr(# (A),u,z #), the carrier of LattStr(# (A),u,z #):], the carrier of LattStr(# (A),u,z #)) Element of bool [:[: the carrier of LattStr(# (A),u,z #), the carrier of LattStr(# (A),u,z #):], the carrier of LattStr(# (A),u,z #):]
u9 is Element of (A)
K is Element of (A)
the L_join of LattStr(# (A),u,z #) . (u9,K) is set
[u9,K] is V15() set
{u9,K} is set
{u9} is set
{{u9,K},{u9}} is set
K11( the L_join of LattStr(# (A),u,z #),[u9,K]) is set
u9 \/ K is finite Element of Fin (A)
(A,(u9 \/ K)) is Element of (A)
{ b₁ where b₁ is Element of (A) : for b₂ being Element of (A) holds
( ( not b₂ in u9 \/ K or not ( Fin A, Fin A,b₂,b₁) or b₂ = b₁ ) & ( not b₂ = b₁ or ( b₂ in u9 \/ K & ( Fin A, Fin A,b₂,b₁) ) ) ) } is set
L is Element of (A)
M is Element of (A)
the L_meet of LattStr(# (A),u,z #) . (L,M) is set
[L,M] is V15() set
{L,M} is set
{L} is set
{{L,M},{L}} is set
K11( the L_meet of LattStr(# (A),u,z #),[L,M]) is set
(A,L,M) is finite Element of Fin (A)
{ ((Fin A),(Fin A),b₁,b₂) where b₁, b₂ is Element of (A) : ( b₁ in L & b₂ in M ) } is set
(A) /\ { ((Fin A),(Fin A),b₁,b₂) where b₁, b₂ is Element of (A) : ( b₁ in L & b₂ in M ) } is Relation-like Fin A -defined Fin A -valued Element of bool [:(Fin A),(Fin A):]
(A,(A,L,M)) is Element of (A)
{ b₁ where b₁ is Element of (A) : for b₂ being Element of (A) holds
( ( not b₂ in (A,L,M) or not ( Fin A, Fin A,b₂,b₁) or b₂ = b₁ ) & ( not b₂ = b₁ or ( b₂ in (A,L,M) & ( Fin A, Fin A,b₂,b₁) ) ) ) } is set
u is strict LattStr
the carrier of u is set
the L_join of u is Relation-like [: the carrier of u, the carrier of u:] -defined the carrier of u -valued V6() V18([: the carrier of u, the carrier of u:], the carrier of u) Element of bool [:[: the carrier of u, the carrier of u:], the carrier of u:]
[: the carrier of u, the carrier of u:] is Relation-like set
[:[: the carrier of u, the carrier of u:], the carrier of u:] is Relation-like set
bool [:[: the carrier of u, the carrier of u:], the carrier of u:] is non empty cup-closed diff-closed preBoolean set
the L_meet of u is Relation-like [: the carrier of u, the carrier of u:] -defined the carrier of u -valued V6() V18([: the carrier of u, the carrier of u:], the carrier of u) Element of bool [:[: the carrier of u, the carrier of u:], the carrier of u:]
z is strict LattStr
the carrier of z is set
the L_join of z is Relation-like [: the carrier of z, the carrier of z:] -defined the carrier of z -valued V6() V18([: the carrier of z, the carrier of z:], the carrier of z) Element of bool [:[: the carrier of z, the carrier of z:], the carrier of z:]
[: the carrier of z, the carrier of z:] is Relation-like set
[:[: the carrier of z, the carrier of z:], the carrier of z:] is Relation-like set
bool [:[: the carrier of z, the carrier of z:], the carrier of z:] is non empty cup-closed diff-closed preBoolean set
the L_meet of z is Relation-like [: the carrier of z, the carrier of z:] -defined the carrier of z -valued V6() V18([: the carrier of z, the carrier of z:], the carrier of z) Element of bool [:[: the carrier of z, the carrier of z:], the carrier of z:]
[:(A),(A):] is Relation-like non empty set
[:[:(A),(A):],(A):] is Relation-like non empty set
bool [:[:(A),(A):],(A):] is non empty cup-closed diff-closed preBoolean set
L is Relation-like [:(A),(A):] -defined (A) -valued V6() non empty V14([:(A),(A):]) V18([:(A),(A):],(A)) Element of bool [:[:(A),(A):],(A):]
x is Element of (A)
y is Element of (A)
((Fin (A)),(A),L,x,y) is Element of (A)
[x,y] is V15() set
{x,y} is set
{x} is set
{{x,y},{x}} is set
K11(L,[x,y]) is set
x \/ y is finite Element of Fin (A)
(A,(x \/ y)) is Element of (A)
{ b₁ where b₁ is Element of (A) : for b₂ being Element of (A) holds
( ( not b₂ in x \/ y or not ( Fin A, Fin A,b₂,b₁) or b₂ = b₁ ) & ( not b₂ = b₁ or ( b₂ in x \/ y & ( Fin A, Fin A,b₂,b₁) ) ) ) } is set
M is Relation-like [:(A),(A):] -defined (A) -valued V6() non empty V14([:(A),(A):]) V18([:(A),(A):],(A)) Element of bool [:[:(A),(A):],(A):]
((Fin (A)),(A),M,x,y) is Element of (A)
K11(M,[x,y]) is set
u9 is Relation-like [:(A),(A):] -defined (A) -valued V6() non empty V14([:(A),(A):]) V18([:(A),(A):],(A)) Element of bool [:[:(A),(A):],(A):]
x is Element of (A)
y is Element of (A)
((Fin (A)),(A),u9,x,y) is Element of (A)
[x,y] is V15() set
{x,y} is set
{x} is set
{{x,y},{x}} is set
K11(u9,[x,y]) is set
(A,x,y) is finite Element of Fin (A)
{ ((Fin A),(Fin A),b₁,b₂) where b₁, b₂ is Element of (A) : ( b₁ in x & b₂ in y ) } is set
(A) /\ { ((Fin A),(Fin A),b₁,b₂) where b₁, b₂ is Element of (A) : ( b₁ in x & b₂ in y ) } is Relation-like Fin A -defined Fin A -valued Element of bool [:(Fin A),(Fin A):]
(A,(A,x,y)) is Element of (A)
{ b₁ where b₁ is Element of (A) : for b₂ being Element of (A) holds
( ( not b₂ in (A,x,y) or not ( Fin A, Fin A,b₂,b₁) or b₂ = b₁ ) & ( not b₂ = b₁ or ( b₂ in (A,x,y) & ( Fin A, Fin A,b₂,b₁) ) ) ) } is set
K is Relation-like [:(A),(A):] -defined (A) -valued V6() non empty V14([:(A),(A):]) V18([:(A),(A):],(A)) Element of bool [:[:(A),(A):],(A):]
((Fin (A)),(A),K,x,y) is Element of (A)
K11(K,[x,y]) is set
A is set
(A) is strict LattStr
the carrier of (A) is set
(A) is non empty Element of bool (Fin (A))
(A) is Relation-like Fin A -defined Fin A -valued non empty Element of bool [:(Fin A),(Fin A):]
Fin A is non empty cup-closed diff-closed preBoolean set
[:(Fin A),(Fin A):] is Relation-like non empty set
bool [:(Fin A),(Fin A):] is non empty cup-closed diff-closed preBoolean set
{ b₁ where b₁ is Element of [:(Fin A),(Fin A):] : b₁ `1 misses b<sub>1</sub> `2 } is set
Fin (A) is non empty cup-closed diff-closed preBoolean set
bool (Fin (A)) is non empty cup-closed diff-closed preBoolean set
{ b₁ where b₁ is finite Element of Fin (A) : for b₂, b₃ being Element of (A) holds
( not b₂ in b₁ or not b₃ in b₁ or not ( Fin A, Fin A,b₂,b₃) or b₂ = b₃ ) } is set
A is set
(A) is non empty strict LattStr
the carrier of (A) is set
u is Element of the carrier of (A)
z is Element of the carrier of (A)
u "\/" z is Element of the carrier of (A)
the L_join of (A) is Relation-like [: the carrier of (A), the carrier of (A):] -defined the carrier of (A) -valued V6() V18([: the carrier of (A), the carrier of (A):], the carrier of (A)) Element of bool [:[: the carrier of (A), the carrier of (A):], the carrier of (A):]
[: the carrier of (A), the carrier of (A):] is Relation-like set
[:[: the carrier of (A), the carrier of (A):], the carrier of (A):] is Relation-like set
bool [:[: the carrier of (A), the carrier of (A):], the carrier of (A):] is non empty cup-closed diff-closed preBoolean set
the L_join of (A) . (u,z) is Element of the carrier of (A)
[u,z] is V15() set
{u,z} is set
{u} is set
{{u,z},{u}} is set
K11( the L_join of (A),[u,z]) is set
z "\/" u is Element of the carrier of (A)
the L_join of (A) . (z,u) is Element of the carrier of (A)
[z,u] is V15() set
{z,u} is set
{z} is set
{{z,u},{z}} is set
K11( the L_join of (A),[z,u]) is set
(A) is Relation-like Fin A -defined Fin A -valued non empty Element of bool [:(Fin A),(Fin A):]
Fin A is non empty cup-closed diff-closed preBoolean set
[:(Fin A),(Fin A):] is Relation-like non empty set
bool [:(Fin A),(Fin A):] is non empty cup-closed diff-closed preBoolean set
{ b₁ where b₁ is Element of [:(Fin A),(Fin A):] : b₁ `1 misses b<sub>1</sub> `2 } is set
Fin (A) is non empty cup-closed diff-closed preBoolean set
(A) is non empty Element of bool (Fin (A))
bool (Fin (A)) is non empty cup-closed diff-closed preBoolean set
{ b₁ where b₁ is finite Element of Fin (A) : for b₂, b₃ being Element of (A) holds
( not b₂ in b₁ or not b₃ in b₁ or not ( Fin A, Fin A,b₂,b₃) or b₂ = b₃ ) } is set
K is Element of (A)
u9 is Element of (A)
K \/ u9 is finite Element of Fin (A)
(A,(K \/ u9)) is Element of (A)
{ b₁ where b₁ is Element of (A) : for b₂ being Element of (A) holds
( ( not b₂ in K \/ u9 or not ( Fin A, Fin A,b₂,b₁) or b₂ = b₁ ) & ( not b₂ = b₁ or ( b₂ in K \/ u9 & ( Fin A, Fin A,b₂,b₁) ) ) ) } is set
A is set
(A) is non empty strict LattStr
the carrier of (A) is set
u is Element of the carrier of (A)
z is Element of the carrier of (A)
u9 is Element of the carrier of (A)
z "\/" u9 is Element of the carrier of (A)
the L_join of (A) is Relation-like [: the carrier of (A), the carrier of (A):] -defined the carrier of (A) -valued V6() V18([: the carrier of (A), the carrier of (A):], the carrier of (A)) Element of bool [:[: the carrier of (A), the carrier of (A):], the carrier of (A):]
[: the carrier of (A), the carrier of (A):] is Relation-like set
[:[: the carrier of (A), the carrier of (A):], the carrier of (A):] is Relation-like set
bool [:[: the carrier of (A), the carrier of (A):], the carrier of (A):] is non empty cup-closed diff-closed preBoolean set
the L_join of (A) . (z,u9) is Element of the carrier of (A)
[z,u9] is V15() set
{z,u9} is set
{z} is set
{{z,u9},{z}} is set
K11( the L_join of (A),[z,u9]) is set
u "\/" (z "\/" u9) is Element of the carrier of (A)
the L_join of (A) . (u,(z "\/" u9)) is Element of the carrier of (A)
[u,(z "\/" u9)] is V15() set
{u,(z "\/" u9)} is set
{u} is set
{{u,(z "\/" u9)},{u}} is set
K11( the L_join of (A),[u,(z "\/" u9)]) is set
u "\/" z is Element of the carrier of (A)
the L_join of (A) . (u,z) is Element of the carrier of (A)
[u,z] is V15() set
{u,z} is set
{{u,z},{u}} is set
K11( the L_join of (A),[u,z]) is set
(u "\/" z) "\/" u9 is Element of the carrier of (A)
the L_join of (A) . ((u "\/" z),u9) is Element of the carrier of (A)
[(u "\/" z),u9] is V15() set
{(u "\/" z),u9} is set
{(u "\/" z)} is set
{{(u "\/" z),u9},{(u "\/" z)}} is set
K11( the L_join of (A),[(u "\/" z),u9]) is set
(A) is Relation-like Fin A -defined Fin A -valued non empty Element of bool [:(Fin A),(Fin A):]
Fin A is non empty cup-closed diff-closed preBoolean set
[:(Fin A),(Fin A):] is Relation-like non empty set
bool [:(Fin A),(Fin A):] is non empty cup-closed diff-closed preBoolean set
{ b₁ where b₁ is Element of [:(Fin A),(Fin A):] : b₁ `1 misses b<sub>1</sub> `2 } is set
Fin (A) is non empty cup-closed diff-closed preBoolean set
(A) is non empty Element of bool (Fin (A))
bool (Fin (A)) is non empty cup-closed diff-closed preBoolean set
{ b₁ where b₁ is finite Element of Fin (A) : for b₂, b₃ being Element of (A) holds
( not b₂ in b₁ or not b₃ in b₁ or not ( Fin A, Fin A,b₂,b₃) or b₂ = b₃ ) } is set
L is Element of (A)
M is Element of (A)
L \/ M is finite Element of Fin (A)
(A,(L \/ M)) is Element of (A)
{ b₁ where b₁ is Element of (A) : for b₂ being Element of (A) holds
( ( not b₂ in L \/ M or not ( Fin A, Fin A,b₂,b₁) or b₂ = b₁ ) & ( not b₂ = b₁ or ( b₂ in L \/ M & ( Fin A, Fin A,b₂,b₁) ) ) ) } is set
the L_join of (A) . (u,(A,(L \/ M))) is set
[u,(A,(L \/ M))] is V15() set
{u,(A,(L \/ M))} is set
{{u,(A,(L \/ M))},{u}} is set
K11( the L_join of (A),[u,(A,(L \/ M))]) is set
K is Element of (A)
(A,(L \/ M)) \/ K is finite Element of Fin (A)
(A,((A,(L \/ M)) \/ K)) is Element of (A)
{ b₁ where b₁ is Element of (A) : for b₂ being Element of (A) holds
( ( not b₂ in (A,(L \/ M)) \/ K or not ( Fin A, Fin A,b₂,b₁) or b₂ = b₁ ) & ( not b₂ = b₁ or ( b₂ in (A,(L \/ M)) \/ K & ( Fin A, Fin A,b₂,b₁) ) ) ) } is set
K \/ (L \/ M) is finite Element of Fin (A)
(A,(K \/ (L \/ M))) is Element of (A)
{ b₁ where b₁ is Element of (A) : for b₂ being Element of (A) holds
( ( not b₂ in K \/ (L \/ M) or not ( Fin A, Fin A,b₂,b₁) or b₂ = b₁ ) & ( not b₂ = b₁ or ( b₂ in K \/ (L \/ M) & ( Fin A, Fin A,b₂,b₁) ) ) ) } is set
K \/ L is finite Element of Fin (A)
(K \/ L) \/ M is finite Element of Fin (A)
(A,((K \/ L) \/ M)) is Element of (A)
{ b₁ where b₁ is Element of (A) : for b₂ being Element of (A) holds
( ( not b₂ in (K \/ L) \/ M or not ( Fin A, Fin A,b₂,b₁) or b₂ = b₁ ) & ( not b₂ = b₁ or ( b₂ in (K \/ L) \/ M & ( Fin A, Fin A,b₂,b₁) ) ) ) } is set
(A,(K \/ L)) is Element of (A)
{ b₁ where b₁ is Element of (A) : for b₂ being Element of (A) holds
( ( not b₂ in K \/ L or not ( Fin A, Fin A,b₂,b₁) or b₂ = b₁ ) & ( not b₂ = b₁ or ( b₂ in K \/ L & ( Fin A, Fin A,b₂,b₁) ) ) ) } is set
(A,(K \/ L)) \/ M is finite Element of Fin (A)
(A,((A,(K \/ L)) \/ M)) is Element of (A)
{ b₁ where b₁ is Element of (A) : for b₂ being Element of (A) holds
( ( not b₂ in (A,(K \/ L)) \/ M or not ( Fin A, Fin A,b₂,b₁) or b₂ = b₁ ) & ( not b₂ = b₁ or ( b₂ in (A,(K \/ L)) \/ M & ( Fin A, Fin A,b₂,b₁) ) ) ) } is set
the L_join of (A) . ((A,(K \/ L)),M) is set
[(A,(K \/ L)),M] is V15() set
{(A,(K \/ L)),M} is set
{(A,(K \/ L))} is set
{{(A,(K \/ L)),M},{(A,(K \/ L))}} is set
K11( the L_join of (A),[(A,(K \/ L)),M]) is set
A is set
(A) is Relation-like Fin A -defined Fin A -valued non empty Element of bool [:(Fin A),(Fin A):]
Fin A is non empty cup-closed diff-closed preBoolean set
[:(Fin A),(Fin A):] is Relation-like non empty set
bool [:(Fin A),(Fin A):] is non empty cup-closed diff-closed preBoolean set
{ b₁ where b₁ is Element of [:(Fin A),(Fin A):] : b₁ `1 misses b<sub>1</sub> `2 } is set
Fin (A) is non empty cup-closed diff-closed preBoolean set
(A) is non empty Element of bool (Fin (A))
bool (Fin (A)) is non empty cup-closed diff-closed preBoolean set
{ b₁ where b₁ is finite Element of Fin (A) : for b₂, b₃ being Element of (A) holds
( not b₂ in b₁ or not b₃ in b₁ or not ( Fin A, Fin A,b₂,b₃) or b₂ = b₃ ) } is set
(A) is non empty strict LattStr
the L_join of (A) is Relation-like [: the carrier of (A), the carrier of (A):] -defined the carrier of (A) -valued V6() V18([: the carrier of (A), the carrier of (A):], the carrier of (A)) Element of bool [:[: the carrier of (A), the carrier of (A):], the carrier of (A):]
the carrier of (A) is set
[: the carrier of (A), the carrier of (A):] is Relation-like set
[:[: the carrier of (A), the carrier of (A):], the carrier of (A):] is Relation-like set
bool [:[: the carrier of (A), the carrier of (A):], the carrier of (A):] is non empty cup-closed diff-closed preBoolean set
the L_meet of (A) is Relation-like [: the carrier of (A), the carrier of (A):] -defined the carrier of (A) -valued V6() V18([: the carrier of (A), the carrier of (A):], the carrier of (A)) Element of bool [:[: the carrier of (A), the carrier of (A):], the carrier of (A):]
Z is Element of (A)
u is Element of (A)
the L_meet of (A) . (Z,u) is set
[Z,u] is V15() set
{Z,u} is set
{Z} is set
{{Z,u},{Z}} is set
K11( the L_meet of (A),[Z,u]) is set
the L_join of (A) . (( the L_meet of (A) . (Z,u)),u) is set
[( the L_meet of (A) . (Z,u)),u] is V15() set
{( the L_meet of (A) . (Z,u)),u} is set
{( the L_meet of (A) . (Z,u))} is set
{{( the L_meet of (A) . (Z,u)),u},{( the L_meet of (A) . (Z,u))}} is set
K11( the L_join of (A),[( the L_meet of (A) . (Z,u)),u]) is set
(A,Z,u) is finite Element of Fin (A)
{ ((Fin A),(Fin A),b₁,b₂) where b₁, b₂ is Element of (A) : ( b₁ in Z & b₂ in u ) } is set
(A) /\ { ((Fin A),(Fin A),b₁,b₂) where b₁, b₂ is Element of (A) : ( b₁ in Z & b₂ in u ) } is Relation-like Fin A -defined Fin A -valued Element of bool [:(Fin A),(Fin A):]
(A,(A,Z,u)) is Element of (A)
{ b₁ where b₁ is Element of (A) : for b₂ being Element of (A) holds
( ( not b₂ in (A,Z,u) or not ( Fin A, Fin A,b₂,b₁) or b₂ = b₁ ) & ( not b₂ = b₁ or ( b₂ in (A,Z,u) & ( Fin A, Fin A,b₂,b₁) ) ) ) } is set
the L_join of (A) . ((A,(A,Z,u)),u) is set
[(A,(A,Z,u)),u] is V15() set
{(A,(A,Z,u)),u} is set
{(A,(A,Z,u))} is set
{{(A,(A,Z,u)),u},{(A,(A,Z,u))}} is set
K11( the L_join of (A),[(A,(A,Z,u)),u]) is set
(A,(A,Z,u)) \/ u is finite Element of Fin (A)
(A,((A,(A,Z,u)) \/ u)) is Element of (A)
{ b₁ where b₁ is Element of (A) : for b₂ being Element of (A) holds
( ( not b₂ in (A,(A,Z,u)) \/ u or not ( Fin A, Fin A,b₂,b₁) or b₂ = b₁ ) & ( not b₂ = b₁ or ( b₂ in (A,(A,Z,u)) \/ u & ( Fin A, Fin A,b₂,b₁) ) ) ) } is set
(A,Z,u) \/ u is finite Element of Fin (A)
(A,((A,Z,u) \/ u)) is Element of (A)
{ b₁ where b₁ is Element of (A) : for b₂ being Element of (A) holds
( ( not b₂ in (A,Z,u) \/ u or not ( Fin A, Fin A,b₂,b₁) or b₂ = b₁ ) & ( not b₂ = b₁ or ( b₂ in (A,Z,u) \/ u & ( Fin A, Fin A,b₂,b₁) ) ) ) } is set
(A,u) is Element of (A)
{ b₁ where b₁ is Element of (A) : for b₂ being Element of (A) holds
( ( not b₂ in u or not ( Fin A, Fin A,b₂,b₁) or b₂ = b₁ ) & ( not b₂ = b₁ or ( b₂ in u & ( Fin A, Fin A,b₂,b₁) ) ) ) } is set
A is set
(A) is non empty strict LattStr
the carrier of (A) is set
Z is Element of the carrier of (A)
u is Element of the carrier of (A)
Z "/\" u is Element of the carrier of (A)
the L_meet of (A) is Relation-like [: the carrier of (A), the carrier of (A):] -defined the carrier of (A) -valued V6() V18([: the carrier of (A), the carrier of (A):], the carrier of (A)) Element of bool [:[: the carrier of (A), the carrier of (A):], the carrier of (A):]
[: the carrier of (A), the carrier of (A):] is Relation-like set
[:[: the carrier of (A), the carrier of (A):], the carrier of (A):] is Relation-like set
bool [:[: the carrier of (A), the carrier of (A):], the carrier of (A):] is non empty cup-closed diff-closed preBoolean set
the L_meet of (A) . (Z,u) is Element of the carrier of (A)
[Z,u] is V15() set
{Z,u} is set
{Z} is set
{{Z,u},{Z}} is set
K11( the L_meet of (A),[Z,u]) is set
(Z "/\" u) "\/" u is Element of the carrier of (A)
the L_join of (A) is Relation-like [: the carrier of (A), the carrier of (A):] -defined the carrier of (A) -valued V6() V18([: the carrier of (A), the carrier of (A):], the carrier of (A)) Element of bool [:[: the carrier of (A), the carrier of (A):], the carrier of (A):]
the L_join of (A) . ((Z "/\" u),u) is Element of the carrier of (A)
[(Z "/\" u),u] is V15() set
{(Z "/\" u),u} is set
{(Z "/\" u)} is set
{{(Z "/\" u),u},{(Z "/\" u)}} is set
K11( the L_join of (A),[(Z "/\" u),u]) is set
(A) is Relation-like Fin A -defined Fin A -valued non empty Element of bool [:(Fin A),(Fin A):]
Fin A is non empty cup-closed diff-closed preBoolean set
[:(Fin A),(Fin A):] is Relation-like non empty set
bool [:(Fin A),(Fin A):] is non empty cup-closed diff-closed preBoolean set
{ b₁ where b₁ is Element of [:(Fin A),(Fin A):] : b₁ `1 misses b<sub>1</sub> `2 } is set
Fin (A) is non empty cup-closed diff-closed preBoolean set
(A) is non empty Element of bool (Fin (A))
bool (Fin (A)) is non empty cup-closed diff-closed preBoolean set
{ b₁ where b₁ is finite Element of Fin (A) : for b₂, b₃ being Element of (A) holds
( not b₂ in b₁ or not b₃ in b₁ or not ( Fin A, Fin A,b₂,b₃) or b₂ = b₃ ) } is set
z is Element of (A)
u9 is Element of (A)
the L_meet of (A) . (z,u9) is set
[z,u9] is V15() set
{z,u9} is set
{z} is set
{{z,u9},{z}} is set
K11( the L_meet of (A),[z,u9]) is set
the L_join of (A) . (( the L_meet of (A) . (z,u9)),u9) is set
[( the L_meet of (A) . (z,u9)),u9] is V15() set
{( the L_meet of (A) . (z,u9)),u9} is set
{( the L_meet of (A) . (z,u9))} is set
{{( the L_meet of (A) . (z,u9)),u9},{( the L_meet of (A) . (z,u9))}} is set
K11( the L_join of (A),[( the L_meet of (A) . (z,u9)),u9]) is set
A is set
(A) is non empty strict LattStr
the carrier of (A) is set
u is Element of the carrier of (A)
z is Element of the carrier of (A)
u "/\" z is Element of the carrier of (A)
the L_meet of (A) is Relation-like [: the carrier of (A), the carrier of (A):] -defined the carrier of (A) -valued V6() V18([: the carrier of (A), the carrier of (A):], the carrier of (A)) Element of bool [:[: the carrier of (A), the carrier of (A):], the carrier of (A):]
[: the carrier of (A), the carrier of (A):] is Relation-like set
[:[: the carrier of (A), the carrier of (A):], the carrier of (A):] is Relation-like set
bool [:[: the carrier of (A), the carrier of (A):], the carrier of (A):] is non empty cup-closed diff-closed preBoolean set
the L_meet of (A) . (u,z) is Element of the carrier of (A)
[u,z] is V15() set
{u,z} is set
{u} is set
{{u,z},{u}} is set
K11( the L_meet of (A),[u,z]) is set
z "/\" u is Element of the carrier of (A)
the L_meet of (A) . (z,u) is Element of the carrier of (A)
[z,u] is V15() set
{z,u} is set
{z} is set
{{z,u},{z}} is set
K11( the L_meet of (A),[z,u]) is set
(A) is Relation-like Fin A -defined Fin A -valued non empty Element of bool [:(Fin A),(Fin A):]
Fin A is non empty cup-closed diff-closed preBoolean set
[:(Fin A),(Fin A):] is Relation-like non empty set
bool [:(Fin A),(Fin A):] is non empty cup-closed diff-closed preBoolean set
{ b₁ where b₁ is Element of [:(Fin A),(Fin A):] : b₁ `1 misses b<sub>1</sub> `2 } is set
Fin (A) is non empty cup-closed diff-closed preBoolean set
(A) is non empty Element of bool (Fin (A))
bool (Fin (A)) is non empty cup-closed diff-closed preBoolean set
{ b₁ where b₁ is finite Element of Fin (A) : for b₂, b₃ being Element of (A) holds
( not b₂ in b₁ or not b₃ in b₁ or not ( Fin A, Fin A,b₂,b₃) or b₂ = b₃ ) } is set
u9 is Element of (A)
K is Element of (A)
(A,u9,K) is finite Element of Fin (A)
{ ((Fin A),(Fin A),b₁,b₂) where b₁, b₂ is Element of (A) : ( b₁ in u9 & b₂ in K ) } is set
(A) /\ { ((Fin A),(Fin A),b₁,b₂) where b₁, b₂ is Element of (A) : ( b₁ in u9 & b₂ in K ) } is Relation-like Fin A -defined Fin A -valued Element of bool [:(Fin A),(Fin A):]
(A,(A,u9,K)) is Element of (A)
{ b₁ where b₁ is Element of (A) : for b₂ being Element of (A) holds
( ( not b₂ in (A,u9,K) or not ( Fin A, Fin A,b₂,b₁) or b₂ = b₁ ) & ( not b₂ = b₁ or ( b₂ in (A,u9,K) & ( Fin A, Fin A,b₂,b₁) ) ) ) } is set
(A,K,u9) is finite Element of Fin (A)
{ ((Fin A),(Fin A),b₁,b₂) where b₁, b₂ is Element of (A) : ( b₁ in K & b₂ in u9 ) } is set
(A) /\ { ((Fin A),(Fin A),b₁,b₂) where b₁, b₂ is Element of (A) : ( b₁ in K & b₂ in u9 ) } is Relation-like Fin A -defined Fin A -valued Element of bool [:(Fin A),(Fin A):]
(A,(A,K,u9)) is Element of (A)
{ b₁ where b₁ is Element of (A) : for b₂ being Element of (A) holds
( ( not b₂ in (A,K,u9) or not ( Fin A, Fin A,b₂,b₁) or b₂ = b₁ ) & ( not b₂ = b₁ or ( b₂ in (A,K,u9) & ( Fin A, Fin A,b₂,b₁) ) ) ) } is set
A is set
(A) is non empty strict LattStr
the carrier of (A) is set
u is Element of the carrier of (A)
z is Element of the carrier of (A)
u9 is Element of the carrier of (A)
z "/\" u9 is Element of the carrier of (A)
the L_meet of (A) is Relation-like [: the carrier of (A), the carrier of (A):] -defined the carrier of (A) -valued V6() V18([: the carrier of (A), the carrier of (A):], the carrier of (A)) Element of bool [:[: the carrier of (A), the carrier of (A):], the carrier of (A):]
[: the carrier of (A), the carrier of (A):] is Relation-like set
[:[: the carrier of (A), the carrier of (A):], the carrier of (A):] is Relation-like set
bool [:[: the carrier of (A), the carrier of (A):], the carrier of (A):] is non empty cup-closed diff-closed preBoolean set
the L_meet of (A) . (z,u9) is Element of the carrier of (A)
[z,u9] is V15() set
{z,u9} is set
{z} is set
{{z,u9},{z}} is set
K11( the L_meet of (A),[z,u9]) is set
u "/\" (z "/\" u9) is Element of the carrier of (A)
the L_meet of (A) . (u,(z "/\" u9)) is Element of the carrier of (A)
[u,(z "/\" u9)] is V15() set
{u,(z "/\" u9)} is set
{u} is set
{{u,(z "/\" u9)},{u}} is set
K11( the L_meet of (A),[u,(z "/\" u9)]) is set
u "/\" z is Element of the carrier of (A)
the L_meet of (A) . (u,z) is Element of the carrier of (A)
[u,z] is V15() set
{u,z} is set
{{u,z},{u}} is set
K11( the L_meet of (A),[u,z]) is set
(u "/\" z) "/\" u9 is Element of the carrier of (A)
the L_meet of (A) . ((u "/\" z),u9) is Element of the carrier of (A)
[(u "/\" z),u9] is V15() set
{(u "/\" z),u9} is set
{(u "/\" z)} is set
{{(u "/\" z),u9},{(u "/\" z)}} is set
K11( the L_meet of (A),[(u "/\" z),u9]) is set
(A) is Relation-like Fin A -defined Fin A -valued non empty Element of bool [:(Fin A),(Fin A):]
Fin A is non empty cup-closed diff-closed preBoolean set
[:(Fin A),(Fin A):] is Relation-like non empty set
bool [:(Fin A),(Fin A):] is non empty cup-closed diff-closed preBoolean set
{ b₁ where b₁ is Element of [:(Fin A),(Fin A):] : b₁ `1 misses b<sub>1</sub> `2 } is set
Fin (A) is non empty cup-closed diff-closed preBoolean set
(A) is non empty Element of bool (Fin (A))
bool (Fin (A)) is non empty cup-closed diff-closed preBoolean set
{ b₁ where b₁ is finite Element of Fin (A) : for b₂, b₃ being Element of (A) holds
( not b₂ in b₁ or not b₃ in b₁ or not ( Fin A, Fin A,b₂,b₃) or b₂ = b₃ ) } is set
L is Element of (A)
M is Element of (A)
(A,L,M) is finite Element of Fin (A)
{ ((Fin A),(Fin A),b₁,b₂) where b₁, b₂ is Element of (A) : ( b₁ in L & b₂ in M ) } is set
(A) /\ { ((Fin A),(Fin A),b₁,b₂) where b₁, b₂ is Element of (A) : ( b₁ in L & b₂ in M ) } is Relation-like Fin A -defined Fin A -valued Element of bool [:(Fin A),(Fin A):]
(A,(A,L,M)) is Element of (A)
{ b₁ where b₁ is Element of (A) : for b₂ being Element of (A) holds
( ( not b₂ in (A,L,M) or not ( Fin A, Fin A,b₂,b₁) or b₂ = b₁ ) & ( not b₂ = b₁ or ( b₂ in (A,L,M) & ( Fin A, Fin A,b₂,b₁) ) ) ) } is set
the L_meet of (A) . (u,(A,(A,L,M))) is set
[u,(A,(A,L,M))] is V15() set
{u,(A,(A,L,M))} is set
{{u,(A,(A,L,M))},{u}} is set
K11( the L_meet of (A),[u,(A,(A,L,M))]) is set
K is Element of (A)
(A,K,(A,(A,L,M))) is finite Element of Fin (A)
{ ((Fin A),(Fin A),b₁,b₂) where b₁, b₂ is Element of (A) : ( b₁ in K & b₂ in (A,(A,L,M)) ) } is set
(A) /\ { ((Fin A),(Fin A),b₁,b₂) where b₁, b₂ is Element of (A) : ( b₁ in K & b₂ in (A,(A,L,M)) ) } is Relation-like Fin A -defined Fin A -valued Element of bool [:(Fin A),(Fin A):]
(A,(A,K,(A,(A,L,M)))) is Element of (A)
{ b₁ where b₁ is Element of (A) : for b₂ being Element of (A) holds
( ( not b₂ in (A,K,(A,(A,L,M))) or not ( Fin A, Fin A,b₂,b₁) or b₂ = b₁ ) & ( not b₂ = b₁ or ( b₂ in (A,K,(A,(A,L,M))) & ( Fin A, Fin A,b₂,b₁) ) ) ) } is set
(A,K,(A,L,M)) is finite Element of Fin (A)
{ ((Fin A),(Fin A),b₁,b₂) where b₁, b₂ is Element of (A) : ( b₁ in K & b₂ in (A,L,M) ) } is set
(A) /\ { ((Fin A),(Fin A),b₁,b₂) where b₁, b₂ is Element of (A) : ( b₁ in K & b₂ in (A,L,M) ) } is Relation-like Fin A -defined Fin A -valued Element of bool [:(Fin A),(Fin A):]
(A,(A,K,(A,L,M))) is Element of (A)
{ b₁ where b₁ is Element of (A) : for b₂ being Element of (A) holds
( ( not b₂ in (A,K,(A,L,M)) or not ( Fin A, Fin A,b₂,b₁) or b₂ = b₁ ) & ( not b₂ = b₁ or ( b₂ in (A,K,(A,L,M)) & ( Fin A, Fin A,b₂,b₁) ) ) ) } is set
(A,K,L) is finite Element of Fin (A)
{ ((Fin A),(Fin A),b₁,b₂) where b₁, b₂ is Element of (A) : ( b₁ in K & b₂ in L ) } is set
(A) /\ { ((Fin A),(Fin A),b₁,b₂) where b₁, b₂ is Element of (A) : ( b₁ in K & b₂ in L ) } is Relation-like Fin A -defined Fin A -valued Element of bool [:(Fin A),(Fin A):]
(A,(A,K,L),M) is finite Element of Fin (A)
{ ((Fin A),(Fin A),b₁,b₂) where b₁, b₂ is Element of (A) : ( b₁ in (A,K,L) & b₂ in M ) } is set
(A) /\ { ((Fin A),(Fin A),b₁,b₂) where b₁, b₂ is Element of (A) : ( b₁ in (A,K,L) & b₂ in M ) } is Relation-like Fin A -defined Fin A -valued Element of bool [:(Fin A),(Fin A):]
(A,(A,(A,K,L),M)) is Element of (A)
{ b₁ where b₁ is Element of (A) : for b₂ being Element of (A) holds
( ( not b₂ in (A,(A,K,L),M) or not ( Fin A, Fin A,b₂,b₁) or b₂ = b₁ ) & ( not b₂ = b₁ or ( b₂ in (A,(A,K,L),M) & ( Fin A, Fin A,b₂,b₁) ) ) ) } is set
(A,(A,K,L)) is Element of (A)
{ b₁ where b₁ is Element of (A) : for b₂ being Element of (A) holds
( ( not b₂ in (A,K,L) or not ( Fin A, Fin A,b₂,b₁) or b₂ = b₁ ) & ( not b₂ = b₁ or ( b₂ in (A,K,L) & ( Fin A, Fin A,b₂,b₁) ) ) ) } is set
(A,(A,(A,K,L)),M) is finite Element of Fin (A)
{ ((Fin A),(Fin A),b₁,b₂) where b₁, b₂ is Element of (A) : ( b₁ in (A,(A,K,L)) & b₂ in M ) } is set
(A) /\ { ((Fin A),(Fin A),b₁,b₂) where b₁, b₂ is Element of (A) : ( b₁ in (A,(A,K,L)) & b₂ in M ) } is Relation-like Fin A -defined Fin A -valued Element of bool [:(Fin A),(Fin A):]
(A,(A,(A,(A,K,L)),M)) is Element of (A)
{ b₁ where b₁ is Element of (A) : for b₂ being Element of (A) holds
( ( not b₂ in (A,(A,(A,K,L)),M) or not ( Fin A, Fin A,b₂,b₁) or b₂ = b₁ ) & ( not b₂ = b₁ or ( b₂ in (A,(A,(A,K,L)),M) & ( Fin A, Fin A,b₂,b₁) ) ) ) } is set
the L_meet of (A) . ((A,(A,K,L)),M) is set
[(A,(A,K,L)),M] is V15() set
{(A,(A,K,L)),M} is set
{(A,(A,K,L))} is set
{{(A,(A,K,L)),M},{(A,(A,K,L))}} is set
K11( the L_meet of (A),[(A,(A,K,L)),M]) is set
A is set
(A) is Relation-like Fin A -defined Fin A -valued non empty Element of bool [:(Fin A),(Fin A):]
Fin A is non empty cup-closed diff-closed preBoolean set
[:(Fin A),(Fin A):] is Relation-like non empty set
bool [:(Fin A),(Fin A):] is non empty cup-closed diff-closed preBoolean set
{ b₁ where b₁ is Element of [:(Fin A),(Fin A):] : b₁ `1 misses b<sub>1</sub> `2 } is set
Fin (A) is non empty cup-closed diff-closed preBoolean set
(A) is non empty Element of bool (Fin (A))
bool (Fin (A)) is non empty cup-closed diff-closed preBoolean set
{ b₁ where b₁ is finite Element of Fin (A) : for b₂, b₃ being Element of (A) holds
( not b₂ in b₁ or not b₃ in b₁ or not ( Fin A, Fin A,b₂,b₃) or b₂ = b₃ ) } is set
(A) is non empty strict LattStr
the L_meet of (A) is Relation-like [: the carrier of (A), the carrier of (A):] -defined the carrier of (A) -valued V6() V18([: the carrier of (A), the carrier of (A):], the carrier of (A)) Element of bool [:[: the carrier of (A), the carrier of (A):], the carrier of (A):]
the carrier of (A) is set
[: the carrier of (A), the carrier of (A):] is Relation-like set
[:[: the carrier of (A), the carrier of (A):], the carrier of (A):] is Relation-like set
bool [:[: the carrier of (A), the carrier of (A):], the carrier of (A):] is non empty cup-closed diff-closed preBoolean set
the L_join of (A) is Relation-like [: the carrier of (A), the carrier of (A):] -defined the carrier of (A) -valued V6() V18([: the carrier of (A), the carrier of (A):], the carrier of (A)) Element of bool [:[: the carrier of (A), the carrier of (A):], the carrier of (A):]
Z is Element of (A)
u is Element of (A)
the L_meet of (A) . (Z,u) is set
[Z,u] is V15() set
{Z,u} is set
{Z} is set
{{Z,u},{Z}} is set
K11( the L_meet of (A),[Z,u]) is set
z is Element of (A)
the L_join of (A) . (u,z) is set
[u,z] is V15() set
{u,z} is set
{u} is set
{{u,z},{u}} is set
K11( the L_join of (A),[u,z]) is set
the L_meet of (A) . (Z,( the L_join of (A) . (u,z))) is set
[Z,( the L_join of (A) . (u,z))] is V15() set
{Z,( the L_join of (A) . (u,z))} is set
{{Z,( the L_join of (A) . (u,z))},{Z}} is set
K11( the L_meet of (A),[Z,( the L_join of (A) . (u,z))]) is set
the L_meet of (A) . (Z,z) is set
[Z,z] is V15() set
{Z,z} is set
{{Z,z},{Z}} is set
K11( the L_meet of (A),[Z,z]) is set
the L_join of (A) . (( the L_meet of (A) . (Z,u)),( the L_meet of (A) . (Z,z))) is set
[( the L_meet of (A) . (Z,u)),( the L_meet of (A) . (Z,z))] is V15() set
{( the L_meet of (A) . (Z,u)),( the L_meet of (A) . (Z,z))} is set
{( the L_meet of (A) . (Z,u))} is set
{{( the L_meet of (A) . (Z,u)),( the L_meet of (A) . (Z,z))},{( the L_meet of (A) . (Z,u))}} is set
K11( the L_join of (A),[( the L_meet of (A) . (Z,u)),( the L_meet of (A) . (Z,z))]) is set
(A,Z,z) is finite Element of Fin (A)
{ ((Fin A),(Fin A),b₁,b₂) where b₁, b₂ is Element of (A) : ( b₁ in Z & b₂ in z ) } is set
(A) /\ { ((Fin A),(Fin A),b₁,b₂) where b₁, b₂ is Element of (A) : ( b₁ in Z & b₂ in z ) } is Relation-like Fin A -defined Fin A -valued Element of bool [:(Fin A),(Fin A):]
(A,(A,Z,z)) is Element of (A)
{ b₁ where b₁ is Element of (A) : for b₂ being Element of (A) holds
( ( not b₂ in (A,Z,z) or not ( Fin A, Fin A,b₂,b₁) or b₂ = b₁ ) & ( not b₂ = b₁ or ( b₂ in (A,Z,z) & ( Fin A, Fin A,b₂,b₁) ) ) ) } is set
u \/ z is finite Element of Fin (A)
(A,(u \/ z)) is Element of (A)
{ b₁ where b₁ is Element of (A) : for b₂ being Element of (A) holds
( ( not b₂ in u \/ z or not ( Fin A, Fin A,b₂,b₁) or b₂ = b₁ ) & ( not b₂ = b₁ or ( b₂ in u \/ z & ( Fin A, Fin A,b₂,b₁) ) ) ) } is set
(A,Z,u) is finite Element of Fin (A)
{ ((Fin A),(Fin A),b₁,b₂) where b₁, b₂ is Element of (A) : ( b₁ in Z & b₂ in u ) } is set
(A) /\ { ((Fin A),(Fin A),b₁,b₂) where b₁, b₂ is Element of (A) : ( b₁ in Z & b₂ in u ) } is Relation-like Fin A -defined Fin A -valued Element of bool [:(Fin A),(Fin A):]
(A,(A,Z,u)) is Element of (A)
{ b₁ where b₁ is Element of (A) : for b₂ being Element of (A) holds
( ( not b₂ in (A,Z,u) or not ( Fin A, Fin A,b₂,b₁) or b₂ = b₁ ) & ( not b₂ = b₁ or ( b₂ in (A,Z,u) & ( Fin A, Fin A,b₂,b₁) ) ) ) } is set
u9 is Element of (A)
(A,Z,u9) is finite Element of Fin (A)
{ ((Fin A),(Fin A),b₁,b₂) where b₁, b₂ is Element of (A) : ( b₁ in Z & b₂ in u9 ) } is set
(A) /\ { ((Fin A),(Fin A),b₁,b₂) where b₁, b₂ is Element of (A) : ( b₁ in Z & b₂ in u9 ) } is Relation-like Fin A -defined Fin A -valued Element of bool [:(Fin A),(Fin A):]
(A,(A,Z,u9)) is Element of (A)
{ b₁ where b₁ is Element of (A) : for b₂ being Element of (A) holds
( ( not b₂ in (A,Z,u9) or not ( Fin A, Fin A,b₂,b₁) or b₂ = b₁ ) & ( not b₂ = b₁ or ( b₂ in (A,Z,u9) & ( Fin A, Fin A,b₂,b₁) ) ) ) } is set
(A,Z,(A,(u \/ z))) is finite Element of Fin (A)
{ ((Fin A),(Fin A),b₁,b₂) where b₁, b₂ is Element of (A) : ( b₁ in Z & b₂ in (A,(u \/ z)) ) } is set
(A) /\ { ((Fin A),(Fin A),b₁,b₂) where b₁, b₂ is Element of (A) : ( b₁ in Z & b₂ in (A,(u \/ z)) ) } is Relation-like Fin A -defined Fin A -valued Element of bool [:(Fin A),(Fin A):]
(A,(A,Z,(A,(u \/ z)))) is Element of (A)
{ b₁ where b₁ is Element of (A) : for b₂ being Element of (A) holds
( ( not b₂ in (A,Z,(A,(u \/ z))) or not ( Fin A, Fin A,b₂,b₁) or b₂ = b₁ ) & ( not b₂ = b₁ or ( b₂ in (A,Z,(A,(u \/ z))) & ( Fin A, Fin A,b₂,b₁) ) ) ) } is set
(A,Z,(u \/ z)) is finite Element of Fin (A)
{ ((Fin A),(Fin A),b₁,b₂) where b₁, b₂ is Element of (A) : ( b₁ in Z & b₂ in u \/ z ) } is set
(A) /\ { ((Fin A),(Fin A),b₁,b₂) where b₁, b₂ is Element of (A) : ( b₁ in Z & b₂ in u \/ z ) } is Relation-like Fin A -defined Fin A -valued Element of bool [:(Fin A),(Fin A):]
(A,(A,Z,(u \/ z))) is Element of (A)
{ b₁ where b₁ is Element of (A) : for b₂ being Element of (A) holds
( ( not b₂ in (A,Z,(u \/ z)) or not ( Fin A, Fin A,b₂,b₁) or b₂ = b₁ ) & ( not b₂ = b₁ or ( b₂ in (A,Z,(u \/ z)) & ( Fin A, Fin A,b₂,b₁) ) ) ) } is set
(A,Z,u) \/ (A,Z,z) is finite Element of Fin (A)
(A,((A,Z,u) \/ (A,Z,z))) is Element of (A)
{ b₁ where b₁ is Element of (A) : for b₂ being Element of (A) holds
( ( not b₂ in (A,Z,u) \/ (A,Z,z) or not ( Fin A, Fin A,b₂,b₁) or b₂ = b₁ ) & ( not b₂ = b₁ or ( b₂ in (A,Z,u) \/ (A,Z,z) & ( Fin A, Fin A,b₂,b₁) ) ) ) } is set
(A,(A,Z,u)) \/ (A,Z,z) is finite Element of Fin (A)
(A,((A,(A,Z,u)) \/ (A,Z,z))) is Element of (A)
{ b₁ where b₁ is Element of (A) : for b₂ being Element of (A) holds
( ( not b₂ in (A,(A,Z,u)) \/ (A,Z,z) or not ( Fin A, Fin A,b₂,b₁) or b₂ = b₁ ) & ( not b₂ = b₁ or ( b₂ in (A,(A,Z,u)) \/ (A,Z,z) & ( Fin A, Fin A,b₂,b₁) ) ) ) } is set
(A,(A,Z,u)) \/ (A,(A,Z,z)) is finite Element of Fin (A)
(A,((A,(A,Z,u)) \/ (A,(A,Z,z)))) is Element of (A)
{ b₁ where b₁ is Element of (A) : for b₂ being Element of (A) holds
( ( not b₂ in (A,(A,Z,u)) \/ (A,(A,Z,z)) or not ( Fin A, Fin A,b₂,b₁) or b₂ = b₁ ) & ( not b₂ = b₁ or ( b₂ in (A,(A,Z,u)) \/ (A,(A,Z,z)) & ( Fin A, Fin A,b₂,b₁) ) ) ) } is set
K is Element of (A)
K \/ (A,(A,Z,z)) is finite Element of Fin (A)
(A,(K \/ (A,(A,Z,z)))) is Element of (A)
{ b₁ where b₁ is Element of (A) : for b₂ being Element of (A) holds
( ( not b₂ in K \/ (A,(A,Z,z)) or not ( Fin A, Fin A,b₂,b₁) or b₂ = b₁ ) & ( not b₂ = b₁ or ( b₂ in K \/ (A,(A,Z,z)) & ( Fin A, Fin A,b₂,b₁) ) ) ) } is set
L is Element of (A)
K \/ L is finite Element of Fin (A)
(A,(K \/ L)) is Element of (A)
{ b₁ where b₁ is Element of (A) : for b₂ being Element of (A) holds
( ( not b₂ in K \/ L or not ( Fin A, Fin A,b₂,b₁) or b₂ = b₁ ) & ( not b₂ = b₁ or ( b₂ in K \/ L & ( Fin A, Fin A,b₂,b₁) ) ) ) } is set
A is set
(A) is non empty strict LattStr
the carrier of (A) is set
u is Element of the carrier of (A)
z is Element of the carrier of (A)
u "\/" z is Element of the carrier of (A)
the L_join of (A) is Relation-like [: the carrier of (A), the carrier of (A):] -defined the carrier of (A) -valued V6() V18([: the carrier of (A), the carrier of (A):], the carrier of (A)) Element of bool [:[: the carrier of (A), the carrier of (A):], the carrier of (A):]
[: the carrier of (A), the carrier of (A):] is Relation-like set
[:[: the carrier of (A), the carrier of (A):], the carrier of (A):] is Relation-like set
bool [:[: the carrier of (A), the carrier of (A):], the carrier of (A):] is non empty cup-closed diff-closed preBoolean set
the L_join of (A) . (u,z) is Element of the carrier of (A)
[u,z] is V15() set
{u,z} is set
{u} is set
{{u,z},{u}} is set
K11( the L_join of (A),[u,z]) is set
u "/\" (u "\/" z) is Element of the carrier of (A)
the L_meet of (A) is Relation-like [: the carrier of (A), the carrier of (A):] -defined the carrier of (A) -valued V6() V18([: the carrier of (A), the carrier of (A):], the carrier of (A)) Element of bool [:[: the carrier of (A), the carrier of (A):], the carrier of (A):]
the L_meet of (A) . (u,(u "\/" z)) is Element of the carrier of (A)
[u,(u "\/" z)] is V15() set
{u,(u "\/" z)} is set
{{u,(u "\/" z)},{u}} is set
K11( the L_meet of (A),[u,(u "\/" z)]) is set
(A) is Relation-like Fin A -defined Fin A -valued non empty Element of bool [:(Fin A),(Fin A):]
Fin A is non empty cup-closed diff-closed preBoolean set
[:(Fin A),(Fin A):] is Relation-like non empty set
bool [:(Fin A),(Fin A):] is non empty cup-closed diff-closed preBoolean set
{ b₁ where b₁ is Element of [:(Fin A),(Fin A):] : b₁ `1 misses b<sub>1</sub> `2 } is set
Fin (A) is non empty cup-closed diff-closed preBoolean set
(A) is non empty Element of bool (Fin (A))
bool (Fin (A)) is non empty cup-closed diff-closed preBoolean set
{ b₁ where b₁ is finite Element of Fin (A) : for b₂, b₃ being Element of (A) holds
( not b₂ in b₁ or not b₃ in b₁ or not ( Fin A, Fin A,b₂,b₃) or b₂ = b₃ ) } is set
u9 is Element of (A)
the L_meet of (A) . (u9,u9) is set
[u9,u9] is V15() set
{u9,u9} is set
{u9} is set
{{u9,u9},{u9}} is set
K11( the L_meet of (A),[u9,u9]) is set
K is Element of (A)
the L_meet of (A) . (u9,K) is set
[u9,K] is V15() set
{u9,K} is set
{{u9,K},{u9}} is set
K11( the L_meet of (A),[u9,K]) is set
the L_join of (A) . (( the L_meet of (A) . (u9,u9)),( the L_meet of (A) . (u9,K))) is set
[( the L_meet of (A) . (u9,u9)),( the L_meet of (A) . (u9,K))] is V15() set
{( the L_meet of (A) . (u9,u9)),( the L_meet of (A) . (u9,K))} is set
{( the L_meet of (A) . (u9,u9))} is set
{{( the L_meet of (A) . (u9,u9)),( the L_meet of (A) . (u9,K))},{( the L_meet of (A) . (u9,u9))}} is set
K11( the L_join of (A),[( the L_meet of (A) . (u9,u9)),( the L_meet of (A) . (u9,K))]) is set
(A,u9,u9) is finite Element of Fin (A)
{ ((Fin A),(Fin A),b₁,b₂) where b₁, b₂ is Element of (A) : ( b₁ in u9 & b₂ in u9 ) } is set
(A) /\ { ((Fin A),(Fin A),b₁,b₂) where b₁, b₂ is Element of (A) : ( b₁ in u9 & b₂ in u9 ) } is Relation-like Fin A -defined Fin A -valued Element of bool [:(Fin A),(Fin A):]
(A,(A,u9,u9)) is Element of (A)
{ b₁ where b₁ is Element of (A) : for b₂ being Element of (A) holds
( ( not b₂ in (A,u9,u9) or not ( Fin A, Fin A,b₂,b₁) or b₂ = b₁ ) & ( not b₂ = b₁ or ( b₂ in (A,u9,u9) & ( Fin A, Fin A,b₂,b₁) ) ) ) } is set
the L_join of (A) . ((A,(A,u9,u9)),( the L_meet of (A) . (u9,K))) is set
[(A,(A,u9,u9)),( the L_meet of (A) . (u9,K))] is V15() set
{(A,(A,u9,u9)),( the L_meet of (A) . (u9,K))} is set
{(A,(A,u9,u9))} is set
{{(A,(A,u9,u9)),( the L_meet of (A) . (u9,K))},{(A,(A,u9,u9))}} is set
K11( the L_join of (A),[(A,(A,u9,u9)),( the L_meet of (A) . (u9,K))]) is set
(A,u9) is Element of (A)
{ b₁ where b₁ is Element of (A) : for b₂ being Element of (A) holds
( ( not b₂ in u9 or not ( Fin A, Fin A,b₂,b₁) or b₂ = b₁ ) & ( not b₂ = b₁ or ( b₂ in u9 & ( Fin A, Fin A,b₂,b₁) ) ) ) } is set
the L_join of (A) . ((A,u9),( the L_meet of (A) . (u9,K))) is set
[(A,u9),( the L_meet of (A) . (u9,K))] is V15() set
{(A,u9),( the L_meet of (A) . (u9,K))} is set
{(A,u9)} is set
{{(A,u9),( the L_meet of (A) . (u9,K))},{(A,u9)}} is set
K11( the L_join of (A),[(A,u9),( the L_meet of (A) . (u9,K))]) is set
u "/\" z is Element of the carrier of (A)
the L_meet of (A) . (u,z) is Element of the carrier of (A)
K11( the L_meet of (A),[u,z]) is set
u "\/" (u "/\" z) is Element of the carrier of (A)
the L_join of (A) . (u,(u "/\" z)) is Element of the carrier of (A)
[u,(u "/\" z)] is V15() set
{u,(u "/\" z)} is set
{{u,(u "/\" z)},{u}} is set
K11( the L_join of (A),[u,(u "/\" z)]) is set
(u "/\" z) "\/" u is Element of the carrier of (A)
the L_join of (A) . ((u "/\" z),u) is Element of the carrier of (A)
[(u "/\" z),u] is V15() set
{(u "/\" z),u} is set
{(u "/\" z)} is set
{{(u "/\" z),u},{(u "/\" z)}} is set
K11( the L_join of (A),[(u "/\" z),u]) is set
z "/\" u is Element of the carrier of (A)
the L_meet of (A) . (z,u) is Element of the carrier of (A)
[z,u] is V15() set
{z,u} is set
{z} is set
{{z,u},{z}} is set
K11( the L_meet of (A),[z,u]) is set
(z "/\" u) "\/" u is Element of the carrier of (A)
the L_join of (A) . ((z "/\" u),u) is Element of the carrier of (A)
[(z "/\" u),u] is V15() set
{(z "/\" u),u} is set
{(z "/\" u)} is set
{{(z "/\" u),u},{(z "/\" u)}} is set
K11( the L_join of (A),[(z "/\" u),u]) is set
A is set
(A) is non empty strict LattStr
the carrier of (A) is set
u is Element of the carrier of (A)
z is Element of the carrier of (A)
u "\/" z is Element of the carrier of (A)
the L_join of (A) is Relation-like [: the carrier of (A), the carrier of (A):] -defined the carrier of (A) -valued V6() V18([: the carrier of (A), the carrier of (A):], the carrier of (A)) Element of bool [:[: the carrier of (A), the carrier of (A):], the carrier of (A):]
[: the carrier of (A), the carrier of (A):] is Relation-like set
[:[: the carrier of (A), the carrier of (A):], the carrier of (A):] is Relation-like set
bool [:[: the carrier of (A), the carrier of (A):], the carrier of (A):] is non empty cup-closed diff-closed preBoolean set
the L_join of (A) . (u,z) is Element of the carrier of (A)
[u,z] is V15() set
{u,z} is set
{u} is set
{{u,z},{u}} is set
K11( the L_join of (A),[u,z]) is set
z "\/" u is Element of the carrier of (A)
the L_join of (A) . (z,u) is Element of the carrier of (A)
[z,u] is V15() set
{z,u} is set
{z} is set
{{z,u},{z}} is set
K11( the L_join of (A),[z,u]) is set
u is Element of the carrier of (A)
z is Element of the carrier of (A)
u9 is Element of the carrier of (A)
z "\/" u9 is Element of the carrier of (A)
the L_join of (A) is Relation-like [: the carrier of (A), the carrier of (A):] -defined the carrier of (A) -valued V6() V18([: the carrier of (A), the carrier of (A):], the carrier of (A)) Element of bool [:[: the carrier of (A), the carrier of (A):], the carrier of (A):]
[: the carrier of (A), the carrier of (A):] is Relation-like set
[:[: the carrier of (A), the carrier of (A):], the carrier of (A):] is Relation-like set
bool [:[: the carrier of (A), the carrier of (A):], the carrier of (A):] is non empty cup-closed diff-closed preBoolean set
the L_join of (A) . (z,u9) is Element of the carrier of (A)
[z,u9] is V15() set
{z,u9} is set
{z} is set
{{z,u9},{z}} is set
K11( the L_join of (A),[z,u9]) is set
u "\/" (z "\/" u9) is Element of the carrier of (A)
the L_join of (A) . (u,(z "\/" u9)) is Element of the carrier of (A)
[u,(z "\/" u9)] is V15() set
{u,(z "\/" u9)} is set
{u} is set
{{u,(z "\/" u9)},{u}} is set
K11( the L_join of (A),[u,(z "\/" u9)]) is set
u "\/" z is Element of the carrier of (A)
the L_join of (A) . (u,z) is Element of the carrier of (A)
[u,z] is V15() set
{u,z} is set
{{u,z},{u}} is set
K11( the L_join of (A),[u,z]) is set
(u "\/" z) "\/" u9 is Element of the carrier of (A)
the L_join of (A) . ((u "\/" z),u9) is Element of the carrier of (A)
[(u "\/" z),u9] is V15() set
{(u "\/" z),u9} is set
{(u "\/" z)} is set
{{(u "\/" z),u9},{(u "\/" z)}} is set
K11( the L_join of (A),[(u "\/" z),u9]) is set
u is Element of the carrier of (A)
z is Element of the carrier of (A)
u "/\" z is Element of the carrier of (A)
the L_meet of (A) is Relation-like [: the carrier of (A), the carrier of (A):] -defined the carrier of (A) -valued V6() V18([: the carrier of (A), the carrier of (A):], the carrier of (A)) Element of bool [:[: the carrier of (A), the carrier of (A):], the carrier of (A):]
[: the carrier of (A), the carrier of (A):] is Relation-like set
[:[: the carrier of (A), the carrier of (A):], the carrier of (A):] is Relation-like set
bool [:[: the carrier of (A), the carrier of (A):], the carrier of (A):] is non empty cup-closed diff-closed preBoolean set
the L_meet of (A) . (u,z) is Element of the carrier of (A)
[u,z] is V15() set
{u,z} is set
{u} is set
{{u,z},{u}} is set
K11( the L_meet of (A),[u,z]) is set
(u "/\" z) "\/" z is Element of the carrier of (A)
the L_join of (A) is Relation-like [: the carrier of (A), the carrier of (A):] -defined the carrier of (A) -valued V6() V18([: the carrier of (A), the carrier of (A):], the carrier of (A)) Element of bool [:[: the carrier of (A), the carrier of (A):], the carrier of (A):]
the L_join of (A) . ((u "/\" z),z) is Element of the carrier of (A)
[(u "/\" z),z] is V15() set
{(u "/\" z),z} is set
{(u "/\" z)} is set
{{(u "/\" z),z},{(u "/\" z)}} is set
K11( the L_join of (A),[(u "/\" z),z]) is set
u is Element of the carrier of (A)
z is Element of the carrier of (A)
u "/\" z is Element of the carrier of (A)
the L_meet of (A) is Relation-like [: the carrier of (A), the carrier of (A):] -defined the carrier of (A) -valued V6() V18([: the carrier of (A), the carrier of (A):], the carrier of (A)) Element of bool [:[: the carrier of (A), the carrier of (A):], the carrier of (A):]
[: the carrier of (A), the carrier of (A):] is Relation-like set
[:[: the carrier of (A), the carrier of (A):], the carrier of (A):] is Relation-like set
bool [:[: the carrier of (A), the carrier of (A):], the carrier of (A):] is non empty cup-closed diff-closed preBoolean set
the L_meet of (A) . (u,z) is Element of the carrier of (A)
[u,z] is V15() set
{u,z} is set
{u} is set
{{u,z},{u}} is set
K11( the L_meet of (A),[u,z]) is set
z "/\" u is Element of the carrier of (A)
the L_meet of (A) . (z,u) is Element of the carrier of (A)
[z,u] is V15() set
{z,u} is set
{z} is set
{{z,u},{z}} is set
K11( the L_meet of (A),[z,u]) is set
u is Element of the carrier of (A)
z is Element of the carrier of (A)
u9 is Element of the carrier of (A)
z "/\" u9 is Element of the carrier of (A)
the L_meet of (A) is Relation-like [: the carrier of (A), the carrier of (A):] -defined the carrier of (A) -valued V6() V18([: the carrier of (A), the carrier of (A):], the carrier of (A)) Element of bool [:[: the carrier of (A), the carrier of (A):], the carrier of (A):]
[: the carrier of (A), the carrier of (A):] is Relation-like set
[:[: the carrier of (A), the carrier of (A):], the carrier of (A):] is Relation-like set
bool [:[: the carrier of (A), the carrier of (A):], the carrier of (A):] is non empty cup-closed diff-closed preBoolean set
the L_meet of (A) . (z,u9) is Element of the carrier of (A)
[z,u9] is V15() set
{z,u9} is set
{z} is set
{{z,u9},{z}} is set
K11( the L_meet of (A),[z,u9]) is set
u "/\" (z "/\" u9) is Element of the carrier of (A)
the L_meet of (A) . (u,(z "/\" u9)) is Element of the carrier of (A)
[u,(z "/\" u9)] is V15() set
{u,(z "/\" u9)} is set
{u} is set
{{u,(z "/\" u9)},{u}} is set
K11( the L_meet of (A),[u,(z "/\" u9)]) is set
u "/\" z is Element of the carrier of (A)
the L_meet of (A) . (u,z) is Element of the carrier of (A)
[u,z] is V15() set
{u,z} is set
{{u,z},{u}} is set
K11( the L_meet of (A),[u,z]) is set
(u "/\" z) "/\" u9 is Element of the carrier of (A)
the L_meet of (A) . ((u "/\" z),u9) is Element of the carrier of (A)
[(u "/\" z),u9] is V15() set
{(u "/\" z),u9} is set
{(u "/\" z)} is set
{{(u "/\" z),u9},{(u "/\" z)}} is set
K11( the L_meet of (A),[(u "/\" z),u9]) is set
u is Element of the carrier of (A)
z is Element of the carrier of (A)
u "\/" z is Element of the carrier of (A)
the L_join of (A) is Relation-like [: the carrier of (A), the carrier of (A):] -defined the carrier of (A) -valued V6() V18([: the carrier of (A), the carrier of (A):], the carrier of (A)) Element of bool [:[: the carrier of (A), the carrier of (A):], the carrier of (A):]
[: the carrier of (A), the carrier of (A):] is Relation-like set
[:[: the carrier of (A), the carrier of (A):], the carrier of (A):] is Relation-like set
bool [:[: the carrier of (A), the carrier of (A):], the carrier of (A):] is non empty cup-closed diff-closed preBoolean set
the L_join of (A) . (u,z) is Element of the carrier of (A)
[u,z] is V15() set
{u,z} is set
{u} is set
{{u,z},{u}} is set
K11( the L_join of (A),[u,z]) is set
u "/\" (u "\/" z) is Element of the carrier of (A)
the L_meet of (A) is Relation-like [: the carrier of (A), the carrier of (A):] -defined the carrier of (A) -valued V6() V18([: the carrier of (A), the carrier of (A):], the carrier of (A)) Element of bool [:[: the carrier of (A), the carrier of (A):], the carrier of (A):]
the L_meet of (A) . (u,(u "\/" z)) is Element of the carrier of (A)
[u,(u "\/" z)] is V15() set
{u,(u "\/" z)} is set
{{u,(u "\/" z)},{u}} is set
K11( the L_meet of (A),[u,(u "\/" z)]) is set
A is set
(A) is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr
the carrier of (A) is set
u is Element of the carrier of (A)
z is Element of the carrier of (A)
u9 is Element of the carrier of (A)
z "\/" u9 is Element of the carrier of (A)
the L_join of (A) is Relation-like [: the carrier of (A), the carrier of (A):] -defined the carrier of (A) -valued V6() V18([: the carrier of (A), the carrier of (A):], the carrier of (A)) Element of bool [:[: the carrier of (A), the carrier of (A):], the carrier of (A):]
[: the carrier of (A), the carrier of (A):] is Relation-like set
[:[: the carrier of (A), the carrier of (A):], the carrier of (A):] is Relation-like set
bool [:[: the carrier of (A), the carrier of (A):], the carrier of (A):] is non empty cup-closed diff-closed preBoolean set
the L_join of (A) . (z,u9) is Element of the carrier of (A)
[z,u9] is V15() set
{z,u9} is set
{z} is set
{{z,u9},{z}} is set
K11( the L_join of (A),[z,u9]) is set
u "/\" (z "\/" u9) is Element of the carrier of (A)
the L_meet of (A) is Relation-like [: the carrier of (A), the carrier of (A):] -defined the carrier of (A) -valued V6() V18([: the carrier of (A), the carrier of (A):], the carrier of (A)) Element of bool [:[: the carrier of (A), the carrier of (A):], the carrier of (A):]
the L_meet of (A) . (u,(z "\/" u9)) is Element of the carrier of (A)
[u,(z "\/" u9)] is V15() set
{u,(z "\/" u9)} is set
{u} is set
{{u,(z "\/" u9)},{u}} is set
K11( the L_meet of (A),[u,(z "\/" u9)]) is set
u "/\" z is Element of the carrier of (A)
the L_meet of (A) . (u,z) is Element of the carrier of (A)
[u,z] is V15() set
{u,z} is set
{{u,z},{u}} is set
K11( the L_meet of (A),[u,z]) is set
u "/\" u9 is Element of the carrier of (A)
the L_meet of (A) . (u,u9) is Element of the carrier of (A)
[u,u9] is V15() set
{u,u9} is set
{{u,u9},{u}} is set
K11( the L_meet of (A),[u,u9]) is set
(u "/\" z) "\/" (u "/\" u9) is Element of the carrier of (A)
the L_join of (A) . ((u "/\" z),(u "/\" u9)) is Element of the carrier of (A)
[(u "/\" z),(u "/\" u9)] is V15() set
{(u "/\" z),(u "/\" u9)} is set
{(u "/\" z)} is set
{{(u "/\" z),(u "/\" u9)},{(u "/\" z)}} is set
K11( the L_join of (A),[(u "/\" z),(u "/\" u9)]) is set
(A) is Relation-like Fin A -defined Fin A -valued non empty Element of bool [:(Fin A),(Fin A):]
Fin A is non empty cup-closed diff-closed preBoolean set
[:(Fin A),(Fin A):] is Relation-like non empty set
bool [:(Fin A),(Fin A):] is non empty cup-closed diff-closed preBoolean set
{ b₁ where b₁ is Element of [:(Fin A),(Fin A):] : b₁ `1 misses b<sub>1</sub> `2 } is set
Fin (A) is non empty cup-closed diff-closed preBoolean set
(A) is non empty Element of bool (Fin (A))
bool (Fin (A)) is non empty cup-closed diff-closed preBoolean set
{ b₁ where b₁ is finite Element of Fin (A) : for b₂, b₃ being Element of (A) holds
( not b₂ in b₁ or not b₃ in b₁ or not ( Fin A, Fin A,b₂,b₃) or b₂ = b₃ ) } is set
z "\/" u9 is Element of the carrier of (A)
u "/\" (z "\/" u9) is Element of the carrier of (A)
the L_meet of (A) . (u,(z "\/" u9)) is Element of the carrier of (A)
[u,(z "\/" u9)] is V15() set
{u,(z "\/" u9)} is set
{{u,(z "\/" u9)},{u}} is set
K11( the L_meet of (A),[u,(z "\/" u9)]) is set
K is Element of (A)
L is Element of (A)
M is Element of (A)
the L_join of (A) . (L,M) is set
[L,M] is V15() set
{L,M} is set
{L} is set
{{L,M},{L}} is set
K11( the L_join of (A),[L,M]) is set
the L_meet of (A) . (K,( the L_join of (A) . (L,M))) is set
[K,( the L_join of (A) . (L,M))] is V15() set
{K,( the L_join of (A) . (L,M))} is set
{K} is set
{{K,( the L_join of (A) . (L,M))},{K}} is set
K11( the L_meet of (A),[K,( the L_join of (A) . (L,M))]) is set
u "/\" z is Element of the carrier of (A)
u "/\" u9 is Element of the carrier of (A)
(u "/\" z) "\/" (u "/\" u9) is Element of the carrier of (A)
the L_join of (A) . ((u "/\" z),(u "/\" u9)) is Element of the carrier of (A)
[(u "/\" z),(u "/\" u9)] is V15() set
{(u "/\" z),(u "/\" u9)} is set
{(u "/\" z)} is set
{{(u "/\" z),(u "/\" u9)},{(u "/\" z)}} is set
K11( the L_join of (A),[(u "/\" z),(u "/\" u9)]) is set
(A) is Relation-like Fin A -defined Fin A -valued non empty Element of bool [:(Fin A),(Fin A):]
Fin A is non empty cup-closed diff-closed preBoolean set
[:(Fin A),(Fin A):] is Relation-like non empty set
bool [:(Fin A),(Fin A):] is non empty cup-closed diff-closed preBoolean set
{ b₁ where b₁ is Element of [:(Fin A),(Fin A):] : b₁ `1 misses b<sub>1</sub> `2 } is set
Fin (A) is non empty cup-closed diff-closed preBoolean set
(A) is non empty Element of bool (Fin (A))
bool (Fin (A)) is non empty cup-closed diff-closed preBoolean set
{ b₁ where b₁ is finite Element of Fin (A) : for b₂, b₃ being Element of (A) holds
( not b₂ in b₁ or not b₃ in b₁ or not ( Fin A, Fin A,b₂,b₃) or b₂ = b₃ ) } is set
the carrier of (A) is set
u is Element of (A)
z is Element of the carrier of (A)
u9 is Element of the carrier of (A)
z "/\" u9 is Element of the carrier of (A)
the L_meet of (A) is Relation-like [: the carrier of (A), the carrier of (A):] -defined the carrier of (A) -valued V6() V18([: the carrier of (A), the carrier of (A):], the carrier of (A)) Element of bool [:[: the carrier of (A), the carrier of (A):], the carrier of (A):]
[: the carrier of (A), the carrier of (A):] is Relation-like set
[:[: the carrier of (A), the carrier of (A):], the carrier of (A):] is Relation-like set
bool [:[: the carrier of (A), the carrier of (A):], the carrier of (A):] is non empty cup-closed diff-closed preBoolean set
the L_meet of (A) . (z,u9) is Element of the carrier of (A)
[z,u9] is V15() set
{z,u9} is set
{z} is set
{{z,u9},{z}} is set
K11( the L_meet of (A),[z,u9]) is set
u9 "/\" z is Element of the carrier of (A)
the L_meet of (A) . (u9,z) is Element of the carrier of (A)
[u9,z] is V15() set
{u9,z} is set
{u9} is set
{{u9,z},{u9}} is set
K11( the L_meet of (A),[u9,z]) is set
z "\/" u9 is Element of the carrier of (A)
the L_join of (A) is Relation-like [: the carrier of (A), the carrier of (A):] -defined the carrier of (A) -valued V6() V18([: the carrier of (A), the carrier of (A):], the carrier of (A)) Element of bool [:[: the carrier of (A), the carrier of (A):], the carrier of (A):]
the L_join of (A) . (z,u9) is Element of the carrier of (A)
K11( the L_join of (A),[z,u9]) is set
K is Element of (A)
u \/ K is finite Element of Fin (A)
(A,(u \/ K)) is Element of (A)
{ b₁ where b₁ is Element of (A) : for b₂ being Element of (A) holds
( ( not b₂ in u \/ K or not ( Fin A, Fin A,b₂,b₁) or b₂ = b₁ ) & ( not b₂ = b₁ or ( b₂ in u \/ K & ( Fin A, Fin A,b₂,b₁) ) ) ) } is set
u9 "/\" z is Element of the carrier of (A)
A is set
(A) is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded LattStr
the carrier of (A) is set
(A) is non empty Element of bool (Fin (A))
(A) is Relation-like Fin A -defined Fin A -valued non empty Element of bool [:(Fin A),(Fin A):]
Fin A is non empty cup-closed diff-closed preBoolean set
[:(Fin A),(Fin A):] is Relation-like non empty set
bool [:(Fin A),(Fin A):] is non empty cup-closed diff-closed preBoolean set
{ b₁ where b₁ is Element of [:(Fin A),(Fin A):] : b₁ `1 misses b<sub>1</sub> `2 } is set
Fin (A) is non empty cup-closed diff-closed preBoolean set
bool (Fin (A)) is non empty cup-closed diff-closed preBoolean set
{ b₁ where b₁ is finite Element of Fin (A) : for b₂, b₃ being Element of (A) holds
( not b₂ in b₁ or not b₃ in b₁ or not ( Fin A, Fin A,b₂,b₃) or b₂ = b₃ ) } is set
A is set
(A) is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded LattStr
Bottom (A) is Element of the carrier of (A)
the carrier of (A) is set
(A) is non empty Element of bool (Fin (A))
(A) is Relation-like Fin A -defined Fin A -valued non empty Element of bool [:(Fin A),(Fin A):]
Fin A is non empty cup-closed diff-closed preBoolean set
[:(Fin A),(Fin A):] is Relation-like non empty set
bool [:(Fin A),(Fin A):] is non empty cup-closed diff-closed preBoolean set
{ b₁ where b₁ is Element of [:(Fin A),(Fin A):] : b₁ `1 misses b<sub>1</sub> `2 } is set
Fin (A) is non empty cup-closed diff-closed preBoolean set
bool (Fin (A)) is non empty cup-closed diff-closed preBoolean set
{ b₁ where b₁ is finite Element of Fin (A) : for b₂, b₃ being Element of (A) holds
( not b₂ in b₁ or not b₃ in b₁ or not ( Fin A, Fin A,b₂,b₃) or b₂ = b₃ ) } is set
Z is Element of the carrier of (A)
u is Element of the carrier of (A)
Z "\/" u is Element of the carrier of (A)
the L_join of (A) is Relation-like [: the carrier of (A), the carrier of (A):] -defined the carrier of (A) -valued V6() V18([: the carrier of (A), the carrier of (A):], the carrier of (A)) Element of bool [:[: the carrier of (A), the carrier of (A):], the carrier of (A):]
[: the carrier of (A), the carrier of (A):] is Relation-like set
[:[: the carrier of (A), the carrier of (A):], the carrier of (A):] is Relation-like set
bool [:[: the carrier of (A), the carrier of (A):], the carrier of (A):] is non empty cup-closed diff-closed preBoolean set
the L_join of (A) . (Z,u) is Element of the carrier of (A)
[Z,u] is V15() set
{Z,u} is set
{Z} is set
{{Z,u},{Z}} is set
K11( the L_join of (A),[Z,u]) is set
z is Element of (A)
u9 is Element of (A)
z \/ u9 is finite Element of Fin (A)
(A,(z \/ u9)) is Element of (A)
{ b₁ where b₁ is Element of (A) : for b₂ being Element of (A) holds
( ( not b₂ in z \/ u9 or not ( Fin A, Fin A,b₂,b₁) or b₂ = b₁ ) & ( not b₂ = b₁ or ( b₂ in z \/ u9 & ( Fin A, Fin A,b₂,b₁) ) ) ) } is set