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