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