consider P being non empty Poset;
take I --> P ; :: thesis: ( I --> P is Poset-yielding & I --> P is non-Empty )
thus ( I --> P is Poset-yielding & I --> P is non-Empty ) ; :: thesis: verum