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