set P = the non empty Poset;
take I --> the non empty Poset ; :: thesis: ( I --> the non empty Poset is Poset-yielding & I --> the non empty Poset is non-Empty )
thus ( I --> the non empty Poset is Poset-yielding & I --> the non empty Poset is non-Empty ) ; :: thesis: verum