RelStr(# the carrier of (P pcs-times Q), the InternalRel of (P pcs-times Q) #) = [:P,Q:] by YELLOW_3:def 2;
hence P pcs-times Q is transitive by WAYBEL_8:13; :: thesis: verum