RelStr(# the carrier of (R *' f), the InternalRel of (R *' f) #) = RelStr(# the carrier of R, the InternalRel of R #) by Def3;
hence R *' f is transitive by WAYBEL_8:13; :: thesis: verum