TolStr(# the carrier of (P pcs-times Q), the ToleranceRel of (P pcs-times Q) #) = [^P,Q^] ;
hence P pcs-times Q is pcs-tol-symmetric by Th5; :: thesis: verum