:: deftheorem defines pcs-singleton PCS_0:def 27 :
for p being set holds pcs-singleton p = pcs-total {p};