take
{
0
,1
}
;
:: thesis:
( not
{
0
,1
}
is
trivial
&
{
0
,1
}
is
finite
)
thus
( not
{
0
,1
}
is
trivial
&
{
0
,1
}
is
finite
)
by
Th3
;
:: thesis:
verum