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