consider P being pcs;
take 0 --> P ; :: thesis: ( 0 --> P is pcs-chain-like & 0 --> P is pcs-yielding )
thus ( 0 --> P is pcs-chain-like & 0 --> P is pcs-yielding ) ; :: thesis: verum