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

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