set
D
=
{
{}
}
;
set
R
= the
Order
of
{
{}
}
;
reconsider
A
=
RelStr
(#
{
{}
}
, the
Order
of
{
{}
}
#) as
with_suprema
with_infima
Poset
;
take
A
;
:: thesis:
(
A
is
finite
& not
A
is
empty
)
thus
(
A
is
finite
& not
A
is
empty
) ;
:: thesis:
verum