:: deftheorem defines pcs-coherent-power PCS_0:def 49 :
for P being pcs-Str holds pcs-coherent-power P = { X where X is Subset of P : X is pcs-self-coherent } ;