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

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