:: deftheorem defines pcs-power PCS_0:def 50 :
for P being pcs-Str holds pcs-power P = pcs-general-power (pcs-coherent-power P);