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