take I --> pcs-empty ; :: thesis: I --> pcs-empty is pcs-yielding
thus I --> pcs-empty is pcs-yielding ; :: thesis: verum