:: deftheorem defines --> PCS_0:def 43 :
for P, Q being pcs-Str holds P --> Q = (pcs-reverse P) pcs-times Q;