:: deftheorem defines pcs-empty PCS_0:def 26 :
pcs-empty = pcs-total 0;