take {} P ; :: thesis: {} P is pcs-self-coherent
thus {} P is pcs-self-coherent ; :: thesis: verum