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-reflexive by Th3; :: thesis: verum