{} P in pcs-coherent-power P ;
hence not pcs-coherent-power P is empty ; :: thesis: verum