:: deftheorem defines pcs-total PCS_0:def 25 :
for D being set holds pcs-total D = pcs-Str(# D,(nabla D),(nabla D) #);