take
{
0
}
;
:: thesis:
( not
{
0
}
is
empty
&
{
0
}
is
finite
&
{
0
}
is
natural-membered
)
thus
( not
{
0
}
is
empty
&
{
0
}
is
finite
&
{
0
}
is
natural-membered
) ;
:: thesis:
verum