:: deftheorem defines pcs-sum PCS_0:def 39 :
for P, Q being pcs-Str holds pcs-sum (P,Q) = pcs-union <%P,Q%>;