set D = {{} };
consider R being Order of {{} };
reconsider A = RelStr(# {{} },R #) 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