set P = the pcs;
take 0 --> the pcs ; :: thesis: ( 0 --> the pcs is pcs-chain-like & 0 --> the pcs is pcs-yielding )
thus ( 0 --> the pcs is pcs-chain-like & 0 --> the pcs is pcs-yielding ) ; :: thesis: verum