:: deftheorem defines pcs-general-power PCS_0:def 48 :
for P being pcs-Str
for D being set holds pcs-general-power (P,D) = pcs-Str(# D,(pcs-general-power-IR (P,D)),(pcs-general-power-TR (P,D)) #);