set R = the 1 -element strict Poset;
take the 1 -element strict Poset ; :: thesis: ( the 1 -element strict Poset is completely-distributive & the 1 -element strict Poset is strict )
thus ( the 1 -element strict Poset is completely-distributive & the 1 -element strict Poset is strict ) ; :: thesis: verum