:: deftheorem defines CPFuncZero LPSPACC1:def 6 :
for A being set holds CPFuncZero A = A --> 0c;