set R = the non empty trivial strict Poset;
take the non empty trivial strict Poset ; :: thesis: ( the non empty trivial strict Poset is completely-distributive & the non empty trivial strict Poset is trivial & the non empty trivial strict Poset is strict )
thus ( the non empty trivial strict Poset is completely-distributive & the non empty trivial strict Poset is trivial & the non empty trivial strict Poset is strict ) ; :: thesis: verum