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