take
{
{
0
}
}
;
:: thesis:
(
{
{
0
}
}
is
mutually-disjoint
& not
{
{
0
}
}
is
empty
&
{
{
0
}
}
is
with_non-empty_elements
)
thus
(
{
{
0
}
}
is
mutually-disjoint
& not
{
{
0
}
}
is
empty
&
{
{
0
}
}
is
with_non-empty_elements
)
by
TAXONOM2:10
;
:: thesis:
verum