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