A1: RelStr(# the carrier of (R --> p),the InternalRel of (R --> p) #) = RelStr(# the carrier of R,the InternalRel of R #) by Def7;
RelStr(# the carrier of R,the InternalRel of R #) is transitive by Lm2;
hence R --> p is transitive by A1, Lm2; :: thesis: verum